- // --- Functions related to the visible operation dependency graph implementation discussed in the SPIN paper
-
- // This method checks whether a choice/event (transition) is reachable from the choice/event that produces
- // the state right before this state in the VOD graph
- // We use a BFS algorithm for this purpose
- private boolean isReachableInVODGraph(int currentChoice, VM vm) {
- // Current event
- int choiceIndex = currentChoice % refChoices.length;
- int currEvent = refChoices[choiceIndex];
- // Previous event
- int stateId = vm.getStateId(); // A state that has been seen
- int prevEvent = newStateEventMap.get(stateId);
- // Only start traversing the graph if prevEvent has an outgoing edge
- if (vodGraphMap.containsKey(prevEvent)) {
- // Record visited choices as we search in the graph
- HashSet<Integer> visitedChoice = new HashSet<>();
- visitedChoice.add(prevEvent);
- // Get the first nodes to visit (the neighbors of prevEvent)
- LinkedList<Integer> nodesToVisit = new LinkedList<>();
- nodesToVisit.addAll(vodGraphMap.get(prevEvent));
- // Traverse the graph using BFS
- while (!nodesToVisit.isEmpty()) {
- int choice = nodesToVisit.removeFirst();
- if (choice == currEvent) {
- return true;
- }
- if (visitedChoice.contains(choice)) { // If there is a loop then just continue the exploration
- continue;
- }
- // Continue searching
- visitedChoice.add(choice);
- HashSet<Integer> choiceNextNodes = vodGraphMap.get(choice);
- if (choiceNextNodes != null) {
- // Add only if there is a mapping for next nodes
- for (Integer nextNode : choiceNextNodes) {
- // Skip cycles
- if (nextNode == choice) {
- continue;
+ // --- 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);