diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index 45bcb262..c80b590d 100644 --- a/prism/src/explicit/MDP.java +++ b/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. diff --git a/prism/src/explicit/MDPExplicit.java b/prism/src/explicit/MDPExplicit.java index 33211f66..22b2a696 100644 --- a/prism/src/explicit/MDPExplicit.java +++ b/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; diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index c332fc91..17b13cad 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/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; diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index de3d8667..11649f3c 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/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 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; diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index 315ae1cd..8b907640 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/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; }