Cleaning up.
authorrtrimana <rtrimana@uci.edu>
Tue, 9 Jun 2020 19:08:07 +0000 (12:08 -0700)
committerrtrimana <rtrimana@uci.edu>
Tue, 9 Jun 2020 19:08:07 +0000 (12:08 -0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java

index f503dfa..bf9ecfa 100644 (file)
@@ -69,8 +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 HashMap<Integer, Integer> stateToChoiceCounterMap;      // Maps state IDs to the choice counter
-  private HashMap<Integer, HashSet<TransitionEvent>> rGraph;      // Reachability graph for past executions
+  private ReachabilityGraph rGraph;                               // Reachability graph for past executions
 
   // Boolean states
   private boolean isBooleanCGFlipped;
@@ -141,8 +140,6 @@ public class DPORStateReducer extends ListenerAdapter {
               " which is " + detail + " Transition: " + transition + "\n");
     }
     if (stateReductionMode) {
-      // Only add a transition into R-Graph when it advances the state
-      addTransitionToRGRaph();
       updateStateInfo(search);
     }
   }
@@ -237,10 +234,10 @@ public class DPORStateReducer extends ListenerAdapter {
         // If this is a new CG then we need to update data structures
         resetStatesForNewExecution(icsCG, vm);
         // If we don't see a fair scheduling of events/choices then we have to enforce it
-        fairSchedulingAndTransition(icsCG, vm);
+        ensureFairSchedulingAndSetupTransition(icsCG, vm);
         // Update backtrack set of an executed event (transition): one transition before this one
         updateBacktrackSet(currentExecution, choiceCounter - 1);
-        // Explore the next backtrack point: 
+        // Explore the next backtrack point:
         // 1) if we have seen this state or this state contains cycles that involve all events, and
         // 2) after the current CG is advanced at least once
         if (terminateCurrentExecution() && choiceCounter > 0) {
@@ -317,16 +314,18 @@ public class DPORStateReducer extends ListenerAdapter {
   // 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
-  // TODO:    (2) last state with two or more incoming events (transitions)
+  // TODO:    (2) last state with two or more incoming events/transitions
   private class Execution {
     private HashMap<IntChoiceFromSet, Integer> cgToChoiceMap;   // Map between CG to choice numbers for O(1) access
-    private ArrayList<TransitionEvent> executionTrace;           // The BacktrackPoint objects of this execution
+    private ArrayList<TransitionEvent> executionTrace;          // The BacktrackPoint objects of this execution
+    private boolean isNew;                                      // Track if this is the first time it is accessed
     private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;  // Record fields that are accessed
     private HashMap<Integer, TransitionEvent> stateToTransitionMap;  // For O(1) access to backtrack point
 
     public Execution() {
       cgToChoiceMap = new HashMap<>();
       executionTrace = new ArrayList<>();
+      isNew = true;
       readWriteFieldsMap = new HashMap<>();
       stateToTransitionMap = new HashMap<>();
     }
@@ -339,13 +338,6 @@ public class DPORStateReducer extends ListenerAdapter {
       cgToChoiceMap = null;
     }
 
-    public TransitionEvent getTransitionFromState(int stateId) {
-      if (stateToTransitionMap.containsKey(stateId)) {
-        return stateToTransitionMap.get(stateId);
-      }
-      return null;
-    }
-
     public int getChoiceFromCG(IntChoiceFromSet icsCG) {
       return cgToChoiceMap.get(icsCG);
     }
@@ -354,20 +346,29 @@ public class DPORStateReducer extends ListenerAdapter {
       return executionTrace;
     }
 
-    public HashMap<Integer, ReadWriteSet> getReadWriteFieldsMap() {
-      return readWriteFieldsMap;
-    }
-
     public TransitionEvent getFirstTransition() {
       return executionTrace.get(0);
     }
 
-    public TransitionEvent getLastTransition() {
+    public HashMap<Integer, ReadWriteSet> getReadWriteFieldsMap() {
+      return readWriteFieldsMap;
+    }
+
+    public TransitionEvent getTransitionFromState(int stateId) {
+      if (stateToTransitionMap.containsKey(stateId)) {
+        return stateToTransitionMap.get(stateId);
+      }
+      // Return the latest transition for unseen states (that have just been encountered in this transition)
       return executionTrace.get(executionTrace.size() - 1);
     }
 
     public boolean isNew() {
-      return executionTrace.size() == 1;
+      if (isNew) {
+        // Right after this is accessed, it is no longer new
+        isNew = false;
+        return true;
+      }
+      return false;
     }
 
     public void mapCGToChoice(IntChoiceFromSet icsCG, int choice) {
@@ -383,89 +384,62 @@ public class DPORStateReducer extends ListenerAdapter {
   // 1) a predecessor execution
   // 2) the predecessor choice in that predecessor execution
   private class Predecessor {
-    private int predecessorChoice;           // Predecessor choice
-    private Execution predecessorExecution;  // Predecessor execution
+    private int choice;           // Predecessor choice
+    private Execution execution;  // Predecessor execution
 
     public Predecessor(int predChoice, Execution predExec) {
-      predecessorChoice = predChoice;
-      predecessorExecution = predExec;
-    }
-
-    public int getPredecessorChoice() {
-      return predecessorChoice;
-    }
-
-    public Execution getPredecessorExecution() {
-      return predecessorExecution;
-    }
-  }
-
-  // This class compactly stores backtrack points:
-  // 1) CG,
-  // 2) state ID,
-  // 3) choice,
-  // 4) predecessors (for backward DFS).
-  private class TransitionEvent {
-    private IntChoiceFromSet transitionCG;     // CG at this transition
-    private int stateId;                       // State at this transition
-    private int choice;                        // Choice chosen at this transition
-    private Execution execution;               // The execution where this transition belongs
-    private int choiceCounter;                 // Choice counter at this transition
-    private HashSet<Predecessor> predecessors; // Maps incoming events/transitions (execution and choice)
-
-    public TransitionEvent() {
-      transitionCG = null;
-      stateId = -1;
-      choice = -1;
-      execution = null;
-      choiceCounter = -1;
-      predecessors = new HashSet<>();
-    }
-
-    public void setTransitionCG(IntChoiceFromSet cg) {
-      transitionCG = cg;
-    }
-
-    public void setStateId(int stId) {
-      stateId = stId;
-    }
-
-    public void setChoice(int cho) {
-      choice = cho;
-    }
-
-    public void setChoiceCounter(int choCounter) {
-      choiceCounter = choCounter;
-    }
-
-    public IntChoiceFromSet getTransitionCG() { return transitionCG; }
-
-    public int getStateId() {
-      return stateId;
+      choice = predChoice;
+      execution = predExec;
     }
 
     public int getChoice() {
       return choice;
     }
 
-    public int getChoiceCounter() {
-      return choiceCounter;
+    public Execution getExecution() {
+      return execution;
     }
+  }
 
-    public void setExecution(Execution exec) {
-      execution = exec;
+  // This class represents a Reachability Graph
+  private class ReachabilityGraph {
+    private int hiStateId;                                     // Maximum state Id
+    private HashMap<Integer, HashSet<TransitionEvent>> graph;  // Reachability graph for past executions
+
+    public ReachabilityGraph() {
+      hiStateId = 0;
+      graph = new HashMap<>();
     }
 
-    public Execution getExecution() {
-      return execution;
+    public void addReachableTransition(int stateId, TransitionEvent transition) {
+      HashSet<TransitionEvent> transitionSet;
+      if (graph.containsKey(stateId)) {
+        transitionSet = graph.get(stateId);
+      } else {
+        transitionSet = new HashSet<>();
+        graph.put(stateId, transitionSet);
+      }
+      // Insert into the set if it does not contain it yet
+      if (!transitionSet.contains(transition)) {
+        transitionSet.add(transition);
+      }
+      // Update highest state ID
+      if (hiStateId < stateId) {
+        hiStateId = stateId;
+      }
     }
 
-    public HashSet<Predecessor> getPredecessors() {
-      return predecessors;
+    public HashSet<TransitionEvent> getReachableTransitionsAtState(int stateId) {
+      return graph.get(stateId);
     }
 
-    public void recordPredecessor(Execution execution, int choice) {
-      predecessors.add(new Predecessor(choice, execution));
+    public HashSet<TransitionEvent> getReachableTransitions(int stateId) {
+      HashSet<TransitionEvent> reachableTransitions = new HashSet<>();
+      // All transitions from states higher than the given state ID (until the highest state ID) are reachable
+      for(int stId = stateId; stId <= hiStateId; stId++) {
+        reachableTransitions.addAll(graph.get(stId));
+      }
+      return reachableTransitions;
     }
   }
 
@@ -550,6 +524,79 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
+  // This class compactly stores backtrack points:
+  // 1) CG,
+  // 2) state ID,
+  // 3) choice,
+  // 4) predecessors (for backward DFS).
+  private class TransitionEvent {
+    private int choice;                        // Choice chosen at this transition
+    private int choiceCounter;                 // Choice counter at this transition
+    private Execution execution;               // The execution where this transition belongs
+    private HashSet<Predecessor> predecessors; // Maps incoming events/transitions (execution and choice)
+    private int stateId;                       // State at this transition
+    private IntChoiceFromSet transitionCG;     // CG at this transition
+
+    public TransitionEvent() {
+      choice = 0;
+      choiceCounter = 0;
+      execution = null;
+      predecessors = new HashSet<>();
+      stateId = 0;
+      transitionCG = null;
+    }
+
+    public int getChoice() {
+      return choice;
+    }
+
+    public int getChoiceCounter() {
+      return choiceCounter;
+    }
+
+    public Execution getExecution() {
+      return execution;
+    }
+
+    public HashSet<Predecessor> getPredecessors() {
+      return predecessors;
+    }
+
+    public int getStateId() {
+      return stateId;
+    }
+
+    public IntChoiceFromSet getTransitionCG() { return transitionCG; }
+
+    public void recordPredecessor(Execution execution, int choice) {
+      predecessors.add(new Predecessor(choice, execution));
+    }
+
+    public void setChoice(int cho) {
+      choice = cho;
+    }
+
+    public void setChoiceCounter(int choCounter) {
+      choiceCounter = choCounter;
+    }
+
+    public void setExecution(Execution exec) {
+      execution = exec;
+    }
+
+    public void setPredecessors(HashSet<Predecessor> preds) {
+      predecessors = new HashSet<>(preds);
+    }
+
+    public void setStateId(int stId) {
+      stateId = stId;
+    }
+
+    public void setTransitionCG(IntChoiceFromSet cg) {
+      transitionCG = cg;
+    }
+  }
+
   // -- CONSTANTS
   private final static String DO_CALL_METHOD = "doCall";
   // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure
@@ -571,7 +618,14 @@ public class DPORStateReducer extends ListenerAdapter {
   private final static String JAVA_STRING_LIB = "java.lang.String";
 
   // -- FUNCTIONS
-  private void fairSchedulingAndTransition(IntChoiceFromSet icsCG, VM vm) {
+  private Integer[] copyChoices(Integer[] choicesToCopy) {
+
+    Integer[] copyOfChoices = new Integer[choicesToCopy.length];
+    System.arraycopy(choicesToCopy, 0, copyOfChoices, 0, choicesToCopy.length);
+    return copyOfChoices;
+  }
+
+  private void ensureFairSchedulingAndSetupTransition(IntChoiceFromSet icsCG, VM vm) {
     // Check the next choice and if the value is not the same as the expected then force the expected value
     int choiceIndex = choiceCounter % refChoices.length;
     int nextChoice = icsCG.getNextChoice();
@@ -584,6 +638,18 @@ 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
+    for (Integer stId : justVisitedStates) {  // Map this transition to all the previously passed states
+      currentExecution.mapStateToTransition(stId, transition);
+    }
+    currentExecution.mapCGToChoice(icsCG, choiceCounter);
+    // Store restorable state object for this state (always store the latest)
+    RestorableVMState restorableState = vm.getRestorableState();
+    restorableStateMap.put(stateId, restorableState);
+  }
+
+  private TransitionEvent setupTransition(IntChoiceFromSet icsCG, int stateId, int choiceIndex) {
     // Get a new transition
     TransitionEvent transition;
     if (currentExecution.isNew()) {
@@ -591,6 +657,7 @@ public class DPORStateReducer extends ListenerAdapter {
       transition = currentExecution.getFirstTransition();
     } else {
       transition = new TransitionEvent();
+      currentExecution.addTransition(transition);
       transition.recordPredecessor(currentExecution, choiceCounter - 1);
     }
     transition.setExecution(currentExecution);
@@ -598,20 +665,12 @@ public class DPORStateReducer extends ListenerAdapter {
     transition.setStateId(stateId);
     transition.setChoice(refChoices[choiceIndex]);
     transition.setChoiceCounter(choiceCounter);
-    // Add new transition to the current execution
-    currentExecution.mapStateToTransition(stateId, transition);
-    currentExecution.addTransition(transition);
-    currentExecution.mapCGToChoice(icsCG, choiceCounter);
-    // Store restorable state object for this state (always store the latest)
-    RestorableVMState restorableState = vm.getRestorableState();
-    restorableStateMap.put(stateId, restorableState);
-  }
-
-  private Integer[] copyChoices(Integer[] choicesToCopy) {
+    // Add transition into R-Graph
+    for (Integer stId : justVisitedStates) {
+      rGraph.addReachableTransition(stId, transition);
+    }
 
-    Integer[] copyOfChoices = new Integer[choicesToCopy.length];
-    System.arraycopy(choicesToCopy, 0, copyOfChoices, 0, choicesToCopy.length);
-    return copyOfChoices;
+    return transition;
   }
 
   // --- Functions related to cycle detection and reachability graph
@@ -656,8 +715,7 @@ public class DPORStateReducer extends ListenerAdapter {
     currentExecution = new Execution();
     currentExecution.addTransition(new TransitionEvent()); // Always start with 1 backtrack point
     doneBacktrackSet = new HashSet<>();
-    stateToChoiceCounterMap = new HashMap<>();
-    rGraph = new HashMap<>();
+    rGraph = new ReachabilityGraph();
     // Booleans
     isEndOfExecution = false;
   }
@@ -672,26 +730,6 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
-  // Save the current transition into R-Graph
-  // Basically the current transition is reachable from the final state of the previous transition in this execution
-  private void addTransitionToRGRaph() {
-    // Get the current transition
-    TransitionEvent currTrans = currentExecution.getLastTransition();
-    // This transition is reachable from this source state when it has advanced the state
-    int stateId = currTrans.getStateId();
-    // Add transition into R-Graph
-    HashSet<TransitionEvent> transitionSet;
-    if (rGraph.containsKey(stateId)) {
-      transitionSet = rGraph.get(stateId);
-    } else {
-      transitionSet = new HashSet<>();
-    }
-    // Insert into the set if it does not contain it yet
-    if (!transitionSet.contains(currTrans)) {
-      transitionSet.add(currTrans);
-    }
-  }
-
   private boolean terminateCurrentExecution() {
     // We need to check all the states that have just been visited
     // Often a transition (choice/event) can result into forwarding/backtracking to a number of states
@@ -713,14 +751,16 @@ public class DPORStateReducer extends ListenerAdapter {
       stateToEventMap.put(stateId, eventSet);
     }
     analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
-    stateToChoiceCounterMap.put(stateId, choiceCounter);
     justVisitedStates.add(stateId);
-    currVisitedStates.add(stateId);
+    if (!prevVisitedStates.contains(stateId)) {
+      // It is a currently visited states if the state has not been seen in previous executions
+      currVisitedStates.add(stateId);
+    }
   }
 
   // --- Functions related to Read/Write access analysis on shared fields
 
-  private void addNewBacktrackPoint(int stateId, Integer[] newChoiceList, Execution parentExecution, int parentChoice) {
+  private void addNewBacktrackPoint(int stateId, Integer[] newChoiceList, TransitionEvent conflictTransition) {
     // Insert backtrack point to the right state ID
     LinkedList<BacktrackExecution> backtrackExecList;
     if (backtrackMap.containsKey(stateId)) {
@@ -731,7 +771,7 @@ public class DPORStateReducer extends ListenerAdapter {
     }
     // Add the new backtrack execution object
     TransitionEvent backtrackTransition = new TransitionEvent();
-    backtrackTransition.recordPredecessor(parentExecution, parentChoice);
+    backtrackTransition.setPredecessors(conflictTransition.getPredecessors());
     backtrackExecList.addFirst(new BacktrackExecution(newChoiceList, backtrackTransition));
     // Add to priority queue
     if (!backtrackStateQ.contains(stateId)) {
@@ -817,17 +857,16 @@ public class DPORStateReducer extends ListenerAdapter {
     return currentChoice;
   }
 
-  private void createBacktrackingPoint(Execution execution, int currentChoice, int conflictChoice) {
-
+  private void createBacktrackingPoint(Execution execution, int currentChoice,
+                                       Execution conflictExecution, int conflictChoice) {
     // Create a new list of choices for backtrack based on the current choice and conflicting event number
     // E.g. if we have a conflict between 1 and 3, then we create the list {3, 1, 0, 2}
     // for the original set {0, 1, 2, 3}
     Integer[] newChoiceList = new Integer[refChoices.length];
-    //int firstChoice = choices[actualChoice];
-    ArrayList<TransitionEvent> pastTrace = execution.getExecutionTrace();
-    ArrayList<TransitionEvent> currTrace = currentExecution.getExecutionTrace();
-    int currChoice = currTrace.get(currentChoice).getChoice();
-    int stateId = pastTrace.get(conflictChoice).getStateId();
+    ArrayList<TransitionEvent> currentTrace = execution.getExecutionTrace();
+    ArrayList<TransitionEvent> conflictTrace = conflictExecution.getExecutionTrace();
+    int currChoice = currentTrace.get(currentChoice).getChoice();
+    int stateId = conflictTrace.get(conflictChoice).getStateId();
     // Check if this trace has been done from this state
     if (isTraceAlreadyConstructed(currChoice, stateId)) {
       return;
@@ -841,8 +880,8 @@ public class DPORStateReducer extends ListenerAdapter {
         j++;
       }
     }
-    // Parent choice is conflict choice - 1
-    addNewBacktrackPoint(stateId, newChoiceList, execution, conflictChoice - 1);
+    // Predecessor of the new backtrack point is the same as the conflict point's
+    addNewBacktrackPoint(stateId, newChoiceList, conflictTrace.get(conflictChoice));
   }
 
   private boolean excludeThisForItContains(String[] excludedStrings, String className) {
@@ -873,7 +912,6 @@ public class DPORStateReducer extends ListenerAdapter {
   }
 
   private void exploreNextBacktrackPoints(VM vm, IntChoiceFromSet icsCG) {
-
                // Check if we are reaching the end of our execution: no more backtracking points to explore
                // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough)
                if (!backtrackStateQ.isEmpty()) {
@@ -901,65 +939,26 @@ public class DPORStateReducer extends ListenerAdapter {
                isEndOfExecution = true;
   }
 
-  private boolean isConflictFound(Execution execution, int reachableChoice, int conflictChoice,
+  private boolean isConflictFound(Execution execution, int reachableChoice, Execution conflictExecution, int conflictChoice,
                                   ReadWriteSet currRWSet) {
-
     ArrayList<TransitionEvent> executionTrace = execution.getExecutionTrace();
     HashMap<Integer, ReadWriteSet> execRWFieldsMap = execution.getReadWriteFieldsMap();
+    ArrayList<TransitionEvent> conflictTrace = conflictExecution.getExecutionTrace();
     // Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
     if (!execRWFieldsMap.containsKey(conflictChoice) ||
-            executionTrace.get(reachableChoice).getChoice() == executionTrace.get(conflictChoice).getChoice()) {
+            executionTrace.get(reachableChoice).getChoice() == conflictTrace.get(conflictChoice).getChoice()) {
       return false;
     }
     // R/W set of choice/event that may have a potential conflict
     ReadWriteSet evtRWSet = execRWFieldsMap.get(conflictChoice);
     // Check for conflicts with Read and Write fields for Write instructions
     Set<String> currWriteSet = currRWSet.getWriteSet();
-    for(String writeField : currWriteSet) {
-      int currObjId = currRWSet.writeFieldObjectId(writeField);
-      if (evtRWSet.readFieldExists(writeField) && evtRWSet.readFieldObjectId(writeField) == currObjId) {
-        // Remove this from the read set as we are tracking per memory location
-        evtRWSet.removeWriteField(writeField);
-        return true;
-      } else if (evtRWSet.writeFieldExists(writeField) && evtRWSet.writeFieldObjectId(writeField) == currObjId) {
-        // Remove this from the write set as we are tracking per memory location
-        evtRWSet.removeReadField(writeField);
-        return true;
-      }
-    }
-    // Check for conflicts with Write fields for Read instructions
-    Set<String> currReadSet = currRWSet.getReadSet();
-    for(String readField : currReadSet) {
-      int currObjId = currRWSet.readFieldObjectId(readField);
-      if (evtRWSet.writeFieldExists(readField) && evtRWSet.writeFieldObjectId(readField) == currObjId) {
-        // Remove this from the write set as we are tracking per memory location
-        evtRWSet.removeWriteField(readField);
-        return true;
-      }
-    }
-    // Return false if no conflict is found
-    return false;
-  }
-
-  private boolean isConflictFound(Execution execution, int reachableChoice, int conflictChoice) {
-
-    ArrayList<TransitionEvent> executionTrace = execution.getExecutionTrace();
-    HashMap<Integer, ReadWriteSet> execRWFieldsMap = execution.getReadWriteFieldsMap();
-    // Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
-    if (!execRWFieldsMap.containsKey(conflictChoice) ||
-            executionTrace.get(reachableChoice).getChoice() == executionTrace.get(conflictChoice).getChoice()) {
-      return false;
-    }
-    // Current R/W set
-    ReadWriteSet currRWSet = execRWFieldsMap.get(reachableChoice);
-    // R/W set of choice/event that may have a potential conflict
-    ReadWriteSet evtRWSet = execRWFieldsMap.get(conflictChoice);
-    // Check for conflicts with Read and Write fields for Write instructions
-    Set<String> currWriteSet = currRWSet.getWriteSet();
     for(String writeField : currWriteSet) {
       int currObjId = currRWSet.writeFieldObjectId(writeField);
       if ((evtRWSet.readFieldExists(writeField) && evtRWSet.readFieldObjectId(writeField) == currObjId) ||
-              (evtRWSet.writeFieldExists(writeField) && evtRWSet.writeFieldObjectId(writeField) == currObjId)) {
+          (evtRWSet.writeFieldExists(writeField) && evtRWSet.writeFieldObjectId(writeField) == currObjId)) {
+        // Remove this from the write set as we are tracking per memory location
+        currRWSet.removeWriteField(writeField);
         return true;
       }
     }
@@ -968,6 +967,8 @@ public class DPORStateReducer extends ListenerAdapter {
     for(String readField : currReadSet) {
       int currObjId = currRWSet.readFieldObjectId(readField);
       if (evtRWSet.writeFieldExists(readField) && evtRWSet.writeFieldObjectId(readField) == currObjId) {
+        // Remove this from the read set as we are tracking per memory location
+        currRWSet.removeReadField(readField);
         return true;
       }
     }
@@ -1028,7 +1029,6 @@ public class DPORStateReducer extends ListenerAdapter {
       refChoices = copyChoices(choices);
       // Clear data structures
       currVisitedStates = new HashSet<>();
-      stateToChoiceCounterMap = new HashMap<>();
       stateToEventMap = new HashMap<>();
       isEndOfExecution = false;
     }
@@ -1064,20 +1064,24 @@ public class DPORStateReducer extends ListenerAdapter {
     int conflictChoice = currentChoice;
     // Copy ReadWriteSet object
     HashMap<Integer, ReadWriteSet> currRWFieldsMap = execution.getReadWriteFieldsMap();
-    ReadWriteSet currRWSet = currRWFieldsMap.get(currentChoice).getCopy();
+    ReadWriteSet currRWSet = currRWFieldsMap.get(currentChoice);
+    if (currRWSet == null) {
+      return;
+    }
+    currRWSet = currRWSet.getCopy();
     // 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, conflictChoice, currRWSet, visited);
+    updateBacktrackSetRecursive(execution, currentChoice, execution, conflictChoice, currRWSet, visited);
   }
 
-  private void updateBacktrackSetRecursive(Execution execution, int currentChoice, int conflictChoice,
+  private void updateBacktrackSetRecursive(Execution execution, int currentChoice, Execution conflictExecution, int conflictChoice,
                                            ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
     // Halt when we have found the first read/write conflicts for all memory locations
     if (currRWSet.isEmpty()) {
       return;
     }
-    TransitionEvent confTrans = execution.getExecutionTrace().get(conflictChoice);
+    TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice);
     // Halt when we have visited this transition (in a cycle)
     if (visited.contains(confTrans)) {
       return;
@@ -1086,14 +1090,14 @@ public class DPORStateReducer extends ListenerAdapter {
     // Explore all predecessors
     for (Predecessor predecessor : confTrans.getPredecessors()) {
       // Get the predecessor (previous conflict choice)
-      conflictChoice = predecessor.getPredecessorChoice();
-      execution = predecessor.getPredecessorExecution();
+      conflictChoice = predecessor.getChoice();
+      conflictExecution = predecessor.getExecution();
       // Check if a conflict is found
-      if (isConflictFound(execution, currentChoice, conflictChoice, currRWSet)) {
-        createBacktrackingPoint(execution, currentChoice, conflictChoice);
+      if (isConflictFound(execution, currentChoice, conflictExecution, conflictChoice, currRWSet)) {
+        createBacktrackingPoint(execution, currentChoice, conflictExecution, conflictChoice);
       }
       // Continue performing DFS if conflict is not found
-      updateBacktrackSetRecursive(execution, currentChoice, conflictChoice, currRWSet, visited);
+      updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited);
     }
   }
 
@@ -1101,11 +1105,10 @@ public class DPORStateReducer extends ListenerAdapter {
 
   private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {
     // Perform this analysis only when:
-    // 1) there is a state match,
-    // 2) this is not during a switch to a new execution,
-    // 3) at least 2 choices/events have been explored (choiceCounter > 1),
-    // 4) state > 0 (state 0 is for boolean CG)
-    if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 && (stateId > 0)) {
+    // 1) this is not during a switch to a new execution,
+    // 2) at least 2 choices/events have been explored (choiceCounter > 1),
+    // 3) state > 0 (state 0 is for boolean CG)
+    if (!isEndOfExecution && choiceCounter > 1 && stateId > 0) {
       if (currVisitedStates.contains(stateId)) {
         // Get the backtrack point from the current execution
         TransitionEvent transition = currentExecution.getTransitionFromState(stateId);
@@ -1113,10 +1116,9 @@ public class DPORStateReducer extends ListenerAdapter {
         updateBacktrackSetsFromPreviousExecution(stateId);
       } else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution
         // Update past executions with a predecessor
-        HashSet<TransitionEvent> reachableTransitions = rGraph.get(stateId);
+        HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitionsAtState(stateId);
         for(TransitionEvent transition : reachableTransitions) {
-          Execution execution = transition.getExecution();
-          transition.recordPredecessor(execution, choiceCounter - 1);
+          transition.recordPredecessor(currentExecution, choiceCounter - 1);
         }
         updateBacktrackSetsFromPreviousExecution(stateId);
       }
@@ -1126,7 +1128,7 @@ public class DPORStateReducer extends ListenerAdapter {
   // Update the backtrack sets from previous executions
   private void updateBacktrackSetsFromPreviousExecution(int stateId) {
     // Collect all the reachable transitions from R-Graph
-    HashSet<TransitionEvent> reachableTransitions = rGraph.get(stateId);
+    HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitions(stateId);
     for(TransitionEvent transition : reachableTransitions) {
       Execution execution = transition.getExecution();
       int currentChoice = transition.getChoiceCounter();