diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 2a43b132..e6f3ba8d 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/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