+
+ // --- Functions related to the visible operation dependency graph implementation discussed in the SPIN paper
+
+ // This method checks whether a choice is reachable in the VOD graph from a reference choice (BFS algorithm)
+ //private boolean isReachableInVODGraph(int checkedChoice, int referenceChoice) {
+ private boolean isReachableInVODGraph(int currentChoice) {
+ // Extract previous and current events
+ int choiceIndex = currentChoice % refChoices.length;
+ int currEvent = refChoices[choiceIndex];
+ int prevEvent = refChoices[choiceIndex - 1];
+ // Record visited choices as we search in the graph
+ HashSet<Integer> visitedChoice = new HashSet<>();
+ visitedChoice.add(prevEvent);
+ LinkedList<Integer> nodesToVisit = new LinkedList<>();
+ // If the state doesn't advance as the threads/sub-programs are executed (basically there is no new state),
+ // there is a chance that the graph doesn't have new nodes---thus this check will return a null.
+ if (vodGraphMap.containsKey(prevEvent)) {
+ nodesToVisit.addAll(vodGraphMap.get(prevEvent));
+ while(!nodesToVisit.isEmpty()) {
+ int choice = nodesToVisit.getFirst();
+ if (choice == currEvent) {
+ return true;
+ }
+ if (visitedChoice.contains(choice)) { // If there is a loop then we don't find it
+ return false;
+ }
+ // Continue searching
+ visitedChoice.add(choice);
+ HashSet<Integer> choiceNextNodes = vodGraphMap.get(choice);
+ if (choiceNextNodes != null) {
+ // Add only if there is a mapping for next nodes
+ for (Integer nextNode : choiceNextNodes) {
+ // Skip cycles
+ if (nextNode == choice) {
+ continue;
+ }
+ nodesToVisit.addLast(nextNode);
+ }
+ }
+ }
+ }
+ return false;
+ }
+
+ private void updateVODGraph(int currChoiceValue) {
+ // Update the graph when we have the current choice value
+ HashSet<Integer> choiceSet;
+ if (vodGraphMap.containsKey(prevChoiceValue)) {
+ // If the key already exists, just retrieve it
+ choiceSet = vodGraphMap.get(prevChoiceValue);
+ } else {
+ // Create a new entry
+ choiceSet = new HashSet<>();
+ vodGraphMap.put(prevChoiceValue, choiceSet);
+ }
+ choiceSet.add(currChoiceValue);
+ prevChoiceValue = currChoiceValue;
+ }