private HashSet<IntChoiceFromSet> unusedCG;
// Reference to the state graph in the ConflictTracker class
- private HashMap<Integer, ConflictTracker.Node> stateGraph;
+ // TODO: The following is a full-blown graph traversal that we can do if we need to in the future
+ //private HashMap<Integer, ConflictTracker.Node> stateGraph;
private HashMap<Integer, HashSet<Integer>> stateToEventMap;
// Map state to event
// Visited states in the previous and current executions/traces for terminating condition
backtrackSet = new HashSet<>();
conflictPairMap = new HashMap<>();
unusedCG = new HashSet<>();
- // TODO: We are assuming that the StateReducer is always used together with the ConflictTracker
- stateGraph = ConflictTracker.nodes;
+ // TODO: The following is a full-blown graph traversal that we can do if we need to in the future
+ //stateGraph = ConflictTracker.nodes;
stateToEventMap = new HashMap<>();
prevVisitedStates = new HashSet<>();
currVisitedStates = new HashSet<>();
isInitialized = false;
isResetAfterAnalysis = false;
cgMap.clear();
- readWriteFieldsMap.clear();
+ resetReadWriteAnalysis();
backtrackMap.clear();
backtrackSet.clear();
- conflictPairMap.clear();
}
}
}
}
+ private void resetReadWriteAnalysis() {
+ // Reset the following data structure when the choice counter reaches 0 again
+ conflictPairMap.clear();
+ readWriteFieldsMap.clear();
+ }
+
private IntChoiceFromSet setNewCG(IntChoiceFromSet icsCG) {
icsCG.setNewValues(choices);
icsCG.reset();
// Use a modulo since choiceCounter is going to keep increasing
int choiceIndex = choiceCounter % (choices.length - 1);
icsCG.advance(choices[choiceIndex]);
+ if (choiceIndex == 0) {
+ resetReadWriteAnalysis();
+ }
return icsCG;
}
IntChoiceFromSet setCG = setNewCG(icsCG);
unusedCG.add(setCG);
}
- //choiceCounter = choiceCounter < choiceUpperBound ? choiceCounter + 1 : 0;
choiceCounter++;
}
// Basically, we have to check that we have executed all events between two occurrences of such state.
private boolean containsCyclesWithAllEvents(int stId) {
- HashSet<ConflictTracker.Node> visitingStates = new HashSet<>();
HashSet<Integer> visitedEvents = stateToEventMap.get(stId);
boolean containsCyclesWithAllEvts = false;
if (checkIfAllEventsInvolved(visitedEvents)) {
currCG = icsCG;
choices = icsCG.getAllChoices();
// Reset a few things for the sub-graph
- conflictPairMap.clear();
- readWriteFieldsMap.clear();
+ resetReadWriteAnalysis();
choiceCounter = 0;
}
}
private void updateVODGraph(int currChoiceValue) {
// Update the graph when we have the current choice value
- updateVODGraph(prevChoiceValue, currChoiceValue);
- prevChoiceValue = currChoiceValue;
- }
-
- private void updateVODGraph(int prevChoice, int currChoice) {
-
HashSet<Integer> choiceSet;
- if (vodGraphMap.containsKey(prevChoice)) {
+ if (vodGraphMap.containsKey(prevChoiceValue)) {
// If the key already exists, just retrieve it
- choiceSet = vodGraphMap.get(prevChoice);
+ choiceSet = vodGraphMap.get(prevChoiceValue);
} else {
// Create a new entry
choiceSet = new HashSet<>();
- vodGraphMap.put(prevChoice, choiceSet);
+ vodGraphMap.put(prevChoiceValue, choiceSet);
}
- choiceSet.add(currChoice);
+ choiceSet.add(currChoiceValue);
+ prevChoiceValue = currChoiceValue;
}
private void mapStateToEvent(Search search) {
// If it has been serviced before, we just skip this
if (recordConflictPair(currentChoice, eventNumber)) {
// Lines 4-8 of the algorithm in the paper page 11 (see the heading note above)
- if (vm.isNewState() ||
- (!vm.isNewState() && isReachableInVODGraph(choices[currentChoice], choices[currentChoice-1]))) {
+ if (vm.isNewState() || isReachableInVODGraph(choices[currentChoice], choices[currentChoice-1])) {
createBacktrackChoiceList(currentChoice, eventNumber);
// Break if a conflict is found!
break;