From: rtrimana <rtrimana@uci.edu>
Date: Thu, 2 Jul 2020 22:31:13 +0000 (-0700)
Subject: Fixing a bug: in the second round of boolean CG, we might encounter states in the... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=a5b0389c6d6608271a0cd1f05cbddf10c8d4e1b4;ds=inline

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.
---

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<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;
     }