private PriorityQueue<Integer> backtrackStateQ; // Heap that returns the latest state
private ArrayList<BacktrackPoint> backtrackPointList; // Record backtrack points (CG, state Id, and choice)
private HashMap<Integer, HashSet<Integer>> conflictPairMap; // Record conflicting events
- private HashSet<String> doneBacktrackSet; // Record state ID and trace that are done
+ private HashSet<String> doneBacktrackSet; // Record state ID and trace already constructed
private HashMap<Integer, ReadWriteSet> readWriteFieldsMap; // Record fields that are accessed
private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
// Get the backtrack CG for this backtrack point
int stateId = backtrackPointList.get(confEvtNum).getStateId();
// Check if this trace has been done starting from this state
- if (isTraceConstructed(newChoiceList, stateId)) {
+ if (isTraceAlreadyConstructed(newChoiceList, stateId)) {
return;
}
//BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList);
return true;
}
- private boolean isTraceConstructed(Integer[] choiceList, int stateId) {
- // Concatenate state ID and trace in a string, e.g., "1:10234"
+ private boolean isTraceAlreadyConstructed(Integer[] choiceList, int stateId) {
+ // Concatenate state ID and only the first event in the string, e.g., "1:1 for the trace 10234 at state 1"
+ // TODO: THIS IS AN OPTIMIZATION!
+ // This is the optimized version because after we execute, e.g., the trace 1:10234, we don't need to try
+ // another trace that starts with event 1 at state 1, e.g., the trace 1:13024
+ // The second time this event 1 is explored, it will generate the same state as the first one
StringBuilder sb = new StringBuilder();
sb.append(stateId);
sb.append(':');
- for(Integer choice : choiceList) {
- sb.append(choice);
- }
+ sb.append(choiceList[0]);
// Check if the trace has been constructed as a backtrack point for this state
if (doneBacktrackSet.contains(sb.toString())) {
return true;