Attempting state-based DPOR implementation from the SPIN paper.

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 6d5a026deaf20e552e058bcae870085ee912154b..2194ff160d3074b2a9325a2c75cab2b97f2d0d1f 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -76,7 +76,7 @@ public class StateReducer extends ListenerAdapter {
   private HashSet<String> backtrackSet;
   private HashMap<Integer, HashSet<Integer>> conflictPairMap;
   // Map choicelist with start index
   private HashSet<String> backtrackSet;
   private HashMap<Integer, HashSet<Integer>> conflictPairMap;
   // Map choicelist with start index

-//  private HashMap<Integer[],Integer> choiceListStartIndexMap;
+  //  private HashMap<Integer[],Integer> choiceListStartIndexMap;

 
   // Map that represents graph G
   // (i.e., visible operation dependency graph (VOD Graph)
 
   // Map that represents graph G
   // (i.e., visible operation dependency graph (VOD Graph)


@@ -238,7 +238,7 @@ public class StateReducer extends ListenerAdapter {
           // Advance choice counter for sub-graphs
           choiceCounter++;
           // Do this for every CG after finishing each backtrack list
           // Advance choice counter for sub-graphs
           choiceCounter++;
           // Do this for every CG after finishing each backtrack list

-          if (icsCG.getNextChoice() == -1) {
+          if (icsCG.getNextChoice() == -1 || visitedStateSet.contains(stateId)) {

             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) {


@@ -295,19 +295,12 @@ public class StateReducer extends ListenerAdapter {
               " which is " + detail + " Transition: " + transition + "\n");
     }
     if (stateReductionMode) {
               " which is " + detail + " Transition: " + transition + "\n");
     }
     if (stateReductionMode) {

-      // Line 19 in the paper page 11 (see the heading note above)
-      stateId = search.getStateId();
-      if (visitedStateSet.contains(stateId)) {
-        // VOD graph is not updated if the "new" state has been seen earlier
-        return;
-      }
-      // Add state ID into the visited state set
-      visitedStateSet.add(stateId);

       // Update vodGraph
       int currChoice = choiceCounter - 1;
       int prevChoice = currChoice - 1;
       if (currChoice < 0) {
         // Current choice has to be at least 0 (initial case can be -1)
       // Update vodGraph
       int currChoice = choiceCounter - 1;
       int prevChoice = currChoice - 1;
       if (currChoice < 0) {
         // Current choice has to be at least 0 (initial case can be -1)

+        visitedStateSet.add(stateId);

         return;
       }
       // Current choice and previous choice values could be -1 (since we use -1 as the end-of-array condition)
         return;
       }
       // Current choice and previous choice values could be -1 (since we use -1 as the end-of-array condition)


@@ -315,6 +308,10 @@ public class StateReducer extends ListenerAdapter {
       // When current choice is 0, previous choice could be -1
       int prevChoiceValue = (prevChoice == -1) ? -1 : choices[prevChoice];
       updateVODGraph(prevChoiceValue, currChoiceValue);
       // When current choice is 0, previous choice could be -1
       int prevChoiceValue = (prevChoice == -1) ? -1 : choices[prevChoice];
       updateVODGraph(prevChoiceValue, currChoiceValue);

+      // Line 19 in the paper page 11 (see the heading note above)
+      stateId = search.getStateId();
+      // Add state ID into the visited state set
+      visitedStateSet.add(stateId);

     }
   }
 
     }
   }