projects
/
jpf-core.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Testing the implementation; fixing a bug.
[jpf-core.git]
/
src
/
main
/
gov
/
nasa
/
jpf
/
listener
/
DPORStateReducerEfficient.java
diff --git
a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
index 7512691915478dfd6c6bd197864a5fbb3d602957..594829080a3ef30b4f04fe746f2ab4a38d4fb01e 100644
(file)
--- a/
src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
+++ b/
src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
@@
-444,6
+444,11
@@
public class DPORStateReducerEfficient extends ListenerAdapter {
}
public HashMap<Integer, SummaryNode> getReachableTransitionsSummary(int stateId) {
}
public HashMap<Integer, SummaryNode> getReachableTransitionsSummary(int stateId) {
+ // Just return an empty map if the state ID is not recorded yet
+ // This means that there is no reachable transition from this state
+ if (!graphSummary.containsKey(stateId)) {
+ return new HashMap<>();
+ }
return graphSummary.get(stateId);
}
return graphSummary.get(stateId);
}