Cleaning up, fixing bugs---commented out full-blown graph traversal code.

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 3af3205cea585bf5bf5ddc43af1af7779871239c..96d49a3d3ccfe5d930369f14485812ab0b7d343f 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -90,7 +90,8 @@ public class StateReducer extends ListenerAdapter {
   private HashSet<IntChoiceFromSet> unusedCG;
 
   // Reference to the state graph in the ConflictTracker class
   private HashSet<IntChoiceFromSet> unusedCG;
 
   // Reference to the state graph in the ConflictTracker class

-  private HashMap<Integer, ConflictTracker.Node> stateGraph;
+  // TODO: The following is a full-blown graph traversal that we can do if we need to in the future
+  //private HashMap<Integer, ConflictTracker.Node> stateGraph;

   private HashMap<Integer, HashSet<Integer>> stateToEventMap;
   // Map state to event
   // Visited states in the previous and current executions/traces for terminating condition
   private HashMap<Integer, HashSet<Integer>> stateToEventMap;
   // Map state to event
   // Visited states in the previous and current executions/traces for terminating condition


@@ -119,8 +120,8 @@ public class StateReducer extends ListenerAdapter {
     backtrackSet = new HashSet<>();
     conflictPairMap = new HashMap<>();
     unusedCG = new HashSet<>();
     backtrackSet = new HashSet<>();
     conflictPairMap = new HashMap<>();
     unusedCG = new HashSet<>();

-    // TODO: We are assuming that the StateReducer is always used together with the ConflictTracker
-    stateGraph = ConflictTracker.nodes;
+    // TODO: The following is a full-blown graph traversal that we can do if we need to in the future
+    //stateGraph = ConflictTracker.nodes;

     stateToEventMap = new HashMap<>();
     prevVisitedStates = new HashSet<>();
     currVisitedStates = new HashSet<>();
     stateToEventMap = new HashMap<>();
     prevVisitedStates = new HashSet<>();
     currVisitedStates = new HashSet<>();


@@ -137,10 +138,9 @@ public class StateReducer extends ListenerAdapter {
       isInitialized = false;
       isResetAfterAnalysis = false;
       cgMap.clear();
       isInitialized = false;
       isResetAfterAnalysis = false;
       cgMap.clear();

-      readWriteFieldsMap.clear();
+      resetReadWriteAnalysis();

       backtrackMap.clear();
       backtrackSet.clear();
       backtrackMap.clear();
       backtrackSet.clear();

-      conflictPairMap.clear();

     }
   }
 
     }
   }
 


@@ -164,12 +164,21 @@ public class StateReducer extends ListenerAdapter {
     }
   }
 
     }
   }
 

+  private void resetReadWriteAnalysis() {
+    // Reset the following data structure when the choice counter reaches 0 again
+    conflictPairMap.clear();
+    readWriteFieldsMap.clear();
+  }
+

   private IntChoiceFromSet setNewCG(IntChoiceFromSet icsCG) {
     icsCG.setNewValues(choices);
     icsCG.reset();
     // Use a modulo since choiceCounter is going to keep increasing
     int choiceIndex = choiceCounter % (choices.length - 1);
     icsCG.advance(choices[choiceIndex]);
   private IntChoiceFromSet setNewCG(IntChoiceFromSet icsCG) {
     icsCG.setNewValues(choices);
     icsCG.reset();
     // Use a modulo since choiceCounter is going to keep increasing
     int choiceIndex = choiceCounter % (choices.length - 1);
     icsCG.advance(choices[choiceIndex]);

+    if (choiceIndex == 0) {
+      resetReadWriteAnalysis();
+    }

     return icsCG;
   }
 
     return icsCG;
   }
 


@@ -193,7 +202,6 @@ public class StateReducer extends ListenerAdapter {
       IntChoiceFromSet setCG = setNewCG(icsCG);
       unusedCG.add(setCG);
     }
       IntChoiceFromSet setCG = setNewCG(icsCG);
       unusedCG.add(setCG);
     }

-    //choiceCounter = choiceCounter < choiceUpperBound ? choiceCounter + 1 : 0;

     choiceCounter++;
   }
 
     choiceCounter++;
   }
 


@@ -261,7 +269,6 @@ public class StateReducer extends ListenerAdapter {
   // Basically, we have to check that we have executed all events between two occurrences of such state.
   private boolean containsCyclesWithAllEvents(int stId) {
 
   // Basically, we have to check that we have executed all events between two occurrences of such state.
   private boolean containsCyclesWithAllEvents(int stId) {
 

-    HashSet<ConflictTracker.Node> visitingStates = new HashSet<>();

     HashSet<Integer> visitedEvents = stateToEventMap.get(stId);
     boolean containsCyclesWithAllEvts = false;
     if (checkIfAllEventsInvolved(visitedEvents)) {
     HashSet<Integer> visitedEvents = stateToEventMap.get(stId);
     boolean containsCyclesWithAllEvts = false;
     if (checkIfAllEventsInvolved(visitedEvents)) {


@@ -331,8 +338,7 @@ public class StateReducer extends ListenerAdapter {
       currCG = icsCG;
       choices = icsCG.getAllChoices();
       // Reset a few things for the sub-graph
       currCG = icsCG;
       choices = icsCG.getAllChoices();
       // Reset a few things for the sub-graph

-      conflictPairMap.clear();
-      readWriteFieldsMap.clear();
+      resetReadWriteAnalysis();

       choiceCounter = 0;
     }
   }
       choiceCounter = 0;
     }
   }


@@ -396,22 +402,17 @@ public class StateReducer extends ListenerAdapter {
 
   private void updateVODGraph(int currChoiceValue) {
     // Update the graph when we have the current choice value
 
   private void updateVODGraph(int currChoiceValue) {
     // Update the graph when we have the current choice value

-    updateVODGraph(prevChoiceValue, currChoiceValue);
-    prevChoiceValue = currChoiceValue;
-  }
-
-  private void updateVODGraph(int prevChoice, int currChoice) {
-

     HashSet<Integer> choiceSet;
     HashSet<Integer> choiceSet;

-    if (vodGraphMap.containsKey(prevChoice)) {
+    if (vodGraphMap.containsKey(prevChoiceValue)) {

       // If the key already exists, just retrieve it
       // If the key already exists, just retrieve it

-      choiceSet = vodGraphMap.get(prevChoice);
+      choiceSet = vodGraphMap.get(prevChoiceValue);

     } else {
       // Create a new entry
       choiceSet = new HashSet<>();
     } else {
       // Create a new entry
       choiceSet = new HashSet<>();

-      vodGraphMap.put(prevChoice, choiceSet);
+      vodGraphMap.put(prevChoiceValue, choiceSet);

     }
     }

-    choiceSet.add(currChoice);
+    choiceSet.add(currChoiceValue);
+    prevChoiceValue = currChoiceValue;

   }
 
   private void mapStateToEvent(Search search) {
   }
 
   private void mapStateToEvent(Search search) {


@@ -771,8 +772,7 @@ public class StateReducer extends ListenerAdapter {
                   // If it has been serviced before, we just skip this
                   if (recordConflictPair(currentChoice, eventNumber)) {
                     // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above)
                   // If it has been serviced before, we just skip this
                   if (recordConflictPair(currentChoice, eventNumber)) {
                     // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above)

-                    if (vm.isNewState() ||
-                            (!vm.isNewState() && isReachableInVODGraph(choices[currentChoice], choices[currentChoice-1]))) {
+                    if (vm.isNewState() || isReachableInVODGraph(choices[currentChoice], choices[currentChoice-1])) {

                       createBacktrackChoiceList(currentChoice, eventNumber);
                       // Break if a conflict is found!
                       break;
                       createBacktrackChoiceList(currentChoice, eventNumber);
                       // Break if a conflict is found!
                       break;