From 7805084dc6a9e3865b245e2b170c4cfb68c848e1 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 13 Jun 2013 09:39:07 +0000
Subject: [PATCH] Fix strategy generation for Prob1 (explicit): do an extra
 inner fixed point loop at the end, to avoid problems of generating surplus
 strategy info during early outer iterations.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6921 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/MDPModelChecker.java | 28 +++++++++++++++++++++++--
 1 file changed, 26 insertions(+), 2 deletions(-)

diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java
index 6baaae68..541c2be0 100644
--- a/prism/src/explicit/MDPModelChecker.java
+++ b/prism/src/explicit/MDPModelChecker.java
@@ -463,7 +463,7 @@ public class MDPModelChecker extends ProbModelChecker
 	 * i.e. determine the states of an MDP which, with min/max probability 0,
 	 * reach a state in {@code target}, while remaining in those in @{code remain}.
 	 * {@code min}=true gives Prob0E, {@code min}=false gives Prob0A. 
-	 * Optionally, for min only, store optimal (memoryless) strategy info for 1 states. 
+	 * Optionally, for min only, store optimal (memoryless) strategy info for 0 states. 
 	 * @param mdp The MDP
 	 * @param remain Remain in these states (optional: null means "all")
 	 * @param target Target states
@@ -604,7 +604,7 @@ public class MDPModelChecker extends ProbModelChecker
 				if (min)
 					mdp.prob1Astep(unknown, u, v, soln);
 				else
-					mdp.prob1Estep(unknown, u, v, soln, strat);
+					mdp.prob1Estep(unknown, u, v, soln, null);
 				// Check termination (inner)
 				v_done = soln.equals(v);
 				// v = soln
@@ -618,6 +618,30 @@ public class MDPModelChecker extends ProbModelChecker
 			u.or(v);
 		}
 
+		// If we need to generate a strategy, do another iteration of the inner loop for this
+		// We could do this during the main double fixed point above, but we would generate surplus
+		// strategy info for non-1 states during early iterations of the outer loop,
+		// which are not straightforward to remove since this method does not know which states
+		// already have valid strategy info from Prob0.
+		// Notice that we only need to look at states in u (since we already know the answer),
+		// so we restrict 'unknown' further 
+		unknown.and(u);
+		if (!min && strat != null) {
+			v_done = false;
+			v.clear();
+			v.or(target);
+			soln.clear();
+			soln.or(target);
+			while (!v_done) {
+				mainLog.print(strat);
+				mdp.prob1Estep(unknown, u, v, soln, strat);
+				v_done = soln.equals(v);
+				v.clear();
+				v.or(soln);
+			}
+			u_done = v.equals(u);
+		}
+
 		// Finished precomputation
 		timer = System.currentTimeMillis() - timer;
 		mainLog.print("Prob1 (" + (min ? "min" : "max") + ")");