@Override
public void searchFinished(Search search) {
if (verboseMode) {
+ int summaryOfUniqueTransitions = summarizeUniqueTransitions();
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: Number of unique transitions (DPOR) : " + summarizeUniqueStateIds());
+ out.println("\n==> DEBUG: Number of unique transitions (DPOR) : " + summaryOfUniqueTransitions);
out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
- fileWriter.println("==> DEBUG: State reduction mode : " + stateReductionMode);
- fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions);
- fileWriter.println("==> DEBUG: Number of unique transitions : " + summarizeUniqueStateIds());
+ fileWriter.println("==> DEBUG: State reduction mode : " + stateReductionMode);
+ fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions);
+ fileWriter.println("==> DEBUG: Number of unique transitions (DPOR) : " + summaryOfUniqueTransitions);
fileWriter.println();
fileWriter.close();
}
if (choiceCounter > 0 && terminateCurrentExecution()) {
exploreNextBacktrackPoints(vm, icsCG);
} else {
+ // We only count IntChoiceFromSet CGs
numOfTransitions++;
countUniqueStateId(vm.getStateId(), icsCG.getNextChoice());
}
choiceCounter++;
}
} else {
- numOfTransitions++;
- }
- }
-
- // Count unique state IDs
- private void countUniqueStateId(int stateId, int nextChoiceValue) {
- HashSet<Integer> events;
- // Get the set of events
- if (!stateToUniqueEventMap.containsKey(stateId)) {
- events = new HashSet<>();
- stateToUniqueEventMap.put(stateId, events);
- } else {
- events = stateToUniqueEventMap.get(stateId);
- }
- // Insert the event
- if (!events.contains(nextChoiceValue)) {
- events.add(nextChoiceValue);
- }
- }
-
- // Summarize unique state IDs
- private int summarizeUniqueStateIds() {
- // Just count the set size of each of entry map and sum them up
- int numOfUniqueTransitions = 0;
- for (Map.Entry<Integer,HashSet<Integer>> entry : stateToUniqueEventMap.entrySet()) {
- numOfUniqueTransitions = numOfUniqueTransitions + entry.getValue().size();
- }
- // We also need to count root and boolean CG if this is in state reduction mode (DPOR)
- if (stateReductionMode) {
- numOfUniqueTransitions = numOfUniqueTransitions + 3;
+ // We only count IntChoiceFromSet CGs
+ if (currentCG instanceof IntChoiceFromSet) {
+ numOfTransitions++;
+ }
}
-
- return numOfUniqueTransitions;
}
@Override
return transition;
}
+ // --- Functions related to statistics counting
+ // Count unique state IDs
+ private void countUniqueStateId(int stateId, int nextChoiceValue) {
+ HashSet<Integer> events;
+ // Get the set of events
+ if (!stateToUniqueEventMap.containsKey(stateId)) {
+ events = new HashSet<>();
+ stateToUniqueEventMap.put(stateId, events);
+ } else {
+ events = stateToUniqueEventMap.get(stateId);
+ }
+ // Insert the event
+ if (!events.contains(nextChoiceValue)) {
+ events.add(nextChoiceValue);
+ }
+ }
+
+ // Summarize unique state IDs
+ private int summarizeUniqueTransitions() {
+ // Just count the set size of each of entry map and sum them up
+ int numOfUniqueTransitions = 0;
+ for (Map.Entry<Integer,HashSet<Integer>> entry : stateToUniqueEventMap.entrySet()) {
+ numOfUniqueTransitions = numOfUniqueTransitions + entry.getValue().size();
+ }
+
+ return numOfUniqueTransitions;
+ }
+
// --- Functions related to cycle detection and reachability graph
// Detect cycles in the current execution/trace