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,