Fixing bug: 1) pushed transition should have been the predecessor transition after...
authorrtrimana <rtrimana@uci.edu>
Tue, 22 Sep 2020 18:17:59 +0000 (11:17 -0700)
committerrtrimana <rtrimana@uci.edu>
Tue, 22 Sep 2020 18:17:59 +0000 (11:17 -0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java
src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java

index 70d8935..5b0359e 100644 (file)
@@ -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,
index cdfdcdd..c31b912 100644 (file)
@@ -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,