Extra explicit model checker method.

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

prism/src/explicit/MDPModelChecker.java

@@ -397,6 +397,20 @@ public class MDPModelChecker extends ModelChecker
 		return mdp.mvMultMinMaxSingleChoices(state, lastSoln, min, val);
 	}
 
+	/**
+	 * Compute bounded probabilistic reachability.
+	 * @param mdp: The MDP
+	 * @param target: Target states
+	 * @param k: Bound
+	 * @param min: Min or max probabilities for (true=min, false=max)
+	 * @param init: Initial solution vector - pass null for default
+	 * @param results: Optional array of size b+1 to store (init state) results for each step (null if unused)
+	 */
+	public ModelCheckerResult probReachBounded(MDP mdp, BitSet target, int k, boolean min) throws PrismException
+	{
+		return probReachBounded(mdp, target, k, min, null, null);
+	}
+
 	/**
 	 * Compute bounded probabilistic reachability.
 	 * @param mdp: The MDP