Small edits in method updateBacktrackSetsFromPreviousExecution.

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
index 48297ccde1b33d969bed828cf7b201cd6973995e..7512691915478dfd6c6bd197864a5fbb3d602957 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
@@ -1220,14 +1220,15 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
   private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
                                            Execution conflictExecution, int conflictChoice,
                                            ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
-    TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
     // TODO: THIS IS THE ACCESS SUMMARY
+    TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice);
     // Record this transition into rGraph summary
-    currRWSet = rGraph.recordTransitionSummary(currTrans.getStateId(), currTrans, currRWSet);
+    currRWSet = rGraph.recordTransitionSummary(confTrans.getStateId(), confTrans, currRWSet);
     // Halt when we have found the first read/write conflicts for all memory locations
     if (currRWSet.isEmpty()) {
       return;
     }
+    TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
     if (visited.contains(currTrans)) {
       return;
     }
@@ -1307,11 +1308,12 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
     // Collect all the reachable transitions from R-Graph
     HashMap<Integer, SummaryNode> reachableTransitions = rGraph.getReachableTransitionsSummary(stateId);
     for(Map.Entry<Integer, SummaryNode> transition : reachableTransitions.entrySet()) {
-      TransitionEvent reachableTransition = transition.getValue().getTransitionEvent();
+      SummaryNode summaryNode = transition.getValue();
+      TransitionEvent reachableTransition = summaryNode.getTransitionEvent();
       Execution conflictExecution = reachableTransition.getExecution();
       int conflictChoice = reachableTransition.getChoiceCounter();
       // Copy ReadWriteSet object
-      ReadWriteSet currRWSet = transition.getValue().getReadWriteSet();
+      ReadWriteSet currRWSet = summaryNode.getReadWriteSet();
       currRWSet = currRWSet.getCopy();
       // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
       HashSet<TransitionEvent> visited = new HashSet<>();