Tested updating backtrack sets in the reachability graph.

[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 37353f3ed432ea9c7f19d3652099cacf43bee01d..f4b59233c47accb4f3cc0cae7671d1c98f864aef 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -980,6 +980,23 @@ public class DPORStateReducer extends ListenerAdapter {
 
   // --- Functions related to the reachability analysis when there is a state match
 
+  // TODO: OPTIMIZATION!
+  // Check and make sure that state ID and choice haven't been explored for this trace
+  private boolean alreadyChecked(HashSet<String> checkedStateIdAndChoice, BacktrackPoint backtrackPoint) {
+    int stateId = backtrackPoint.getStateId();
+    int choice = backtrackPoint.getChoice();
+    StringBuilder sb = new StringBuilder();
+    sb.append(stateId);
+    sb.append(':');
+    sb.append(choice);
+    // Check if the trace has been constructed as a backtrack point for this state
+    if (checkedStateIdAndChoice.contains(sb.toString())) {
+      return true;
+    }
+    checkedStateIdAndChoice.add(sb.toString());
+    return false;
+  }
+
   // We use backtrackPointsList to analyze the reachable states/events when there is a state match:
   // 1) Whenever there is state match, there is a cycle of events
   // 2) We need to analyze and find conflicts for the reachable choices/events in the cycle
@@ -995,10 +1012,10 @@ public class DPORStateReducer extends ListenerAdapter {
       if (currVisitedStates.contains(stateId)) {
         // Update the backtrack sets in the cycle
         updateBacktrackSetsInCycle(stateId);
-      } /* else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution
+      } else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution
         // Update the backtrack sets in a previous execution
-        updateBacktrackSetsInPreviousExecution(stateId);
-      }*/
+        updateBacktrackSetsInPreviousExecutions(stateId);
+      }
     }
   }
 
@@ -1047,34 +1064,43 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
-  // TODO: OPTIMIZATION!
-  // Check and make sure that state ID and choice haven't been explored for this trace
-  private boolean isNotChecked(HashMap<Integer, HashSet<Integer>> checkedStateIdAndChoice,
-                               BacktrackPoint backtrackPoint) {
-    int stateId = backtrackPoint.getStateId();
-    int choice = backtrackPoint.getChoice();
-    HashSet<Integer> choiceSet;
-    if (checkedStateIdAndChoice.containsKey(stateId)) {
-      choiceSet = checkedStateIdAndChoice.get(stateId);
-      if (choiceSet.contains(choice)) {
-        // State ID and choice found. It has been checked!
-        return false;
+  private void updateBacktrackSetsInPreviousExecution(Execution rExecution, int stateId,
+                                                      HashSet<String> checkedStateIdAndChoice) {
+    // Find the choice/event that marks the start of the subtrace from the previous execution
+    ArrayList<BacktrackPoint> pastExecutionTrace = rExecution.getExecutionTrace();
+    HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap = rExecution.getReadWriteFieldsMap();
+    int pastConfChoice = getPastConflictChoice(stateId, pastExecutionTrace);
+    int reachableChoice = choiceCounter;
+    // Iterate from the starting point until the end of the past execution trace
+    while (pastConfChoice < pastExecutionTrace.size() - 1) {  // BacktrackPoint list always has a surplus of 1
+      // Get the info of the event from the past execution trace
+      BacktrackPoint confBtrackPoint = pastExecutionTrace.get(pastConfChoice);
+      if (!alreadyChecked(checkedStateIdAndChoice, confBtrackPoint)) {
+        ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice);
+        // Append this event to the current list and map
+        ArrayList<BacktrackPoint> currentTrace = currentExecution.getExecutionTrace();
+        HashMap<Integer, ReadWriteSet> currRWFieldsMap = currentExecution.getReadWriteFieldsMap();
+        currentTrace.add(confBtrackPoint);
+        currRWFieldsMap.put(choiceCounter, rwSet);
+        for (int conflictChoice = reachableChoice - 1; conflictChoice >= 0; conflictChoice--) {
+          if (isConflictFound(reachableChoice, conflictChoice, currentExecution)) {
+            createBacktrackingPoint(reachableChoice, conflictChoice, currentExecution);
+          }
+        }
+        // Remove this event to replace it with a new one
+        currentTrace.remove(currentTrace.size() - 1);
+        currRWFieldsMap.remove(choiceCounter);
       }
-    } else {
-      choiceSet = new HashSet<>();
-      checkedStateIdAndChoice.put(stateId, choiceSet);
+      pastConfChoice++;
     }
-    choiceSet.add(choice);
-
-    return true;
   }
 
   // Update the backtrack sets in a previous execution
-  private void updateBacktrackSetsInPreviousExecution(int stateId) {
+  private void updateBacktrackSetsInPreviousExecutions(int stateId) {
     // Don't check a past trace twice!
     HashSet<Execution> checkedTrace = new HashSet<>();
     // Don't check the same event twice for a revisited state
-    HashMap<Integer, HashSet<Integer>> checkedStateIdAndChoice = new HashMap<>();
+    HashSet<String> checkedStateIdAndChoice = new HashSet<>();
     // Get sorted reachable state IDs
     ArrayList<Integer> reachableStateIds = getReachableStateIds(rGraph.keySet(), stateId);
     // Iterate from this state ID until the biggest state ID
@@ -1083,33 +1109,7 @@ public class DPORStateReducer extends ListenerAdapter {
       ArrayList<Execution> rExecutions = rGraph.get(stId);
       for (Execution rExecution : rExecutions) {
         if (!checkedTrace.contains(rExecution)) {
-          // Find the choice/event that marks the start of the subtrace from the previous execution
-          ArrayList<BacktrackPoint> pastExecutionTrace = rExecution.getExecutionTrace();
-          HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap = rExecution.getReadWriteFieldsMap();
-          int pastConfChoice = getPastConflictChoice(stId, pastExecutionTrace);
-          int conflictChoice = choiceCounter;
-          // Iterate from the starting point until the end of the past execution trace
-          while (pastConfChoice < pastExecutionTrace.size() - 1) {  // BacktrackPoint list always has a surplus of 1
-            // Get the info of the event from the past execution trace
-            BacktrackPoint confBtrackPoint = pastExecutionTrace.get(pastConfChoice);
-            if (isNotChecked(checkedStateIdAndChoice, confBtrackPoint)) {
-              ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice);
-              // Append this event to the current list and map
-              ArrayList<BacktrackPoint> currentTrace = currentExecution.getExecutionTrace();
-              HashMap<Integer, ReadWriteSet> currRWFieldsMap = currentExecution.getReadWriteFieldsMap();
-              currentTrace.add(confBtrackPoint);
-              currRWFieldsMap.put(choiceCounter, rwSet);
-              for (int pastChoice = conflictChoice - 1; pastChoice >= 0; pastChoice--) {
-                if (isConflictFound(conflictChoice, pastChoice, rExecution)) {
-                  createBacktrackingPoint(conflictChoice, pastChoice, rExecution);
-                }
-              }
-              // Remove this event to replace it with a new one
-              currentTrace.remove(currentTrace.size() - 1);
-              currRWFieldsMap.remove(choiceCounter);
-            }
-            pastConfChoice++;
-          }
+          updateBacktrackSetsInPreviousExecution(rExecution, stateId, checkedStateIdAndChoice);
           checkedTrace.add(rExecution);
         }
       }