Merge pull request #12 from lip6/master

merging
lip6 · Apr 17, 2021 · 76d2822 · 76d2822
2 parents 45b346c + e7af7a9
commit 76d2822
Show file tree

Hide file tree

Showing 3 changed files with 30 additions and 22 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
@@ -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<Expression> 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<Expression> 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
@@ -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/....lip6.move.gal.application.pnmcc/src/fr/lip6/move/gal/application/ReachabilitySolver.java b/....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<Integer> 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()) {