// Update the state variables
// Line 19 in the paper page 11 (see the heading note above)
int stateId = search.getStateId();
- currVisitedStates.add(stateId);
// Insert state ID into the map if it is new
if (!stateToEventMap.containsKey(stateId)) {
HashSet<Integer> eventSet = new HashSet<>();
stateToEventMap.put(stateId, eventSet);
}
- justVisitedStates.add(stateId);
analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
+ justVisitedStates.add(stateId);
+ currVisitedStates.add(stateId);
}
// --- Functions related to Read/Write access analysis on shared fields
// 2) We need to analyze and find conflicts for the reachable choices/events in the cycle
// 3) Then we create a new backtrack point for every new conflict
private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {
- // Perform this analysis only when there is a state match and state > 0 (state 0 is for boolean CG)
- if (!vm.isNewState() && (stateId > 0)) {
+ // Perform this analysis only when:
+ // 1) there is a state match,
+ // 2) this is not during a switch to a new execution,
+ // 3) at least 2 choices/events have been explored (choiceCounter > 1),
+ // 4) the matched state has been encountered in the current execution, and
+ // 5) state > 0 (state 0 is for boolean CG)
+ if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 &&
+ currVisitedStates.contains(stateId) && (stateId > 0)) {
// Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
int conflictChoice = stateToChoiceCounterMap.get(stateId);
int currentChoice = choiceCounter - 1;