X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducerWithSummary.java;h=39616d97fef3025d072ae95a3c0b339e5b32b5fc;hp=2f84c9588b51612820b86053b110afb0f9f15249;hb=adca12bcd2d11a210d05ad71d0d03b2ec62f97db;hpb=f3d51ec7dc305c16edf5094886d71daf5b0a7295

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
index 2f84c95..39616d9 100755
--- 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
-        if (terminateCurrentExecution() && choiceCounter > 0) {
+        if (choiceCounter > 0 && terminateCurrentExecution()) {
           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
-      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());
+          mainSummary.put(stateId, stateSummary);
         } 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;
@@ -1214,10 +1216,6 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
 
   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);
@@ -1226,6 +1224,10 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       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)
@@ -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
-      updateBacktrackSetDFS(currExecution, currChoice, eventChoice, rwSet, visited);
+      updateBacktrackSetDFS(currExecution, currChoice, eventChoice, rwSet.getCopy(), visited);
     }
   }
 }