icsCG.advance(choices[choiceIndex]);
unusedCG.add(icsCG);
}
+ //choiceCounter = choiceCounter < choiceUpperBound ? choiceCounter + 1 : 0;
choiceCounter++;
} else {
// Set new CGs to done so that the search algorithm explores the existing CGs
cg.setDone();
}
unusedCG.clear();
+ saveVisitedStates();
}
// Detect cycles in the current execution/trace
// (2) the state has one or more cycles that involve all the events
private boolean containsCyclesWithAllEvents(int stId) {
+ HashSet<ConflictTracker.Node> visitingStates = new HashSet<>();
HashSet<Integer> visitedEvents = new HashSet<>();
boolean containsCyclesWithAllEvts = false;
ConflictTracker.Node currNode = stateGraph.get(stId);
- for(ConflictTracker.Edge edge : currNode.getOutEdges()) {
- dfsFindCycles(edge.getDst(), visitedEvents, new HashSet<>());
- }
+ dfsFindCycles(currNode, visitingStates, visitedEvents, new HashSet<>());
if (checkIfAllEventsInvolved(visitedEvents)) {
containsCyclesWithAllEvts = true;
}
return containsCyclesWithAllEvts;
}
- private void dfsFindCycles(ConflictTracker.Node currNode, HashSet<Integer> visitedEvents,
- HashSet<Integer> visitingEvents) {
+ private void dfsFindCycles(ConflictTracker.Node currNode, HashSet<ConflictTracker.Node> visitingStates,
+ HashSet<Integer> visitedEvents, HashSet<Integer> visitingEvents) {
// Stop when there is a cycle and record all the events
- if (visitingEvents.contains(currNode.getId())) {
+ if (visitingStates.contains(currNode)) {
visitedEvents.addAll(visitingEvents);
} else {
+ visitingStates.add(currNode);
for(ConflictTracker.Edge edge : currNode.getOutEdges()) {
visitingEvents.add(edge.getEventNumber());
- dfsFindCycles(edge.getDst(), visitedEvents, visitingEvents);
+ dfsFindCycles(edge.getDst(), visitingStates, visitedEvents, visitingEvents);
visitingEvents.remove(edge.getEventNumber());
}
+ visitingStates.remove(currNode);
}
}
return true;
}
+ private void saveVisitedStates() {
+ // CG is being reset
+ // Save all the visited states
+ prevVisitedStates.addAll(currVisitedStates);
+ currVisitedStates.clear();
+ }
+
@Override
public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
choiceCounter = 0;
}
// Check if we have seen this state or this state contains cycles that involve all events
-// if (prevStateId != -1 && stateId != prevStateId && isVisitedMultipleTimes(stateId)) {
if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) {
// Traverse the sub-graphs
if (isResetAfterAnalysis) {
// Set done if this was the last backtrack list
icsCG.setDone();
}
+ saveVisitedStates();
}
} else {
// Update and reset the CG if needed (do this for the first time after the analysis)
resetAllCGs();
isResetAfterAnalysis = true;
}
- // Save all the visited states
- prevVisitedStates.addAll(currVisitedStates);
}
+ // Update the VOD graph always with the latest
+ updateVODGraph(icsCG.getNextChoice());
}
}
}
+ 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;
" which is " + detail + " Transition: " + transition + "\n");
}
if (stateReductionMode) {
- // Update vodGraph
- int currChoice = choiceCounter - 1;
- // Adjust currChoice with modulo
- currChoice = currChoice >= 0 ? currChoice % (choices.length -1) : currChoice;
- if (currChoice < 0 || choices[currChoice] == -1 ||
- prevChoiceValue == choices[currChoice]) {
- // When current choice is 0, previous choice could be -1
-// updateVODGraph(prevChoiceValue, choices[currChoice]);
- // Update the state ID variables
- stateId = search.getStateId();
- currVisitedStates.add(stateId);
- return;
- }
- // When current choice is 0, previous choice could be -1
- updateVODGraph(prevChoiceValue, choices[currChoice]);
- // Current choice becomes previous choice in the next iteration
- prevChoiceValue = choices[currChoice];
// Update the state ID variables
stateId = search.getStateId();
currVisitedStates.add(stateId);
// Update the state variables
// Line 19 in the paper page 11 (see the heading note above)
stateId = search.getStateId();
+ currVisitedStates.add(stateId);
out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
" and depth: " + depth + "\n");
if (currChoiceNextNodes != null) {
// Add only if there is a mapping for next nodes
for (Integer nextNode : currChoiceNextNodes) {
+ // Skip cycles
+ if (nextNode == currChoice) {
+ continue;
+ }
nodesToVisit.addLast(nextNode);
}
}