diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/ReachabilitySolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/ReachabilitySolver.java index dc082187e..d16fce92c 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/solver/ReachabilitySolver.java +++ b/pnmcc/fr.lip6.move.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 tokill = DeadlockTester.testDeadTransitionWithSMT(sr); + List 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 tokill = DeadlockTester.testDeadTransitionWithSMT(sr); + List 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 index 193e52868..833d56250 100644 --- 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 testDeadTransitionWithSMT(StructuralReduction sr) { + public static List testDeadTransitionWithSMT(StructuralReduction sr, int timeout) { List props = new ArrayList<>(); SparseIntArray initial = new SparseIntArray(sr.getMarks()); for (int tid=0; tid < sr.getTransitionCount() ; tid++) { @@ -1241,7 +1241,7 @@ public static List testDeadTransitionWithSMT(StructuralReduction sr) { List deadTrans = new ArrayList(); if (! problems.getUnsolved().isEmpty()) { List repr = new ArrayList<>(); - solved += SMTBasedReachabilitySolver.solveProblems(problems, sr, 60, false, repr); + solved += SMTBasedReachabilitySolver.solveProblems(problems, sr, timeout, false, repr); if (solved > 0) { for (Entry ent : localDone.entrySet()) { if (ent.getValue()) {