From e1fb1260f046bad6333fa9548c91c8fa87ac4ca0 Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Sat, 17 Apr 2021 01:51:05 +0200 Subject: [PATCH 1/3] throw only if non empty tokill --- .../fr/lip6/move/gal/application/ReachabilitySolver.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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()) { From 699317b59215e7bcbb8f5ddf3493a0ba74e11a8e Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Sat, 17 Apr 2021 10:19:38 +0200 Subject: [PATCH 2/3] use care around agglomerations that are one to many and have coefficient --- .../fr/lip6/move/gal/structural/StructuralReduction.java | 6 ++++++ 1 file changed, 6 insertions(+) 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) { From e7af7a92f04e77149b006c69e248474c72427b2b Mon Sep 17 00:00:00 2001 From: Yann Thierry-Mieg Date: Sat, 17 Apr 2021 10:47:13 +0200 Subject: [PATCH 3/3] reduce the cost of reset : it's now free --- .../move/gal/structural/RandomExplorer.java | 40 ++++++++++--------- 1 file changed, 21 insertions(+), 19 deletions(-) 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; } }