From: rtrimana <rtrimana@uci.edu>
Date: Thu, 10 Sep 2020 19:00:40 +0000 (-0700)
Subject: Small edits in method updateBacktrackSetsFromPreviousExecution.
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=8511b128120f1f1832816f1f24cfc0b942254fc9;p=jpf-core.git

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 48297cc..7512691 100644
--- 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<>();