Further cleaning up (naming, comments, etc.).

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 823bd525491681dca1f469204423ca44ccf92f7a..93fbca772c1ea9d0f0ec169e323885caf88d97dc 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -69,7 +69,7 @@ public class DPORStateReducer extends ListenerAdapter {
   private Execution currentExecution;                             // Holds the information about the current execution
   private HashSet<String> doneBacktrackSet;                       // Record state ID and trace already constructed
   private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
-  private ReachabilityGraph rGraph;                               // Reachability graph for past executions
+  private RGraph rGraph;                                          // R-Graph for past executions
 
   // Boolean states
   private boolean isBooleanCGFlipped;
@@ -215,7 +215,6 @@ public class DPORStateReducer extends ListenerAdapter {
 
   @Override
   public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
-
     if (stateReductionMode) {
       // Check the boolean CG and if it is flipped, we are resetting the analysis
       if (currentCG instanceof BooleanChoiceGenerator) {
@@ -310,7 +309,7 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
-  // This class stores a representation of the execution graph node
+  // This class stores a representation of an execution
   // TODO: We can modify this class to implement some optimization (e.g., clock-vector)
   // TODO: We basically need to keep track of:
   // TODO:    (1) last read/write access to each memory location
@@ -401,12 +400,13 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
-  // This class represents a Reachability Graph
-  private class ReachabilityGraph {
+  // This class represents a R-Graph (in the paper it is a state transition graph R)
+  // This implementation stores reachable transitions from and connects with past executions
+  private class RGraph {
     private int hiStateId;                                     // Maximum state Id
-    private HashMap<Integer, HashSet<TransitionEvent>> graph;  // Reachability graph for past executions
+    private HashMap<Integer, HashSet<TransitionEvent>> graph;  // Reachable transitions from past executions
 
-    public ReachabilityGraph() {
+    public RGraph() {
       hiStateId = 0;
       graph = new HashMap<>();
     }
@@ -524,7 +524,7 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
-  // This class compactly stores backtrack points:
+  // This class compactly stores transitions:
   // 1) CG,
   // 2) state ID,
   // 3) choice,
@@ -639,8 +639,9 @@ public class DPORStateReducer extends ListenerAdapter {
     // Get state ID and associate it with this transition
     int stateId = vm.getStateId();
     TransitionEvent transition = setupTransition(icsCG, stateId, choiceIndex);
-    // Add new transition to the current execution
+    // Add new transition to the current execution and map it in R-Graph
     for (Integer stId : justVisitedStates) {  // Map this transition to all the previously passed states
+      rGraph.addReachableTransition(stId, transition);
       currentExecution.mapStateToTransition(stId, transition);
     }
     currentExecution.mapCGToChoice(icsCG, choiceCounter);
@@ -665,10 +666,6 @@ public class DPORStateReducer extends ListenerAdapter {
     transition.setStateId(stateId);
     transition.setChoice(refChoices[choiceIndex]);
     transition.setChoiceCounter(choiceCounter);
-    // Add transition into R-Graph
-    for (Integer stId : justVisitedStates) {
-      rGraph.addReachableTransition(stId, transition);
-    }
 
     return transition;
   }
@@ -682,7 +679,6 @@ public class DPORStateReducer extends ListenerAdapter {
   // With simple approach we only need to check for a re-visited state.
   // Basically, we have to check that we have executed all events between two occurrences of such state.
   private boolean completeFullCycle(int stId) {
-
     // False if the state ID hasn't been recorded
     if (!stateToEventMap.containsKey(stId)) {
       return false;
@@ -715,7 +711,7 @@ public class DPORStateReducer extends ListenerAdapter {
     currentExecution = new Execution();
     currentExecution.addTransition(new TransitionEvent()); // Always start with 1 backtrack point
     doneBacktrackSet = new HashSet<>();
-    rGraph = new ReachabilityGraph();
+    rGraph = new RGraph();
     // Booleans
     isEndOfExecution = false;
   }
@@ -743,7 +739,6 @@ public class DPORStateReducer extends ListenerAdapter {
 
   private void updateStateInfo(Search search) {
     // Update the state variables
-    // Line 19 in the paper page 11 (see the heading note above)
     int stateId = search.getStateId();
     // Insert state ID into the map if it is new
     if (!stateToEventMap.containsKey(stateId)) {
@@ -1060,8 +1055,6 @@ public class DPORStateReducer extends ListenerAdapter {
   // 1) recursively, and
   // 2) track accesses per memory location (per shared variable/field)
   private void updateBacktrackSet(Execution execution, int currentChoice) {
-    // Choice/event we want to check for conflict against (start from actual choice)
-    int conflictChoice = currentChoice;
     // Copy ReadWriteSet object
     HashMap<Integer, ReadWriteSet> currRWFieldsMap = execution.getReadWriteFieldsMap();
     ReadWriteSet currRWSet = currRWFieldsMap.get(currentChoice);
@@ -1072,11 +1065,13 @@ public class DPORStateReducer extends ListenerAdapter {
     // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
     HashSet<TransitionEvent> visited = new HashSet<>();
     // Update backtrack set recursively
-//    updateBacktrackSetRecursive(execution, currentChoice, execution, conflictChoice, currRWSet, visited);
-    int hbChoice = currentChoice;
-    updateBacktrackSetRecursive(execution, currentChoice, execution, conflictChoice, execution, hbChoice, currRWSet, visited);
+    // TODO: The following is the call to the original version of the method
+//    updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited);
+    // TODO: The following is the call to the version of the method with pushing up happens-before transitions
+    updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, execution, currentChoice, currRWSet, visited);
   }
 
+//  TODO: This is the original version of the recursive method
 //  private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
 //                                           Execution conflictExecution, int conflictChoice,
 //                                           ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {