- // Update the backtrack sets in a previous execution
- updateBacktrackSetsInPreviousExecutions(stateId);
- }
- }
- }
-
- // Get the start event for the past execution trace when there is a state matched from a past execution
- private int getPastConflictChoice(int stateId, ArrayList<BacktrackPoint> pastBacktrackPointList) {
- // Iterate and find the first occurrence of the state ID
- // It is guaranteed that a choice should be found because the state ID is in the list
- int pastConfChoice = 0;
- for(int i = 0; i<pastBacktrackPointList.size(); i++) {
- BacktrackPoint backtrackPoint = pastBacktrackPointList.get(i);
- int stId = backtrackPoint.getStateId();
- if (stId == stateId) {
- pastConfChoice = i;
- break;
- }
- }
- return pastConfChoice;
- }
-
- // Get a sorted list of reachable state IDs starting from the input stateId
- private ArrayList<Integer> getReachableStateIds(Set<Integer> stateIds, int stateId) {
- // Only include state IDs equal or greater than the input stateId: these are reachable states
- ArrayList<Integer> sortedStateIds = new ArrayList<>();
- for(Integer stId : stateIds) {
- if (stId >= stateId) {
- sortedStateIds.add(stId);
- }
- }
- Collections.sort(sortedStateIds);
- return sortedStateIds;
- }
-
- // Update the backtrack sets in the cycle
- private void updateBacktrackSetsInCycle(int stateId) {
- // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
- int reachableChoice = stateToChoiceCounterMap.get(stateId);
- int cycleEndChoice = choiceCounter - 1;
- // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward)
- while (reachableChoice < cycleEndChoice) {
- for (int conflictChoice = reachableChoice + 1; conflictChoice <= cycleEndChoice; conflictChoice++) {
- if (isConflictFound(reachableChoice, conflictChoice, currentExecution)) {
- createBacktrackingPoint(reachableChoice, conflictChoice, currentExecution);
- }
- }
- reachableChoice++;
- }
- }
-
- // Update the backtrack sets in a previous execution
- private void updateBacktrackSetsInPreviousExecution(Execution rExecution, int stateId,
- HashSet<String> checkedStateIdAndChoice) {
- // 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(stateId, pastExecutionTrace);
- int reachableChoice = 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 (!isAlreadyChecked(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 conflictChoice = reachableChoice - 1; conflictChoice >= 0; conflictChoice--) {
- if (isConflictFound(reachableChoice, conflictChoice, currentExecution)) {
- createBacktrackingPoint(reachableChoice, conflictChoice, currentExecution);
- }