Fixing a potential bug: we now store the event number in the ArrayList together with...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 72fc44e6c67f8ec4a48cfa8dd141a2ab043c33c3..53cd5663f607d496ef980dab13f416bd8239c3fe 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -60,9 +60,9 @@ 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 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<Integer> currVisitedStates; // States being visited in the current execution
@@ -72,7 +72,7 @@ public class DPORStateReducer extends ListenerAdapter {
   // Data structure to analyze field Read/Write accesses and conflicts
   private HashMap<Integer, LinkedList<Integer[]>> backtrackMap;       // Track created backtracking points
   private PriorityQueue<Integer> backtrackStateQ;                     // Heap that returns the latest state
-  private ArrayList<IntChoiceFromSet> cgList;                         // Record CGs for backtracking points
+  private ArrayList<BacktrackPoint> backtrackPointList;               // Record backtrack points (CG and choice)
   private HashMap<Integer, IntChoiceFromSet> cgMap;                   // Maps state IDs to CGs
   private HashMap<Integer, HashSet<Integer>> conflictPairMap;         // Record conflicting events
   private HashSet<String> doneBacktrackSet;                           // Record state ID and trace that are done
@@ -188,7 +188,8 @@ public class DPORStateReducer extends ListenerAdapter {
           int choiceIndex = choiceCounter % choices.length;
           icsCG.advance(choices[choiceIndex]);
           // Index the ChoiceGenerator to set backtracking points
-          cgList.add(icsCG);
+          BacktrackPoint backtrackPoint = new BacktrackPoint(icsCG, choices[choiceIndex]);
+          backtrackPointList.add(backtrackPoint);
         } else {
           // Set done all CGs while transitioning to a new execution
           icsCG.setDone();
@@ -326,19 +327,19 @@ public class DPORStateReducer extends ListenerAdapter {
   // 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
+    private int choice;                   // Choice chosen at this backtrack point
 
-    public BacktrackPoint(IntChoiceFromSet cg, Integer[] choices) {
+    public BacktrackPoint(IntChoiceFromSet cg, int cho) {
       backtrackCG = cg;
-      backtrackChoices = choices;
+      choice = cho;
     }
 
     public IntChoiceFromSet getBacktrackCG() {
       return backtrackCG;
     }
 
-    public Integer[] getBacktrackChoices() {
-      return backtrackChoices;
+    public int getChoice() {
+      return choice;
     }
   }
 
@@ -423,7 +424,7 @@ public class DPORStateReducer extends ListenerAdapter {
     // Backtracking
     backtrackMap = new HashMap<>();
     backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder());
-    cgList = new ArrayList<>();
+    backtrackPointList = new ArrayList<>();
     cgMap = new HashMap<>();
     conflictPairMap = new HashMap<>();
     doneBacktrackSet = new HashSet<>();
@@ -572,10 +573,9 @@ public class DPORStateReducer extends ListenerAdapter {
     Integer[] newChoiceList = new Integer[refChoices.length];
     // 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
+    // We use the actual choices here in case they have been modified/adjusted by the fair scheduling method
     newChoiceList[0] = choices[actualCurrCho];
-    newChoiceList[1] = choices[actualConfEvtNum];
+    newChoiceList[1] = backtrackPointList.get(confEvtNum).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++) {
       if (refChoices[i] != newChoiceList[0] && refChoices[i] != newChoiceList[1]) {
@@ -583,8 +583,8 @@ public class DPORStateReducer extends ListenerAdapter {
         j++;
       }
     }
-    // Record the backtracking point in the stack as well
-    IntChoiceFromSet backtrackCG = cgList.get(confEvtNum);
+    // Get the backtrack CG for this backtrack point
+    IntChoiceFromSet backtrackCG = backtrackPointList.get(confEvtNum).getBacktrackCG();
     // Check if this trace has been done starting from this state
     if (isTraceConstructed(newChoiceList, backtrackCG)) {
       return;
@@ -737,8 +737,8 @@ public class DPORStateReducer extends ListenerAdapter {
       readWriteFieldsMap.clear();
       stateToEventMap.clear();
       isEndOfExecution = false;
-                       // Adding this CG as the first CG for this execution
-                       cgList.add(icsCG);
+      // Adding this CG as the first backtrack point for this execution
+      backtrackPointList.add(new BacktrackPoint(icsCG, choices[0]));
     }
   }
 
@@ -779,12 +779,13 @@ public class DPORStateReducer extends ListenerAdapter {
       }
     }
     // Clear unused CGs
-    for(IntChoiceFromSet cg : cgList) {
+    for(BacktrackPoint backtrackPoint : backtrackPointList) {
+      IntChoiceFromSet cg = backtrackPoint.getBacktrackCG();
       if (!backtrackCGs.contains(cg)) {
         cg.setDone();
       }
     }
-    cgList.clear();
+    backtrackPointList.clear();
   }
 
   // --- Functions related to the visible operation dependency graph implementation discussed in the SPIN paper