From 11a20606896f5b99be7d897800f8bf1e4065e9cb Mon Sep 17 00:00:00 2001
From: rtrimana <rtrimana@uci.edu>
Date: Mon, 23 Mar 2020 14:41:04 -0700
Subject: [PATCH] Cleaning up, fixing bugs---commented out full-blown graph
 traversal code.

---
 .../gov/nasa/jpf/listener/StateReducer.java   | 42 +++++++++----------
 1 file changed, 21 insertions(+), 21 deletions(-)

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 3af3205..96d49a3 100644
--- 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 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
@@ -119,8 +120,8 @@ public class StateReducer extends ListenerAdapter {
     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<>();
@@ -137,10 +138,9 @@ public class StateReducer extends ListenerAdapter {
       isInitialized = false;
       isResetAfterAnalysis = false;
       cgMap.clear();
-      readWriteFieldsMap.clear();
+      resetReadWriteAnalysis();
       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]);
+    if (choiceIndex == 0) {
+      resetReadWriteAnalysis();
+    }
     return icsCG;
   }
 
@@ -193,7 +202,6 @@ public class StateReducer extends ListenerAdapter {
       IntChoiceFromSet setCG = setNewCG(icsCG);
       unusedCG.add(setCG);
     }
-    //choiceCounter = choiceCounter < choiceUpperBound ? choiceCounter + 1 : 0;
     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) {
 
-    HashSet<ConflictTracker.Node> visitingStates = new HashSet<>();
     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
-      conflictPairMap.clear();
-      readWriteFieldsMap.clear();
+      resetReadWriteAnalysis();
       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
-    updateVODGraph(prevChoiceValue, currChoiceValue);
-    prevChoiceValue = currChoiceValue;
-  }
-
-  private void updateVODGraph(int prevChoice, int currChoice) {
-
     HashSet<Integer> choiceSet;
-    if (vodGraphMap.containsKey(prevChoice)) {
+    if (vodGraphMap.containsKey(prevChoiceValue)) {
       // If the key already exists, just retrieve it
-      choiceSet = vodGraphMap.get(prevChoice);
+      choiceSet = vodGraphMap.get(prevChoiceValue);
     } 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) {
@@ -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 (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;
-- 
2.34.1