From: rtrimana <rtrimana@uci.edu>
Date: Thu, 9 Apr 2020 16:40:28 +0000 (-0700)
Subject: Optimization: Compare just the state and the fist event/choice of the trace to not... 
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=3f2ed878a49e2214926a724ccf7ced0939f5a0af

Optimization: Compare just the state and the fist event/choice of the trace to not repeat the same backtrack trace twice (the two will map to the same state and the algorithm will stop the second execution, so there is no need to record and explore it twice, e.g., the traces 2 0 1 3 and 2 1 0 3 at state 3.
---

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 54170ea..e613f09 100644
--- 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 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;