Fixing bugs: the main one is to create a local copy of the set that contains accesses...

[jpf-core.git] / src / main / gov / nasa / jpf / listener / DPORStateReducer.java

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 82f3db8bd94a50b0aa290d00f1a50458cf15fd36..11d44ab8e0c8643bbd5726ac42470eaf03d653a9 100755 (executable)
--- 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);
     }
   }