From b641fa6049e4a531777c2b7a21e3160e12a2d629 Mon Sep 17 00:00:00 2001
From: rtrimana <rtrimana@uci.edu>
Date: Thu, 17 Sep 2020 09:46:29 -0700
Subject: [PATCH] Adding checks to ensure that a predecessor is only recorded
 once for a transition.

---
 .../nasa/jpf/listener/DPORStateReducer.java   | 25 ++++++++++++++++++-
 .../listener/DPORStateReducerEfficient.java   | 25 ++++++++++++++++++-
 2 files changed, 48 insertions(+), 2 deletions(-)

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 5ce8c40..70d8935 100644
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -531,6 +531,8 @@ public class DPORStateReducer 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
 
@@ -539,6 +541,7 @@ public class DPORStateReducer extends ListenerAdapter {
       choiceCounter = 0;
       execution = null;
       predecessors = new HashSet<>();
+      recordedPredecessors = new HashMap<>();
       stateId = 0;
       transitionCG = null;
     }
@@ -565,8 +568,28 @@ public class DPORStateReducer 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(choice, execution));
+      }
     }
 
     public void setChoice(int cho) {
diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
index 5948290..aa54e5e 100644
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
@@ -618,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
 
@@ -626,6 +628,7 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
       choiceCounter = 0;
       execution = null;
       predecessors = new HashSet<>();
+      recordedPredecessors = new HashMap<>();
       stateId = 0;
       transitionCG = null;
     }
@@ -652,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(choice, execution));
+      }
     }
 
     public void setChoice(int cho) {
-- 
2.34.1