Fixing bug: 1) pushed transition should have been the predecessor transition after...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 70d89356d1bce74435dbf8d56373854da6b51b24..5b0359ed5a92198f351200cda526b7ab573b3e2e 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -1182,8 +1182,8 @@ public class DPORStateReducer extends ListenerAdapter {
       // Check if a conflict is found
       if (isConflictFound(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice, currRWSet)) {
         createBacktrackingPoint(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice);
-        newConflictChoice = conflictChoice;
-        newConflictExecution = conflictExecution;
+        newConflictChoice = predecessorChoice;
+        newConflictExecution = predecessorExecution;
       }
       // Continue performing DFS if conflict is not found
       updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice,

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
index cdfdcdd0a7fdf48c0d7002eb282d35a7fc49a236..c31b9124dfdc6f19633e4eacb88d035157981e7d 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
@@ -509,7 +509,15 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
 
     public void recordTransitionSummaryAtState(int stateId, HashMap<Integer, SummaryNode> transitionSummary) {
       // Record transition summary into graphSummary
-      graphSummary.put(stateId, transitionSummary);
+      HashMap<Integer, SummaryNode> transSummary;
+      if (!graphSummary.containsKey(stateId)) {
+        transSummary = new HashMap<>(transitionSummary);
+        graphSummary.put(stateId, transSummary);
+      } else {
+        transSummary = graphSummary.get(stateId);
+        // Merge the two transition summaries
+        transSummary.putAll(transitionSummary);
+      }
     }
   }
 
@@ -1310,6 +1318,10 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
                                            Execution conflictExecution, int conflictChoice,
                                            ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
     TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
+    if (visited.contains(currTrans)) {
+      return;
+    }
+    visited.add(currTrans);
     // TODO: THIS IS THE ACCESS SUMMARY
     TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice);
     // Record this transition into rGraph summary
@@ -1320,10 +1332,6 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
     if (currRWSet.isEmpty()) {
       return;
     }
-    if (visited.contains(currTrans)) {
-      return;
-    }
-    visited.add(currTrans);
     // Explore all predecessors
     for (Predecessor predecessor : currTrans.getPredecessors()) {
       // Get the predecessor (previous conflict choice)
@@ -1335,8 +1343,8 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
       // Check if a conflict is found
       if (isConflictFound(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice, currRWSet)) {
         createBacktrackingPoint(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice);
-        newConflictChoice = conflictChoice;
-        newConflictExecution = conflictExecution;
+        newConflictChoice = predecessorChoice;
+        newConflictExecution = predecessorExecution;
       }
       // Continue performing DFS if conflict is not found
       updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice,