Changing StringBuilder into HashMap and HashSet.

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 3e387a9..c9738fa 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -30,7 +30,6 @@ import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
 
 import java.io.FileWriter;
 import java.io.PrintWriter;
 
 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;
 import java.util.*;
 import java.util.logging.Logger;
 import java.io.IOException;


@@ -71,7 +70,7 @@ public class DPORStateReducer extends ListenerAdapter {
   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 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
 
   private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
   private RGraph rGraph;                                          // R-Graph for past executions
 


@@ -80,7 +79,6 @@ public class DPORStateReducer extends ListenerAdapter {
   private boolean isEndOfExecution;
 
   // Statistics
   private boolean isEndOfExecution;
 
   // Statistics

-  private int numOfConflicts;

   private int numOfTransitions;
        
   public DPORStateReducer(Config config, JPF jpf) {
   private int numOfTransitions;
        
   public DPORStateReducer(Config config, JPF jpf) {


@@ -99,7 +97,6 @@ public class DPORStateReducer extends ListenerAdapter {
       }
     }
     isBooleanCGFlipped = false;
       }
     }
     isBooleanCGFlipped = false;

-               numOfConflicts = 0;

                numOfTransitions = 0;
                nonRelevantClasses = new HashSet<>();
                nonRelevantFields = new HashSet<>();
                numOfTransitions = 0;
                nonRelevantClasses = new HashSet<>();
                nonRelevantFields = new HashSet<>();


@@ -171,19 +168,13 @@ public class DPORStateReducer extends ListenerAdapter {
 
   @Override
   public void searchFinished(Search search) {
 
   @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);
     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);
       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();
       fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions);
       fileWriter.println();
       fileWriter.close();


@@ -230,8 +221,6 @@ public class DPORStateReducer extends ListenerAdapter {
         if (!isBooleanCGFlipped) {
           isBooleanCGFlipped = true;
         } else {
         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();
         }
           // Allocate new objects for data structure when the boolean is flipped from "false" to "true"
           initializeStatesVariables();
         }


@@ -716,7 +705,7 @@ public class DPORStateReducer extends ListenerAdapter {
     backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder());
     currentExecution = new Execution();
     currentExecution.addTransition(new TransitionEvent()); // Always start with 1 backtrack point
     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;
     rGraph = new RGraph();
     // Booleans
     isEndOfExecution = false;


@@ -1037,19 +1026,20 @@ public class DPORStateReducer extends ListenerAdapter {
   // 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"
   // 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
     // 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;
   }
 
     return false;
   }