Adding happens-before push back.

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index bf9ecfa7ab31bc40e3f61a77c1d9219afabd56c3..823bd525491681dca1f469204423ca44ccf92f7a 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -1072,10 +1072,42 @@ public class DPORStateReducer extends ListenerAdapter {
     // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
     HashSet<TransitionEvent> visited = new HashSet<>();
     // Update backtrack set recursively
-    updateBacktrackSetRecursive(execution, currentChoice, execution, conflictChoice, currRWSet, visited);
+//    updateBacktrackSetRecursive(execution, currentChoice, execution, conflictChoice, currRWSet, visited);
+    int hbChoice = currentChoice;
+    updateBacktrackSetRecursive(execution, currentChoice, execution, conflictChoice, execution, hbChoice, currRWSet, visited);
   }
 
-  private void updateBacktrackSetRecursive(Execution execution, int currentChoice, Execution conflictExecution, int conflictChoice,
+//  private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
+//                                           Execution conflictExecution, int conflictChoice,
+//                                           ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
+//    // Halt when we have found the first read/write conflicts for all memory locations
+//    if (currRWSet.isEmpty()) {
+//      return;
+//    }
+//    TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice);
+//    // Halt when we have visited this transition (in a cycle)
+//    if (visited.contains(confTrans)) {
+//      return;
+//    }
+//    visited.add(confTrans);
+//    // Explore all predecessors
+//    for (Predecessor predecessor : confTrans.getPredecessors()) {
+//      // Get the predecessor (previous conflict choice)
+//      conflictChoice = predecessor.getChoice();
+//      conflictExecution = predecessor.getExecution();
+//      // Check if a conflict is found
+//      if (isConflictFound(execution, currentChoice, conflictExecution, conflictChoice, currRWSet)) {
+//        createBacktrackingPoint(execution, currentChoice, conflictExecution, conflictChoice);
+//      }
+//      // Continue performing DFS if conflict is not found
+//      updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited);
+//    }
+//  }
+
+  // TODO: This is the version of the method with pushing up happens-before transitions
+  private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
+                                           Execution conflictExecution, int conflictChoice,
+                                           Execution hbExecution, int hbChoice,
                                            ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
     // Halt when we have found the first read/write conflicts for all memory locations
     if (currRWSet.isEmpty()) {
@@ -1092,12 +1124,18 @@ public class DPORStateReducer extends ListenerAdapter {
       // Get the predecessor (previous conflict choice)
       conflictChoice = predecessor.getChoice();
       conflictExecution = predecessor.getExecution();
+      // Push up one happens-before transition
+      int pushedChoice = hbChoice;
+      Execution pushedExecution = hbExecution;
       // Check if a conflict is found
       if (isConflictFound(execution, currentChoice, conflictExecution, conflictChoice, currRWSet)) {
-        createBacktrackingPoint(execution, currentChoice, conflictExecution, conflictChoice);
+        createBacktrackingPoint(pushedExecution, pushedChoice, conflictExecution, conflictChoice);
+        pushedChoice = conflictChoice;
+        pushedExecution = conflictExecution;
       }
       // Continue performing DFS if conflict is not found
-      updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited);
+      updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice,
+              pushedExecution, pushedChoice, currRWSet, visited);
     }
   }