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

@@ -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,