Fixing a bug: in the second round of boolean CG, we might encounter states in the...
authorrtrimana <rtrimana@uci.edu>
Thu, 2 Jul 2020 22:31:13 +0000 (15:31 -0700)
committerrtrimana <rtrimana@uci.edu>
Thu, 2 Jul 2020 22:31:13 +0000 (15:31 -0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java

index a54c7fa..3e387a9 100644 (file)
@@ -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++) {
-        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;
     }