Minor changes to input arguments of some methods/functions.

[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 7512691915478dfd6c6bd197864a5fbb3d602957..1f5408d90b9dc27aaa44f45f86f88ac7e1bdf73d 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
@@ -373,7 +373,7 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
     private int choice;           // Predecessor choice
     private Execution execution;  // Predecessor execution
 
-    public Predecessor(int predChoice, Execution predExec) {
+    public Predecessor(Execution predExec, int predChoice) {
       choice = predChoice;
       execution = predExec;
     }
@@ -444,6 +444,11 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
     }
 
     public HashMap<Integer, SummaryNode> getReachableTransitionsSummary(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);
     }
 
@@ -613,6 +618,8 @@ 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)
+    private HashMap<Execution, HashSet<Integer>> recordedPredecessors;
+                                               // Memorize event and choice number to not record them twice
     private int stateId;                       // State at this transition
     private IntChoiceFromSet transitionCG;     // CG at this transition
 
@@ -621,6 +628,7 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
       choiceCounter = 0;
       execution = null;
       predecessors = new HashSet<>();
+      recordedPredecessors = new HashMap<>();
       stateId = 0;
       transitionCG = null;
     }
@@ -647,8 +655,28 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
 
     public IntChoiceFromSet getTransitionCG() { return transitionCG; }
 
+    private boolean isRecordedPredecessor(Execution execution, int choice) {
+      // See if we have recorded this predecessor earlier
+      HashSet<Integer> recordedChoices;
+      if (recordedPredecessors.containsKey(execution)) {
+        recordedChoices = recordedPredecessors.get(execution);
+        if (recordedChoices.contains(choice)) {
+          return true;
+        }
+      } else {
+        recordedChoices = new HashSet<>();
+        recordedPredecessors.put(execution, recordedChoices);
+      }
+      // Record the choice if we haven't seen it
+      recordedChoices.add(choice);
+
+      return false;
+    }
+
     public void recordPredecessor(Execution execution, int choice) {
-      predecessors.add(new Predecessor(choice, execution));
+      if (!isRecordedPredecessor(execution, choice)) {
+        predecessors.add(new Predecessor(execution, choice));
+      }
     }
 
     public void setChoice(int cho) {
@@ -1220,15 +1248,15 @@ 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
     TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice);
     // Record this transition into rGraph summary
-    currRWSet = rGraph.recordTransitionSummary(confTrans.getStateId(), confTrans, currRWSet);
+    currRWSet = rGraph.recordTransitionSummary(currTrans.getStateId(), confTrans, 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);
     if (visited.contains(currTrans)) {
       return;
     }