X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducerWithSummary.java;h=a750c4d9763d2d9653e8c228c064767b1ff0fda3;hb=c3dddbf13bb97e250db9d092cef9787d321fe8f0;hp=2bc18a9f83a5e0210a577be66959cec9bd9294f8;hpb=65940568a7cd0c600af6e481d12b97afb3c55b19;p=jpf-core.git

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
index 2bc18a9..a750c4d 100755
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
@@ -1338,11 +1338,19 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     Set<Integer> eventChoicesAtStateId = mainSummary.getEventChoicesAtStateId(stateId);
     for (Integer eventChoice : eventChoicesAtStateId) {
       // Get the ReadWriteSet object for this event at state ID
-      ReadWriteSet rwSet = mainSummary.getRWSetForEventChoiceAtState(eventChoice, stateId);
+      ReadWriteSet rwSet = mainSummary.getRWSetForEventChoiceAtState(eventChoice, stateId).getCopy();
+      // We have to first check for conflicts between the event and the current transition
+      // Push up one happens-before transition
+      int conflictEventChoice = eventChoice;
+      if (isConflictFound(eventChoice, currExecution, currChoice, rwSet)) {
+        createBacktrackingPoint(eventChoice, currExecution, currChoice);
+        // We need to extract the pushed happens-before event choice from the predecessor execution and choice
+        conflictEventChoice = currExecution.getExecutionTrace().get(currChoice).getChoice();
+      }
       // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
       HashSet<TransitionEvent> visited = new HashSet<>();
       // Update the backtrack sets recursively
-      updateBacktrackSetDFS(currExecution, currChoice, eventChoice, rwSet.getCopy(), visited);
+      updateBacktrackSetDFS(currExecution, currChoice, conflictEventChoice, rwSet, visited);
     }
   }
 }