Fixing bugs and cleaning up: Continuing sub-graph executions when there is no matched...

[jpf-core.git] / src / main / gov / nasa / jpf / listener / StateReducer.java

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index afa1f87fae24ecf4714bc87f460ad1666c687fee..e03135454330bf21df98cb80db167cfc819fd8de 100644 (file)
--- 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;
   }
 
     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'
   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 {
       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
   }
 
   @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
           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) {
   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)) {
       // 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) {
         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();
         }
           // Set done if this was the last backtrack list
           icsCG.setDone();
         }

+        setDoneUnusedCG();

         saveVisitedStates();
       }
     } else {
         saveVisitedStates();
       }
     } else {