From 3ff7df7b0a3b5c13b177d07abb08b310669f4713 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 11 Jun 2013 23:44:26 +0000
Subject: [PATCH] Attach strategy generation for MDP Gauss-Seidel (explicit).

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

diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java
index f42e5374..1b6af59f 100644
--- a/prism/src/explicit/MDPModelChecker.java
+++ b/prism/src/explicit/MDPModelChecker.java
@@ -414,7 +414,7 @@ public class MDPModelChecker extends ProbModelChecker
 			res = computeReachProbsValIter(mdp, no, yes, min, init, known, strat);
 			break;
 		case GAUSS_SEIDEL:
-			res = computeReachProbsGaussSeidel(mdp, no, yes, min, init, known);
+			res = computeReachProbsGaussSeidel(mdp, no, yes, min, init, known, strat);
 			break;
 		case POLICY_ITERATION:
 			res = computeReachProbsPolIter(mdp, no, yes, min);
@@ -720,21 +720,18 @@ public class MDPModelChecker extends ProbModelChecker
 	 * @param min Min or max probabilities (true=min, false=max)
 	 * @param init Optionally, an initial solution vector (will be overwritten) 
 	 * @param known Optionally, a set of states for which the exact answer is known
+	 * @param strat Storage for (memoryless) strategy choice indices (ignored if null)
 	 * Note: if 'known' is specified (i.e. is non-null, 'init' must also be given and is used for the exact values.  
 	 */
-	protected ModelCheckerResult computeReachProbsGaussSeidel(MDP mdp, BitSet no, BitSet yes, boolean min, double init[], BitSet known) throws PrismException
+	protected ModelCheckerResult computeReachProbsGaussSeidel(MDP mdp, BitSet no, BitSet yes, boolean min, double init[], BitSet known, int strat[]) throws PrismException
 	{
 		ModelCheckerResult res;
 		BitSet unknown;
 		int i, n, iters;
 		double soln[], initVal, maxDiff;
-		int strat[] = null;
-		boolean genStrat, done;
+		boolean done;
 		long timer;
 
-		// Are we generating an optimal strategy?
-		genStrat = exportAdv;
-		
 		// Start value iteration
 		timer = System.currentTimeMillis();
 		mainLog.println("Starting Gauss-Seidel (" + (min ? "min" : "max") + ")...");
@@ -770,14 +767,6 @@ public class MDPModelChecker extends ProbModelChecker
 		if (known != null)
 			unknown.andNot(known);
 
-		// Create/initialise strategy storage
-		if (genStrat) {
-			strat = new int[n];
-			for (i = 0; i < n; i++) {
-				strat[i] = -1;
-			}
-		}
-
 		// Start iterations
 		iters = 0;
 		done = false;
@@ -801,19 +790,6 @@ public class MDPModelChecker extends ProbModelChecker
 			throw new PrismException(msg);
 		}
 
-		// Export adversary
-		if (genStrat && exportAdv) {
-			// Prune strategy
-			restrictStrategyToReachableStates(mdp, strat);
-			// Print strategy
-			PrismLog out = new PrismFileLog(exportAdvFilename);
-			out.print("Strat:");
-			for (i = 0; i < n; i++) {
-				out.print(" " + i + ":" + strat[i]);
-			}
-			out.println();
-		}
-
 		// Return results
 		res = new ModelCheckerResult();
 		res.soln = soln;