+ checkedStateIdAndChoice.put(stateId, choiceSet);
+ }
+ choiceSet.add(choice);
+
+ return true;
+ }
+
+ // Update the backtrack sets in a previous execution
+ private void updateBacktrackSetsInPreviousExecution(int stateId) {
+ // Don't check a past trace twice!
+ HashSet<ReachableTrace> 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<ReachableTrace> rTraces = rGraph.get(stId);
+ for (ReachableTrace rTrace : rTraces) {
+ if (!checkedTrace.contains(rTrace)) {
+ // Find the choice/event that marks the start of the subtrace from the previous execution
+ ArrayList<BacktrackPoint> pastBacktrackPointList = rTrace.getPastBacktrackPointList();
+ HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap = rTrace.getPastReadWriteFieldsMap();
+ int pastConfChoice = getPastConflictChoice(stId, pastBacktrackPointList);
+ int conflictChoice = choiceCounter;
+ // Iterate from the starting point until the end of the past execution trace
+ while (pastConfChoice < pastBacktrackPointList.size() - 1) { // BacktrackPoint list always has a surplus of 1
+ // Get the info of the event from the past execution trace
+ BacktrackPoint confBtrackPoint = pastBacktrackPointList.get(pastConfChoice);
+ if (isNotChecked(checkedStateIdAndChoice, confBtrackPoint)) {
+ ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice);
+ // Append this event to the current list and map
+ backtrackPointList.add(confBtrackPoint);
+ readWriteFieldsMap.put(choiceCounter, rwSet);
+ for (int eventCounter = conflictChoice - 1; eventCounter >= 0; eventCounter--) {
+ if (isConflictFound(eventCounter, conflictChoice, true) && isNewConflict(conflictChoice, eventCounter)) {
+ createBacktrackingPoint(conflictChoice, eventCounter, true);
+ }
+ }
+ // Remove this event to replace it with a new one
+ backtrackPointList.remove(backtrackPointList.size() - 1);
+ readWriteFieldsMap.remove(choiceCounter);
+ }
+ pastConfChoice++;
+ }
+ checkedTrace.add(rTrace);
+ }
+ }