- // Update the backtrack sets in a previous execution
- private void updateBacktrackSetsInPreviousExecution(int stateId) {
- // Don't check a past trace twice!
- HashSet<Execution> checkedTrace = new HashSet<>();
- // Don't check the same event twice for a revisited state
- HashMap<Integer, HashSet<Integer>> checkedStateIdAndChoice = new HashMap<>();
- // Get sorted reachable state IDs
- ArrayList<Integer> reachableStateIds = getReachableStateIds(rGraph.keySet(), stateId);
- // Iterate from this state ID until the biggest state ID
- for(Integer stId : reachableStateIds) {
- // Find the right reachability graph object that contains the stateId
- ArrayList<Execution> rExecutions = rGraph.get(stId);
- for (Execution rExecution : rExecutions) {
- if (!checkedTrace.contains(rExecution)) {
- // Find the choice/event that marks the start of the subtrace from the previous execution
- ArrayList<BacktrackPoint> pastExecutionTrace = rExecution.getExecutionTrace();
- HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap = rExecution.getReadWriteFieldsMap();
- int pastConfChoice = getPastConflictChoice(stId, pastExecutionTrace);
- int conflictChoice = choiceCounter;
- // Iterate from the starting point until the end of the past execution trace
- while (pastConfChoice < pastExecutionTrace.size() - 1) { // BacktrackPoint list always has a surplus of 1
- // Get the info of the event from the past execution trace
- BacktrackPoint confBtrackPoint = pastExecutionTrace.get(pastConfChoice);
- if (isNotChecked(checkedStateIdAndChoice, confBtrackPoint)) {
- ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice);
- // Append this event to the current list and map
- ArrayList<BacktrackPoint> currentTrace = currentExecution.getExecutionTrace();
- HashMap<Integer, ReadWriteSet> currRWFieldsMap = currentExecution.getReadWriteFieldsMap();
- currentTrace.add(confBtrackPoint);
- currRWFieldsMap.put(choiceCounter, rwSet);
- for (int pastChoice = conflictChoice - 1; pastChoice >= 0; pastChoice--) {
- if (isConflictFound(conflictChoice, pastChoice, rExecution)) {
- createBacktrackingPoint(conflictChoice, pastChoice, rExecution);
- }
- }
- // Remove this event to replace it with a new one
- currentTrace.remove(currentTrace.size() - 1);
- currRWFieldsMap.remove(choiceCounter);
- }
- pastConfChoice++;
- }
- checkedTrace.add(rExecution);
- }
- }
+ // Update the backtrack sets from previous executions
+ private void updateBacktrackSetsFromPreviousExecution(int stateId) {
+ // Collect all the reachable transitions from R-Graph
+ HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitions(stateId);
+ for(TransitionEvent transition : reachableTransitions) {
+ Execution execution = transition.getExecution();
+ int currentChoice = transition.getChoiceCounter();
+ updateBacktrackSet(execution, currentChoice);