diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java
index 2b2e03f6..a21ae970 100644
--- a/prism/src/prism/NondetModel.java
+++ b/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)
diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java
index cef47c55..dbc4c1a4 100644
--- a/prism/src/prism/ProbModel.java
+++ b/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.