Cleaning up the code; still need to test everything.

[jpf-core.git] / src / main / gov / nasa / jpf / listener / DPORStateReducerEfficient.java

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
index bb617af63c656f8efa9992e5938705c36f51f178..48297ccde1b33d969bed828cf7b201cd6973995e 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
@@ -393,14 +393,12 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
     private int hiStateId;                                     // Maximum state Id
     private HashMap<Integer, HashSet<TransitionEvent>> graph;  // Reachable transitions from past executions
     // TODO: THIS IS THE ACCESS SUMMARY
-    private HashMap<Integer, HashMap<Integer, ReadWriteSet>> graphSummary;
-    private HashMap<Integer, HashMap<Integer, TransitionEvent>> eventSummary;
+    private HashMap<Integer, HashMap<Integer, SummaryNode>> graphSummary;
 
     public RGraph() {
       hiStateId = 0;
       graph = new HashMap<>();
       graphSummary = new HashMap<>();
-      eventSummary = new HashMap<>();
     }
 
     public void addReachableTransition(int stateId, TransitionEvent transition) {
@@ -445,11 +443,7 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
       return reachableTransitions;
     }
 
-    public HashMap<Integer, TransitionEvent> getReachableSummaryTransitions(int stateId) {
-      return eventSummary.get(stateId);
-    }
-
-    public HashMap<Integer, ReadWriteSet> getReachableSummaryRWSets(int stateId) {
+    public HashMap<Integer, SummaryNode> getReachableTransitionsSummary(int stateId) {
       return graphSummary.get(stateId);
     }
 
@@ -487,27 +481,23 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
     public ReadWriteSet recordTransitionSummary(int stateId, TransitionEvent transition, ReadWriteSet rwSet) {
       // Record transition into graphSummary
       // TransitionMap maps event (choice) number to a R/W set
-      HashMap<Integer, ReadWriteSet> transitionMap;
+      HashMap<Integer, SummaryNode> transitionSummary;
       if (graphSummary.containsKey(stateId)) {
-        transitionMap = graphSummary.get(stateId);
+        transitionSummary = graphSummary.get(stateId);
       } else {
-        transitionMap = new HashMap<>();
-        graphSummary.put(stateId, transitionMap);
+        transitionSummary = new HashMap<>();
+        graphSummary.put(stateId, transitionSummary);
       }
       int choice = transition.getChoice();
-      ReadWriteSet recordedRWSet;
+      SummaryNode summaryNode;
       // Insert transition into the map if we haven't had this event number recorded
-      if (!transitionMap.containsKey(choice)) {
-        recordedRWSet = rwSet.getCopy();
-        transitionMap.put(choice, recordedRWSet);
-        // Insert the actual TransitionEvent object into the map
-        HashMap<Integer, TransitionEvent> eventMap = new HashMap<>();
-        eventMap.put(choice, transition);
-        eventSummary.put(stateId, eventMap);
+      if (!transitionSummary.containsKey(choice)) {
+        summaryNode = new SummaryNode(transition, rwSet.getCopy());
+        transitionSummary.put(choice, summaryNode);
       } else {
-        recordedRWSet = transitionMap.get(choice);
+        summaryNode = transitionSummary.get(choice);
         // Perform union and subtraction between the recorded and the given R/W sets
-        rwSet = performUnion(recordedRWSet, rwSet);
+        rwSet = performUnion(summaryNode.getReadWriteSet(), rwSet);
       }
       return rwSet;
     }
@@ -594,6 +584,25 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
     }
   }
 
+  // This class provides a data structure to store TransitionEvent and ReadWriteSet for a summary
+  private class SummaryNode {
+    private TransitionEvent transitionEvent;
+    private ReadWriteSet readWriteSet;
+
+    public SummaryNode(TransitionEvent transEvent, ReadWriteSet rwSet) {
+      transitionEvent = transEvent;
+      readWriteSet = rwSet;
+    }
+
+    public TransitionEvent getTransitionEvent() {
+      return transitionEvent;
+    }
+
+    public ReadWriteSet getReadWriteSet() {
+      return readWriteSet;
+    }
+  }
+
   // This class compactly stores transitions:
   // 1) CG,
   // 2) state ID,
@@ -1211,12 +1220,14 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
   private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
                                            Execution conflictExecution, int conflictChoice,
                                            ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
+    TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
+    // TODO: THIS IS THE ACCESS SUMMARY
+    // Record this transition into rGraph summary
+    currRWSet = rGraph.recordTransitionSummary(currTrans.getStateId(), currTrans, currRWSet);
     // Halt when we have found the first read/write conflicts for all memory locations
     if (currRWSet.isEmpty()) {
       return;
     }
-    TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
-    // Halt when we have visited this transition (in a cycle)
     if (visited.contains(currTrans)) {
       return;
     }
@@ -1235,10 +1246,6 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
         newConflictChoice = conflictChoice;
         newConflictExecution = conflictExecution;
       }
-      // TODO: THIS IS THE ACCESS SUMMARY
-      // Record this transition into rGraph summary
-      int stateId = predecessor.getExecution().getExecutionTrace().get(predecessorChoice).getStateId();
-      currRWSet = rGraph.recordTransitionSummary(stateId, currTrans, currRWSet);
       // Continue performing DFS if conflict is not found
       updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice,
               currRWSet, visited);
@@ -1298,14 +1305,13 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
 
   private void updateBacktrackSetsFromPreviousExecution(Execution execution, int currentChoice, int stateId) {
     // Collect all the reachable transitions from R-Graph
-    HashMap<Integer, TransitionEvent> reachableTransitions = rGraph.getReachableSummaryTransitions(stateId);
-    HashMap<Integer, ReadWriteSet> reachableRWSets = rGraph.getReachableSummaryRWSets(stateId);
-    for(Map.Entry<Integer, TransitionEvent> transition : reachableTransitions.entrySet()) {
-      TransitionEvent reachableTransition = transition.getValue();
+    HashMap<Integer, SummaryNode> reachableTransitions = rGraph.getReachableTransitionsSummary(stateId);
+    for(Map.Entry<Integer, SummaryNode> transition : reachableTransitions.entrySet()) {
+      TransitionEvent reachableTransition = transition.getValue().getTransitionEvent();
       Execution conflictExecution = reachableTransition.getExecution();
       int conflictChoice = reachableTransition.getChoiceCounter();
       // Copy ReadWriteSet object
-      ReadWriteSet currRWSet = reachableRWSets.get(transition.getKey());
+      ReadWriteSet currRWSet = transition.getValue().getReadWriteSet();
       currRWSet = currRWSet.getCopy();
       // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
       HashSet<TransitionEvent> visited = new HashSet<>();