explicit.SCCComputer: provide variant of computeSCCs where the state space is restricted with an IntPredicate

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

prism/src/explicit/SCCComputer.java

@@ -28,6 +28,8 @@
 
 package explicit;
 
+import java.util.function.IntPredicate;
+
 import prism.PrismComponent;
 import prism.PrismException;
 
@@ -85,7 +87,22 @@ public abstract class SCCComputer extends PrismComponent
 	 * Compute strongly connected components (SCCs) and notify the consumer.
 	 * Ignores trivial SCCS if {@code filterTrivialSCCs} is set to true.
 	 */
-	public abstract void computeSCCs(boolean filterTrivialSCCs) throws PrismException;
+	public void computeSCCs(boolean filterTrivialSCCs) throws PrismException
+	{
+		computeSCCs(filterTrivialSCCs, null);
+	}
+
+	/**
+	 * Compute strongly connected components (SCCs) and notify the consumer.
+	 * Ignores trivial SCCS if {@code filterTrivialSCCs} is set to true.
+	 * If {@code restrict != null}, restricts the underlying graph to only those states s
+	 * for which {@code restrict.test(s)} evaluates to true ("relevant states").
+	 * Edges to non-relevant states are ignored and the non-relevant
+	 * states are not considered as potential initial states.
+	 * @param filterTrivialSCCs ignore trivial SCCs
+	 * @param restrict predicate that indicates that a state is relevant ({@code null}: all states are relevant)
+	 */
+	public abstract void computeSCCs(boolean filterTrivialSCCs, IntPredicate restrictStates) throws PrismException;
 
 	/**
 	 * Returns true if {@code state}, assumed to be an SCC, is a trivial SCC,

prism/src/explicit/SCCComputerTarjan.java

@@ -31,6 +31,7 @@ import java.util.ArrayList;
 import java.util.BitSet;
 import java.util.LinkedList;
 import java.util.List;
+import java.util.function.IntPredicate;
 
 import prism.PrismComponent;
 import prism.PrismException;
@@ -55,6 +56,7 @@ public class SCCComputerTarjan extends SCCComputer
 	private BitSet onStack;
 	/** Should we filter trivial SCCs? */
 	private boolean filterTrivialSCCs;
+	private IntPredicate restrict;
 
 	/**
 	 * Build (B)SCC computer for a given model.
@@ -74,10 +76,11 @@ public class SCCComputerTarjan extends SCCComputer
 	// Methods for SCCComputer interface
 
 	@Override
-	public void computeSCCs(boolean filterTrivialSCCs) throws PrismException
+	public void computeSCCs(boolean filterTrivialSCCs, IntPredicate restrict) throws PrismException
 	{
 		this.filterTrivialSCCs = filterTrivialSCCs;
 		consumer.notifyStart(model);
+		this.restrict = restrict;
 		tarjan();
 		consumer.notifyDone();
 	}
@@ -91,6 +94,8 @@ public class SCCComputerTarjan extends SCCComputer
 	public void tarjan() throws PrismException
 	{
 		for (int i = 0; i < numNodes; i++) {
+			if (restrict != null && !restrict.test(i))
+				continue; // skip state if not one of the relevant states
 			if (nodeList.get(i).lowlink == -1)
 				tarjan(i);
 		}
@@ -116,6 +121,10 @@ public class SCCComputerTarjan extends SCCComputer
 				continue;
 			}
 
+			if (restrict != null && !restrict.test(e)) {
+				continue; // ignore edge to state that is not relevant
+			}
+
 			Node n = nodeList.get(e);
 			if (n.index == -1) {
 				tarjan(e);