private boolean isEndOfExecution;
// Statistics
- private int numOfTransitions;
+ private int numOfConflicts;
+ private int numOfTransitions;
public DPORStateReducer(Config config, JPF jpf) {
verboseMode = config.getBoolean("printout_state_transition", false);
out = null;
}
isBooleanCGFlipped = false;
+ numOfConflicts = 0;
numOfTransitions = 0;
restorableStateMap = new HashMap<>();
initializeStatesVariables();
@Override
public void searchFinished(Search search) {
+ if (stateReductionMode) {
+ // Number of conflicts = first trace + subsequent backtrack points
+ numOfConflicts += 1 + doneBacktrackSet.size();
+ }
if (verboseMode) {
out.println("\n==> DEBUG: ----------------------------------- search finished");
out.println("\n==> DEBUG: State reduction mode : " + stateReductionMode);
+ out.println("\n==> DEBUG: Number of conflicts : " + numOfConflicts);
out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions);
out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
}
if (!isBooleanCGFlipped) {
isBooleanCGFlipped = true;
} else {
+ // Number of conflicts = first trace + subsequent backtrack points
+ numOfConflicts = 1 + doneBacktrackSet.size();
// Allocate new objects for data structure when the boolean is flipped from "false" to "true"
initializeStatesVariables();
}