Printing out the number of transitions.

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

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index f034f0998da06b9cfb9bd4d34583f9d9874cafa9..a35286454e3025d6311d0b50c72cb7ab0f538082 100644 (file)
--- 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;
 
   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);
   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;
       out = null;
     }
     isBooleanCGFlipped = false;

+               numOfTransitions = 0;

     restorableStateMap = new HashMap<>();
     initializeStatesVariables();
   }
     restorableStateMap = new HashMap<>();
     initializeStatesVariables();
   }


@@ -162,6 +166,9 @@ public class DPORStateReducer extends ListenerAdapter {
   @Override
   public void searchFinished(Search search) {
     if (verboseMode) {
   @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");
     }
   }
       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());
         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);
           exploreNextBacktrackPoints(vm, icsCG);

+        } else {
+          numOfTransitions++;

         }
         justVisitedStates.clear();
         choiceCounter++;
       }
         }
         justVisitedStates.clear();
         choiceCounter++;
       }

+    } else {
+      numOfTransitions++;

     }
   }
 
     }
   }
 


@@ -639,35 +652,32 @@ public class DPORStateReducer extends ListenerAdapter {
 
   private void exploreNextBacktrackPoints(VM vm, IntChoiceFromSet icsCG) {
 
 
   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) {
   }
 
   private ReadWriteSet getReadWriteSet(int currentChoice) {