X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducer.java;h=ef0994cbdeba690d46c526b1016c54a488bc09dc;hp=72fc44e6c67f8ec4a48cfa8dd141a2ab043c33c3;hb=42c68a0ac3563a679987c53ce282d6807cd3d9d6;hpb=b1c560c27cc9169acd9ad874b09df56eea7187a9 diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 72fc44e..ef0994c 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -28,23 +28,18 @@ import gov.nasa.jpf.vm.bytecode.WriteInstruction; import gov.nasa.jpf.vm.choice.IntChoiceFromSet; import gov.nasa.jpf.vm.choice.IntIntervalGenerator; +import java.io.FileWriter; import java.io.PrintWriter; +import java.lang.reflect.Field; import java.util.*; +import java.util.logging.Logger; +import java.io.IOException; -// TODO: Fix for Groovy's model-checking -// TODO: This is a setter to change the values of the ChoiceGenerator to implement POR /** - * Simple tool to log state changes. - * - * 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. + * This a DPOR implementation for event-driven applications with loops that create cycles of state matching + * In this new DPOR 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 { @@ -52,6 +47,7 @@ public class DPORStateReducer extends ListenerAdapter { private boolean verboseMode; private boolean stateReductionMode; private final PrintWriter out; + private PrintWriter fileWriter; private String detail; private int depth; private int id; @@ -60,33 +56,33 @@ 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 lastCGStateId; // Record the state of the currently active CG private int maxEventChoice; // Data structure to track the events seen by each state to track cycles (containing all events) for termination - private HashSet currVisitedStates; // States being visited in the current execution - private HashSet justVisitedStates; // States just visited in the previous choice/event - private HashSet prevVisitedStates; // States visited in the previous execution + private HashSet currVisitedStates; // States being visited in the current execution + private HashSet justVisitedStates; // States just visited in the previous choice/event + private HashSet prevVisitedStates; // States visited in the previous execution + private HashSet nonRelevantClasses;// Class info objects of non-relevant classes + private HashSet nonRelevantFields; // Field info objects of non-relevant fields + private HashSet relevantFields; // Field info objects of relevant fields 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 doneBacktrackSet; // Record state ID and trace that are done - 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 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 RGraph rGraph; // R-Graph for past executions // 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); @@ -95,7 +91,20 @@ public class DPORStateReducer extends ListenerAdapter { } else { out = null; } + String outputFile = config.getString("file_output"); + if (!outputFile.isEmpty()) { + try { + fileWriter = new PrintWriter(new FileWriter(outputFile, true), true); + } catch (IOException e) { + } + } isBooleanCGFlipped = false; + numOfConflicts = 0; + numOfTransitions = 0; + nonRelevantClasses = new HashSet<>(); + nonRelevantFields = new HashSet<>(); + relevantFields = new HashSet<>(); + restorableStateMap = new HashMap<>(); initializeStatesVariables(); } @@ -158,10 +167,26 @@ public class DPORStateReducer extends ListenerAdapter { } } + static Logger log = JPF.getLogger("report"); + @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"); + + fileWriter.println("==> DEBUG: State reduction mode : " + stateReductionMode); + fileWriter.println("==> DEBUG: Number of conflicts : " + numOfConflicts); + fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions); + fileWriter.println(); + fileWriter.close(); } } @@ -187,8 +212,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(); @@ -199,13 +222,14 @@ public class DPORStateReducer extends ListenerAdapter { @Override public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator currentCG) { - 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 { + // 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(); } @@ -214,20 +238,26 @@ public class DPORStateReducer extends ListenerAdapter { 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); + 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: + // 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++; + } // 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); - } justVisitedStates.clear(); choiceCounter++; } + } else { + numOfTransitions++; } } @@ -245,37 +275,14 @@ public class DPORStateReducer extends ListenerAdapter { currentChoice = checkAndAdjustChoice(currentChoice, vm); // Record accesses from executed instructions if (executedInsn instanceof JVMFieldInstruction) { - // Analyze only after being initialized - String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName(); // We don't care about libraries - if (!isFieldExcluded(fieldClass)) { - analyzeReadWriteAccesses(executedInsn, fieldClass, currentChoice); + if (!isFieldExcluded(executedInsn)) { + analyzeReadWriteAccesses(executedInsn, currentChoice); } } else if (executedInsn instanceof INVOKEINTERFACE) { // Handle the read/write accesses that occur through iterators analyzeReadWriteAccesses(executedInsn, ti, currentChoice); } - // Analyze conflicts from next instructions - if (nextInsn instanceof JVMFieldInstruction) { - // Skip the constructor because it is called once and does not have shared access with other objects - if (!nextInsn.getMethodInfo().getName().equals("")) { - String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName(); - if (!isFieldExcluded(fieldClass)) { - // Check for conflict (go backward from current choice and get the first conflict) - for (int eventCounter = currentChoice - 1; eventCounter >= 0; eventCounter--) { - // Check for conflicts with Write fields for both Read and Write instructions - // 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); - } - } - } - } - } - } } } } @@ -286,59 +293,298 @@ public class DPORStateReducer extends ListenerAdapter { // -- INNER CLASSES + // This class compactly stores backtrack execution: + // 1) backtrack choice list, and + // 2) first backtrack point (linking with predecessor execution) + private class BacktrackExecution { + private Integer[] choiceList; + private TransitionEvent firstTransition; + + public BacktrackExecution(Integer[] choList, TransitionEvent fTransition) { + choiceList = choList; + firstTransition = fTransition; + } + + public Integer[] getChoiceList() { + return choiceList; + } + + public TransitionEvent getFirstTransition() { + return firstTransition; + } + } + + // This class stores a representation of an execution + // 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 + 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 boolean isNew; // Track if this is the first time it is accessed + private HashMap readWriteFieldsMap; // Record fields that are accessed + + public Execution() { + cgToChoiceMap = new HashMap<>(); + executionTrace = new ArrayList<>(); + isNew = true; + readWriteFieldsMap = new HashMap<>(); + } + + public void addTransition(TransitionEvent newBacktrackPoint) { + executionTrace.add(newBacktrackPoint); + } + + public void clearCGToChoiceMap() { + cgToChoiceMap = null; + } + + public int getChoiceFromCG(IntChoiceFromSet icsCG) { + return cgToChoiceMap.get(icsCG); + } + + public ArrayList getExecutionTrace() { + return executionTrace; + } + + public TransitionEvent getFirstTransition() { + return executionTrace.get(0); + } + + public HashMap getReadWriteFieldsMap() { + return readWriteFieldsMap; + } + + public boolean isNew() { + 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) { + cgToChoiceMap.put(icsCG, choice); + } + } + + // This class compactly stores a predecessor + // 1) a predecessor execution + // 2) the predecessor choice in that predecessor execution + private class Predecessor { + private int choice; // Predecessor choice + private Execution execution; // Predecessor execution + + public Predecessor(int predChoice, Execution predExec) { + choice = predChoice; + execution = predExec; + } + + public int getChoice() { + return choice; + } + + public Execution getExecution() { + return execution; + } + } + + // This class represents a R-Graph (in the paper it is a state transition graph R) + // This implementation stores reachable transitions from and connects with past executions + private class RGraph { + private int hiStateId; // Maximum state Id + private HashMap> graph; // Reachable transitions from past executions + + public RGraph() { + hiStateId = 0; + graph = new HashMap<>(); + } + + 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 getReachableTransitionsAtState(int stateId) { + return graph.get(stateId); + } + + 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; + } + } + // This class compactly stores Read and Write field sets // We store the field name and its object ID // Sharing the same field means the same field name and object ID private class ReadWriteSet { - private HashMap readSet; - private HashMap writeSet; + private HashMap readMap; + private HashMap writeMap; public ReadWriteSet() { - readSet = new HashMap<>(); - writeSet = new HashMap<>(); + readMap = new HashMap<>(); + writeMap = new HashMap<>(); } public void addReadField(String field, int objectId) { - readSet.put(field, objectId); + readMap.put(field, objectId); } public void addWriteField(String field, int objectId) { - writeSet.put(field, objectId); + writeMap.put(field, objectId); + } + + public void removeReadField(String field) { + readMap.remove(field); + } + + public void removeWriteField(String field) { + writeMap.remove(field); + } + + public boolean isEmpty() { + return readMap.isEmpty() && writeMap.isEmpty(); + } + + public ReadWriteSet getCopy() { + ReadWriteSet copyRWSet = new ReadWriteSet(); + // Copy the maps in the set into the new object copy + copyRWSet.setReadMap(new HashMap<>(this.getReadMap())); + copyRWSet.setWriteMap(new HashMap<>(this.getWriteMap())); + return copyRWSet; + } + + public Set getReadSet() { + return readMap.keySet(); + } + + public Set getWriteSet() { + return writeMap.keySet(); } public boolean readFieldExists(String field) { - return readSet.containsKey(field); + return readMap.containsKey(field); } public boolean writeFieldExists(String field) { - return writeSet.containsKey(field); + return writeMap.containsKey(field); } public int readFieldObjectId(String field) { - return readSet.get(field); + return readMap.get(field); } public int writeFieldObjectId(String field) { - return writeSet.get(field); + return writeMap.get(field); + } + + private HashMap getReadMap() { + return readMap; + } + + private HashMap getWriteMap() { + return writeMap; + } + + private void setReadMap(HashMap rMap) { + readMap = rMap; + } + + private void setWriteMap(HashMap wMap) { + writeMap = wMap; } } - // This class compactly stores backtracking points: 1) backtracking ChoiceGenerator, and 2) backtracking choices - private class BacktrackPoint { - private IntChoiceFromSet backtrackCG; // CG to backtrack from - private Integer[] backtrackChoices; // Choices to set for this backtrack CG + // This class compactly stores transitions: + // 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 BacktrackPoint(IntChoiceFromSet cg, Integer[] choices) { - backtrackCG = cg; - backtrackChoices = choices; + public void setChoiceCounter(int choCounter) { + choiceCounter = choCounter; } - public IntChoiceFromSet getBacktrackCG() { - return backtrackCG; + public void setExecution(Execution exec) { + execution = exec; } - public Integer[] getBacktrackChoices() { - return backtrackChoices; + public void setPredecessors(HashSet preds) { + predecessors = new HashSet<>(preds); + } + + public void setStateId(int stId) { + stateId = stId; + } + + public void setTransitionCG(IntChoiceFromSet cg) { + transitionCG = cg; } } @@ -363,7 +609,14 @@ public class DPORStateReducer extends ListenerAdapter { private final static String JAVA_STRING_LIB = "java.lang.String"; // -- FUNCTIONS - private void checkAndEnforceFairScheduling(IntChoiceFromSet icsCG) { + 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(); @@ -374,16 +627,40 @@ public class DPORStateReducer extends ListenerAdapter { icsCG.setChoice(currCGIndex, expectedChoice); } } + // 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 and map it in R-Graph + for (Integer stId : justVisitedStates) { // Map this transition to all the previously passed states + rGraph.addReachableTransition(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 Integer[] copyChoices(Integer[] choicesToCopy) { + private TransitionEvent setupTransition(IntChoiceFromSet icsCG, int stateId, int choiceIndex) { + // Get a new transition + TransitionEvent transition; + if (currentExecution.isNew()) { + // We need to handle the first transition differently because this has a predecessor execution + transition = currentExecution.getFirstTransition(); + } else { + transition = new TransitionEvent(); + currentExecution.addTransition(transition); + transition.recordPredecessor(currentExecution, choiceCounter - 1); + } + transition.setExecution(currentExecution); + transition.setTransitionCG(icsCG); + transition.setStateId(stateId); + transition.setChoice(refChoices[choiceIndex]); + transition.setChoiceCounter(choiceCounter); - Integer[] copyOfChoices = new Integer[choicesToCopy.length]; - System.arraycopy(choicesToCopy, 0, copyOfChoices, 0, choicesToCopy.length); - return copyOfChoices; + return transition; } - // --- Functions related to cycle detection + // --- Functions related to cycle detection and reachability graph // Detect cycles in the current execution/trace // We terminate the execution iff: @@ -391,8 +668,7 @@ public class DPORStateReducer extends ListenerAdapter { // (2) the state has one or more cycles that involve all the events // With simple approach we only need to check for a re-visited state. // Basically, we have to check that we have executed all events between two occurrences of such state. - private boolean containsCyclesWithAllEvents(int stId) { - + private boolean completeFullCycle(int stId) { // False if the state ID hasn't been recorded if (!stateToEventMap.containsKey(stId)) { return false; @@ -413,7 +689,6 @@ public class DPORStateReducer extends ListenerAdapter { choices = null; refChoices = null; choiceCounter = 0; - lastCGStateId = 0; maxEventChoice = 0; // Cycle tracking currVisitedStates = new HashSet<>(); @@ -423,17 +698,12 @@ public class DPORStateReducer extends ListenerAdapter { // Backtracking backtrackMap = new HashMap<>(); backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder()); - cgList = new ArrayList<>(); - cgMap = new HashMap<>(); - conflictPairMap = new HashMap<>(); + currentExecution = new Execution(); + currentExecution.addTransition(new TransitionEvent()); // Always start with 1 backtrack point doneBacktrackSet = new HashSet<>(); - readWriteFieldsMap = new HashMap<>(); - // VOD graph - prevChoiceValue = -1; - vodGraphMap = new HashMap<>(); + rGraph = new RGraph(); // Booleans isEndOfExecution = false; - isFirstResetDone = false; } private void mapStateToEvent(int nextChoiceValue) { @@ -450,7 +720,7 @@ public class DPORStateReducer extends ListenerAdapter { // 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 for(Integer stateId : justVisitedStates) { - if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) { + if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) { return true; } } @@ -459,34 +729,35 @@ public class DPORStateReducer extends ListenerAdapter { private void updateStateInfo(Search search) { // Update the state variables - // Line 19 in the paper page 11 (see the heading note above) int stateId = search.getStateId(); - currVisitedStates.add(stateId); // Insert state ID into the map if it is new if (!stateToEventMap.containsKey(stateId)) { HashSet eventSet = new HashSet<>(); stateToEventMap.put(stateId, eventSet); } + analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId); justVisitedStates.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(IntChoiceFromSet backtrackCG, Integer[] newChoiceList) { - int stateId = backtrackCG.getStateId(); + private void addNewBacktrackPoint(int stateId, Integer[] newChoiceList, TransitionEvent conflictTransition) { // Insert backtrack point to the right state ID - LinkedList backtrackList; + LinkedList backtrackExecList; if (backtrackMap.containsKey(stateId)) { - backtrackList = backtrackMap.get(stateId); + backtrackExecList = 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); + backtrackExecList = new LinkedList<>(); + backtrackMap.put(stateId, backtrackExecList); } + // Add the new backtrack execution object + TransitionEvent backtrackTransition = new TransitionEvent(); + backtrackTransition.setPredecessors(conflictTransition.getPredecessors()); + backtrackExecList.addFirst(new BacktrackExecution(newChoiceList, backtrackTransition)); // Add to priority queue if (!backtrackStateQ.contains(stateId)) { backtrackStateQ.add(stateId); @@ -494,17 +765,28 @@ public class DPORStateReducer extends ListenerAdapter { } // Analyze Read/Write accesses that are directly invoked on fields - private void analyzeReadWriteAccesses(Instruction executedInsn, String fieldClass, int currentChoice) { + private void analyzeReadWriteAccesses(Instruction executedInsn, int currentChoice) { + // Get the field info + FieldInfo fieldInfo = ((JVMFieldInstruction) executedInsn).getFieldInfo(); + // Analyze only after being initialized + String fieldClass = fieldInfo.getFullName(); // Do the analysis to get Read and Write accesses to fields ReadWriteSet rwSet = getReadWriteSet(currentChoice); - int objectId = ((JVMFieldInstruction) executedInsn).getFieldInfo().getClassInfo().getClassObjectRef(); + int objectId = fieldInfo.getClassInfo().getClassObjectRef(); // Record the field in the map if (executedInsn instanceof WriteInstruction) { - // Exclude certain field writes because of infrastructure needs, e.g., Event class field writes - for (String str : EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST) { - if (fieldClass.startsWith(str)) { - return; + // We first check the non-relevant fields set + if (!nonRelevantFields.contains(fieldInfo)) { + // Exclude certain field writes because of infrastructure needs, e.g., Event class field writes + for (String str : EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST) { + if (fieldClass.startsWith(str)) { + nonRelevantFields.add(fieldInfo); + return; + } } + } else { + // If we have this field in the non-relevant fields set then we return right away + return; } rwSet.addWriteField(fieldClass, objectId); } else if (executedInsn instanceof ReadInstruction) { @@ -533,9 +815,17 @@ public class DPORStateReducer extends ListenerAdapter { return; } // We exclude library classes (they start with java, org, etc.) and some more - String objClassName = eiAccessObj.getClassInfo().getName(); - if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, objClassName) || - excludeThisForItStartsWith(EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST, objClassName)) { + ClassInfo classInfo = eiAccessObj.getClassInfo(); + String objClassName = classInfo.getName(); + // Check if this class info is part of the non-relevant classes set already + if (!nonRelevantClasses.contains(classInfo)) { + if (excludeThisForItStartsWith(EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST, objClassName) || + excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, objClassName)) { + nonRelevantClasses.add(classInfo); + return; + } + } else { + // If it is part of the non-relevant classes set then return immediately return; } // Extract fields from this object and put them into the read write @@ -556,41 +846,46 @@ public class DPORStateReducer extends ListenerAdapter { private int checkAndAdjustChoice(int currentChoice, VM vm) { // 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); - if (currChoiceInd != currChoiceFromCG) { - currentChoice = (currentChoice - currChoiceInd) + currChoiceFromCG; + 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(); + // Iterate until we find the IntChoiceFromSet CG + while (!(parentCG instanceof IntChoiceFromSet)) { + parentCG = ((IntIntervalGenerator) parentCG).getPreviousChoiceGenerator(); + } + // Find the choice related to the IntIntervalGenerator CG from the map + currentChoice = currentExecution.getChoiceFromCG((IntChoiceFromSet) parentCG); } return currentChoice; } - private void createBacktrackingPoint(int currentChoice, int confEvtNum) { - + 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]; + 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; + } // Put the conflicting event numbers first and reverse the order - int actualCurrCho = currentChoice % refChoices.length; - int actualConfEvtNum = confEvtNum % refChoices.length; - // We use the actual choices here in case they have been modified/adjusted - newChoiceList[0] = choices[actualCurrCho]; - newChoiceList[1] = choices[actualConfEvtNum]; + newChoiceList[0] = currChoice; // Put the rest of the event numbers into the array starting from the minimum to the upper bound - for (int i = 0, j = 2; i < refChoices.length; i++) { - if (refChoices[i] != newChoiceList[0] && refChoices[i] != newChoiceList[1]) { + for (int i = 0, j = 1; i < refChoices.length; i++) { + if (refChoices[i] != newChoiceList[0]) { newChoiceList[j] = refChoices[i]; j++; } } - // Record the backtracking point in the stack as well - IntChoiceFromSet backtrackCG = cgList.get(confEvtNum); - // Check if this trace has been done starting from this state - if (isTraceConstructed(newChoiceList, backtrackCG)) { - return; - } - //BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList); - addNewBacktrackPoint(backtrackCG, newChoiceList); + // 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) { @@ -620,103 +915,120 @@ public class DPORStateReducer extends ListenerAdapter { return false; } - private void exploreNextBacktrackPoints(IntChoiceFromSet icsCG, VM vm) { - // We can start exploring the next backtrack point after the current CG is advanced at least once - if (icsCG.getNextChoiceIndex() > 0) { - // Check if we are reaching the end of our execution: no more backtracking points to explore - if (!backtrackMap.isEmpty()) { - 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 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 (TransitionEvent backtrackTransition : currentExecution.getExecutionTrace()) { + backtrackTransition.getTransitionCG().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); + 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); + // 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 boolean isConflictFound(Execution execution, int reachableChoice, Execution conflictExecution, int conflictChoice, + ReadWriteSet currRWSet) { + ArrayList executionTrace = execution.getExecutionTrace(); + ArrayList conflictTrace = conflictExecution.getExecutionTrace(); + HashMap confRWFieldsMap = conflictExecution.getReadWriteFieldsMap(); + // Skip if this event does not have any Read/Write set or the two events are basically the same event (number) + if (!confRWFieldsMap.containsKey(conflictChoice) || + executionTrace.get(reachableChoice).getChoice() == conflictTrace.get(conflictChoice).getChoice()) { + return false; } + // R/W set of choice/event that may have a potential conflict + ReadWriteSet confRWSet = confRWFieldsMap.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 ((confRWSet.readFieldExists(writeField) && confRWSet.readFieldObjectId(writeField) == currObjId) || + (confRWSet.writeFieldExists(writeField) && confRWSet.writeFieldObjectId(writeField) == currObjId)) { + // Remove this from the write set as we are tracking per memory location + currRWSet.removeWriteField(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 (confRWSet.writeFieldExists(readField) && confRWSet.writeFieldObjectId(readField) == currObjId) { + // Remove this from the read set as we are tracking per memory location + currRWSet.removeReadField(readField); + return true; + } + } + // Return false if no conflict is found + return false; } private ReadWriteSet getReadWriteSet(int currentChoice) { // Do the analysis to get Read and Write accesses to fields ReadWriteSet rwSet; // We already have an entry - if (readWriteFieldsMap.containsKey(currentChoice)) { - rwSet = readWriteFieldsMap.get(currentChoice); + HashMap currReadWriteFieldsMap = currentExecution.getReadWriteFieldsMap(); + if (currReadWriteFieldsMap.containsKey(currentChoice)) { + rwSet = currReadWriteFieldsMap.get(currentChoice); } else { // We need to create a new entry rwSet = new ReadWriteSet(); - readWriteFieldsMap.put(currentChoice, rwSet); + currReadWriteFieldsMap.put(currentChoice, rwSet); } return rwSet; } - 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) || choices[actualCurrCho] == choices[actualEvtCntr]) { - return false; - } - ReadWriteSet rwSet = readWriteFieldsMap.get(eventCounter); - int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef(); - // Check for conflicts with Write fields for both Read and Write instructions - if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) && - rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) || - (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) && - rwSet.readFieldObjectId(fieldClass) == currObjId)) { + private boolean isFieldExcluded(Instruction executedInsn) { + // Get the field info + FieldInfo fieldInfo = ((JVMFieldInstruction) executedInsn).getFieldInfo(); + // Check if the non-relevant fields set already has it + if (nonRelevantFields.contains(fieldInfo)) { return true; } - return false; - } - - private boolean isFieldExcluded(String field) { + // Check if the relevant fields set already has it + if (relevantFields.contains(fieldInfo)) { + return false; + } + // Analyze only after being initialized + String field = fieldInfo.getFullName(); // Check against "starts-with", "ends-with", and "contains" list if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, field) || excludeThisForItEndsWith(EXCLUDED_FIELDS_ENDS_WITH_LIST, field) || excludeThisForItContains(EXCLUDED_FIELDS_CONTAINS_LIST, field)) { + nonRelevantFields.add(fieldInfo); return true; } - + relevantFields.add(fieldInfo); return false; } - private boolean isNewConflict(int currentEvent, int eventNumber) { - HashSet conflictSet; - if (!conflictPairMap.containsKey(currentEvent)) { - conflictSet = new HashSet<>(); - conflictPairMap.put(currentEvent, conflictSet); - } else { - conflictSet = conflictPairMap.get(currentEvent); - } - // If this conflict has been recorded before, we return false because - // we don't want to save this backtrack point twice - if (conflictSet.contains(eventNumber)) { - return false; - } - // If it hasn't been recorded, then do otherwise - conflictSet.add(eventNumber); - return true; - } - - private boolean isTraceConstructed(Integer[] choiceList, IntChoiceFromSet backtrackCG) { - // Concatenate state ID and trace in a string, e.g., "1:10234" - int stateId = backtrackCG.getStateId(); + // Check if this trace is already constructed + private boolean isTraceAlreadyConstructed(int firstChoice, 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(':'); - for(Integer choice : choiceList) { - sb.append(choice); - } + sb.append(firstChoice); // Check if the trace has been constructed as a backtrack point for this state if (doneBacktrackSet.contains(sb.toString())) { return true; @@ -725,123 +1037,154 @@ public class DPORStateReducer extends ListenerAdapter { return false; } - private void resetStatesForNewExecution(IntChoiceFromSet icsCG) { + // Reset data structure for each new execution + private void resetStatesForNewExecution(IntChoiceFromSet icsCG, VM vm) { if (choices == null || choices != icsCG.getAllChoices()) { // Reset state variables choiceCounter = 0; choices = icsCG.getAllChoices(); refChoices = copyChoices(choices); - lastCGStateId = icsCG.getStateId(); - // Clearing data structures - conflictPairMap.clear(); - readWriteFieldsMap.clear(); - stateToEventMap.clear(); + // Clear data structures + currVisitedStates = new HashSet<>(); + stateToEventMap = new HashMap<>(); isEndOfExecution = false; - // Adding this CG as the first CG for this execution - cgList.add(icsCG); } } - private void setBacktrackCG(int stateId) { + // Set a backtrack point for a particular state + 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 + LinkedList backtrackExecutions = backtrackMap.get(stateId); + BacktrackExecution backtrackExecution = backtrackExecutions.removeLast(); + backtrackCG.setNewValues(backtrackExecution.getChoiceList()); // Get the last from the queue + backtrackCG.setStateId(stateId); backtrackCG.reset(); + // Update current execution with this new execution + Execution newExecution = new Execution(); + TransitionEvent firstTransition = backtrackExecution.getFirstTransition(); + newExecution.addTransition(firstTransition); + // Try to free some memory since this map is only used for the current execution + currentExecution.clearCGToChoiceMap(); + currentExecution = newExecution; // Remove from the queue if we don't have more backtrack points for that state - if (backtrackChoices.isEmpty()) { - cgMap.remove(stateId); + if (backtrackExecutions.isEmpty()) { backtrackMap.remove(stateId); backtrackStateQ.remove(stateId); } } - private void setNextBacktrackPoint(IntChoiceFromSet icsCG) { + // Update backtrack sets + // 1) recursively, and + // 2) track accesses per memory location (per shared variable/field) + private void updateBacktrackSet(Execution execution, int currentChoice) { + // Copy ReadWriteSet object + HashMap currRWFieldsMap = execution.getReadWriteFieldsMap(); + 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 + // TODO: The following is the call to the original version of the method +// updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited); + // TODO: The following is the call to the version of the method with pushing up happens-before transitions + updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, execution, currentChoice, currRWSet, visited); + } - 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); - } - isFirstResetDone = true; - } else { - // Check if we still have backtrack points for the last state after the last backtrack - if (backtrackMap.containsKey(lastCGStateId)) { - setBacktrackCG(lastCGStateId); - } else { - // 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(); - setBacktrackCG(hiStateId); - } - } +// TODO: This is the original version of the recursive method +// 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 = conflictExecution.getExecutionTrace().get(conflictChoice); +// // Halt when we have visited this transition (in a cycle) +// if (visited.contains(confTrans)) { +// return; +// } +// visited.add(confTrans); +// // Explore all predecessors +// for (Predecessor predecessor : confTrans.getPredecessors()) { +// // Get the predecessor (previous conflict choice) +// conflictChoice = predecessor.getChoice(); +// conflictExecution = predecessor.getExecution(); +// // Check if a conflict is found +// if (isConflictFound(execution, currentChoice, conflictExecution, conflictChoice, currRWSet)) { +// createBacktrackingPoint(execution, currentChoice, conflictExecution, conflictChoice); +// } +// // Continue performing DFS if conflict is not found +// updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited); +// } +// } + + // TODO: This is the version of the method with pushing up happens-before transitions + private void updateBacktrackSetRecursive(Execution execution, int currentChoice, + Execution conflictExecution, int conflictChoice, + Execution hbExecution, int hbChoice, + ReadWriteSet currRWSet, HashSet visited) { + // Halt when we have found the first read/write conflicts for all memory locations + if (currRWSet.isEmpty()) { + return; + } + TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice); + // Halt when we have visited this transition (in a cycle) + if (visited.contains(confTrans)) { + return; } - // Clear unused CGs - for(IntChoiceFromSet cg : cgList) { - if (!backtrackCGs.contains(cg)) { - cg.setDone(); + visited.add(confTrans); + // Explore all predecessors + for (Predecessor predecessor : confTrans.getPredecessors()) { + // Get the predecessor (previous conflict choice) + conflictChoice = predecessor.getChoice(); + conflictExecution = predecessor.getExecution(); + // Push up one happens-before transition + int pushedChoice = hbChoice; + Execution pushedExecution = hbExecution; + // Check if a conflict is found + if (isConflictFound(execution, currentChoice, conflictExecution, conflictChoice, currRWSet)) { + createBacktrackingPoint(pushedExecution, pushedChoice, conflictExecution, conflictChoice); + pushedChoice = conflictChoice; + pushedExecution = conflictExecution; } + // Continue performing DFS if conflict is not found + updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, + pushedExecution, pushedChoice, currRWSet, visited); } - 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; - } - nodesToVisit.addLast(nextNode); - } + // Remove the transition after being explored + visited.remove(confTrans); + } + + // --- Functions related to the reachability analysis when there is a state match + + private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) { + // Perform this analysis only when: + // 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) || prevVisitedStates.contains(stateId)) { + // Update reachable transitions in the graph with a predecessor + HashSet reachableTransitions = rGraph.getReachableTransitionsAtState(stateId); + for(TransitionEvent transition : reachableTransitions) { + transition.recordPredecessor(currentExecution, choiceCounter - 1); } + updateBacktrackSetsFromPreviousExecution(stateId); } } - 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); + // Update the backtrack sets from previous executions + private void updateBacktrackSetsFromPreviousExecution(int stateId) { + // Collect all the reachable transitions from R-Graph + HashSet reachableTransitions = rGraph.getReachableTransitions(stateId); + for(TransitionEvent transition : reachableTransitions) { + Execution execution = transition.getExecution(); + int currentChoice = transition.getChoiceCounter(); + updateBacktrackSet(execution, currentChoice); } - choiceSet.add(currChoiceValue); - prevChoiceValue = currChoiceValue; } }