X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducer.java;h=c8c780683013dca10fc1cddfde977b9053872955;hb=ec75783ad3fb62f4bf53822da5cf2e7db0721891;hp=362da3b247b00d42aa2d43ad10f155a8103edf87;hpb=d5bff4fb65cff43b56e7a4fd7fd79b2faf7e4bdb;p=jpf-core.git diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 362da3b..c8c7806 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -39,12 +39,13 @@ import java.util.*; * This DPOR implementation is augmented by the algorithm presented in this SPIN paper: * http://spinroot.com/spin/symposia/ws08/spin2008_submission_33.pdf * - * The algorithm is presented on page 11 of the paper. Basically, we create a graph G - * (i.e., visible operation dependency graph) - * that maps inter-related threads/sub-programs that trigger state changes. - * The key to this approach is that we evaluate graph G in every iteration/recursion to - * only update the backtrack sets of the threads/sub-programs that are reachable in graph G - * from the currently running thread/sub-program. + * The algorithm is presented on page 11 of the paper. Basically, we have a graph G + * (i.e., visible operation dependency graph). + * This DPOR implementation actually fixes the algorithm in the SPIN paper that does not + * consider cases where a state could be matched early. In this new algorithm/implementation, + * each run is terminated iff: + * - we find a state that matches a state in a previous run, or + * - we have a matched state in the current run that consists of cycles that contain all choices/events. */ public class DPORStateReducer extends ListenerAdapter { @@ -60,7 +61,7 @@ public class DPORStateReducer extends ListenerAdapter { // DPOR-related fields // Basic information private Integer[] choices; - private Integer[] refChoices; + private Integer[] refChoices; // Second reference to a copy of choices (choices may be modified for fair scheduling) private int choiceCounter; private int maxEventChoice; // Data structure to track the events seen by each state to track cycles (containing all events) for termination @@ -69,23 +70,22 @@ public class DPORStateReducer extends ListenerAdapter { private HashSet prevVisitedStates; // States visited in the previous execution private HashMap> stateToEventMap; // Data structure to analyze field Read/Write accesses and conflicts - private HashMap> backtrackMap; // Track created backtracking points - private PriorityQueue backtrackStateQ; // Heap that returns the latest state - private ArrayList cgList; // Record CGs for backtracking points - private HashMap cgMap; // Maps state IDs to CGs - private HashMap> conflictPairMap; // Record conflicting events -// private HashSet activeBacktrackCGs; // Record active backtrack CGs - private HashMap readWriteFieldsMap; // Record fields that are accessed - - // Visible operation dependency graph implementation (SPIN paper) related fields - private int prevChoiceValue; - private HashMap> vodGraphMap; // Visible operation dependency graph (VOD graph) + private HashMap> backtrackMap; // Track created backtracking points + private PriorityQueue backtrackStateQ; // Heap that returns the latest state + private ArrayList backtrackPointList; // Record backtrack points (CG, state Id, and choice) + private HashMap> conflictPairMap; // Record conflicting events + private HashSet doneBacktrackSet; // Record state ID and trace already constructed + private HashMap readWriteFieldsMap; // Record fields that are accessed + private HashMap restorableStateMap; // Maps state IDs to the restorable state object // Boolean states private boolean isBooleanCGFlipped; - private boolean isFirstResetDone; private boolean isEndOfExecution; + // Statistics + private int numOfConflicts; + private int numOfTransitions; + public DPORStateReducer(Config config, JPF jpf) { verboseMode = config.getBoolean("printout_state_transition", false); stateReductionMode = config.getBoolean("activate_state_reduction", true); @@ -94,31 +94,11 @@ public class DPORStateReducer extends ListenerAdapter { } else { out = null; } - // DPOR-related - choices = null; - refChoices = null; - choiceCounter = 0; - maxEventChoice = 0; - // Cycle tracking - currVisitedStates = new HashSet<>(); - justVisitedStates = new HashSet<>(); - prevVisitedStates = new HashSet<>(); - stateToEventMap = new HashMap<>(); - // Backtracking - backtrackMap = new HashMap<>(); - backtrackStateQ = new PriorityQueue<>(); - cgList = new ArrayList<>(); - cgMap = new HashMap<>(); - conflictPairMap = new HashMap<>(); -// activeBacktrackCGs = new HashSet<>(); - readWriteFieldsMap = new HashMap<>(); - // VOD graph - prevChoiceValue = -1; - vodGraphMap = new HashMap<>(); - // Booleans isBooleanCGFlipped = false; - isEndOfExecution = false; - isFirstResetDone = false; + numOfConflicts = 0; + numOfTransitions = 0; + restorableStateMap = new HashMap<>(); + initializeStatesVariables(); } @Override @@ -182,7 +162,15 @@ public class DPORStateReducer extends ListenerAdapter { @Override public void searchFinished(Search search) { + if (stateReductionMode) { + // Number of conflicts = first trace + subsequent backtrack points + numOfConflicts += 1 + doneBacktrackSet.size(); + } if (verboseMode) { + out.println("\n==> DEBUG: ----------------------------------- search finished"); + out.println("\n==> DEBUG: State reduction mode : " + stateReductionMode); + out.println("\n==> DEBUG: Number of conflicts : " + numOfConflicts); + out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions); out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n"); } } @@ -209,8 +197,6 @@ public class DPORStateReducer extends ListenerAdapter { // Use a modulo since choiceCounter is going to keep increasing int choiceIndex = choiceCounter % choices.length; icsCG.advance(choices[choiceIndex]); - // Index the ChoiceGenerator to set backtracking points - cgList.add(icsCG); } else { // Set done all CGs while transitioning to a new execution icsCG.setDone(); @@ -224,31 +210,38 @@ public class DPORStateReducer extends ListenerAdapter { if (stateReductionMode) { // Check the boolean CG and if it is flipped, we are resetting the analysis -// if (currentCG instanceof BooleanChoiceGenerator) { -// if (!isBooleanCGFlipped) { -// isBooleanCGFlipped = true; -// } else { -// initializeStateReduction(); -// } -// } + if (currentCG instanceof BooleanChoiceGenerator) { + if (!isBooleanCGFlipped) { + isBooleanCGFlipped = true; + } else { + // Number of conflicts = first trace + subsequent backtrack points + numOfConflicts = 1 + doneBacktrackSet.size(); + // Allocate new objects for data structure when the boolean is flipped from "false" to "true" + initializeStatesVariables(); + } + } // Check every choice generated and ensure fair scheduling! if (currentCG instanceof IntChoiceFromSet) { IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG; // If this is a new CG then we need to update data structures - resetStatesForNewExecution(icsCG); + resetStatesForNewExecution(icsCG, vm); // If we don't see a fair scheduling of events/choices then we have to enforce it - checkAndEnforceFairScheduling(icsCG); + fairSchedulingAndBacktrackPoint(icsCG, vm); // Map state to event mapStateToEvent(icsCG.getNextChoice()); - // Update the VOD graph always with the latest - updateVODGraph(icsCG.getNextChoice()); - // Check if we have seen this state or this state contains cycles that involve all events - if (terminateCurrentExecution()) { - exploreNextBacktrackPoints(icsCG, vm); + // Explore the next backtrack point: + // 1) if we have seen this state or this state contains cycles that involve all events, and + // 2) after the current CG is advanced at least once + if (terminateCurrentExecution() && choiceCounter > 0) { + exploreNextBacktrackPoints(vm, icsCG); + } else { + numOfTransitions++; } justVisitedStates.clear(); choiceCounter++; } + } else { + numOfTransitions++; } } @@ -288,10 +281,7 @@ public class DPORStateReducer extends ListenerAdapter { // Check and record a backtrack set for just once! if (isConflictFound(nextInsn, eventCounter, currentChoice, fieldClass) && isNewConflict(currentChoice, eventCounter)) { - // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above) - if (vm.isNewState() || isReachableInVODGraph(currentChoice)) { - createBacktrackingPoint(currentChoice, eventCounter); - } + createBacktrackingPoint(currentChoice, eventCounter); } } } @@ -327,6 +317,14 @@ public class DPORStateReducer extends ListenerAdapter { writeSet.put(field, objectId); } + public Set getReadSet() { + return readSet.keySet(); + } + + public Set getWriteSet() { + return writeSet.keySet(); + } + public boolean readFieldExists(String field) { return readSet.containsKey(field); } @@ -344,22 +342,45 @@ public class DPORStateReducer extends ListenerAdapter { } } - // This class compactly stores backtracking points: 1) backtracking ChoiceGenerator, and 2) backtracking choices + // This class compactly stores backtrack points: 1) backtrack state ID, and 2) backtracking choices private class BacktrackPoint { - private IntChoiceFromSet backtrackCG; // CG to backtrack from - private Integer[] backtrackChoices; // Choices to set for this backtrack CG + private IntChoiceFromSet backtrackCG; // CG at this backtrack point + private int stateId; // State at this backtrack point + private int choice; // Choice chosen at this backtrack point - public BacktrackPoint(IntChoiceFromSet cg, Integer[] choices) { + public BacktrackPoint(IntChoiceFromSet cg, int stId, int cho) { backtrackCG = cg; - backtrackChoices = choices; + stateId = stId; + choice = cho; } - public IntChoiceFromSet getBacktrackCG() { - return backtrackCG; + public IntChoiceFromSet getBacktrackCG() { return backtrackCG; } + + public int getStateId() { + return stateId; } - public Integer[] getBacktrackChoices() { - return backtrackChoices; + public int getChoice() { + return choice; + } + } + + // This class compactly stores: 1) restorable VM state, and 2) global choice counter + private class RestorableState { + private RestorableVMState restorableState; + private int choiceCounter; + + public RestorableState (RestorableVMState restState, int choCtr) { + restorableState = restState; + choiceCounter = choCtr; + } + + public RestorableVMState getRestorableState() { + return restorableState; + } + + public int getChoiceCounter() { + return choiceCounter; } } @@ -384,7 +405,7 @@ public class DPORStateReducer extends ListenerAdapter { private final static String JAVA_STRING_LIB = "java.lang.String"; // -- FUNCTIONS - private void checkAndEnforceFairScheduling(IntChoiceFromSet icsCG) { + private void fairSchedulingAndBacktrackPoint(IntChoiceFromSet icsCG, VM vm) { // Check the next choice and if the value is not the same as the expected then force the expected value int choiceIndex = choiceCounter % refChoices.length; int nextChoice = icsCG.getNextChoice(); @@ -395,6 +416,12 @@ public class DPORStateReducer extends ListenerAdapter { icsCG.setChoice(currCGIndex, expectedChoice); } } + // Record state ID and choice/event as backtrack point + int stateId = vm.getStateId(); + backtrackPointList.add(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex])); + // Store restorable state object for this state (always store the latest) + RestorableVMState restorableState = vm.getRestorableState(); + restorableStateMap.put(stateId, new RestorableState(restorableState, choiceCounter)); } private Integer[] copyChoices(Integer[] choicesToCopy) { @@ -429,6 +456,28 @@ public class DPORStateReducer extends ListenerAdapter { return true; } + private void initializeStatesVariables() { + // DPOR-related + choices = null; + refChoices = null; + choiceCounter = 0; + maxEventChoice = 0; + // Cycle tracking + currVisitedStates = new HashSet<>(); + justVisitedStates = new HashSet<>(); + prevVisitedStates = new HashSet<>(); + stateToEventMap = new HashMap<>(); + // Backtracking + backtrackMap = new HashMap<>(); + backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder()); + backtrackPointList = new ArrayList<>(); + conflictPairMap = new HashMap<>(); + doneBacktrackSet = new HashSet<>(); + readWriteFieldsMap = new HashMap<>(); + // Booleans + isEndOfExecution = false; + } + private void mapStateToEvent(int nextChoiceValue) { // Update all states with this event/choice // This means that all past states now see this transition @@ -461,24 +510,21 @@ public class DPORStateReducer extends ListenerAdapter { stateToEventMap.put(stateId, eventSet); } justVisitedStates.add(stateId); + analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId); } // --- Functions related to Read/Write access analysis on shared fields - private void addNewBacktrackPoint(IntChoiceFromSet backtrackCG, Integer[] newChoiceList) { - int stateId = backtrackCG.getStateId(); + private void addNewBacktrackPoint(int stateId, Integer[] newChoiceList) { // Insert backtrack point to the right state ID LinkedList backtrackList; if (backtrackMap.containsKey(stateId)) { backtrackList = backtrackMap.get(stateId); } else { backtrackList = new LinkedList<>(); + backtrackMap.put(stateId, backtrackList); } backtrackList.addFirst(newChoiceList); - // Add CG for this state ID if there isn't one yet - if (!cgMap.containsKey(stateId)) { - cgMap.put(stateId, backtrackCG); - } // Add to priority queue if (!backtrackStateQ.contains(stateId)) { backtrackStateQ.add(stateId); @@ -549,7 +595,21 @@ public class DPORStateReducer extends ListenerAdapter { // If current choice is not the same, then this is caused by the firing of IntIntervalGenerator // for certain method calls in the infrastructure, e.g., eventSince() int currChoiceInd = currentChoice % refChoices.length; - int currChoiceFromCG = getCurrentChoice(vm); + int currChoiceFromCG = currChoiceInd; + ChoiceGenerator currentCG = vm.getChoiceGenerator(); + // This is the main event CG + if (currentCG instanceof IntIntervalGenerator) { + // This is the interval CG used in device handlers + ChoiceGenerator parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator(); + int actualEvtNum = ((IntChoiceFromSet) parentCG).getNextChoice(); + // Find the index of the event/choice in refChoices + for (int i = 0; i 0) { - if (backtrackMap.isEmpty()) { - // This means we are reaching the end of our execution: no more backtracking points to explore - return; - } - setNextBacktrackPoint(icsCG); - // Save all the visited states when starting a new execution of trace - prevVisitedStates.addAll(currVisitedStates); - currVisitedStates.clear(); - // This marks a transitional period to the new CG - isEndOfExecution = true; - } - } - - private int getCurrentChoice(VM vm) { - ChoiceGenerator currentCG = vm.getChoiceGenerator(); - // This is the main event CG - if (currentCG instanceof IntChoiceFromSet) { - return ((IntChoiceFromSet) currentCG).getNextChoiceIndex(); - } else { - // This is the interval CG used in device handlers - ChoiceGenerator parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator(); - return ((IntChoiceFromSet) parentCG).getNextChoiceIndex(); - } + private void exploreNextBacktrackPoints(VM vm, IntChoiceFromSet icsCG) { + + // Check if we are reaching the end of our execution: no more backtracking points to explore + // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough) + if (!backtrackStateQ.isEmpty()) { + // Set done all the other backtrack points + for (BacktrackPoint backtrackPoint : backtrackPointList) { + backtrackPoint.getBacktrackCG().setDone(); + } + // Reset the next backtrack point with the latest state + int hiStateId = backtrackStateQ.peek(); + // Restore the state first if necessary + if (vm.getStateId() != hiStateId) { + RestorableVMState restorableState = restorableStateMap.get(hiStateId).getRestorableState(); + vm.restoreState(restorableState); + } + // Set the backtrack CG + IntChoiceFromSet backtrackCG = (IntChoiceFromSet) vm.getChoiceGenerator(); + setBacktrackCG(hiStateId, backtrackCG); + } else { + // Set done this last CG (we save a few rounds) + icsCG.setDone(); + } + // Save all the visited states when starting a new execution of trace + prevVisitedStates.addAll(currVisitedStates); + currVisitedStates.clear(); + // This marks a transitional period to the new CG + isEndOfExecution = true; } private ReadWriteSet getReadWriteSet(int currentChoice) { @@ -648,11 +713,45 @@ public class DPORStateReducer extends ListenerAdapter { return rwSet; } + private boolean isConflictFound(int eventCounter, int currentChoice) { + + int actualCurrCho = currentChoice % refChoices.length; + // Skip if this event does not have any Read/Write set or the two events are basically the same event (number) + if (!readWriteFieldsMap.containsKey(eventCounter) || + choices[actualCurrCho] == backtrackPointList.get(eventCounter).getChoice()) { + return false; + } + // Current R/W set + ReadWriteSet currRWSet = readWriteFieldsMap.get(currentChoice); + // R/W set of choice/event that may have a potential conflict + ReadWriteSet evtRWSet = readWriteFieldsMap.get(eventCounter); + // Check for conflicts with Read and Write fields for Write instructions + Set currWriteSet = currRWSet.getWriteSet(); + for(String writeField : currWriteSet) { + int currObjId = currRWSet.writeFieldObjectId(writeField); + if ((evtRWSet.readFieldExists(writeField) && evtRWSet.readFieldObjectId(writeField) == currObjId) || + (evtRWSet.writeFieldExists(writeField) && evtRWSet.writeFieldObjectId(writeField) == currObjId)) { + return true; + } + } + // Check for conflicts with Write fields for Read instructions + Set currReadSet = currRWSet.getReadSet(); + for(String readField : currReadSet) { + int currObjId = currRWSet.readFieldObjectId(readField); + if (evtRWSet.writeFieldExists(readField) && evtRWSet.writeFieldObjectId(readField) == currObjId) { + return true; + } + } + // Return false if no conflict is found + return false; + } + private boolean isConflictFound(Instruction nextInsn, int eventCounter, int currentChoice, String fieldClass) { - int actualEvtCntr = eventCounter % refChoices.length; + int actualCurrCho = currentChoice % refChoices.length; // Skip if this event does not have any Read/Write set or the two events are basically the same event (number) - if (!readWriteFieldsMap.containsKey(eventCounter) || (actualEvtCntr == actualCurrCho)) { + if (!readWriteFieldsMap.containsKey(eventCounter) || + choices[actualCurrCho] == backtrackPointList.get(eventCounter).getChoice()) { return false; } ReadWriteSet rwSet = readWriteFieldsMap.get(eventCounter); @@ -696,128 +795,75 @@ public class DPORStateReducer extends ListenerAdapter { return true; } - private void resetStatesForNewExecution(IntChoiceFromSet icsCG) { + 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(':'); + 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; + } + doneBacktrackSet.add(sb.toString()); + return false; + } + + private void resetStatesForNewExecution(IntChoiceFromSet icsCG, VM vm) { if (choices == null || choices != icsCG.getAllChoices()) { // Reset state variables - choiceCounter = 1; + choiceCounter = 0; choices = icsCG.getAllChoices(); refChoices = copyChoices(choices); // Clearing data structures - backtrackMap.clear(); conflictPairMap.clear(); readWriteFieldsMap.clear(); stateToEventMap.clear(); isEndOfExecution = false; - // Adding this CG as the first CG for this execution - cgList.add(icsCG); + backtrackPointList.clear(); } } - private IntChoiceFromSet setBacktrackCG(int stateId) { + private void setBacktrackCG(int stateId, IntChoiceFromSet backtrackCG) { // Set a backtrack CG based on a state ID - IntChoiceFromSet backtrackCG = cgMap.get(stateId); LinkedList backtrackChoices = backtrackMap.get(stateId); backtrackCG.setNewValues(backtrackChoices.removeLast()); // Get the last from the queue + backtrackCG.setStateId(stateId); backtrackCG.reset(); // Remove from the queue if we don't have more backtrack points for that state if (backtrackChoices.isEmpty()) { - cgMap.remove(stateId); backtrackMap.remove(stateId); backtrackStateQ.remove(stateId); } - return backtrackCG; } - private void setNextBacktrackPoint(IntChoiceFromSet icsCG) { - - HashSet backtrackCGs = new HashSet<>(cgMap.values()); - if (!isFirstResetDone) { - // Reset the last CG of every LinkedList in the map and set done everything else - for (Integer stateId : cgMap.keySet()) { - setBacktrackCG(stateId); - } -// activeBacktrackCGs.addAll(cgMap.values()); - isFirstResetDone = true; - } else { - // Check if we still have backtrack points for the current CG - int currStateId = icsCG.getStateId(); - if (backtrackMap.containsKey(currStateId)) { - setBacktrackCG(currStateId); - } else { -// activeBacktrackCGs.remove(icsCG); - // We try to reset new CGs (if we do have) when we are running out of active CGs - if (!backtrackStateQ.isEmpty()) { - // Reset the next CG with the latest state - int hiStateId = backtrackStateQ.peek(); - IntChoiceFromSet backtrackCG = setBacktrackCG(hiStateId); -// activeBacktrackCGs.add(backtrackCG); - } - } - } - // Clear unused CGs - for(IntChoiceFromSet cg : cgList) { - if (!backtrackCGs.contains(cg)) { - cg.setDone(); - } - } - cgList.clear(); - } - - // --- 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 visitedChoice = new HashSet<>(); - visitedChoice.add(prevEvent); - LinkedList 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 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; + // --- Functions related to the reachability analysis when there is a state match + + // We use backtrackPointsList to analyze the reachable states/events when there is a state match: + // 1) Whenever there is state match, there is a cycle of events + // 2) We need to analyze and find conflicts for the reachable choices/events in the cycle + // 3) Then we create a new backtrack point for every new conflict + private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) { + // Perform this analysis only when there is a state match + if (!vm.isNewState()) { + if (restorableStateMap.containsKey(stateId)) { + // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts + int conflictChoice = restorableStateMap.get(stateId).getChoiceCounter(); + int currentChoice = choiceCounter - 1; + // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward) + while (conflictChoice < currentChoice) { + for (int eventCounter = conflictChoice + 1; eventCounter <= currentChoice; eventCounter++) { + if (isConflictFound(eventCounter, conflictChoice) && isNewConflict(conflictChoice, eventCounter)) { + createBacktrackingPoint(conflictChoice, eventCounter); } - nodesToVisit.addLast(nextNode); } + conflictChoice++; } } } - return false; - } - - private void updateVODGraph(int currChoiceValue) { - // Update the graph when we have the current choice value - HashSet 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; } }