Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/jpf-core

diff --combined src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 8531e2cc4db5c1588ba3db63204858786fae26f8,e613f09fb15609ebc3f45e9f337351dbc1a80e06..7d5546c2be70d4028d79069dce39edb81b6cbb85
--- 1/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
--- 2/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@@ -28,7 -28,6 +28,7 @@@ import gov.nasa.jpf.vm.bytecode.WriteIn
  import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
  import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
  
 +import java.awt.*;
  import java.io.PrintWriter;
  import java.util.*;
  
@@@ -74,7 -73,7 +74,7 @@@ public class DPORStateReducer extends L
    private PriorityQueue<Integer> backtrackStateQ;                 // Heap that returns the latest state
    private ArrayList<BacktrackPoint> backtrackPointList;           // Record backtrack points (CG, state Id, and choice)
    private HashMap<Integer, HashSet<Integer>> conflictPairMap;     // Record conflicting events
-   private HashSet<String> doneBacktrackSet;                       // Record state ID and trace that are done
+   private HashSet<String> doneBacktrackSet;                       // Record state ID and trace already constructed
    private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;      // Record fields that are accessed
    private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
  
@@@ -377,11 -376,7 +377,11 @@@
        }
      }
      // Record state ID and choice/event as backtrack point
 -    backtrackPointList.add(new BacktrackPoint(icsCG, vm.getStateId(), refChoices[choiceIndex]));
 +    int stateId = vm.getStateId();
 +    backtrackPointList.add(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex]));
 +    // Store restorable state object for this state (always store the latest)
 +    RestorableVMState restorableState = vm.getRestorableState();
 +    restorableStateMap.put(stateId, restorableState);
    }
  
    private Integer[] copyChoices(Integer[] choicesToCopy) {
@@@ -473,6 -468,9 +473,6 @@@
        stateToEventMap.put(stateId, eventSet);
      }
      justVisitedStates.add(stateId);
 -    // Store restorable state object for this state (always store the latest)
 -    RestorableVMState restorableState = search.getVM().getRestorableState();
 -    restorableStateMap.put(stateId, restorableState);
    }
  
    // --- Functions related to Read/Write access analysis on shared fields
@@@ -557,20 -555,15 +557,20 @@@
      // 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 = 0;
 +    int currChoiceFromCG = currChoiceInd;
      ChoiceGenerator<?> currentCG = vm.getChoiceGenerator();
      // This is the main event CG
 -    if (currentCG instanceof IntChoiceFromSet) {
 -      currChoiceFromCG = currChoiceInd;
 -    } else {
 +    if (currentCG instanceof IntIntervalGenerator) {
        // This is the interval CG used in device handlers
        ChoiceGenerator<?> parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator();
 -      currChoiceFromCG = ((IntChoiceFromSet) parentCG).getNextChoiceIndex();
 +      int actualEvtNum = ((IntChoiceFromSet) parentCG).getNextChoice();
 +      // Find the index of the event/choice in refChoices
 +      for (int i = 0; i<refChoices.length; i++) {
 +        if (actualEvtNum == refChoices[i]) {
 +          currChoiceFromCG = i;
 +          break;
 +        }
 +      }
      }
      if (currChoiceInd != currChoiceFromCG) {
        currentChoice = (currentChoice - currChoiceInd) + currChoiceFromCG;
@@@ -599,9 -592,10 +599,9 @@@
      // Get the backtrack CG for this backtrack point
      int stateId = backtrackPointList.get(confEvtNum).getStateId();
      // Check if this trace has been done starting from this state
-     if (isTraceConstructed(newChoiceList, stateId)) {
+     if (isTraceAlreadyConstructed(newChoiceList, stateId)) {
        return;
      }
 -    //BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList);
      addNewBacktrackPoint(stateId, newChoiceList);
    }
  
@@@ -727,14 -721,16 +727,16 @@@
      return true;
    }
  
-   private boolean isTraceConstructed(Integer[] choiceList, int stateId) {
-     // Concatenate state ID and trace in a string, e.g., "1:10234"
+   private boolean isTraceAlreadyConstructed(Integer[] choiceList, 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(choiceList[0]);
      // Check if the trace has been constructed as a backtrack point for this state
      if (doneBacktrackSet.contains(sb.toString())) {
        return true;