add and transmit a timeout flag

lip6 · May 14, 2024 · 624a794 · 624a794
1 parent 454ad22
commit 624a794
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/...ove.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/ReachabilitySolver.java b/...ove.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/ReachabilitySolver.java
@@ -703,7 +703,7 @@ private static int applySMTBasedReductionRules(StructuralReduction sr, Reduction
 		}
 		if (lastReduction != 4) {
 			if (lastReduction != 1 && (reduced == 0 || iteration==0)) {
-				List<Integer> tokill = DeadlockTester.testDeadTransitionWithSMT(sr);
+				List<Integer> tokill = DeadlockTester.testDeadTransitionWithSMT(sr,30);
 				if (! tokill.isEmpty()) {
 					System.out.println("Found "+tokill.size()+ " dead transitions using SMT." );
 					if (rt == ReductionType.LIVENESS) {
@@ -736,7 +736,7 @@ private static boolean arcValuesTriggerSMTDeadTransitions(StructuralReduction sr
 		}
 
 		if (hasGT1ArcValues) {
-			List<Integer> tokill = DeadlockTester.testDeadTransitionWithSMT(sr);
+			List<Integer> tokill = DeadlockTester.testDeadTransitionWithSMT(sr,20);
 			if (! tokill.isEmpty()) {
 				System.out.println("Found "+tokill.size()+ " dead transitions using SMT." );
 			}

diff --git a/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/DeadlockTester.java b/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/structural/smt/DeadlockTester.java
@@ -1218,7 +1218,7 @@ static boolean queryVariables(SparseIntArray state, SparseIntArray parikh, Spars
 	}
 
 
-	public static List<Integer> testDeadTransitionWithSMT(StructuralReduction sr) {
+	public static List<Integer> testDeadTransitionWithSMT(StructuralReduction sr, int timeout) {
 		List<Property> props = new ArrayList<>();
 		SparseIntArray initial = new SparseIntArray(sr.getMarks());
 		for (int tid=0; tid < sr.getTransitionCount() ; tid++) {
@@ -1241,7 +1241,7 @@ public static List<Integer> testDeadTransitionWithSMT(StructuralReduction sr) {
 		List<Integer> deadTrans = new ArrayList<Integer>();
 		if (! problems.getUnsolved().isEmpty()) {
 			List<Integer> repr = new ArrayList<>();
-			solved += SMTBasedReachabilitySolver.solveProblems(problems, sr, 60, false, repr);
+			solved += SMTBasedReachabilitySolver.solveProblems(problems, sr, timeout, false, repr);
 			if (solved > 0) {
 				for (Entry<String, Boolean> ent : localDone.entrySet()) {
 					if (ent.getValue()) {