Printing out the number of transitions.
authorrtrimana <rtrimana@uci.edu>
Sat, 11 Apr 2020 21:26:46 +0000 (14:26 -0700)
committerrtrimana <rtrimana@uci.edu>
Sat, 11 Apr 2020 21:26:46 +0000 (14:26 -0700)
main.jpf
src/main/gov/nasa/jpf/listener/DPORStateReducer.java

index d6a241e..281c0e3 100644 (file)
--- a/main.jpf
+++ b/main.jpf
@@ -9,8 +9,8 @@ target = main
 ##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.StateReducer
 ##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.DPORStateReducer
 ##listener=gov.nasa.jpf.listener.ConflictTrackerOld
-#listener=gov.nasa.jpf.listener.DPORStateReducer
-listener=gov.nasa.jpf.listener.DPORStateReducer,gov.nasa.jpf.listener.ConflictTrackerOld
+listener=gov.nasa.jpf.listener.DPORStateReducer
+#listener=gov.nasa.jpf.listener.DPORStateReducer,gov.nasa.jpf.listener.ConflictTrackerOld
 
 # Potentially conflicting variables
 # Alarms
@@ -47,11 +47,11 @@ apps=App1,App2
 debug_mode=true
 
 # Debug mode for StateReducer
-#printout_state_transition=true
-#activate_state_reduction=true
+printout_state_transition=true
+#activate_state_reduction=false
 
 # Timeout in minutes (default is 0 which means no timeout)
-timeout=30
+#timeout=30
 
 #search.class = gov.nasa.jpf.search.heuristic.RandomHeuristic
 #search.heuristic.beam_search=true
index f034f09..a352864 100644 (file)
@@ -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) {