From a5b0389c6d6608271a0cd1f05cbddf10c8d4e1b4 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Thu, 2 Jul 2020 15:31:13 -0700 Subject: [PATCH] Fixing a bug: in the second round of boolean CG, we might encounter states in the first round that are considered new states; adding a guard condition for a map read. --- src/main/gov/nasa/jpf/listener/DPORStateReducer.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index a54c7fa..3e387a9 100644 --- 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 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; } -- 2.34.1