Optimization: Compare just the state and the fist event/choice of the trace to not...
authorrtrimana <rtrimana@uci.edu>
Thu, 9 Apr 2020 16:40:28 +0000 (09:40 -0700)
committerrtrimana <rtrimana@uci.edu>
Thu, 9 Apr 2020 16:40:28 +0000 (09:40 -0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java

index 54170ea..e613f09 100644 (file)
@@ -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 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
 
@@ -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
-    if (isTraceConstructed(newChoiceList, stateId)) {
+    if (isTraceAlreadyConstructed(newChoiceList, stateId)) {
       return;
     }
     //BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList);
@@ -721,14 +721,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;