X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducer.java;h=bf9ecfa7ab31bc40e3f61a77c1d9219afabd56c3;hb=b0ecd85513936005411770ecab045c1a127c2fc5;hp=f503dfa92f5ff9556f4b7e83b302acbf577594d7;hpb=9ec360a1ff7dab0435778fc07216add56ebb0c9e;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 f503dfa..bf9ecfa 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -69,8 +69,7 @@ public class DPORStateReducer extends ListenerAdapter { private Execution currentExecution; // Holds the information about the current execution private HashSet doneBacktrackSet; // Record state ID and trace already constructed private HashMap restorableStateMap; // Maps state IDs to the restorable state object - private HashMap stateToChoiceCounterMap; // Maps state IDs to the choice counter - private HashMap> rGraph; // Reachability graph for past executions + private ReachabilityGraph rGraph; // Reachability graph for past executions // Boolean states private boolean isBooleanCGFlipped; @@ -141,8 +140,6 @@ public class DPORStateReducer extends ListenerAdapter { " which is " + detail + " Transition: " + transition + "\n"); } if (stateReductionMode) { - // Only add a transition into R-Graph when it advances the state - addTransitionToRGRaph(); updateStateInfo(search); } } @@ -237,10 +234,10 @@ public class DPORStateReducer extends ListenerAdapter { // If this is a new CG then we need to update data structures resetStatesForNewExecution(icsCG, vm); // If we don't see a fair scheduling of events/choices then we have to enforce it - fairSchedulingAndTransition(icsCG, vm); + ensureFairSchedulingAndSetupTransition(icsCG, vm); // Update backtrack set of an executed event (transition): one transition before this one updateBacktrackSet(currentExecution, choiceCounter - 1); - // Explore the next backtrack point: + // 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) { @@ -317,16 +314,18 @@ public class DPORStateReducer extends ListenerAdapter { // TODO: We can modify this class to implement some optimization (e.g., clock-vector) // TODO: We basically need to keep track of: // TODO: (1) last read/write access to each memory location - // TODO: (2) last state with two or more incoming events (transitions) + // TODO: (2) last state with two or more incoming events/transitions private class Execution { private HashMap cgToChoiceMap; // Map between CG to choice numbers for O(1) access - private ArrayList executionTrace; // The BacktrackPoint objects of this execution + private ArrayList executionTrace; // The BacktrackPoint objects of this execution + private boolean isNew; // Track if this is the first time it is accessed private HashMap readWriteFieldsMap; // Record fields that are accessed private HashMap stateToTransitionMap; // For O(1) access to backtrack point public Execution() { cgToChoiceMap = new HashMap<>(); executionTrace = new ArrayList<>(); + isNew = true; readWriteFieldsMap = new HashMap<>(); stateToTransitionMap = new HashMap<>(); } @@ -339,13 +338,6 @@ public class DPORStateReducer extends ListenerAdapter { cgToChoiceMap = null; } - public TransitionEvent getTransitionFromState(int stateId) { - if (stateToTransitionMap.containsKey(stateId)) { - return stateToTransitionMap.get(stateId); - } - return null; - } - public int getChoiceFromCG(IntChoiceFromSet icsCG) { return cgToChoiceMap.get(icsCG); } @@ -354,20 +346,29 @@ public class DPORStateReducer extends ListenerAdapter { return executionTrace; } - public HashMap getReadWriteFieldsMap() { - return readWriteFieldsMap; - } - public TransitionEvent getFirstTransition() { return executionTrace.get(0); } - public TransitionEvent getLastTransition() { + public HashMap getReadWriteFieldsMap() { + return readWriteFieldsMap; + } + + public TransitionEvent getTransitionFromState(int stateId) { + if (stateToTransitionMap.containsKey(stateId)) { + return stateToTransitionMap.get(stateId); + } + // Return the latest transition for unseen states (that have just been encountered in this transition) return executionTrace.get(executionTrace.size() - 1); } public boolean isNew() { - return executionTrace.size() == 1; + if (isNew) { + // Right after this is accessed, it is no longer new + isNew = false; + return true; + } + return false; } public void mapCGToChoice(IntChoiceFromSet icsCG, int choice) { @@ -383,89 +384,62 @@ public class DPORStateReducer extends ListenerAdapter { // 1) a predecessor execution // 2) the predecessor choice in that predecessor execution private class Predecessor { - private int predecessorChoice; // Predecessor choice - private Execution predecessorExecution; // Predecessor execution + private int choice; // Predecessor choice + private Execution execution; // Predecessor execution public Predecessor(int predChoice, Execution predExec) { - predecessorChoice = predChoice; - predecessorExecution = predExec; - } - - public int getPredecessorChoice() { - return predecessorChoice; - } - - public Execution getPredecessorExecution() { - return predecessorExecution; - } - } - - // This class compactly stores backtrack points: - // 1) CG, - // 2) state ID, - // 3) choice, - // 4) predecessors (for backward DFS). - private class TransitionEvent { - private IntChoiceFromSet transitionCG; // CG at this transition - private int stateId; // State at this transition - private int choice; // Choice chosen at this transition - private Execution execution; // The execution where this transition belongs - private int choiceCounter; // Choice counter at this transition - private HashSet predecessors; // Maps incoming events/transitions (execution and choice) - - public TransitionEvent() { - transitionCG = null; - stateId = -1; - choice = -1; - execution = null; - choiceCounter = -1; - predecessors = new HashSet<>(); - } - - public void setTransitionCG(IntChoiceFromSet cg) { - transitionCG = cg; - } - - public void setStateId(int stId) { - stateId = stId; - } - - public void setChoice(int cho) { - choice = cho; - } - - public void setChoiceCounter(int choCounter) { - choiceCounter = choCounter; - } - - public IntChoiceFromSet getTransitionCG() { return transitionCG; } - - public int getStateId() { - return stateId; + choice = predChoice; + execution = predExec; } public int getChoice() { return choice; } - public int getChoiceCounter() { - return choiceCounter; + public Execution getExecution() { + return execution; } + } - public void setExecution(Execution exec) { - execution = exec; + // This class represents a Reachability Graph + private class ReachabilityGraph { + private int hiStateId; // Maximum state Id + private HashMap> graph; // Reachability graph for past executions + + public ReachabilityGraph() { + hiStateId = 0; + graph = new HashMap<>(); } - public Execution getExecution() { - return execution; + public void addReachableTransition(int stateId, TransitionEvent transition) { + HashSet transitionSet; + if (graph.containsKey(stateId)) { + transitionSet = graph.get(stateId); + } else { + transitionSet = new HashSet<>(); + graph.put(stateId, transitionSet); + } + // Insert into the set if it does not contain it yet + if (!transitionSet.contains(transition)) { + transitionSet.add(transition); + } + // Update highest state ID + if (hiStateId < stateId) { + hiStateId = stateId; + } } - public HashSet getPredecessors() { - return predecessors; + public HashSet getReachableTransitionsAtState(int stateId) { + return graph.get(stateId); } - public void recordPredecessor(Execution execution, int choice) { - predecessors.add(new Predecessor(choice, execution)); + public HashSet getReachableTransitions(int stateId) { + HashSet reachableTransitions = new HashSet<>(); + // All transitions from states higher than the given state ID (until the highest state ID) are reachable + for(int stId = stateId; stId <= hiStateId; stId++) { + reachableTransitions.addAll(graph.get(stId)); + } + return reachableTransitions; } } @@ -550,6 +524,79 @@ public class DPORStateReducer extends ListenerAdapter { } } + // This class compactly stores backtrack points: + // 1) CG, + // 2) state ID, + // 3) choice, + // 4) predecessors (for backward DFS). + private class TransitionEvent { + private int choice; // Choice chosen at this transition + private int choiceCounter; // Choice counter at this transition + private Execution execution; // The execution where this transition belongs + private HashSet predecessors; // Maps incoming events/transitions (execution and choice) + private int stateId; // State at this transition + private IntChoiceFromSet transitionCG; // CG at this transition + + public TransitionEvent() { + choice = 0; + choiceCounter = 0; + execution = null; + predecessors = new HashSet<>(); + stateId = 0; + transitionCG = null; + } + + public int getChoice() { + return choice; + } + + public int getChoiceCounter() { + return choiceCounter; + } + + public Execution getExecution() { + return execution; + } + + public HashSet getPredecessors() { + return predecessors; + } + + public int getStateId() { + return stateId; + } + + public IntChoiceFromSet getTransitionCG() { return transitionCG; } + + public void recordPredecessor(Execution execution, int choice) { + predecessors.add(new Predecessor(choice, execution)); + } + + public void setChoice(int cho) { + choice = cho; + } + + public void setChoiceCounter(int choCounter) { + choiceCounter = choCounter; + } + + public void setExecution(Execution exec) { + execution = exec; + } + + public void setPredecessors(HashSet preds) { + predecessors = new HashSet<>(preds); + } + + public void setStateId(int stId) { + stateId = stId; + } + + public void setTransitionCG(IntChoiceFromSet cg) { + transitionCG = cg; + } + } + // -- CONSTANTS private final static String DO_CALL_METHOD = "doCall"; // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure @@ -571,7 +618,14 @@ public class DPORStateReducer extends ListenerAdapter { private final static String JAVA_STRING_LIB = "java.lang.String"; // -- FUNCTIONS - private void fairSchedulingAndTransition(IntChoiceFromSet icsCG, VM vm) { + private Integer[] copyChoices(Integer[] choicesToCopy) { + + Integer[] copyOfChoices = new Integer[choicesToCopy.length]; + System.arraycopy(choicesToCopy, 0, copyOfChoices, 0, choicesToCopy.length); + return copyOfChoices; + } + + private void ensureFairSchedulingAndSetupTransition(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(); @@ -584,6 +638,18 @@ public class DPORStateReducer extends ListenerAdapter { } // Get state ID and associate it with this transition int stateId = vm.getStateId(); + TransitionEvent transition = setupTransition(icsCG, stateId, choiceIndex); + // Add new transition to the current execution + for (Integer stId : justVisitedStates) { // Map this transition to all the previously passed states + currentExecution.mapStateToTransition(stId, transition); + } + currentExecution.mapCGToChoice(icsCG, choiceCounter); + // Store restorable state object for this state (always store the latest) + RestorableVMState restorableState = vm.getRestorableState(); + restorableStateMap.put(stateId, restorableState); + } + + private TransitionEvent setupTransition(IntChoiceFromSet icsCG, int stateId, int choiceIndex) { // Get a new transition TransitionEvent transition; if (currentExecution.isNew()) { @@ -591,6 +657,7 @@ public class DPORStateReducer extends ListenerAdapter { transition = currentExecution.getFirstTransition(); } else { transition = new TransitionEvent(); + currentExecution.addTransition(transition); transition.recordPredecessor(currentExecution, choiceCounter - 1); } transition.setExecution(currentExecution); @@ -598,20 +665,12 @@ public class DPORStateReducer extends ListenerAdapter { transition.setStateId(stateId); transition.setChoice(refChoices[choiceIndex]); transition.setChoiceCounter(choiceCounter); - // Add new transition to the current execution - currentExecution.mapStateToTransition(stateId, transition); - currentExecution.addTransition(transition); - currentExecution.mapCGToChoice(icsCG, choiceCounter); - // Store restorable state object for this state (always store the latest) - RestorableVMState restorableState = vm.getRestorableState(); - restorableStateMap.put(stateId, restorableState); - } - - private Integer[] copyChoices(Integer[] choicesToCopy) { + // Add transition into R-Graph + for (Integer stId : justVisitedStates) { + rGraph.addReachableTransition(stId, transition); + } - Integer[] copyOfChoices = new Integer[choicesToCopy.length]; - System.arraycopy(choicesToCopy, 0, copyOfChoices, 0, choicesToCopy.length); - return copyOfChoices; + return transition; } // --- Functions related to cycle detection and reachability graph @@ -656,8 +715,7 @@ public class DPORStateReducer extends ListenerAdapter { currentExecution = new Execution(); currentExecution.addTransition(new TransitionEvent()); // Always start with 1 backtrack point doneBacktrackSet = new HashSet<>(); - stateToChoiceCounterMap = new HashMap<>(); - rGraph = new HashMap<>(); + rGraph = new ReachabilityGraph(); // Booleans isEndOfExecution = false; } @@ -672,26 +730,6 @@ public class DPORStateReducer extends ListenerAdapter { } } - // Save the current transition into R-Graph - // Basically the current transition is reachable from the final state of the previous transition in this execution - private void addTransitionToRGRaph() { - // Get the current transition - TransitionEvent currTrans = currentExecution.getLastTransition(); - // This transition is reachable from this source state when it has advanced the state - int stateId = currTrans.getStateId(); - // Add transition into R-Graph - HashSet transitionSet; - if (rGraph.containsKey(stateId)) { - transitionSet = rGraph.get(stateId); - } else { - transitionSet = new HashSet<>(); - } - // Insert into the set if it does not contain it yet - if (!transitionSet.contains(currTrans)) { - transitionSet.add(currTrans); - } - } - private boolean terminateCurrentExecution() { // We need to check all the states that have just been visited // Often a transition (choice/event) can result into forwarding/backtracking to a number of states @@ -713,14 +751,16 @@ public class DPORStateReducer extends ListenerAdapter { stateToEventMap.put(stateId, eventSet); } analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId); - stateToChoiceCounterMap.put(stateId, choiceCounter); justVisitedStates.add(stateId); - currVisitedStates.add(stateId); + if (!prevVisitedStates.contains(stateId)) { + // It is a currently visited states if the state has not been seen in previous executions + currVisitedStates.add(stateId); + } } // --- Functions related to Read/Write access analysis on shared fields - private void addNewBacktrackPoint(int stateId, Integer[] newChoiceList, Execution parentExecution, int parentChoice) { + private void addNewBacktrackPoint(int stateId, Integer[] newChoiceList, TransitionEvent conflictTransition) { // Insert backtrack point to the right state ID LinkedList backtrackExecList; if (backtrackMap.containsKey(stateId)) { @@ -731,7 +771,7 @@ public class DPORStateReducer extends ListenerAdapter { } // Add the new backtrack execution object TransitionEvent backtrackTransition = new TransitionEvent(); - backtrackTransition.recordPredecessor(parentExecution, parentChoice); + backtrackTransition.setPredecessors(conflictTransition.getPredecessors()); backtrackExecList.addFirst(new BacktrackExecution(newChoiceList, backtrackTransition)); // Add to priority queue if (!backtrackStateQ.contains(stateId)) { @@ -817,17 +857,16 @@ public class DPORStateReducer extends ListenerAdapter { return currentChoice; } - private void createBacktrackingPoint(Execution execution, int currentChoice, int conflictChoice) { - + private void createBacktrackingPoint(Execution execution, int currentChoice, + Execution conflictExecution, int conflictChoice) { // Create a new list of choices for backtrack based on the current choice and conflicting event number // E.g. if we have a conflict between 1 and 3, then we create the list {3, 1, 0, 2} // for the original set {0, 1, 2, 3} Integer[] newChoiceList = new Integer[refChoices.length]; - //int firstChoice = choices[actualChoice]; - ArrayList pastTrace = execution.getExecutionTrace(); - ArrayList currTrace = currentExecution.getExecutionTrace(); - int currChoice = currTrace.get(currentChoice).getChoice(); - int stateId = pastTrace.get(conflictChoice).getStateId(); + ArrayList currentTrace = execution.getExecutionTrace(); + ArrayList conflictTrace = conflictExecution.getExecutionTrace(); + int currChoice = currentTrace.get(currentChoice).getChoice(); + int stateId = conflictTrace.get(conflictChoice).getStateId(); // Check if this trace has been done from this state if (isTraceAlreadyConstructed(currChoice, stateId)) { return; @@ -841,8 +880,8 @@ public class DPORStateReducer extends ListenerAdapter { j++; } } - // Parent choice is conflict choice - 1 - addNewBacktrackPoint(stateId, newChoiceList, execution, conflictChoice - 1); + // Predecessor of the new backtrack point is the same as the conflict point's + addNewBacktrackPoint(stateId, newChoiceList, conflictTrace.get(conflictChoice)); } private boolean excludeThisForItContains(String[] excludedStrings, String className) { @@ -873,7 +912,6 @@ public class DPORStateReducer extends ListenerAdapter { } 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()) { @@ -901,65 +939,26 @@ public class DPORStateReducer extends ListenerAdapter { isEndOfExecution = true; } - private boolean isConflictFound(Execution execution, int reachableChoice, int conflictChoice, + private boolean isConflictFound(Execution execution, int reachableChoice, Execution conflictExecution, int conflictChoice, ReadWriteSet currRWSet) { - ArrayList executionTrace = execution.getExecutionTrace(); HashMap execRWFieldsMap = execution.getReadWriteFieldsMap(); + ArrayList conflictTrace = conflictExecution.getExecutionTrace(); // Skip if this event does not have any Read/Write set or the two events are basically the same event (number) if (!execRWFieldsMap.containsKey(conflictChoice) || - executionTrace.get(reachableChoice).getChoice() == executionTrace.get(conflictChoice).getChoice()) { + executionTrace.get(reachableChoice).getChoice() == conflictTrace.get(conflictChoice).getChoice()) { return false; } // R/W set of choice/event that may have a potential conflict ReadWriteSet evtRWSet = execRWFieldsMap.get(conflictChoice); // 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) { - // Remove this from the read set as we are tracking per memory location - evtRWSet.removeWriteField(writeField); - return true; - } else if (evtRWSet.writeFieldExists(writeField) && evtRWSet.writeFieldObjectId(writeField) == currObjId) { - // Remove this from the write set as we are tracking per memory location - evtRWSet.removeReadField(writeField); - 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) { - // Remove this from the write set as we are tracking per memory location - evtRWSet.removeWriteField(readField); - return true; - } - } - // Return false if no conflict is found - return false; - } - - private boolean isConflictFound(Execution execution, int reachableChoice, int conflictChoice) { - - ArrayList executionTrace = execution.getExecutionTrace(); - HashMap execRWFieldsMap = execution.getReadWriteFieldsMap(); - // Skip if this event does not have any Read/Write set or the two events are basically the same event (number) - if (!execRWFieldsMap.containsKey(conflictChoice) || - executionTrace.get(reachableChoice).getChoice() == executionTrace.get(conflictChoice).getChoice()) { - return false; - } - // Current R/W set - ReadWriteSet currRWSet = execRWFieldsMap.get(reachableChoice); - // R/W set of choice/event that may have a potential conflict - ReadWriteSet evtRWSet = execRWFieldsMap.get(conflictChoice); - // 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)) { + (evtRWSet.writeFieldExists(writeField) && evtRWSet.writeFieldObjectId(writeField) == currObjId)) { + // Remove this from the write set as we are tracking per memory location + currRWSet.removeWriteField(writeField); return true; } } @@ -968,6 +967,8 @@ public class DPORStateReducer extends ListenerAdapter { for(String readField : currReadSet) { int currObjId = currRWSet.readFieldObjectId(readField); if (evtRWSet.writeFieldExists(readField) && evtRWSet.writeFieldObjectId(readField) == currObjId) { + // Remove this from the read set as we are tracking per memory location + currRWSet.removeReadField(readField); return true; } } @@ -1028,7 +1029,6 @@ public class DPORStateReducer extends ListenerAdapter { refChoices = copyChoices(choices); // Clear data structures currVisitedStates = new HashSet<>(); - stateToChoiceCounterMap = new HashMap<>(); stateToEventMap = new HashMap<>(); isEndOfExecution = false; } @@ -1064,20 +1064,24 @@ public class DPORStateReducer extends ListenerAdapter { int conflictChoice = currentChoice; // Copy ReadWriteSet object HashMap currRWFieldsMap = execution.getReadWriteFieldsMap(); - ReadWriteSet currRWSet = currRWFieldsMap.get(currentChoice).getCopy(); + ReadWriteSet currRWSet = currRWFieldsMap.get(currentChoice); + if (currRWSet == null) { + return; + } + currRWSet = currRWSet.getCopy(); // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle HashSet visited = new HashSet<>(); // Update backtrack set recursively - updateBacktrackSetRecursive(execution, currentChoice, conflictChoice, currRWSet, visited); + updateBacktrackSetRecursive(execution, currentChoice, execution, conflictChoice, currRWSet, visited); } - private void updateBacktrackSetRecursive(Execution execution, int currentChoice, int conflictChoice, + private void updateBacktrackSetRecursive(Execution execution, int currentChoice, Execution conflictExecution, int conflictChoice, ReadWriteSet currRWSet, HashSet visited) { // Halt when we have found the first read/write conflicts for all memory locations if (currRWSet.isEmpty()) { return; } - TransitionEvent confTrans = execution.getExecutionTrace().get(conflictChoice); + TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice); // Halt when we have visited this transition (in a cycle) if (visited.contains(confTrans)) { return; @@ -1086,14 +1090,14 @@ public class DPORStateReducer extends ListenerAdapter { // Explore all predecessors for (Predecessor predecessor : confTrans.getPredecessors()) { // Get the predecessor (previous conflict choice) - conflictChoice = predecessor.getPredecessorChoice(); - execution = predecessor.getPredecessorExecution(); + conflictChoice = predecessor.getChoice(); + conflictExecution = predecessor.getExecution(); // Check if a conflict is found - if (isConflictFound(execution, currentChoice, conflictChoice, currRWSet)) { - createBacktrackingPoint(execution, currentChoice, conflictChoice); + if (isConflictFound(execution, currentChoice, conflictExecution, conflictChoice, currRWSet)) { + createBacktrackingPoint(execution, currentChoice, conflictExecution, conflictChoice); } // Continue performing DFS if conflict is not found - updateBacktrackSetRecursive(execution, currentChoice, conflictChoice, currRWSet, visited); + updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited); } } @@ -1101,11 +1105,10 @@ public class DPORStateReducer extends ListenerAdapter { private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) { // Perform this analysis only when: - // 1) there is a state match, - // 2) this is not during a switch to a new execution, - // 3) at least 2 choices/events have been explored (choiceCounter > 1), - // 4) state > 0 (state 0 is for boolean CG) - if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 && (stateId > 0)) { + // 1) this is not during a switch to a new execution, + // 2) at least 2 choices/events have been explored (choiceCounter > 1), + // 3) state > 0 (state 0 is for boolean CG) + if (!isEndOfExecution && choiceCounter > 1 && stateId > 0) { if (currVisitedStates.contains(stateId)) { // Get the backtrack point from the current execution TransitionEvent transition = currentExecution.getTransitionFromState(stateId); @@ -1113,10 +1116,9 @@ public class DPORStateReducer extends ListenerAdapter { updateBacktrackSetsFromPreviousExecution(stateId); } else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution // Update past executions with a predecessor - HashSet reachableTransitions = rGraph.get(stateId); + HashSet reachableTransitions = rGraph.getReachableTransitionsAtState(stateId); for(TransitionEvent transition : reachableTransitions) { - Execution execution = transition.getExecution(); - transition.recordPredecessor(execution, choiceCounter - 1); + transition.recordPredecessor(currentExecution, choiceCounter - 1); } updateBacktrackSetsFromPreviousExecution(stateId); } @@ -1126,7 +1128,7 @@ public class DPORStateReducer extends ListenerAdapter { // Update the backtrack sets from previous executions private void updateBacktrackSetsFromPreviousExecution(int stateId) { // Collect all the reachable transitions from R-Graph - HashSet reachableTransitions = rGraph.get(stateId); + HashSet reachableTransitions = rGraph.getReachableTransitions(stateId); for(TransitionEvent transition : reachableTransitions) { Execution execution = transition.getExecution(); int currentChoice = transition.getChoiceCounter();