Adding another version of DPOR implementation that considers only the end states...

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

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
index 2026793494c74c2871a31a99a15856049326c2c5..bdf17a78848ed8a70dff3bf0a57b92d43e6d653b 100755 (executable)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java
@@ -101,10 +101,10 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     }
     isBooleanCGFlipped = false;
     mainSummary = new MainSummary();
-               numOfTransitions = 0;
-               nonRelevantClasses = new HashSet<>();
-               nonRelevantFields = new HashSet<>();
-               relevantFields = new HashSet<>();
+    numOfTransitions = 0;
+    nonRelevantClasses = new HashSet<>();
+    nonRelevantFields = new HashSet<>();
+    relevantFields = new HashSet<>();
     restorableStateMap = new HashMap<>();
     stateToPredInfo = new HashMap<>();
     initializeStatesVariables();
@@ -1080,31 +1080,31 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
   }
 
   private void exploreNextBacktrackPoints(VM vm, IntChoiceFromSet icsCG) {
-               // Check if we are reaching the end of our execution: no more backtracking points to explore
-               // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough)
-               if (!backtrackStateQ.isEmpty()) {
-                       // Set done all the other backtrack points
-                       for (TransitionEvent backtrackTransition : currentExecution.getExecutionTrace()) {
+    // Check if we are reaching the end of our execution: no more backtracking points to explore
+    // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough)
+    if (!backtrackStateQ.isEmpty()) {
+      // Set done all the other backtrack points
+      for (TransitionEvent backtrackTransition : currentExecution.getExecutionTrace()) {
         backtrackTransition.getTransitionCG().setDone();
-                       }
-                       // Reset the next backtrack point with the latest state
-                       int hiStateId = backtrackStateQ.peek();
-                       // Restore the state first if necessary
-                       if (vm.getStateId() != hiStateId) {
-                               RestorableVMState restorableState = restorableStateMap.get(hiStateId);
-                               vm.restoreState(restorableState);
-                       }
-                       // Set the backtrack CG
-                       IntChoiceFromSet backtrackCG = (IntChoiceFromSet) vm.getChoiceGenerator();
-                       setBacktrackCG(hiStateId, backtrackCG);
-               } else {
-                       // Set done this last CG (we save a few rounds)
-                       icsCG.setDone();
-               }
-               // Save all the visited states when starting a new execution of trace
-               prevVisitedStates.addAll(currVisitedStates.keySet());
-               // This marks a transitional period to the new CG
-               isEndOfExecution = true;
+      }
+      // Reset the next backtrack point with the latest state
+      int hiStateId = backtrackStateQ.peek();
+      // Restore the state first if necessary
+      if (vm.getStateId() != hiStateId) {
+        RestorableVMState restorableState = restorableStateMap.get(hiStateId);
+        vm.restoreState(restorableState);
+      }
+      // Set the backtrack CG
+      IntChoiceFromSet backtrackCG = (IntChoiceFromSet) vm.getChoiceGenerator();
+      setBacktrackCG(hiStateId, backtrackCG);
+    } else {
+      // Set done this last CG (we save a few rounds)
+      icsCG.setDone();
+    }
+    // Save all the visited states when starting a new execution of trace
+    prevVisitedStates.addAll(currVisitedStates.keySet());
+    // This marks a transitional period to the new CG
+    isEndOfExecution = true;
   }
 
   private boolean isConflictFound(int eventChoice, Execution conflictExecution, int conflictChoice,