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

[jpf-core.git] / src / main / gov / nasa / jpf / listener / DPORStateReducer.java

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 8531e2cc4db5c1588ba3db63204858786fae26f8..7d5546c2be70d4028d79069dce39edb81b6cbb85 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -74,7 +74,7 @@ public class DPORStateReducer extends ListenerAdapter {
   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
 
@@ -599,7 +599,7 @@ public class DPORStateReducer extends ListenerAdapter {
     // 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;
     }
     addNewBacktrackPoint(stateId, newChoiceList);
@@ -727,14 +727,16 @@ public class DPORStateReducer extends ListenerAdapter {
     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;