Fixing a bug: summary of conflict transitions is to be paired up with a transition...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
index c0a7db5958c1fc016570b2f51af8efc192bee68b..5762ec5ec6628788dd3f03457199a06b9e5fbe51 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
@@ -393,12 +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, SummaryNode>> graphSummary;
+    //private HashMap<Integer, HashMap<Integer, SummaryNode>> graphSummary;
 
     public RGraph() {
       hiStateId = 0;
       graph = new HashMap<>();
-      graphSummary = new HashMap<>();
+      //graphSummary = new HashMap<>();
     }
 
     public void addReachableTransition(int stateId, TransitionEvent transition) {
@@ -443,14 +443,14 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
 //      return reachableTransitions;
 //    }
 
-    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)) {
-        return new HashMap<>();
-      }
-      return graphSummary.get(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)) {
+//        return new HashMap<>();
+//      }
+//      return graphSummary.get(stateId);
+//    }
 
 //    private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) {
 //      // Combine the same write accesses and record in the recordedRWSet
@@ -507,18 +507,18 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
 //      return rwSet;
 //    }
 
-    public void recordTransitionSummaryAtState(int stateId, HashMap<Integer, SummaryNode> transitionSummary) {
-      // Record transition summary into graphSummary
-      HashMap<Integer, SummaryNode> transSummary;
-      if (!graphSummary.containsKey(stateId)) {
-        transSummary = new HashMap<>(transitionSummary);
-        graphSummary.put(stateId, transSummary);
-      } else {
-        transSummary = graphSummary.get(stateId);
-        // Merge the two transition summaries
-        transSummary.putAll(transitionSummary);
-      }
-    }
+//    public void recordTransitionSummaryAtState(int stateId, HashMap<Integer, SummaryNode> transitionSummary) {
+//      // Record transition summary into graphSummary
+//      HashMap<Integer, SummaryNode> transSummary;
+//      if (!graphSummary.containsKey(stateId)) {
+//        transSummary = new HashMap<>(transitionSummary);
+//        graphSummary.put(stateId, transSummary);
+//      } else {
+//        transSummary = graphSummary.get(stateId);
+//        // Merge the two transition summaries
+//        transSummary.putAll(transitionSummary);
+//      }
+//    }
   }
 
   // This class compactly stores Read and Write field sets
@@ -1325,9 +1325,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());
+//    rGraph.recordTransitionSummaryAtState(currTrans.getStateId(), currTrans.getTransitionSummary());
     // Halt when we have found the first read/write conflicts for all memory locations
     if (currRWSet.isEmpty()) {
       return;
@@ -1398,25 +1398,33 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
         for(TransitionEvent transition : reachableTransitions) {
           transition.recordPredecessor(currentExecution, choiceCounter - 1);
         }
-        updateBacktrackSetsFromPreviousExecution(currentExecution, choiceCounter - 1, stateId);
+        updateBacktrackSetsFromPreviousExecution(stateId);
       }
     }
   }
 
-  private void updateBacktrackSetsFromPreviousExecution(Execution execution, int currentChoice, int stateId) {
+  private void updateBacktrackSetsFromPreviousExecution(int stateId) {
     // Collect all the reachable transitions from R-Graph
-    HashMap<Integer, SummaryNode> reachableTransitions = rGraph.getReachableTransitionSummary(stateId);
-    for(Map.Entry<Integer, SummaryNode> transition : reachableTransitions.entrySet()) {
-      SummaryNode summaryNode = transition.getValue();
-      TransitionEvent reachableTransition = summaryNode.getTransitionEvent();
-      Execution conflictExecution = reachableTransition.getExecution();
-      int conflictChoice = reachableTransition.getChoiceCounter();
-      // Copy ReadWriteSet object
-      ReadWriteSet currRWSet = summaryNode.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<>();
-      updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited);
+    //HashMap<Integer, SummaryNode> reachableTransitions = rGraph.getReachableTransitionSummary(stateId);
+    HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitionsAtState(stateId);
+    for(TransitionEvent transition : reachableTransitions) {
+      // Current transition that stems from this state ID
+      Execution currentExecution = transition.getExecution();
+      int currentChoice = transition.getChoiceCounter();
+      // Iterate over the stored conflict transitions in the summary
+      for(Map.Entry<Integer, SummaryNode> conflictTransition : transition.getTransitionSummary().entrySet()) {
+        SummaryNode summaryNode = conflictTransition.getValue();
+        // Conflict transition in the summary node
+        TransitionEvent confTrans = summaryNode.getTransitionEvent();
+        Execution conflictExecution = confTrans.getExecution();
+        int conflictChoice = confTrans.getChoiceCounter();
+        // Copy ReadWriteSet object
+        ReadWriteSet currRWSet = summaryNode.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<>();
+        updateBacktrackSetRecursive(currentExecution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited);
+      }
     }
   }
 }