Tested backtrack in a cycle (local).

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index ee61c190a0738687c8e75cf5eb26a828a39a2cae..37353f3ed432ea9c7f19d3652099cacf43bee01d 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -605,8 +605,8 @@ public class DPORStateReducer extends ListenerAdapter {
       stateToEventMap.put(stateId, eventSet);
     }
     saveExecutionToRGraph(stateId);
-    stateToChoiceCounterMap.put(stateId, choiceCounter);
     analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
+    stateToChoiceCounterMap.put(stateId, choiceCounter);
     justVisitedStates.add(stateId);
     currVisitedStates.add(stateId);
   }
@@ -722,7 +722,7 @@ public class DPORStateReducer extends ListenerAdapter {
     return currentChoice;
   }
 
-  private void createBacktrackingPoint(int currentChoice, int conflictChoice, Execution execution) {
+  private void createBacktrackingPoint(int backtrackChoice, int conflictChoice, Execution execution) {
 
     // 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}
@@ -731,14 +731,14 @@ public class DPORStateReducer extends ListenerAdapter {
     //int firstChoice = choices[actualChoice];
     ArrayList<BacktrackPoint> pastTrace = execution.getExecutionTrace();
     ArrayList<BacktrackPoint> currTrace = currentExecution.getExecutionTrace();
-    int backtrackEvent = currTrace.get(currentChoice).getChoice();
+    int btrackChoice = currTrace.get(backtrackChoice).getChoice();
     int stateId = pastTrace.get(conflictChoice).getStateId();
     // Check if this trace has been done from this state
-    if (isTraceAlreadyConstructed(backtrackEvent, stateId)) {
+    if (isTraceAlreadyConstructed(btrackChoice, stateId)) {
       return;
     }
     // Put the conflicting event numbers first and reverse the order
-    newChoiceList[0] = backtrackEvent;
+    newChoiceList[0] = btrackChoice;
     newChoiceList[1] = pastTrace.get(conflictChoice).getChoice();
     // 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++) {
@@ -803,7 +803,6 @@ public class DPORStateReducer extends ListenerAdapter {
                }
                // 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;
   }
@@ -866,19 +865,19 @@ public class DPORStateReducer extends ListenerAdapter {
     return false;
   }
 
-  private boolean isConflictFound(int currentChoice, int reachableEvent, Execution execution) {
+  private boolean isConflictFound(int reachableChoice, int conflictChoice, Execution execution) {
 
     ArrayList<BacktrackPoint> executionTrace = execution.getExecutionTrace();
     HashMap<Integer, ReadWriteSet> 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(reachableEvent) ||
-            executionTrace.get(currentChoice).getChoice() == executionTrace.get(reachableEvent).getChoice()) {
+    if (!execRWFieldsMap.containsKey(conflictChoice) ||
+            executionTrace.get(reachableChoice).getChoice() == executionTrace.get(conflictChoice).getChoice()) {
       return false;
     }
     // Current R/W set
-    ReadWriteSet currRWSet = execRWFieldsMap.get(currentChoice);
+    ReadWriteSet currRWSet = execRWFieldsMap.get(reachableChoice);
     // R/W set of choice/event that may have a potential conflict
-    ReadWriteSet evtRWSet = execRWFieldsMap.get(reachableEvent);
+    ReadWriteSet evtRWSet = execRWFieldsMap.get(conflictChoice);
     // Check for conflicts with Read and Write fields for Write instructions
     Set<String> currWriteSet = currRWSet.getWriteSet();
     for(String writeField : currWriteSet) {
@@ -950,6 +949,7 @@ public class DPORStateReducer extends ListenerAdapter {
       choices = icsCG.getAllChoices();
       refChoices = copyChoices(choices);
       // Clear data structures
+      currVisitedStates = new HashSet<>();
       stateToChoiceCounterMap = new HashMap<>();
       stateToEventMap = new HashMap<>();
       isEndOfExecution = false;
@@ -995,10 +995,10 @@ public class DPORStateReducer extends ListenerAdapter {
       if (currVisitedStates.contains(stateId)) {
         // Update the backtrack sets in the cycle
         updateBacktrackSetsInCycle(stateId);
-      } else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution
+      } /* else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution
         // Update the backtrack sets in a previous execution
         updateBacktrackSetsInPreviousExecution(stateId);
-      }
+      }*/
     }
   }
 
@@ -1034,16 +1034,16 @@ public class DPORStateReducer extends ListenerAdapter {
   // Update the backtrack sets in the cycle
   private void updateBacktrackSetsInCycle(int stateId) {
     // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
-    int currentChoice = stateToChoiceCounterMap.get(stateId);
+    int reachableChoice = stateToChoiceCounterMap.get(stateId);
     int cycleEndChoice = choiceCounter - 1;
     // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward)
-    while (currentChoice < cycleEndChoice) {
-      for (int reachableEvent = currentChoice + 1; reachableEvent <= cycleEndChoice; reachableEvent++) {
-        if (isConflictFound(currentChoice, reachableEvent, currentExecution)) {
-          createBacktrackingPoint(currentChoice, reachableEvent, currentExecution);
+    while (reachableChoice < cycleEndChoice) {
+      for (int conflictChoice = reachableChoice + 1; conflictChoice <= cycleEndChoice; conflictChoice++) {
+        if (isConflictFound(reachableChoice, conflictChoice, currentExecution)) {
+          createBacktrackingPoint(reachableChoice, conflictChoice, currentExecution);
         }
       }
-      currentChoice++;
+      reachableChoice++;
     }
   }