Add strategy generation to MDP Gauss-Seidel (explicit).

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

prism/src/explicit/MDP.java

@@ -136,23 +136,27 @@ public interface MDP extends Model
 	 * and store new values directly in {@code vect} as computed.
 	 * The maximum (absolute/relative) difference between old/new
 	 * elements of {@code vect} is also returned.
+	 * Optionally, store optimal (memoryless) strategy info. 
 	 * @param vect Vector to multiply by (and store the result in)
 	 * @param min Min or max for (true=min, false=max)
 	 * @param subset Only do multiplication for these rows (ignored if null)
 	 * @param complement If true, {@code subset} is taken to be its complement (ignored if {@code subset} is null)
 	 * @param absolute If true, compute absolute, rather than relative, difference
+	 * @param strat Storage for (memoryless) strategy choice indices (ignored if null)
 	 * @return The maximum difference between old/new elements of {@code vect}
 	 */
-	public double mvMultGSMinMax(double vect[], boolean min, BitSet subset, boolean complement, boolean absolute);
+	public double mvMultGSMinMax(double vect[], boolean min, BitSet subset, boolean complement, boolean absolute, int strat[]);
 
 	/**
 	 * Do a single row of Jacobi-style matrix-vector multiplication followed by min/max.
 	 * i.e. return min/max_k { (sum_{j!=s} P_k(s,j)*vect[j]) / P_k(s,s) }
+	 * Optionally, store optimal (memoryless) strategy info. 
 	 * @param s Row index
 	 * @param vect Vector to multiply by
 	 * @param min Min or max for (true=min, false=max)
+	 * @param strat Storage for (memoryless) strategy choice indices (ignored if null)
 	 */
-	public double mvMultJacMinMaxSingle(int s, double vect[], boolean min);
+	public double mvMultJacMinMaxSingle(int s, double vect[], boolean min, int strat[]);
 
 	/**
 	 * Do a single row of Jacobi-style matrix-vector multiplication for a specific choice.

prism/src/explicit/MDPExplicit.java

@@ -244,28 +244,28 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP
 	}
 
 	@Override
-	public double mvMultGSMinMax(double vect[], boolean min, BitSet subset, boolean complement, boolean absolute)
+	public double mvMultGSMinMax(double vect[], boolean min, BitSet subset, boolean complement, boolean absolute, int strat[])
 	{
 		int s;
 		double d, diff, maxDiff = 0.0;
 		// Loop depends on subset/complement arguments
 		if (subset == null) {
 			for (s = 0; s < numStates; s++) {
-				d = mvMultJacMinMaxSingle(s, vect, min);
+				d = mvMultJacMinMaxSingle(s, vect, min, strat);
 				diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d);
 				maxDiff = diff > maxDiff ? diff : maxDiff;
 				vect[s] = d;
 			}
 		} else if (complement) {
 			for (s = subset.nextClearBit(0); s < numStates; s = subset.nextClearBit(s + 1)) {
-				d = mvMultJacMinMaxSingle(s, vect, min);
+				d = mvMultJacMinMaxSingle(s, vect, min, strat);
 				diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d);
 				maxDiff = diff > maxDiff ? diff : maxDiff;
 				vect[s] = d;
 			}
 		} else {
 			for (s = subset.nextSetBit(0); s >= 0; s = subset.nextSetBit(s + 1)) {
-				d = mvMultJacMinMaxSingle(s, vect, min);
+				d = mvMultJacMinMaxSingle(s, vect, min, strat);
 				diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d);
 				maxDiff = diff > maxDiff ? diff : maxDiff;
 				vect[s] = d;
@@ -274,7 +274,7 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP
 		// Use this code instead for backwards Gauss-Seidel
 		/*for (s = numStates - 1; s >= 0; s--) {
 			if (subset.get(s)) {
-				d = mvMultJacMinMaxSingle(s, vect, min);
+				d = mvMultJacMinMaxSingle(s, vect, min, strat);
 				diff = absolute ? (Math.abs(d - vect[s])) : (Math.abs(d - vect[s]) / d);
 				maxDiff = diff > maxDiff ? diff : maxDiff;
 				vect[s] = d;

prism/src/explicit/MDPModelChecker.java

@@ -745,7 +745,7 @@ public class MDPModelChecker extends ProbModelChecker
 		while (!done && iters < maxIters) {
 			iters++;
 			// Matrix-vector multiply
-			maxDiff = mdp.mvMultGSMinMax(soln, min, unknown, false, termCrit == TermCrit.ABSOLUTE);
+			maxDiff = mdp.mvMultGSMinMax(soln, min, unknown, false, termCrit == TermCrit.ABSOLUTE, strat);
 			// Check termination
 			done = maxDiff < termCritParam;
 		}
@@ -762,6 +762,19 @@ 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;

prism/src/explicit/MDPSimple.java

@@ -702,13 +702,14 @@ public class MDPSimple extends MDPExplicit implements ModelSimple
 	}
 
 	@Override
-	public double mvMultJacMinMaxSingle(int s, double vect[], boolean min)
+	public double mvMultJacMinMaxSingle(int s, double vect[], boolean min, int strat[])
 	{
-		int k;
+		int j, k, stratCh = -1;
 		double diag, d, prob, minmax;
 		boolean first;
 		List<Distribution> step;
 
+		j = 0;
 		minmax = 0;
 		first = true;
 		step = trans.get(s);
@@ -728,9 +729,24 @@ public class MDPSimple extends MDPExplicit implements ModelSimple
 			if (diag > 0)
 				d /= diag;
 			// Check whether we have exceeded min/max so far
-			if (first || (min && d < minmax) || (!min && d > minmax))
+			if (first || (min && d < minmax) || (!min && d > minmax)) {
 				minmax = d;
+				// If strategy generation is enabled, remember optimal choice
+				if (strat != null) {
+					stratCh = j;
+				}
+			}
 			first = false;
+			j++;
+		}
+		// If strategy generation is enabled, store optimal choice
+		if (strat != null & !first) {
+			// For max, only remember strictly better choices
+			if (min) {
+				strat[s] = stratCh;
+			} else if (strat[s] == -1 || minmax > vect[s]) {
+				strat[s] = stratCh;
+			}
 		}
 
 		return minmax;

prism/src/explicit/MDPSparse.java

@@ -730,9 +730,9 @@ public class MDPSparse extends MDPExplicit
 	}
 
 	@Override
-	public double mvMultJacMinMaxSingle(int s, double vect[], boolean min)
+	public double mvMultJacMinMaxSingle(int s, double vect[], boolean min, int strat[])
 	{
-		int j, k, l1, h1, l2, h2;
+		int j, k, l1, h1, l2, h2, stratCh = -1;
 		double diag, d, minmax;
 		boolean first;
 
@@ -756,10 +756,23 @@ public class MDPSparse extends MDPExplicit
 			if (diag > 0)
 				d /= diag;
 			// Check whether we have exceeded min/max so far
-			if (first || (min && d < minmax) || (!min && d > minmax))
+			if (first || (min && d < minmax) || (!min && d > minmax)) {
 				minmax = d;
+				// If strategy generation is enabled, remember optimal choice
+				if (strat != null)
+					stratCh = j - l1;
+			}
 			first = false;
 		}
+		// If strategy generation is enabled, store optimal choice
+		if (strat != null & !first) {
+			// For max, only remember strictly better choices
+			if (min) {
+				strat[s] = stratCh;
+			} else if (strat[s] == -1 || minmax > vect[s]) {
+				strat[s] = stratCh;
+			}
+		}
 
 		return minmax;
 	}