X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;ds=sidebyside;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FStateReducer.java;h=e03135454330bf21df98cb80db167cfc819fd8de;hb=9f853a376c28deeae82cb6e9e2841c4f2a0d2fa3;hp=afa1f87fae24ecf4714bc87f460ad1666c687fee;hpb=0e881d025a697dacd179e929a963c7596a49b3ef;p=jpf-core.git

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index afa1f87..e031354 100644
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -187,6 +187,12 @@ public class StateReducer extends ListenerAdapter {
     return copyOfChoices;
   }
 
+  private void continueExecutingThisTrace(IntChoiceFromSet icsCG) {
+    // We repeat the same trace if a state match is not found yet
+    IntChoiceFromSet setCG = setNewCG(icsCG);
+    unusedCG.add(setCG);
+  }
+
   private void initializeChoiceGenerators(IntChoiceFromSet icsCG, Integer[] cgChoices) {
     if (choiceCounter <= choiceUpperBound && !cgMap.containsValue(choiceCounter)) {
       // Update the choices of the first CG and add '-1'
@@ -204,11 +210,18 @@ public class StateReducer extends ListenerAdapter {
       IntChoiceFromSet setCG = setNewCG(icsCG);
       cgMap.put(setCG, refChoices[choiceCounter]);
     } else {
-      // We repeat the same trace if a state match is not found yet
-      IntChoiceFromSet setCG = setNewCG(icsCG);
-      unusedCG.add(setCG);
+      continueExecutingThisTrace(icsCG);
+    }
+  }
+
+  private void manageChoiceGeneratorsInSubsequentTraces(IntChoiceFromSet icsCG) {
+    // If this is the first iteration of the trace then set other CGs done
+    if (choiceCounter <= choiceUpperBound) {
+      icsCG.setDone();
+    } else {
+      // If this is the subsequent iterations of the trace then set up new CGs to continue the execution
+      continueExecutingThisTrace(icsCG);
     }
-    choiceCounter++;
   }
 
   @Override
@@ -229,8 +242,10 @@ public class StateReducer extends ListenerAdapter {
           initializeChoiceGenerators(icsCG, cgChoices);
         } else {
           // Set new CGs to done so that the search algorithm explores the existing CGs
-          icsCG.setDone();
+          //icsCG.setDone();
+          manageChoiceGeneratorsInSubsequentTraces(icsCG);
         }
+        choiceCounter++;
       }
     }
   }
@@ -321,12 +336,11 @@ public class StateReducer extends ListenerAdapter {
   private void exploreNextBacktrackSets(IntChoiceFromSet icsCG) {
     // Traverse the sub-graphs
     if (isResetAfterAnalysis) {
-      // Advance choice counter for sub-graphs
-      choiceCounter++;
       // Do this for every CG after finishing each backtrack list
       // We try to update the CG with a backtrack list if the state has been visited multiple times
       //if ((icsCG.getNextChoice() == -1 || choiceCounter > 1) && cgMap.containsKey(icsCG)) {
-      if ((!icsCG.hasMoreChoices() || choiceCounter > 1) && cgMap.containsKey(icsCG)) {
+      //if ((!icsCG.hasMoreChoices() || choiceCounter > 1) && cgMap.containsKey(icsCG)) {
+      if (choiceCounter > 1 && cgMap.containsKey(icsCG)) {
         int event = cgMap.get(icsCG);
         LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
         if (choiceLists != null && choiceLists.peekFirst() != null) {
@@ -338,6 +352,7 @@ public class StateReducer extends ListenerAdapter {
           // Set done if this was the last backtrack list
           icsCG.setDone();
         }
+        setDoneUnusedCG();
         saveVisitedStates();
       }
     } else {