From 8a8c10ed55dfd4dcd299af66c2f418bbd41241c5 Mon Sep 17 00:00:00 2001
From: rtrimana <rtrimana@uci.edu>
Date: Tue, 22 Sep 2020 11:17:59 -0700
Subject: [PATCH] Fixing bug: 1) pushed transition should have been the
 predecessor transition after a conflict is found, 2) execution should return
 immediately upon revisiting a transition during backtrack recursion.

---
 .../nasa/jpf/listener/DPORStateReducer.java   |  4 ++--
 .../listener/DPORStateReducerEfficient.java   | 22 +++++++++++++------
 2 files changed, 17 insertions(+), 9 deletions(-)

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 70d8935..5b0359e 100644
--- 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 cdfdcdd..c31b912 100644
--- 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,
-- 
2.34.1