Fixing a few bugs, e.g., missing rwSet.copy(), misplaced check for empty rwSet, etc.

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
index 2f84c9588b51612820b86053b110afb0f9f15249..39616d97fef3025d072ae95a3c0b339e5b32b5fc 100755 (executable)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
@@ -240,7 +240,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
         // Explore the next backtrack point:
         // 1) if we have seen this state or this state contains cycles that involve all events, and
         // 2) after the current CG is advanced at least once
         // Explore the next backtrack point:
         // 1) if we have seen this state or this state contains cycles that involve all events, and
         // 2) after the current CG is advanced at least once

-        if (terminateCurrentExecution() && choiceCounter > 0) {
+        if (choiceCounter > 0 && terminateCurrentExecution()) {

           exploreNextBacktrackPoints(vm, icsCG);
         } else {
           numOfTransitions++;
           exploreNextBacktrackPoints(vm, icsCG);
         } else {
           numOfTransitions++;


@@ -678,17 +678,19 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       // If the state Id has existed, find the event choice:
       // 1) If the event choice has not existed, insert the ReadWriteSet object
       // 2) If the event choice has existed, perform union between the two ReadWriteSet objects
       // If the state Id has existed, find the event choice:
       // 1) If the event choice has not existed, insert the ReadWriteSet object
       // 2) If the event choice has existed, perform union between the two ReadWriteSet objects

-      HashMap<Integer, ReadWriteSet> stateSummary;
-      if (!mainSummary.containsKey(stateId)) {
-        stateSummary = new HashMap<>();
-        stateSummary.put(eventChoice, rwSet.getCopy());
-        mainSummary.put(stateId, stateSummary);
-      } else {
-        stateSummary = mainSummary.get(stateId);
-        if (!stateSummary.containsKey(eventChoice)) {
+      if (!rwSet.isEmpty()) {
+        HashMap<Integer, ReadWriteSet> stateSummary;
+        if (!mainSummary.containsKey(stateId)) {
+          stateSummary = new HashMap<>();

           stateSummary.put(eventChoice, rwSet.getCopy());
           stateSummary.put(eventChoice, rwSet.getCopy());

+          mainSummary.put(stateId, stateSummary);

         } else {
         } else {

-          rwSet = performUnion(stateSummary.get(eventChoice), rwSet);
+          stateSummary = mainSummary.get(stateId);
+          if (!stateSummary.containsKey(eventChoice)) {
+            stateSummary.put(eventChoice, rwSet.getCopy());
+          } else {
+            rwSet = performUnion(stateSummary.get(eventChoice), rwSet);
+          }

         }
       }
       return rwSet;
         }
       }
       return rwSet;


@@ -1214,10 +1216,6 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
 
   private void updateBacktrackSetDFS(Execution execution, int currentChoice, int conflictEventChoice,
                                      ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
 
   private void updateBacktrackSetDFS(Execution execution, int currentChoice, int conflictEventChoice,
                                      ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {

-    // Halt when we have found the first read/write conflicts for all memory locations
-    if (currRWSet.isEmpty()) {
-      return;
-    }

     TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
     // Record this transition into the state summary of main summary
     currRWSet = mainSummary.updateStateSummary(currTrans.getStateId(), conflictEventChoice, currRWSet);
     TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
     // Record this transition into the state summary of main summary
     currRWSet = mainSummary.updateStateSummary(currTrans.getStateId(), conflictEventChoice, currRWSet);


@@ -1226,6 +1224,10 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       return;
     }
     visited.add(currTrans);
       return;
     }
     visited.add(currTrans);

+    // Halt if the set is empty
+    if (currRWSet.isEmpty()) {
+      return;
+    }

     // Explore all predecessors
     for (Predecessor predecessor : currTrans.getPredecessors()) {
       // Get the predecessor (previous conflict choice)
     // Explore all predecessors
     for (Predecessor predecessor : currTrans.getPredecessors()) {
       // Get the predecessor (previous conflict choice)


@@ -1274,7 +1276,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
       HashSet<TransitionEvent> visited = new HashSet<>();
       // Update the backtrack sets recursively
       // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
       HashSet<TransitionEvent> visited = new HashSet<>();
       // Update the backtrack sets recursively

-      updateBacktrackSetDFS(currExecution, currChoice, eventChoice, rwSet, visited);
+      updateBacktrackSetDFS(currExecution, currChoice, eventChoice, rwSet.getCopy(), visited);

     }
   }
 }
     }
   }
 }