ProbModel/NondetModel: add doReachability with seed states

Sometimes, we have additional knowledge which states of the model
(apart from the initial states) are guaranteed to be reachable.
The added method then provides a way to start the reachability computation
with those states as the seed, which can speed up the computation as less
unknown states have to be discovered.


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

prism/src/prism/NondetModel.java

@@ -214,6 +214,39 @@ public class NondetModel extends ProbModel
 		setReach(reachable);
 	}
 
+	/**
+	 * Compute and store the set of reachable states,
+	 * where the parameter {@seed} provides an initial set of states
+	 * known to be reachable.
+	 * <br/>
+	 * Starts reachability computation from the union of {@code seed} and {@start}.
+	 * <br/>[ REFS: <i>result</i>, DEREFS: seed ]
+	 * @param seed set of states (over ddRowVars) that is known to be reachable
+	 */
+	public void doReachability(JDDNode seed)
+	{
+		JDDNode tmp;
+
+		// do sanity check on seed if checking is enabled
+		if (SanityJDD.enabled)
+			SanityJDD.checkIsStateSet(seed, getAllDDRowVars());
+
+		// remove any nondeterminism from the 0/1-transition function
+		JDD.Ref(trans01);
+		tmp = JDD.MaxAbstract(trans01, allDDNondetVars);
+
+		// S = union of initial states and seed. seed is dereferenced here.
+		JDDNode S = JDD.Or(start.copy(), seed);
+
+		// compute reachable states
+		JDDNode reachable = PrismMTBDD.Reachability(tmp, allDDRowVars, allDDColVars, S);
+		JDD.Deref(tmp);
+		JDD.Deref(S);
+
+		// set the reachable states, compute numStates, create the ODD, etc
+		setReach(reachable);
+	}
+
 	// remove non-reachable states from various dds
 	// (and calculate num transitions, etc.)
 	// (and build mask)

prism/src/prism/ProbModel.java

@@ -570,6 +570,27 @@ public class ProbModel implements Model
 		setReach(PrismMTBDD.Reachability(trans01, allDDRowVars, allDDColVars, start));
 	}
 
+	/**
+	 * Compute and store the set of reachable states, where the parameter {@seed}
+	 * provides an initial set of states known to be reachable.
+	 * <br/>
+	 * Starts reachability computation from the union of {@code seed} and {@start}.
+	 * <br/>[ REFS: <i>result</i>, DEREFS: seed ]
+	 * @param seed set of states (over ddRowVars) that is known to be reachable
+	 */
+	public void doReachability(JDDNode seed)
+	{
+		// do sanity check on seed if checking is enabled
+		if (SanityJDD.enabled)
+			SanityJDD.checkIsStateSet(seed, getAllDDRowVars());
+
+		// S = union of initial states and seed. seed is dereferenced here.
+		JDDNode S = JDD.Or(start.copy(), seed);
+		// compute and store reachable states
+		setReach(PrismMTBDD.Reachability(trans01, allDDRowVars, allDDColVars, S));
+		JDD.Deref(S);
+	}
+
 	// this method allows you to skip the reachability phase
 	// it is only here for experimental purposes - not general use.