Refresh the cached conflict transitions when performing backward DFS due to revisitin...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
index 31b48004ea1f6a77a707f0da02f1b3e5ff07891c..4867d0bdad33ba82610b0cac32a71596528fce63 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
@@ -637,13 +637,13 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
       }
     }
 
-    public ReadWriteSet recordTransitionSummary(TransitionEvent transition, ReadWriteSet rwSet) {
+    public ReadWriteSet recordTransitionSummary(TransitionEvent transition, ReadWriteSet rwSet, boolean refresh) {
       // Record transition into reachability summary
       // TransitionMap maps event (choice) number to a R/W set
       int choice = transition.getChoice();
       SummaryNode summaryNode;
       // Insert transition into the map if we haven't had this event number recorded
-      if (!transitionSummary.containsKey(choice)) {
+      if (!transitionSummary.containsKey(choice) || refresh) {
         summaryNode = new SummaryNode(transition, rwSet.getCopy());
         transitionSummary.put(choice, summaryNode);
       } else {
@@ -1185,13 +1185,14 @@ public class DPORStateReducerEfficient 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, currentChoice, currRWSet, visited);
+    updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited, false);
   }
 
   // Recursive method to perform backward DFS to traverse the graph
   private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
                                            Execution conflictExecution, int conflictChoice,
-                                           ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
+                                           ReadWriteSet currRWSet, HashSet<TransitionEvent> visited,
+                                           boolean refresh) {
     TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
     if (visited.contains(currTrans)) {
       return;
@@ -1199,7 +1200,7 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
     visited.add(currTrans);
     TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice);
     // Record this transition into rGraph summary
-    currRWSet = currTrans.recordTransitionSummary(confTrans, currRWSet);
+    currRWSet = currTrans.recordTransitionSummary(confTrans, currRWSet, refresh);
     // Halt when we have found the first read/write conflicts for all memory locations
     if (currRWSet.isEmpty()) {
       return;
@@ -1220,15 +1221,12 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
       }
       // Continue performing DFS if conflict is not found
       updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice,
-              currRWSet, visited);
+              currRWSet, visited, refresh);
     }
-    // Remove the transition after being explored
-    // TODO: Seems to cause a lot of loops---commented out for now
-    //visited.remove(confTrans);
   }
 
   // --- Functions related to the reachability analysis when there is a state match
-  
+
   private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {
     // Perform this analysis only when:
     // 1) this is not during a switch to a new execution,
@@ -1265,7 +1263,8 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
         currRWSet = currRWSet.getCopy();
         // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
         HashSet<TransitionEvent> visited = new HashSet<>();
-        updateBacktrackSetRecursive(currentExecution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited);
+        updateBacktrackSetRecursive(currentExecution, currentChoice, conflictExecution,
+                conflictChoice, currRWSet, visited, true);
       }
     }
   }