Set<Integer> eventChoicesAtStateId = mainSummary.getEventChoicesAtStateId(stateId);
for (Integer eventChoice : eventChoicesAtStateId) {
// Get the ReadWriteSet object for this event at state ID
- ReadWriteSet rwSet = mainSummary.getRWSetForEventChoiceAtState(eventChoice, stateId);
+ ReadWriteSet rwSet = mainSummary.getRWSetForEventChoiceAtState(eventChoice, stateId).getCopy();
+ // We have to first check for conflicts between the event and the current transition
+ // Push up one happens-before transition
+ int conflictEventChoice = eventChoice;
+ if (isConflictFound(eventChoice, currExecution, currChoice, rwSet)) {
+ createBacktrackingPoint(eventChoice, currExecution, currChoice);
+ // We need to extract the pushed happens-before event choice from the predecessor execution and choice
+ conflictEventChoice = currExecution.getExecutionTrace().get(currChoice).getChoice();
+ }
// Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
HashSet<TransitionEvent> visited = new HashSet<>();
// Update the backtrack sets recursively
- updateBacktrackSetDFS(currExecution, currChoice, eventChoice, rwSet.getCopy(), visited);
+ updateBacktrackSetDFS(currExecution, currChoice, conflictEventChoice, rwSet, visited);
}
}
}