##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
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
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);
out = null;
}
isBooleanCGFlipped = false;
+ numOfTransitions = 0;
restorableStateMap = new HashMap<>();
initializeStatesVariables();
}
@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");
}
}
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++;
}
}
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) {