Bounded until for DTMC/MDP in explicit engine.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5631 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/DTMCModelChecker.java

@@ -846,9 +846,8 @@ public class DTMCModelChecker extends ProbModelChecker
 	 */
 	public ModelCheckerResult computeBoundedReachProbs(DTMC dtmc, BitSet remain, BitSet target, int k, double init[], double results[]) throws PrismException
 	{
-		// TODO: implement until
-
 		ModelCheckerResult res = null;
+		BitSet unknown;
 		int i, n, iters;
 		double soln[], soln2[], tmpsoln[];
 		long timer;
@@ -879,13 +878,20 @@ public class DTMCModelChecker extends ProbModelChecker
 			results[0] = Utils.minMaxOverArraySubset(soln2, dtmc.getInitialStates(), true);
 		}
 
+		// Determine set of states actually need to perform computation for
+		unknown = new BitSet();
+		unknown.set(0, n);
+		unknown.andNot(target);
+		if (remain != null)
+			unknown.and(remain);
+		
 		// Start iterations
 		iters = 0;
 		while (iters < k) {
 
 			iters++;
 			// Matrix-vector multiply
-			dtmc.mvMult(soln, soln2, target, true);
+			dtmc.mvMult(soln, soln2, unknown, false);
 			// Store intermediate results if required
 			// (compute min/max value over initial states for this step)
 			if (results != null) {

prism/src/explicit/MDPModelChecker.java

@@ -991,9 +991,8 @@ public class MDPModelChecker extends ProbModelChecker
 	public ModelCheckerResult computeBoundedReachProbs(MDP mdp, BitSet remain, BitSet target, int k, boolean min, double init[], double results[])
 			throws PrismException
 	{
-		// TODO: implement until
-
 		ModelCheckerResult res = null;
+		BitSet unknown;
 		int i, n, iters;
 		double soln[], soln2[], tmpsoln[];
 		long timer;
@@ -1024,12 +1023,19 @@ public class MDPModelChecker extends ProbModelChecker
 			results[0] = Utils.minMaxOverArraySubset(soln2, mdp.getInitialStates(), true);
 		}
 
+		// Determine set of states actually need to perform computation for
+		unknown = new BitSet();
+		unknown.set(0, n);
+		unknown.andNot(target);
+		if (remain != null)
+			unknown.and(remain);
+		
 		// Start iterations
 		iters = 0;
 		while (iters < k) {
 			iters++;
 			// Matrix-vector multiply and min/max ops
-			mdp.mvMultMinMax(soln, min, soln2, target, true, null);
+			mdp.mvMultMinMax(soln, min, soln2, unknown, false, null);
 			// Store intermediate results if required
 			// (compute min/max value over initial states for this step)
 			if (results != null) {