- // TODO: OPTIMIZATION!
- // Check and make sure that state ID and choice haven't been explored for this trace
- private boolean isNotChecked(HashMap<Integer, HashSet<Integer>> checkedStateIdAndChoice,
- BacktrackPoint backtrackPoint) {
- int stateId = backtrackPoint.getStateId();
- int choice = backtrackPoint.getChoice();
- HashSet<Integer> choiceSet;
- if (checkedStateIdAndChoice.containsKey(stateId)) {
- choiceSet = checkedStateIdAndChoice.get(stateId);
- if (choiceSet.contains(choice)) {
- // State ID and choice found. It has been checked!
- return false;
+ 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 (!alreadyChecked(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);
+ }
+ }
+ // Remove this event to replace it with a new one
+ currentTrace.remove(currentTrace.size() - 1);
+ currRWFieldsMap.remove(choiceCounter);