From: rtrimana <rtrimana@uci.edu>
Date: Sat, 11 Apr 2020 21:26:46 +0000 (-0700)
Subject: Printing out the number of transitions.
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=95356fb902e0ac7c480e4292de1c10e04fdd772d

Printing out the number of transitions.
---

diff --git a/main.jpf b/main.jpf
index d6a241e..281c0e3 100644
--- 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
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) {