Fixing a bug: in the second round of boolean CG, we might encounter states in the...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index a54c7fa..3e387a9 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -440,7 +440,11 @@ public class DPORStateReducer extends ListenerAdapter {
       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++) {
       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++) {

-        reachableTransitions.addAll(graph.get(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;
     }
       }
       return reachableTransitions;
     }