From e7af7a92f04e77149b006c69e248474c72427b2b Mon Sep 17 00:00:00 2001
From: Yann Thierry-Mieg <Yann.Thierry-Mieg@lip6.fr>
Date: Sat, 17 Apr 2021 10:47:13 +0200
Subject: [PATCH] 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<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;
 				}
 			}