Refactor explicit SCC computation, splitting SCCConsumer from SCCComputer.

To obtain the previous behaviour, change

SCCComputer sccs = SCCComputer.createSCCComputer(parent, model);
sccs.computeSCCs();
... = sccs.getSCCs();

to

SCCConsumerStore sccs = new SCCConsumerStore();
SCCComputer sccComp = SCCComputer.createSCCComputer(parent, model, sccs);
sccComp.computeSCCs();
... = sccs.getSCCs();


This additional flexibility in how SCCs can be consumed can be used
in the future for example to handle SCCs on-the-fly, without
having to store all of them at the same time.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12110 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/automata/DASimplifyAcceptance.java

@@ -4,7 +4,9 @@ import java.util.BitSet;
 
 import prism.PrismComponent;
 import prism.PrismException;
+import explicit.LTS;
 import explicit.SCCComputer;
+import explicit.SCCConsumerStore;
 import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceRabin;
 import acceptance.AcceptanceReach;
@@ -29,9 +31,11 @@ public class DASimplifyAcceptance
 		if (da.getAcceptance() instanceof AcceptanceRabin) {
 			DA<BitSet, AcceptanceRabin> dra = (DA<BitSet, AcceptanceRabin>) da;
 			// K_i states that do not occur in a (non-trivial) SCC of the DRA may as well be removed
-			SCCComputer sccComp = explicit.SCCComputer.createSCCComputer(parent, new LTSFromDA(da));
-			sccComp.computeBSCCs();
-			BitSet trivial = sccComp.getNotInSCCs();
+			LTS lts = new LTSFromDA(da);
+			SCCConsumerStore sccStore = new SCCConsumerStore();
+			SCCComputer sccComp = explicit.SCCComputer.createSCCComputer(parent, lts, sccStore);
+			sccComp.computeSCCs();
+			BitSet trivial = sccStore.getNotInSCCs();
 			for (RabinPair pair : dra.getAcceptance()) {
 				if (pair.getK().intersects(trivial)) {
 					pair.getK().andNot(trivial);

prism/src/automata/LTL2WDBA.java

@@ -53,6 +53,7 @@ import explicit.LTS;
 import explicit.LTSExplicit;
 import explicit.NonProbModelChecker;
 import explicit.SCCComputer;
+import explicit.SCCConsumerStore;
 
 /**
  * <p>
@@ -316,9 +317,10 @@ public class LTL2WDBA extends PrismComponent
 	{
 		LTS daLTS = new LTSFromDA(P.da);
 
-		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, daLTS);
+		SCCConsumerStore sccStore = new SCCConsumerStore();
+		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, daLTS, sccStore);
 		sccComputer.computeSCCs();
-		for (BitSet scc : sccComputer.getSCCs()) {
+		for (BitSet scc : sccStore.getSCCs()) {
 			if (hasAcceptingCycle(P, scc)) {
 				// mark all SCC states as final in powerset automaton
 				P.F.or(scc);
@@ -364,9 +366,10 @@ public class LTL2WDBA extends PrismComponent
 		// perform cycle check
 		// TODO: use nested-DFS?
 		boolean hasCycleViaF = false;
-		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, buchilts.lts);
+		SCCConsumerStore sccStore = new SCCConsumerStore();
+		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, buchilts.lts, sccStore);
 		sccComputer.computeSCCs();
-		for (BitSet subSCC : sccComputer.getSCCs()) {
+		for (BitSet subSCC : sccStore.getSCCs()) {
 			if (subSCC.intersects(buchilts.F)) {
 				hasCycleViaF = true;
 				break;

prism/src/explicit/DTMCModelChecker.java

@@ -354,9 +354,10 @@ public class DTMCModelChecker extends ProbModelChecker
 		mainLog.println("\nStarting total reward computation...");
 
 		// Compute bottom strongly connected components (BSCCs)
-		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, dtmc);
-		sccComputer.computeBSCCs();
-		List<BitSet> bsccs = sccComputer.getBSCCs();
+		SCCConsumerStore sccStore = new SCCConsumerStore();
+		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, dtmc, sccStore);
+		sccComputer.computeSCCs();
+		List<BitSet> bsccs = sccStore.getBSCCs();
 		numBSCCs = bsccs.size();
 
 		// Find BSCCs with non-zero reward
@@ -1478,10 +1479,11 @@ public class DTMCModelChecker extends ProbModelChecker
 		solnProbs = new double[n];
 
 		// Compute bottom strongly connected components (BSCCs)
-		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, dtmc);
-		sccComputer.computeBSCCs();
-		List<BitSet> bsccs = sccComputer.getBSCCs();
-		BitSet notInBSCCs = sccComputer.getNotInBSCCs();
+		SCCConsumerStore sccStore = new SCCConsumerStore();
+		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, dtmc, sccStore);
+		sccComputer.computeSCCs();
+		List<BitSet> bsccs = sccStore.getBSCCs();
+		BitSet notInBSCCs = sccStore.getNotInBSCCs();
 		numBSCCs = bsccs.size();
 
 		// See which states in the initial distribution do *not* have non-zero prob
@@ -1569,10 +1571,11 @@ public class DTMCModelChecker extends ProbModelChecker
 		n = dtmc.getNumStates();
 
 		// Compute bottom strongly connected components (BSCCs)
-		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, dtmc);
-		sccComputer.computeBSCCs();
-		List<BitSet> bsccs = sccComputer.getBSCCs();
-		BitSet notInBSCCs = sccComputer.getNotInBSCCs();
+		SCCConsumerStore sccStore = new SCCConsumerStore();
+		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, dtmc, sccStore);
+		sccComputer.computeSCCs();
+		List<BitSet> bsccs = sccStore.getBSCCs();
+		BitSet notInBSCCs = sccStore.getNotInBSCCs();
 		numBSCCs = bsccs.size();
 
 		// Compute steady-state probability for each BSCC...

prism/src/explicit/ECComputerDefault.java

@@ -195,9 +195,10 @@ public class ECComputerDefault extends ECComputer
 
 	private List<BitSet> computeSCCs(NondetModel model) throws PrismException
 	{
-		SCCComputer sccc = SCCComputer.createSCCComputer(this, model);
+		SCCConsumerStore sccs = new SCCConsumerStore();
+		SCCComputer sccc = SCCComputer.createSCCComputer(this, model, sccs);
 		sccc.computeSCCs();
-		return sccc.getSCCs();
+		return sccs.getSCCs();
 	}
 
 	private List<BitSet> translateStates(SubNondetModel model, List<BitSet> sccs)

prism/src/explicit/LTLModelChecker.java

@@ -651,9 +651,10 @@ public class LTLModelChecker extends PrismComponent
 	public BitSet findAcceptingBSCCs(Model model, AcceptanceOmega acceptance) throws PrismException
 	{
 		// Compute bottom strongly connected components (BSCCs)
-		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, model);
-		sccComputer.computeBSCCs();
-		List<BitSet> bsccs = sccComputer.getBSCCs();
+		SCCConsumerStore sccStore = new SCCConsumerStore();
+		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, model, sccStore);
+		sccComputer.computeSCCs();
+		List<BitSet> bsccs = sccStore.getBSCCs();
 
 		BitSet result = new BitSet();
 

prism/src/explicit/NonProbModelChecker.java

@@ -504,7 +504,8 @@ public class NonProbModelChecker extends StateModelChecker
 
 		mainLog.print("Searching for non-trivial, accepting SCCs in product LTS...");
 		mainLog.flush();
-		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, product.getProductModel());
+		SCCConsumerStore sccConsumerStore = new SCCConsumerStore();
+		SCCComputer sccComputer = SCCComputer.createSCCComputer(this, product.getProductModel(), sccConsumerStore);
 		sccComputer.computeSCCs();
 
 		// We determine the SCCs that intersect F, as those are guaranteed to
@@ -513,7 +514,7 @@ public class NonProbModelChecker extends StateModelChecker
 		int accepting = 0;
 		int sccs = 0;
 		BitSet acceptingSCCs = new BitSet();
-		for (BitSet scc : sccComputer.getSCCs()) {
+		for (BitSet scc : sccConsumerStore.getSCCs()) {
 			sccs++;
 			if (scc.intersects(product.getAcceptingStates())) {
 				acceptingSCCs.or(scc);

prism/src/explicit/SCCComputer.java

@@ -4,6 +4,7 @@
 //	Authors:
 //	* Christian von Essen <christian.vonessen@imag.fr> (Verimag, Grenoble)
 //	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//  * Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
 //	
 //------------------------------------------------------------------------------
 //	
@@ -27,9 +28,6 @@
 
 package explicit;
 
-import java.util.BitSet;
-import java.util.List;
-
 import prism.PrismComponent;
 import prism.PrismException;
 
@@ -39,6 +37,9 @@ import prism.PrismException;
  */
 public abstract class SCCComputer extends PrismComponent
 {
+	/** The consumer */
+	protected SCCConsumer consumer;
+
 	// Method used for finding (B)SCCs
 	public enum SCCMethod {
 		TARJAN;
@@ -56,52 +57,45 @@ public abstract class SCCComputer extends PrismComponent
 	/**
 	 * Static method to create a new SCCComputer object, depending on current settings.
 	 */
-	public static SCCComputer createSCCComputer(PrismComponent parent, Model model) throws PrismException
+	public static SCCComputer createSCCComputer(PrismComponent parent, Model model, SCCConsumer consumer) throws PrismException
 	{
 		// Only one algorithm implemented currently
-		return new SCCComputerTarjan(parent, model);
+		return new SCCComputerTarjan(parent, model, consumer);
 	}
 
 	/**
 	 * Base constructor.
 	 */
-	public SCCComputer(PrismComponent parent) throws PrismException
+	public SCCComputer(PrismComponent parent, SCCConsumer consumer) throws PrismException
 	{
 		super(parent);
+		this.consumer = consumer;
 	}
 
 	/**
-	 * Compute (non-trivial) strongly connected components (SCCs) and store them.
-	 * They should be retrieved using {@link #getSCCs()}.
-	 * States in trivial SCCs (those comprising a single state without a self-loop) are also stored.
-	 * They should be retrieved using {@link #getNotInSCCs()}.
-	 */
-	public abstract void computeSCCs();
-
-	/**
-	 * Get the list of computed (non-trivial) SCCs.
-	 */
-	public abstract List<BitSet> getSCCs();
-
-	/**
-	 * Get the states not in any (non-trivial) SCC.
-	 * In other words, this is all states in trivial SCCs (those comprising a single state without a self-loop).
+	 * Compute strongly connected components (SCCs) and notify the consumer.
+	 * This will only report non-trivial SCCs
 	 */
-	public abstract BitSet getNotInSCCs();
+	public void computeSCCs() throws PrismException
+	{
+		computeSCCs(true);
+	}
 
 	/**
-	 * Compute bottom strongly connected components (BSCCs) and store them.
-	 * They can be retrieved using {@link #getBSCCs()} and {@link #getNotInBSCCs()}.
+	 * Compute strongly connected components (SCCs) and notify the consumer.
+	 * Ignores trivial SCCS if {@code filterTrivialSCCs} is set to true.
 	 */
-	public abstract void computeBSCCs();
+	public abstract void computeSCCs(boolean filterTrivialSCCs) throws PrismException;
 
 	/**
-	 * Get the list of computed BSCCs.
+	 * Returns true if {@code state}, assumed to be an SCC, is a trivial SCC,
+	 * i.e., has no self lopp.
+	 * @param model the model
+	 * @param state the state index
 	 */
-	public abstract List<BitSet> getBSCCs();
-	
-	/**
-	 * Get the states not in any BSCC.
-	 */
-	public abstract BitSet getNotInBSCCs();
+	protected boolean isTrivialSCC(Model model, int state)
+	{
+		// false if there is a self-loop, i.e., a successor t == state
+		return !(model.someSuccessorsMatch(state, (t) -> {return t == state;}));
+	}
 }

prism/src/explicit/SCCComputerTarjan.java

@@ -44,14 +44,6 @@ public class SCCComputerTarjan extends SCCComputer
 	private Model model;
 	/* Number of nodes (model states) */
 	private int numNodes;
-	/* Computed list of SCCs */
-	private List<BitSet> sccs = new ArrayList<BitSet>();
-	/* States not in non-trivial SCCs */
-	private BitSet notInSCCs;
-	/* Computed list of BSCCs */
-	private List<BitSet> bsccs = new ArrayList<BitSet>();
-	/* States not in any BSCC */
-	private BitSet notInBSCCs;
 
 	/* Next index to give to a node */
 	private int index = 0;
@@ -61,13 +53,15 @@ public class SCCComputerTarjan extends SCCComputer
 	private ArrayList<Node> nodeList;
 	/* Nodes currently on the stack. */
 	private BitSet onStack;
+	/** Should we filter trivial SCCs? */
+	private boolean filterTrivialSCCs;
 
 	/**
 	 * Build (B)SCC computer for a given model.
 	 */
-	public SCCComputerTarjan(PrismComponent parent, Model model) throws PrismException
+	public SCCComputerTarjan(PrismComponent parent, Model model, SCCConsumer consumer) throws PrismException
 	{
-		super(parent);
+		super(parent, consumer);
 		this.model = model;
 		this.numNodes = model.getNumStates();
 		this.nodeList = new ArrayList<Node>(numNodes);
@@ -80,76 +74,21 @@ public class SCCComputerTarjan extends SCCComputer
 	// Methods for SCCComputer interface
 
 	@Override
-	public void computeSCCs()
+	public void computeSCCs(boolean filterTrivialSCCs) throws PrismException
 	{
+		this.filterTrivialSCCs = filterTrivialSCCs;
+		consumer.notifyStart(model);
 		tarjan();
-		// Now remove trivial SCCs
-		notInSCCs = new BitSet();
-		for (Iterator<BitSet> it = sccs.iterator(); it.hasNext(); ) {
-			BitSet scc = it.next();
-			if (scc.cardinality() == 1) {
-				int s = scc.nextSetBit(0);
-				if (!model.someSuccessorsInSet(s, scc)) {
-					it.remove(); // remove this SCC from sccs list
-					notInSCCs.set(s);
-				}
-			}
-		}
-	}
-
-	@Override
-	public void computeBSCCs()
-	{
-		computeSCCs();
-		notInBSCCs = (BitSet) getNotInSCCs().clone();
-		int n = sccs.size();
-		for (int i = 0; i < n; i++) {
-			BitSet scc = sccs.get(i);
-			boolean bottom = true;
-			for (int s = scc.nextSetBit(0); s >= 0; s = scc.nextSetBit(s + 1)) {
-				if (!model.allSuccessorsInSet(s, scc)) {
-					bottom = false;
-					break;
-				}
-			}
-			if (bottom)
-				bsccs.add(scc);
-			else
-				notInBSCCs.or(scc);
-		}
-	}
-
-	@Override
-	public List<BitSet> getSCCs()
-	{
-		return sccs;
+		consumer.notifyDone();
 	}
 
-	@Override
-	public BitSet getNotInSCCs()
-	{
-		return notInSCCs;
-	}
-	
-	@Override
-	public List<BitSet> getBSCCs()
-	{
-		return bsccs;
-	}
-
-	@Override
-	public BitSet getNotInBSCCs()
-	{
-		return notInBSCCs;
-	}
-	
 	// SCC Computation
 
 	/**
 	 * Execute Tarjan's algorithm. Determine maximal strongly connected components
 	 * (SCCS) for the graph of the model and stored in {@code sccs}.
 	 */
-	public void tarjan()
+	public void tarjan() throws PrismException
 	{
 		for (int i = 0; i < numNodes; i++) {
 			if (nodeList.get(i).lowlink == -1)
@@ -158,7 +97,7 @@ public class SCCComputerTarjan extends SCCComputer
 
 	}
 
-	private void tarjan(int i)
+	private void tarjan(int i) throws PrismException
 	{
 		final Node v = nodeList.get(i);
 		v.index = index;
@@ -166,9 +105,17 @@ public class SCCComputerTarjan extends SCCComputer
 		index++;
 		stack.add(0, i);
 		onStack.set(i);
+
+		boolean hadSelfloop = false;
 		SuccessorsIterator it = model.getSuccessors(i);
 		while (it.hasNext()) {
 			int e = it.nextInt();
+
+			if (e == i) {
+				hadSelfloop = true;
+				continue;
+			}
+
 			Node n = nodeList.get(e);
 			if (n.index == -1) {
 				tarjan(e);
@@ -178,14 +125,24 @@ public class SCCComputerTarjan extends SCCComputer
 			}
 		}
 		if (v.lowlink == v.index) {
+			// this is a singleton SCC if the top of the stack equals i
+			boolean singletonSCC = (stack.get(0) == i);
+			if (singletonSCC && filterTrivialSCCs) {
+				if (!hadSelfloop) { // singleton SCC & no selfloop -> trivial
+					stack.remove(0);
+					onStack.set(i, false);
+					return;
+				}
+			}
+
 			int n;
-			BitSet component = new BitSet();
+			consumer.notifyStartSCC();
 			do {
 				n = stack.remove(0);
 				onStack.set(n, false);
-				component.set(n);
+				consumer.notifyStateInSCC(n);
 			} while (n != i);
-			sccs.add(component);
+			consumer.notifyEndSCC();
 		}
 	}
 

prism/src/explicit/SCCConsumer.java

@@ -0,0 +1,69 @@
+//==============================================================================
+//	
+//	Copyright (c) 2016-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package explicit;
+
+import prism.PrismException;
+
+/**
+ * Interface for a consumer of SCC information, for use with an {@code SCCComputer}.
+ * When a new SCC is discovered, first {@code notifyStartSCC()} will be called.
+ * Subsequently, for each state of the SCC, {@code notifyStateInSCC()} will be called.
+ * When all states of the SCC have been notified, {@code notifyEndSCC()} will be called.
+ * When the whole SCC computation is finished, {@code notifyDone()} will be called once.
+ */
+public interface SCCConsumer {
+	/**
+	 * Call-back function, will be called once at the start.
+	 * Default implementation: Ignore.
+	 */
+	public default void notifyStart(Model model)
+	{
+		// ignore
+	}
+
+	/**
+	 * Call-back function, will be called when a new SCC is discovered.
+	 **/
+	public void notifyStartSCC() throws PrismException;
+
+	/**
+	 * Call-back function, will be called once for each state in the SCC.
+	 */
+	public void notifyStateInSCC(int stateIndex) throws PrismException;
+
+	/**
+	 * Call-back function, will be called when all states of the SCC have been
+	 * discovered.
+	 **/
+	public void notifyEndSCC() throws PrismException;
+
+	/**
+	 * Call-back function. Will be called after SCC computation is complete.
+	 */
+	public default void notifyDone() {}
+
+}

prism/src/explicit/SCCConsumerBSCCs.java

@@ -0,0 +1,77 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package explicit;
+
+import java.util.BitSet;
+
+import prism.PrismComponent;
+import prism.PrismException;
+
+/**
+ * Abstract base class for an SCC consumer that is only interested in
+ * the bottom strongly-connected components (BSCCs). <br/>
+ *
+ * Intercepts the {@code notifyNextSCC()} call, checks whether the SCC
+ * is a BSCC and calls {@code notifyNextBSCC()} if that is the case.
+ */
+public abstract class SCCConsumerBSCCs extends SCCConsumerBitSet {
+
+	protected Model model;
+
+	/** Constructor */
+	public SCCConsumerBSCCs()
+	{
+		model = null;  // will be set by notifyStart call
+	}
+
+	public  void notifyStart(Model model)
+	{
+		this.model = model;
+	}
+
+	/**
+	 * Call-back function. Called upon discovery of a BSCC.
+	 */
+	public abstract void notifyNextBSCC(BitSet bscc) throws PrismException;
+
+	@Override
+	public void notifyNextSCC(BitSet scc) throws PrismException
+	{
+		boolean bottom = true;
+		// BSCC <=> for all states s, all successors are again in the SCC.
+		for (int s = scc.nextSetBit(0); s >= 0; s = scc.nextSetBit(s + 1)) {
+			if (!model.allSuccessorsInSet(s, scc)) {
+				bottom = false;
+				break;
+			}
+		}
+
+		if (bottom) {
+			notifyNextBSCC(scc);
+		}
+	}
+}

prism/src/explicit/SCCConsumerBitSet.java

@@ -0,0 +1,94 @@
+//==============================================================================
+//	
+//	Copyright (c) 2016-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package explicit;
+
+import java.util.BitSet;
+
+import prism.PrismException;
+
+/**
+ * Abstract base class for a consumer of SCC information, for use with an {@code SCCComputer},
+ * where each SCC is stored as a BitSet.
+ * <br>
+ * When a new SCC is discovered, {@code notifyNextSCC()} will be called with a {@code BitSet} of the
+ * states in the SCC. When the SCC computation is finished, {@code notifyDone()} will be
+ * called once.
+ * <br>
+ * By default, for each SCC a fresh BitSet is created. If the BitSets that are
+ * passed to {@code notifyNextSCC} can be reused for the next call, the {@code reuseBitSet}
+ * flag can be set in the constructor.
+ */
+public abstract class SCCConsumerBitSet implements SCCConsumer
+{
+	private BitSet curSCC = null;
+	private boolean reuseBitSet = false;
+
+	/** Default constructor. Don't reuse the BitSets */
+	public SCCConsumerBitSet()
+	{
+		this(false);
+	}
+
+	/**
+	 * Constructor. If {@code reuseBitSet} is set, reuse the same BitSet for all
+	 * calls to {@code notifyNextSCC}.
+	 * @param reuseBitSet allow reuse of BitSets
+	 */
+	public SCCConsumerBitSet(boolean reuseBitSet)
+	{
+		this.reuseBitSet = reuseBitSet;
+		if (reuseBitSet)
+			curSCC = new BitSet();
+	}
+
+	@Override
+	public void notifyStartSCC() throws PrismException
+	{
+		if (reuseBitSet) {
+			curSCC.clear();
+		} else {
+			curSCC = new BitSet();
+		}
+	}
+
+	@Override
+	public void notifyStateInSCC(int stateIndex) throws PrismException
+	{
+		curSCC.set(stateIndex);
+	}
+
+	@Override
+	public void notifyEndSCC() throws PrismException
+	{
+		notifyNextSCC(curSCC);
+		if (!reuseBitSet) {
+			curSCC = null;
+		}
+	}
+
+	public abstract void notifyNextSCC(BitSet scc) throws PrismException;
+}

prism/src/explicit/SCCConsumerStore.java

@@ -0,0 +1,162 @@
+//==============================================================================
+//	
+//	Copyright (c) 2014-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package explicit;
+
+import java.util.ArrayList;
+import java.util.BitSet;
+import java.util.List;
+
+/**
+ * SCC consumer that stores lists of the discovered SCCs and BSCCs.
+ * The list of BSCCs is computed on demand from the list of SCCs.
+ */
+public class SCCConsumerStore extends SCCConsumerBitSet {
+	/* Computed list of SCCs */
+	private List<BitSet> sccs = new ArrayList<BitSet>();
+	/* Computed list of BSCCs */
+	private List<BitSet> bsccs;
+	/* States not in any BSCC */
+	private BitSet notInBSCCs;
+	/* States not in any SCC */
+	private BitSet notInSCCs;
+
+	/** Is the SCC computation finished? */
+	private boolean finished = false;
+
+	private Model model;
+
+	/** Constructor */
+	public SCCConsumerStore()
+	{
+		model = null;  // will be set by notifyStart call
+	}
+
+	@Override
+	public void notifyStart(Model model)
+	{
+		this.model = model;
+	}
+
+	@Override
+	public void notifyNextSCC(BitSet scc)
+	{
+		sccs.add(scc);
+	}
+
+	@Override
+	public void notifyDone()
+	{
+		finished = true;
+	}
+
+	/**
+	 * Get a list of the SCCs. Can only be called once the SCC computation is finished.
+	 */
+	public List<BitSet> getSCCs()
+	{
+		if (!finished)
+			throw new UnsupportedOperationException("SCC computation is not yet finished.");
+
+		return sccs;
+	}
+
+	/**
+	 * Get a list of the BSCCs. Can only be called once the SCC computation is finished.
+	 */
+	public List<BitSet> getBSCCs()
+	{
+		if (!finished)
+			throw new UnsupportedOperationException("SCC computation is not yet finished.");
+
+		// If we don't have the list of BSCCs already, compute it.
+		if (bsccs == null) {
+			computeBSCCs();
+		}
+		return bsccs;
+	}
+
+	/**
+	 * Get the set of states not in any BSCCs. Can only be called once the SCC computation is finished.
+	 */
+	public BitSet getNotInBSCCs()
+	{
+		if (!finished)
+			throw new UnsupportedOperationException("SCC computation is not yet finished.");
+
+		// If we don't have the set already, compute it.
+		if (notInBSCCs == null) {
+			computeBSCCs();
+		}
+		return notInBSCCs;
+	}
+
+	/**
+	 * Compute the list of BSCCs from the list of SCCs.
+	 */
+	private void computeBSCCs()
+	{
+		if (!finished)
+			throw new UnsupportedOperationException("SCC computation is not yet finished.");
+
+		bsccs = new ArrayList<BitSet>();
+		notInBSCCs = (BitSet) getNotInSCCs().clone();
+		for (BitSet scc : sccs) {
+			boolean bottom = true;
+			// BSCC <=> for all states s, all successors are again in SCC
+			for (int s = scc.nextSetBit(0); s >= 0; s = scc.nextSetBit(s + 1)) {
+				if (!model.allSuccessorsInSet(s, scc)) {
+					bottom = false;
+					break;
+				}
+			}
+			if (bottom)
+				// store SCC as a BSCC
+				bsccs.add(scc);
+			else
+				// add states in scc to notInBSCCs
+				notInBSCCs.or(scc);
+		}
+	}
+
+	public BitSet getNotInSCCs()
+	{
+		if (!finished)
+			throw new UnsupportedOperationException("SCC computation is not yet finished.");
+
+		if (notInSCCs != null) {
+			return notInSCCs;
+		}
+		BitSet result = new BitSet();
+		for (BitSet scc : getSCCs()) {
+			result.or(scc);
+		}
+		result.flip(0, model.getNumStates());
+		notInSCCs = result;
+		return notInSCCs;
+	}
+
+}

prism/src/prism/Prism.java

@@ -1095,10 +1095,11 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 
 	/**
 	 * Get an SCCComputer object for the explicit engine.
+	 * @param consumer the SCCConsumer
 	 */
-	public explicit.SCCComputer getExplicitSCCComputer(explicit.Model model) throws PrismException
+	public explicit.SCCComputer getExplicitSCCComputer(explicit.Model model, explicit.SCCConsumer consumer) throws PrismException
 	{
-		return explicit.SCCComputer.createSCCComputer(this, model);
+		return explicit.SCCComputer.createSCCComputer(this, model, consumer);
 	}
 
 	/**
@@ -2454,7 +2455,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		long l; // timer
 		PrismLog tmpLog;
 		SCCComputer sccComputer = null;
-		explicit.SCCComputer sccComputerExpl = null;
+		explicit.SCCConsumerStore sccConsumerExpl = null;
 		//Vector<JDDNode> bsccs;
 		//JDDNode not, bscc;
 
@@ -2475,8 +2476,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 			sccComputer = getSCCComputer(currentModel);
 			sccComputer.computeBSCCs();
 		} else {
-			sccComputerExpl = getExplicitSCCComputer(currentModelExpl);
-			sccComputerExpl.computeBSCCs();
+			sccConsumerExpl = new explicit.SCCConsumerStore();
+			getExplicitSCCComputer(currentModelExpl, sccConsumerExpl).computeSCCs();
 		}
 		l = System.currentTimeMillis() - l;
 		mainLog.println("\nTime for BSCC computation: " + l / 1000.0 + " seconds.");
@@ -2504,7 +2505,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		if (!getExplicit()) {
 			n = sccComputer.getBSCCs().size();
 		} else {
-			n = sccComputerExpl.getBSCCs().size();
+			n = sccConsumerExpl.getBSCCs().size();
 		}
 		for (i = 0; i < n; i++) {
 			tmpLog.println();
@@ -2520,8 +2521,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 					new StateListMTBDD(sccComputer.getBSCCs().get(i), currentModel).printMatlab(tmpLog);
 				JDD.Deref(sccComputer.getBSCCs().get(i));
 			} else {
-				explicit.StateValues.createFromBitSet(sccComputerExpl.getBSCCs().get(i), currentModelExpl).print(tmpLog, true, exportType == EXPORT_MATLAB,
-						true, true);
+				explicit.StateValues.createFromBitSet(sccConsumerExpl.getBSCCs().get(i), currentModelExpl).print(tmpLog, true, exportType == EXPORT_MATLAB, true, true);
 			}
 			if (exportType == EXPORT_MATLAB)
 				tmpLog.println("];");
@@ -2640,7 +2640,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		long l; // timer
 		PrismLog tmpLog;
 		SCCComputer sccComputer = null;
-		explicit.SCCComputer sccComputerExpl = null;
+		explicit.SCCConsumerStore sccConsumerExpl = null;
 
 		// no specific states format for MRMC
 		if (exportType == EXPORT_MRMC)
@@ -2659,8 +2659,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 			sccComputer = getSCCComputer(currentModel);
 			sccComputer.computeSCCs();
 		} else {
-			sccComputerExpl = getExplicitSCCComputer(currentModelExpl);
-			sccComputerExpl.computeSCCs();
+			sccConsumerExpl = new explicit.SCCConsumerStore();
+			getExplicitSCCComputer(currentModelExpl, sccConsumerExpl).computeSCCs();
 		}
 		l = System.currentTimeMillis() - l;
 		mainLog.println("\nTime for SCC computation: " + l / 1000.0 + " seconds.");
@@ -2688,7 +2688,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		if (!getExplicit()) {
 			n = sccComputer.getSCCs().size();
 		} else {
-			n = sccComputerExpl.getSCCs().size();
+			n = sccConsumerExpl.getSCCs().size();
 		}
 		for (i = 0; i < n; i++) {
 			tmpLog.println();
@@ -2704,8 +2704,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 					new StateListMTBDD(sccComputer.getSCCs().get(i), currentModel).printMatlab(tmpLog);
 				JDD.Deref(sccComputer.getSCCs().get(i));
 			} else {
-				explicit.StateValues.createFromBitSet(sccComputerExpl.getSCCs().get(i), currentModelExpl).print(tmpLog, true, exportType == EXPORT_MATLAB,
-						true, true);
+				explicit.StateValues.createFromBitSet(sccConsumerExpl.getSCCs().get(i), currentModelExpl).print(tmpLog, true, exportType == EXPORT_MATLAB, true, true);
 			}
 			if (exportType == EXPORT_MATLAB)
 				tmpLog.println("];");