From 87675e828a150418c3c858aac6304274c36d19b6 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 21 Jul 2017 14:16:31 +0000 Subject: [PATCH] explicit.MDPModelChecker: split numeric computation part of computeReachProbs into separate method Preparation for upcoming interval iteration commits, etc. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12125 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDPModelChecker.java | 41 +++++++++++++++---------- 1 file changed, 25 insertions(+), 16 deletions(-) diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 3b334606..0a9efdac 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -439,22 +439,7 @@ public class MDPModelChecker extends ProbModelChecker // Compute probabilities (if needed) if (numYes + numNo < n) { - switch (mdpSolnMethod) { - case VALUE_ITERATION: - res = computeReachProbsValIter(mdp, no, yes, min, init, known, strat); - break; - case GAUSS_SEIDEL: - res = computeReachProbsGaussSeidel(mdp, no, yes, min, init, known, strat); - break; - case POLICY_ITERATION: - res = computeReachProbsPolIter(mdp, no, yes, min, strat); - break; - case MODIFIED_POLICY_ITERATION: - res = computeReachProbsModPolIter(mdp, no, yes, min, strat); - break; - default: - throw new PrismException("Unknown MDP solution method " + mdpSolnMethod.fullName()); - } + res = computeReachProbsNumeric(mdp, mdpSolnMethod, no, yes, min, init, known, strat); } else { res = new ModelCheckerResult(); res.soln = Utils.bitsetToDoubleArray(yes, n); @@ -486,6 +471,30 @@ public class MDPModelChecker extends ProbModelChecker return res; } + protected ModelCheckerResult computeReachProbsNumeric(MDP mdp, MDPSolnMethod method, BitSet no, BitSet yes, boolean min, double init[], BitSet known, int strat[]) throws PrismException + { + ModelCheckerResult res = null; + + switch (method) { + case VALUE_ITERATION: + res = computeReachProbsValIter(mdp, no, yes, min, init, known, strat); + break; + case GAUSS_SEIDEL: + res = computeReachProbsGaussSeidel(mdp, no, yes, min, init, known, strat); + break; + case POLICY_ITERATION: + res = computeReachProbsPolIter(mdp, no, yes, min, strat); + break; + case MODIFIED_POLICY_ITERATION: + res = computeReachProbsModPolIter(mdp, no, yes, min, strat); + break; + default: + throw new PrismException("Unknown MDP solution method " + mdpSolnMethod.fullName()); + } + + return res; + } + /** * Prob0 precomputation algorithm. * i.e. determine the states of an MDP which, with min/max probability 0,