Optimization: Compare just the state and the fist event/choice of the trace to not...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 54170ea00a0e119654b7d19be87d78da643f851e..e613f09fb15609ebc3f45e9f337351dbc1a80e06 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -73,7 +73,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 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
 
   private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;      // Record fields that are accessed
   private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
 


@@ -592,7 +592,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
     // 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);
       return;
     }
     //BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList);


@@ -721,14 +721,16 @@ public class DPORStateReducer extends ListenerAdapter {
     return true;
   }
 
     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(':');
     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;
     // Check if the trace has been constructed as a backtrack point for this state
     if (doneBacktrackSet.contains(sb.toString())) {
       return true;