From a4536fef4878b59ebb084fa473663ad0a9942676 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 30 Aug 2016 12:32:38 +0000 Subject: [PATCH] add NBA.getSuccessors git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11755 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/jltl2dstar/NBA.java | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/prism/src/jltl2dstar/NBA.java b/prism/src/jltl2dstar/NBA.java index 185780c9..55c1472e 100644 --- a/prism/src/jltl2dstar/NBA.java +++ b/prism/src/jltl2dstar/NBA.java @@ -22,6 +22,7 @@ package jltl2dstar; import java.util.*; +import common.IterableBitSet; import prism.PrismException; import prism.PrismNotSupportedException; @@ -153,6 +154,20 @@ public class NBA implements Iterable { return _final_states; } + /** + * Get the set of successor states for the given set of from states + * and the element of the alphabet. + */ + public MyBitSet getSuccessors(MyBitSet fromStates, APElement elem) + { + MyBitSet result = new MyBitSet(fromStates.size()); + for (int s : IterableBitSet.getSetBits(fromStates)) { + // for each state s, do union of successors for elem. + result.or(get(s).getEdge(elem)); + } + return result; + } + // public MyBitSet calculateFinalTrueLoops(SCCs sccs); /**