reduce the cost of reset : it's now free

lip6 · Apr 17, 2021 · e7af7a9 · e7af7a9
1 parent 699317b
commit e7af7a9
Showing 1 changed file with 21 additions and 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
@@ -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;
 				}
 			}