Fixing a bug: should use equals() to compare the values of Integer objects.

[jpf-core.git] / src / main / gov / nasa / jpf / listener / DPORStateReducerEfficient.java

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
index cdfdcdd0a7fdf48c0d7002eb282d35a7fc49a236..c0a7db5958c1fc016570b2f51af8efc192bee68b 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);
+      }
     }
   }
 
@@ -694,7 +702,7 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
         String writeField = entry.getKey();
         // Remove the entry from rwSet if both field and object ID are the same
         if (writeMap.containsKey(writeField) &&
-                (writeMap.get(writeField) == recordedWriteMap.get(writeField))) {
+                (writeMap.get(writeField).equals(recordedWriteMap.get(writeField)))) {
           writeMap.remove(writeField);
         }
       }
@@ -707,7 +715,7 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
         String readField = entry.getKey();
         // Remove the entry from rwSet if both field and object ID are the same
         if (readMap.containsKey(readField) &&
-                (readMap.get(readField) == recordedReadMap.get(readField))) {
+                (readMap.get(readField).equals(recordedReadMap.get(readField)))) {
           readMap.remove(readField);
         }
       }
@@ -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,