X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducer.java;fp=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducer.java;h=11d44ab8e0c8643bbd5726ac42470eaf03d653a9;hb=d7f927a163c3cf8f1ca1e136433ac3d52f6c0f54;hp=82f3db8bd94a50b0aa290d00f1a50458cf15fd36;hpb=adca12bcd2d11a210d05ad71d0d03b2ec62f97db;p=jpf-core.git

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 82f3db8..11d44ab 100755
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -681,6 +681,13 @@ public class DPORStateReducer extends ListenerAdapter {
       transition = new TransitionEvent();
       currentExecution.addTransition(transition);
       transition.recordPredecessor(currentExecution, choiceCounter - 1);
+      // We have to check if there is a transition whose source state ID is the same
+      // If such exists, then we need to add its predecessors to the predecessor set of the current transition
+      for (TransitionEvent trans : rGraph.getReachableTransitionsAtState(stateId)) {
+        for (Predecessor pred : trans.getPredecessors()) {
+          transition.recordPredecessor(pred.getExecution(), pred.getChoice());
+        }
+      }
     }
     transition.setExecution(currentExecution);
     transition.setTransitionCG(icsCG);
@@ -1159,14 +1166,15 @@ public class DPORStateReducer extends ListenerAdapter {
       int newConflictChoice = conflictChoice;
       Execution newConflictExecution = conflictExecution;
       // Check if a conflict is found
-      if (isConflictFound(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice, currRWSet)) {
+      ReadWriteSet newCurrRWSet = currRWSet.getCopy();
+      if (isConflictFound(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice, newCurrRWSet)) {
         createBacktrackingPoint(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice);
         newConflictChoice = predecessorChoice;
         newConflictExecution = predecessorExecution;
       }
       // Continue performing DFS if conflict is not found
       updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice,
-              currRWSet, visited);
+              newCurrRWSet, visited);
     }
   }