Fixing a bug: summary of conflict transition and ReadWriteSet need to be stored in...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
index 1f5408d90b9dc27aaa44f45f86f88ac7e1bdf73d..cdfdcdd0a7fdf48c0d7002eb282d35a7fc49a236 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
@@ -430,20 +430,20 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
       return graph.get(stateId);
     }
 
-    public HashSet<TransitionEvent> getReachableTransitions(int stateId) {
-      HashSet<TransitionEvent> reachableTransitions = new HashSet<>();
-      // All transitions from states higher than the given state ID (until the highest state ID) are reachable
-      for(int stId = stateId; stId <= hiStateId; stId++) {
-        // We might encounter state IDs from the first round of Boolean CG
-        // The second round of Boolean CG should consider these new states
-        if (graph.containsKey(stId)) {
-          reachableTransitions.addAll(graph.get(stId));
-        }
-      }
-      return reachableTransitions;
-    }
+//    public HashSet<TransitionEvent> getReachableTransitions(int stateId) {
+//      HashSet<TransitionEvent> reachableTransitions = new HashSet<>();
+//      // All transitions from states higher than the given state ID (until the highest state ID) are reachable
+//      for(int stId = stateId; stId <= hiStateId; stId++) {
+//        // We might encounter state IDs from the first round of Boolean CG
+//        // The second round of Boolean CG should consider these new states
+//        if (graph.containsKey(stId)) {
+//          reachableTransitions.addAll(graph.get(stId));
+//        }
+//      }
+//      return reachableTransitions;
+//    }
 
-    public HashMap<Integer, SummaryNode> getReachableTransitionsSummary(int stateId) {
+    public HashMap<Integer, SummaryNode> getReachableTransitionSummary(int stateId) {
       // Just return an empty map if the state ID is not recorded yet
       // This means that there is no reachable transition from this state
       if (!graphSummary.containsKey(stateId)) {
@@ -452,59 +452,64 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
       return graphSummary.get(stateId);
     }
 
-    private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) {
-      // Combine the same write accesses and record in the recordedRWSet
-      HashMap<String, Integer> recordedWriteMap = recordedRWSet.getWriteMap();
-      HashMap<String, Integer> writeMap = rwSet.getWriteMap();
-      for(Map.Entry<String, Integer> entry : recordedWriteMap.entrySet()) {
-        String writeField = entry.getKey();
-        // Remove the entry from rwSet if both field and object ID are the same
-        if (writeMap.containsKey(writeField) &&
-                (writeMap.get(writeField) == recordedWriteMap.get(writeField))) {
-          writeMap.remove(writeField);
-        }
-      }
-      // Then add everything into the recorded map because these will be traversed
-      recordedWriteMap.putAll(writeMap);
-      // Combine the same read accesses and record in the recordedRWSet
-      HashMap<String, Integer> recordedReadMap = recordedRWSet.getReadMap();
-      HashMap<String, Integer> readMap = rwSet.getReadMap();
-      for(Map.Entry<String, Integer> entry : recordedReadMap.entrySet()) {
-        String readField = entry.getKey();
-        // Remove the entry from rwSet if both field and object ID are the same
-        if (readMap.containsKey(readField) &&
-                (readMap.get(readField) == recordedReadMap.get(readField))) {
-          readMap.remove(readField);
-        }
-      }
-      // Then add everything into the recorded map because these will be traversed
-      recordedReadMap.putAll(readMap);
+//    private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) {
+//      // Combine the same write accesses and record in the recordedRWSet
+//      HashMap<String, Integer> recordedWriteMap = recordedRWSet.getWriteMap();
+//      HashMap<String, Integer> writeMap = rwSet.getWriteMap();
+//      for(Map.Entry<String, Integer> entry : recordedWriteMap.entrySet()) {
+//        String writeField = entry.getKey();
+//        // Remove the entry from rwSet if both field and object ID are the same
+//        if (writeMap.containsKey(writeField) &&
+//                (writeMap.get(writeField) == recordedWriteMap.get(writeField))) {
+//          writeMap.remove(writeField);
+//        }
+//      }
+//      // Then add everything into the recorded map because these will be traversed
+//      recordedWriteMap.putAll(writeMap);
+//      // Combine the same read accesses and record in the recordedRWSet
+//      HashMap<String, Integer> recordedReadMap = recordedRWSet.getReadMap();
+//      HashMap<String, Integer> readMap = rwSet.getReadMap();
+//      for(Map.Entry<String, Integer> entry : recordedReadMap.entrySet()) {
+//        String readField = entry.getKey();
+//        // Remove the entry from rwSet if both field and object ID are the same
+//        if (readMap.containsKey(readField) &&
+//                (readMap.get(readField) == recordedReadMap.get(readField))) {
+//          readMap.remove(readField);
+//        }
+//      }
+//      // Then add everything into the recorded map because these will be traversed
+//      recordedReadMap.putAll(readMap);
+//
+//      return rwSet;
+//    }
 
-      return rwSet;
-    }
+//    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, SummaryNode> transitionSummary;
+//      if (graphSummary.containsKey(stateId)) {
+//        transitionSummary = graphSummary.get(stateId);
+//      } else {
+//        transitionSummary = new HashMap<>();
+//        graphSummary.put(stateId, transitionSummary);
+//      }
+//      int choice = transition.getChoice();
+//      SummaryNode summaryNode;
+//      // Insert transition into the map if we haven't had this event number recorded
+//      if (!transitionSummary.containsKey(choice)) {
+//        summaryNode = new SummaryNode(transition, rwSet.getCopy());
+//        transitionSummary.put(choice, summaryNode);
+//      } else {
+//        summaryNode = transitionSummary.get(choice);
+//        // Perform union and subtraction between the recorded and the given R/W sets
+//        rwSet = performUnion(summaryNode.getReadWriteSet(), rwSet);
+//      }
+//      return rwSet;
+//    }
 
-    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, SummaryNode> transitionSummary;
-      if (graphSummary.containsKey(stateId)) {
-        transitionSummary = graphSummary.get(stateId);
-      } else {
-        transitionSummary = new HashMap<>();
-        graphSummary.put(stateId, transitionSummary);
-      }
-      int choice = transition.getChoice();
-      SummaryNode summaryNode;
-      // Insert transition into the map if we haven't had this event number recorded
-      if (!transitionSummary.containsKey(choice)) {
-        summaryNode = new SummaryNode(transition, rwSet.getCopy());
-        transitionSummary.put(choice, summaryNode);
-      } else {
-        summaryNode = transitionSummary.get(choice);
-        // Perform union and subtraction between the recorded and the given R/W sets
-        rwSet = performUnion(summaryNode.getReadWriteSet(), rwSet);
-      }
-      return rwSet;
+    public void recordTransitionSummaryAtState(int stateId, HashMap<Integer, SummaryNode> transitionSummary) {
+      // Record transition summary into graphSummary
+      graphSummary.put(stateId, transitionSummary);
     }
   }
 
@@ -618,6 +623,9 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
     private int choiceCounter;                 // Choice counter at this transition
     private Execution execution;               // The execution where this transition belongs
     private HashSet<Predecessor> predecessors; // Maps incoming events/transitions (execution and choice)
+    // TODO: THIS IS THE ACCESS SUMMARY
+    private HashMap<Integer, SummaryNode> transitionSummary;
+                                               // Summary of pushed transitions at the current transition
     private HashMap<Execution, HashSet<Integer>> recordedPredecessors;
                                                // Memorize event and choice number to not record them twice
     private int stateId;                       // State at this transition
@@ -628,6 +636,7 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
       choiceCounter = 0;
       execution = null;
       predecessors = new HashSet<>();
+      transitionSummary = new HashMap<>();
       recordedPredecessors = new HashMap<>();
       stateId = 0;
       transitionCG = null;
@@ -653,6 +662,10 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
       return stateId;
     }
 
+    public HashMap<Integer, SummaryNode> getTransitionSummary() {
+      return transitionSummary;
+    }
+
     public IntChoiceFromSet getTransitionCG() { return transitionCG; }
 
     private boolean isRecordedPredecessor(Execution execution, int choice) {
@@ -673,12 +686,60 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
       return false;
     }
 
+    private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) {
+      // Combine the same write accesses and record in the recordedRWSet
+      HashMap<String, Integer> recordedWriteMap = recordedRWSet.getWriteMap();
+      HashMap<String, Integer> writeMap = rwSet.getWriteMap();
+      for(Map.Entry<String, Integer> entry : recordedWriteMap.entrySet()) {
+        String writeField = entry.getKey();
+        // Remove the entry from rwSet if both field and object ID are the same
+        if (writeMap.containsKey(writeField) &&
+                (writeMap.get(writeField) == recordedWriteMap.get(writeField))) {
+          writeMap.remove(writeField);
+        }
+      }
+      // Then add everything into the recorded map because these will be traversed
+      recordedWriteMap.putAll(writeMap);
+      // Combine the same read accesses and record in the recordedRWSet
+      HashMap<String, Integer> recordedReadMap = recordedRWSet.getReadMap();
+      HashMap<String, Integer> readMap = rwSet.getReadMap();
+      for(Map.Entry<String, Integer> entry : recordedReadMap.entrySet()) {
+        String readField = entry.getKey();
+        // Remove the entry from rwSet if both field and object ID are the same
+        if (readMap.containsKey(readField) &&
+                (readMap.get(readField) == recordedReadMap.get(readField))) {
+          readMap.remove(readField);
+        }
+      }
+      // Then add everything into the recorded map because these will be traversed
+      recordedReadMap.putAll(readMap);
+
+      return rwSet;
+    }
+
     public void recordPredecessor(Execution execution, int choice) {
       if (!isRecordedPredecessor(execution, choice)) {
         predecessors.add(new Predecessor(execution, choice));
       }
     }
 
+    public ReadWriteSet recordTransitionSummary(TransitionEvent transition, ReadWriteSet rwSet) {
+      // Record transition into reachability summary
+      // TransitionMap maps event (choice) number to a R/W set
+      int choice = transition.getChoice();
+      SummaryNode summaryNode;
+      // Insert transition into the map if we haven't had this event number recorded
+      if (!transitionSummary.containsKey(choice)) {
+        summaryNode = new SummaryNode(transition, rwSet.getCopy());
+        transitionSummary.put(choice, summaryNode);
+      } else {
+        summaryNode = transitionSummary.get(choice);
+        // Perform union and subtraction between the recorded and the given R/W sets
+        rwSet = performUnion(summaryNode.getReadWriteSet(), rwSet);
+      }
+      return rwSet;
+    }
+
     public void setChoice(int cho) {
       choice = cho;
     }
@@ -1252,7 +1313,9 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
     // TODO: THIS IS THE ACCESS SUMMARY
     TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice);
     // Record this transition into rGraph summary
-    currRWSet = rGraph.recordTransitionSummary(currTrans.getStateId(), confTrans, currRWSet);
+    //currRWSet = rGraph.recordTransitionSummary(currTrans.getStateId(), confTrans, currRWSet);
+    currRWSet = currTrans.recordTransitionSummary(confTrans, currRWSet);
+    rGraph.recordTransitionSummaryAtState(currTrans.getStateId(), currTrans.getTransitionSummary());
     // Halt when we have found the first read/write conflicts for all memory locations
     if (currRWSet.isEmpty()) {
       return;
@@ -1334,7 +1397,7 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
 
   private void updateBacktrackSetsFromPreviousExecution(Execution execution, int currentChoice, int stateId) {
     // Collect all the reachable transitions from R-Graph
-    HashMap<Integer, SummaryNode> reachableTransitions = rGraph.getReachableTransitionsSummary(stateId);
+    HashMap<Integer, SummaryNode> reachableTransitions = rGraph.getReachableTransitionSummary(stateId);
     for(Map.Entry<Integer, SummaryNode> transition : reachableTransitions.entrySet()) {
       SummaryNode summaryNode = transition.getValue();
       TransitionEvent reachableTransition = summaryNode.getTransitionEvent();