- // 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;