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

diff --combined src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index c9738fa90c21e9479c7ab5d560f69256d320f6e7,363bc4b1247dad9bb06c25e00cee67bdb10b3240..8e688cf833cf13700c0e9a645fd67b82677355a9
--- 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
@@@ -30,6 -30,7 +30,6 @@@ import gov.nasa.jpf.vm.choice.IntInterv
  
  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;
@@@ -70,7 -71,7 +70,7 @@@ public class DPORStateReducer extends L
    private HashMap<Integer, LinkedList<BacktrackExecution>> backtrackMap;  // Track created backtracking points
    private PriorityQueue<Integer> backtrackStateQ;                 // Heap that returns the latest state
    private Execution currentExecution;                             // Holds the information about the current execution
 -  private HashSet<String> doneBacktrackSet;                       // Record state ID and trace already constructed
 +  private HashMap<Integer, HashSet<Integer>> doneBacktrackMap;    // Record state ID and trace already constructed
    private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
    private RGraph rGraph;                                          // R-Graph for past executions
  
@@@ -79,6 -80,7 +79,6 @@@
    private boolean isEndOfExecution;
  
    // Statistics
 -  private int numOfConflicts;
    private int numOfTransitions;
        
    public DPORStateReducer(Config config, JPF jpf) {
@@@ -97,6 -99,7 +97,6 @@@
        }
      }
      isBooleanCGFlipped = false;
 -              numOfConflicts = 0;
                numOfTransitions = 0;
                nonRelevantClasses = new HashSet<>();
                nonRelevantFields = new HashSet<>();
@@@ -168,13 -171,19 +168,13 @@@
  
    @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();
@@@ -221,6 -230,8 +221,6 @@@
          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();
          }
@@@ -641,8 -652,10 +641,10 @@@
      }
      currentExecution.mapCGToChoice(icsCG, choiceCounter);
      // Store restorable state object for this state (always store the latest)
-     RestorableVMState restorableState = vm.getRestorableState();
-     restorableStateMap.put(stateId, restorableState);
+     if (!restorableStateMap.containsKey(stateId)) {
+       RestorableVMState restorableState = vm.getRestorableState();
+       restorableStateMap.put(stateId, restorableState);
+     }
    }
  
    private TransitionEvent setupTransition(IntChoiceFromSet icsCG, int stateId, int choiceIndex) {
@@@ -705,7 -718,7 +707,7 @@@
      backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder());
      currentExecution = new Execution();
      currentExecution.addTransition(new TransitionEvent()); // Always start with 1 backtrack point
 -    doneBacktrackSet = new HashSet<>();
 +    doneBacktrackMap = new HashMap<>();
      rGraph = new RGraph();
      // Booleans
      isEndOfExecution = false;
@@@ -1026,20 -1039,19 +1028,20 @@@
    // 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(':');
 -    sb.append(firstChoice);
      // Check if the trace has been constructed as a backtrack point for this state
 -    if (doneBacktrackSet.contains(sb.toString())) {
 -      return true;
 +    // TODO: THIS IS AN OPTIMIZATION!
 +    HashSet<Integer> choiceSet;
 +    if (doneBacktrackMap.containsKey(stateId)) {
 +      choiceSet = doneBacktrackMap.get(stateId);
 +      if (choiceSet.contains(firstChoice)) {
 +        return true;
 +      }
 +    } else {
 +      choiceSet = new HashSet<>();
 +      choiceSet.add(firstChoice);
 +      doneBacktrackMap.put(stateId, choiceSet);
      }
 -    doneBacktrackSet.add(sb.toString());
 +
      return false;
    }