From cbc80bab53955639725607b92589296bbbab0c87 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 21 Feb 2010 15:44:30 +0000 Subject: [PATCH] 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 | 14 ++++++++++++++ 1 file changed, 14 insertions(+) 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