diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/RandomExplorer.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/RandomExplorer.java index 7c61c9279a..93a5cad630 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/RandomExplorer.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/RandomExplorer.java @@ -43,6 +43,9 @@ public int[] runGuidedReachabilityDetection (long nbSteps, SparseIntArray parikh wu.dropEmpty(list); wu.dropUnavailable(list, parikh); + SparseIntArray initstate = state.clone(); + int [] initlist = list.clone(); + long nbresets = 0; int [] verdicts = new int [exprs.size()]; @@ -74,14 +77,9 @@ public int[] runGuidedReachabilityDetection (long nbSteps, SparseIntArray parikh if (list[0] == 0){ //System.out.println("Dead end with self loop(s) found at step " + i); nbresets ++; - state = wu.getInitial(); - list = computeEnabled(state); - parikh = parikhori.clone(); - wu.dropEmpty(list); - // each reset weakens the policy - if (rand.nextDouble() < 1.0 - (nbresets*0.001)) { - wu.dropUnavailable(list, parikh); - } + state = initstate.clone(); + list = initlist.clone(); + parikh = parikhori.clone(); mode = (mode + 1)% 4; continue; } @@ -281,6 +279,9 @@ public int[] runRandomReachabilityDetection (long nbSteps, List expr int [] list = computeEnabled(state); wu.dropEmpty(list); + SparseIntArray initstate = state.clone(); + int [] initlist = list.clone(); + int last = -1; long nbresets = 0; @@ -305,9 +306,8 @@ public int[] runRandomReachabilityDetection (long nbSteps, List expr //System.out.println("Dead end with self loop(s) found at step " + i); nbresets ++; last = -1; - state = wu.getInitial(); - list = computeEnabled(state); - wu.dropEmpty(list); + state = initstate.clone(); + list = initlist.clone(); continue; } @@ -401,6 +401,10 @@ public void runGuidedDeadlockDetection (long nbSteps, SparseIntArray parikhori, int [] list = computeEnabled(state); wu.dropEmpty(list); wu.dropUnavailable(list, parikh); + + SparseIntArray initstate = state.clone(); + int [] initlist = list.clone(); + long nbresets = 0; int i=0; @@ -419,11 +423,9 @@ public void runGuidedDeadlockDetection (long nbSteps, SparseIntArray parikhori, } else { //System.out.println("Dead end with self loop(s) found at step " + i); nbresets ++; - state = wu.getInitial(); - list = computeEnabled(state); + state = initstate.clone(); + list = initlist.clone(); parikh = parikhori.clone(); - wu.dropEmpty(list); - wu.dropUnavailable(list, parikh); continue; } } @@ -482,7 +484,8 @@ public void runDeadlockDetection (long nbSteps, boolean fullRand, int timeout) t SparseIntArray state = wu.getInitial(); int [] list = computeEnabled(state); wu.dropEmpty(list); - + SparseIntArray initstate = state.clone(); + int [] initlist = list.clone(); int last = -1; long nbresets = 0; @@ -506,9 +509,8 @@ public void runDeadlockDetection (long nbSteps, boolean fullRand, int timeout) t //System.out.println("Dead end with self loop(s) found at step " + i); nbresets ++; last = -1; - state = wu.getInitial(); - list = computeEnabled(state); - wu.dropEmpty(list); + state = initstate.clone(); + list = initlist.clone(); continue; } } diff --git a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java index 445623e116..e977588226 100644 --- a/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java +++ b/fr.lip6.move.gal.structural/src/fr/lip6/move/gal/structural/StructuralReduction.java @@ -1573,6 +1573,12 @@ private int rulePostAgglo(boolean doComplex, boolean doSimple, ReductionType rt) for (int cons : seenFrom) { if (feeder % cons != 0 || cons > feeder) { ok = false; + break; + } + if (feeder > cons && seenFrom.size() > 1) { + // we could decide to send some tokens left and some right + ok = false; + break; } } if (!ok) { diff --git a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java index fe7a7a0a7e..b0bdd3298f 100644 --- a/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java +++ b/pnmcc/fr.lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java @@ -405,9 +405,9 @@ private static boolean applySMTBasedReductionRules(StructuralReduction sr, Reduc List tokill = DeadlockTester.testDeadTransitionWithSMT(sr, solverPath, isSafe); if (! tokill.isEmpty()) { System.out.println("Found "+tokill.size()+ " dead transitions using SMT." ); - } - if (rt == ReductionType.LIVENESS) { - throw new DeadlockFound(); + if (rt == ReductionType.LIVENESS) { + throw new DeadlockFound(); + } } sr.dropTransitions(tokill,"Dead Transitions using SMT only with invariants"); if (!tokill.isEmpty()) {