X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducer.java;h=a35286454e3025d6311d0b50c72cb7ab0f538082;hp=f034f0998da06b9cfb9bd4d34583f9d9874cafa9;hb=95356fb902e0ac7c480e4292de1c10e04fdd772d;hpb=1f4068e4a688cab36250d691513cfb99dd25fdbf

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index f034f09..a352864 100644
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -87,6 +87,9 @@ public class DPORStateReducer extends ListenerAdapter {
   private boolean isBooleanCGFlipped;
   private boolean isEndOfExecution;
 
+  // Statistics
+  private int numOfTransitions;	
+	
   public DPORStateReducer(Config config, JPF jpf) {
     verboseMode = config.getBoolean("printout_state_transition", false);
     stateReductionMode = config.getBoolean("activate_state_reduction", true);
@@ -96,6 +99,7 @@ public class DPORStateReducer extends ListenerAdapter {
       out = null;
     }
     isBooleanCGFlipped = false;
+		numOfTransitions = 0;
     restorableStateMap = new HashMap<>();
     initializeStatesVariables();
   }
@@ -162,6 +166,9 @@ public class DPORStateReducer extends ListenerAdapter {
   @Override
   public void searchFinished(Search search) {
     if (verboseMode) {
+      out.println("\n==> DEBUG: ----------------------------------- search finished");
+      out.println("\n==> DEBUG: State reduction mode  : " + stateReductionMode);
+      out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions);
       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
     }
   }
@@ -218,13 +225,19 @@ public class DPORStateReducer extends ListenerAdapter {
         fairSchedulingAndBacktrackPoint(icsCG, vm);
         // Map state to event
         mapStateToEvent(icsCG.getNextChoice());
-        // Check if we have seen this state or this state contains cycles that involve all events
-        if (terminateCurrentExecution()) {
+        // 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) {
           exploreNextBacktrackPoints(vm, icsCG);
+        } else {
+          numOfTransitions++;
         }
         justVisitedStates.clear();
         choiceCounter++;
       }
+    } else {
+      numOfTransitions++;
     }
   }
 
@@ -639,35 +652,32 @@ public class DPORStateReducer extends ListenerAdapter {
 
   private void exploreNextBacktrackPoints(VM vm, IntChoiceFromSet icsCG) {
 
-    // We can start exploring the next backtrack point after the current CG is advanced at least once
-    if (choiceCounter > 0) {
-      // 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 (BacktrackPoint backtrackPoint : backtrackPointList) {
-          backtrackPoint.getBacktrackCG().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);
-      currVisitedStates.clear();
-      // This marks a transitional period to the new CG
-      isEndOfExecution = true;
-    }
+		// 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 (BacktrackPoint backtrackPoint : backtrackPointList) {
+				backtrackPoint.getBacktrackCG().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);
+		currVisitedStates.clear();
+		// This marks a transitional period to the new CG
+		isEndOfExecution = true;
   }
 
   private ReadWriteSet getReadWriteSet(int currentChoice) {