resetStatesForNewExecution(icsCG, vm);
// If we don't see a fair scheduling of events/choices then we have to enforce it
fairSchedulingAndBacktrackPoint(icsCG, vm);
- // Map state to event
- mapStateToEvent(icsCG.getNextChoice());
// 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
} else {
numOfTransitions++;
}
+ // Map state to event
+ mapStateToEvent(icsCG.getNextChoice());
justVisitedStates.clear();
choiceCounter++;
}
// Store restorable state object for this state (always store the latest)
RestorableVMState restorableState = vm.getRestorableState();
restorableStateMap.put(stateId, restorableState);
- // Map multiple state IDs to a choice counter
- for (Integer stId : justVisitedStates) {
- stateToChoiceCounterMap.put(stId, choiceCounter);
- }
}
private Integer[] copyChoices(Integer[] choicesToCopy) {
HashSet<Integer> eventSet = new HashSet<>();
stateToEventMap.put(stateId, eventSet);
}
+ stateToChoiceCounterMap.put(stateId, choiceCounter);
analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
justVisitedStates.add(stateId);
currVisitedStates.add(stateId);
if (currentCG instanceof IntIntervalGenerator) {
// This is the interval CG used in device handlers
ChoiceGenerator<?> parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator();
+ // Iterate until we find the IntChoiceFromSet CG
+ while (!(parentCG instanceof IntChoiceFromSet)) {
+ parentCG = ((IntIntervalGenerator) parentCG).getPreviousChoiceGenerator();
+ }
int actualEvtNum = ((IntChoiceFromSet) parentCG).getNextChoice();
// Find the index of the event/choice in refChoices
for (int i = 0; i<refChoices.length; i++) {