diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index c80b590d..13254d3e 100644 --- a/prism/src/explicit/MDP.java +++ b/prism/src/explicit/MDP.java @@ -64,6 +64,15 @@ public interface MDP extends Model */ public Iterator> getTransitionsIterator(int s, int i); + /** + * Check if all the successor states from choice {@code i} of state {@code s} are in the set {@code set}. + * Get an iterator over the transitions . + * @param s The state to check + * @param i Choice index + * @param set The set to test for inclusion + */ + public boolean allSuccessorsInSet(int s, int i, BitSet set); + /** * Perform a single step of precomputation algorithm Prob0, i.e., for states i in {@code subset}, * set bit i of {@code result} iff, for all/some choices, @@ -76,6 +85,30 @@ public interface MDP extends Model */ public void prob0step(BitSet subset, BitSet u, boolean forall, BitSet result); + /** + * Perform a single step of precomputation algorithm Prob1A, i.e., for states i in {@code subset}, + * set bit i of {@code result} iff, for all choices, + * there is a transition to a state in {@code v} and all transitions go to states in {@code u}. + * @param subset Only compute for these states + * @param u Set of states {@code u} + * @param v Set of states {@code v} + * @param result Store results here + */ + public void prob1Astep(BitSet subset, BitSet u, BitSet v, BitSet result); + + /** + * Perform a single step of precomputation algorithm Prob1E, i.e., for states i in {@code subset}, + * set bit i of {@code result} iff, for some choice, + * there is a transition to a state in {@code v} and all transitions go to states in {@code u}. + * Optionally, store optimal (memoryless) strategy info. + * @param subset Only compute for these states + * @param u Set of states {@code u} + * @param v Set of states {@code v} + * @param result Store results here + * @param strat Storage for (memoryless) strategy choice indices (ignored if null) + */ + public void prob1Estep(BitSet subset, BitSet u, BitSet v, BitSet result, int strat[]); + /** * Perform a single step of precomputation algorithm Prob1, i.e., for states i in {@code subset}, * set bit i of {@code result} iff, for all/some choices, diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 17b13cad..f42e5374 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -318,9 +318,10 @@ public class MDPModelChecker extends ProbModelChecker public ModelCheckerResult computeReachProbs(MDP mdp, BitSet remain, BitSet target, boolean min, double init[], BitSet known) throws PrismException { ModelCheckerResult res = null; - BitSet no, yes; + BitSet targetOrig, no, yes; int i, n, numYes, numNo; long timer, timerProb0, timerProb1; + int strat[] = null; boolean genStrat; // Local copy of setting MDPSolnMethod mdpSolnMethod = this.mdpSolnMethod; @@ -352,26 +353,35 @@ public class MDPModelChecker extends ProbModelChecker // Store num states n = mdp.getNumStates(); + // If required, create/initialise strategy storage + // Set all choices to -1, denoting unknown/arbitrary + if (genStrat) { + strat = new int[n]; + for (i = 0; i < n; i++) { + strat[i] = -1; + } + } + // Optimise by enlarging target set (if more info is available) + targetOrig = target; if (init != null && known != null) { - BitSet targetNew = new BitSet(n); + target = new BitSet(n); for (i = 0; i < n; i++) { - targetNew.set(i, target.get(i) || (known.get(i) && init[i] == 1.0)); + target.set(i, targetOrig.get(i) || (known.get(i) && init[i] == 1.0)); } - target = targetNew; } // Precomputation timerProb0 = System.currentTimeMillis(); if (precomp && prob0) { - no = prob0(mdp, remain, target, min); + no = prob0(mdp, remain, target, min, strat); } else { no = new BitSet(); } timerProb0 = System.currentTimeMillis() - timerProb0; timerProb1 = System.currentTimeMillis(); - if (precomp && prob1 && !genStrat) { - yes = prob1(mdp, remain, target, min); + if (precomp && prob1) { + yes = prob1(mdp, remain, target, min, strat); } else { yes = (BitSet) target.clone(); } @@ -382,10 +392,26 @@ public class MDPModelChecker extends ProbModelChecker numNo = no.cardinality(); mainLog.println("target=" + target.cardinality() + ", yes=" + numYes + ", no=" + numNo + ", maybe=" + (n - (numYes + numNo))); + // If still required, generate strategy for no/yes (0/1) states. + // This is not just for the cases max=0 and min=1, where arbitrary choices suffice. + // So just pick the first choice (0) for all these. + if (genStrat) { + if (min) { + for (i = yes.nextSetBit(0); i >= 0; i = yes.nextSetBit(i + 1)) { + if (!target.get(i)) + strat[i] = 0; + } + } else { + for (i = no.nextSetBit(0); i >= 0; i = no.nextSetBit(i + 1)) { + strat[i] = 0; + } + } + } + // Compute probabilities switch (mdpSolnMethod) { case VALUE_ITERATION: - res = computeReachProbsValIter(mdp, no, yes, min, init, known); + res = computeReachProbsValIter(mdp, no, yes, min, init, known, strat); break; case GAUSS_SEIDEL: res = computeReachProbsGaussSeidel(mdp, no, yes, min, init, known); @@ -404,6 +430,20 @@ public class MDPModelChecker extends ProbModelChecker timer = System.currentTimeMillis() - timer; mainLog.println("Probabilistic reachability took " + timer / 1000.0 + " seconds."); + // 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(); + new DTMCFromMDPMemorylessAdversary(mdp, strat).exportToPrismExplicitTra(out); + } + // Update time taken res.timeTaken = timer / 1000.0; res.timeProb0 = timerProb0 / 1000.0; @@ -417,12 +457,14 @@ 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. * @param mdp The MDP * @param remain Remain in these states (optional: null means "all") * @param target Target states * @param min Min or max probabilities (true=min, false=max) + * @param strat Storage for (memoryless) strategy choice indices (ignored if null) */ - public BitSet prob0(MDP mdp, BitSet remain, BitSet target, boolean min) + public BitSet prob0(MDP mdp, BitSet remain, BitSet target, boolean min, int strat[]) { int n, iters; BitSet u, soln, unknown; @@ -478,6 +520,21 @@ public class MDPModelChecker extends ProbModelChecker mainLog.print("Prob0 (" + (min ? "min" : "max") + ")"); mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds."); + // If required, generate strategy. This is for min probs, + // so it can be done *after* the main prob0 algorithm (unlike for prob1). + // We simply pick, for all "no" states, the first choice for which all transitions stay in "no" + if (strat != null) { + for (int i = u.nextSetBit(0); i >= 0; i = u.nextSetBit(i + 1)) { + int numChoices = mdp.getNumChoices(i); + for (int k = 0; k < numChoices; k++) { + if (mdp.allSuccessorsInSet(i, k, u)) { + strat[i] = k; + continue; + } + } + } + } + return u; } @@ -486,12 +543,14 @@ public class MDPModelChecker extends ProbModelChecker * i.e. determine the states of an MDP which, with min/max probability 1, * reach a state in {@code target}, while remaining in those in @{code remain}. * {@code min}=true gives Prob1A, {@code min}=false gives Prob1E. + * Optionally, for max only, store optimal (memoryless) strategy info for 1 states. * @param mdp The MDP * @param remain Remain in these states (optional: null means "all") * @param target Target states * @param min Min or max probabilities (true=min, false=max) + * @param strat Storage for (memoryless) strategy choice indices (ignored if null) */ - public BitSet prob1(MDP mdp, BitSet remain, BitSet target, boolean min) + public BitSet prob1(MDP mdp, BitSet remain, BitSet target, boolean min, int strat[]) { int n, iters; BitSet u, v, soln, unknown; @@ -536,7 +595,10 @@ public class MDPModelChecker extends ProbModelChecker while (!v_done) { iters++; // Single step of Prob1 - mdp.prob1step(unknown, u, v, min, soln); + if (min) + mdp.prob1Astep(unknown, u, v, soln); + else + mdp.prob1Estep(unknown, u, v, soln, strat); // Check termination (inner) v_done = soln.equals(v); // v = soln @@ -560,27 +622,25 @@ public class MDPModelChecker extends ProbModelChecker /** * Compute reachability probabilities using value iteration. + * Optionally, store optimal (memoryless) strategy info. * @param mdp The MDP * @param no Probability 0 states * @param yes Probability 1 states * @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 computeReachProbsValIter(MDP mdp, BitSet no, BitSet yes, boolean min, double init[], BitSet known) throws PrismException + protected ModelCheckerResult computeReachProbsValIter(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[], soln2[], tmpsoln[], initVal; - 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 value iteration (" + (min ? "min" : "max") + ")..."); @@ -617,21 +677,13 @@ 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; while (!done && iters < maxIters) { iters++; // Matrix-vector multiply and min/max ops - mdp.mvMultMinMax(soln, min, soln2, unknown, false, genStrat ? strat : null); + mdp.mvMultMinMax(soln, min, soln2, unknown, false, strat); // Check termination done = PrismUtils.doublesAreClose(soln, soln2, termCritParam, termCrit == TermCrit.ABSOLUTE); // Swap vectors for next iter @@ -652,19 +704,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; @@ -797,7 +836,7 @@ public class MDPModelChecker extends ProbModelChecker double soln[], soln2[]; boolean done; long timer; - int strat[]; + int strat[] = null; DTMCModelChecker mcDTMC; DTMC dtmc; @@ -884,7 +923,7 @@ public class MDPModelChecker extends ProbModelChecker double soln[], soln2[]; boolean done; long timer; - int strat[]; + int strat[] = null; DTMCModelChecker mcDTMC; DTMC dtmc; @@ -1149,7 +1188,7 @@ public class MDPModelChecker extends ProbModelChecker // Precomputation (not optional) timerProb1 = System.currentTimeMillis(); - inf = prob1(mdp, null, target, !min); + inf = prob1(mdp, null, target, !min, null); inf.flip(0, n); timerProb1 = System.currentTimeMillis() - timerProb1; diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 11649f3c..f0cf30e5 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -554,6 +554,12 @@ public class MDPSimple extends MDPExplicit implements ModelSimple return trans.get(s).get(i).iterator(); } + @Override + public boolean allSuccessorsInSet(int s, int i, BitSet set) + { + return trans.get(s).get(i).isSubsetOf(set); + } + @Override public void prob0step(BitSet subset, BitSet u, boolean forall, BitSet result) { @@ -581,6 +587,55 @@ public class MDPSimple extends MDPExplicit implements ModelSimple } } + @Override + public void prob1Astep(BitSet subset, BitSet u, BitSet v, BitSet result) + { + int i; + boolean b1; + for (i = 0; i < numStates; i++) { + if (subset.get(i)) { + b1 = true; + for (Distribution distr : trans.get(i)) { + if (!(distr.isSubsetOf(u) && distr.containsOneOf(v))) { + b1 = false; + continue; + } + } + result.set(i, b1); + } + } + } + + @Override + public void prob1Estep(BitSet subset, BitSet u, BitSet v, BitSet result, int strat[]) + { + int i, j, stratCh = -1; + boolean b1; + for (i = 0; i < numStates; i++) { + if (subset.get(i)) { + j = 0; + b1 = false; + for (Distribution distr : trans.get(i)) { + if (distr.isSubsetOf(u) && distr.containsOneOf(v)) { + b1 = true; + // If strategy generation is enabled, remember optimal choice + if (strat != null) + stratCh = j; + continue; + } + j++; + } + // If strategy generation is enabled, store optimal choice + // (only if this the first time we add the state to S^yes) + if (strat != null & b1 & !result.get(i)) { + strat[i] = stratCh; + } + // Store result + result.set(i, b1); + } + } + } + @Override public void prob1step(BitSet subset, BitSet u, BitSet v, boolean forall, BitSet result) { diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index 8b907640..1d7ab854 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -562,6 +562,22 @@ public class MDPSparse extends MDPExplicit }; } + @Override + public boolean allSuccessorsInSet(int s, int i, BitSet set) + { + int j, k, l2, h2; + j = rowStarts[s] + i; + l2 = choiceStarts[j]; + h2 = choiceStarts[j + 1]; + for (k = l2; k < h2; k++) { + // Assume that only non-zero entries are stored + if (!set.get(cols[k])) { + return false; + } + } + return true; + } + @Override public void prob0step(BitSet subset, BitSet u, boolean forall, BitSet result) { @@ -600,6 +616,85 @@ public class MDPSparse extends MDPExplicit } } + @Override + public void prob1Astep(BitSet subset, BitSet u, BitSet v, BitSet result) + { + int i, j, k, l1, h1, l2, h2; + boolean b1, some, all; + for (i = 0; i < numStates; i++) { + if (subset.get(i)) { + b1 = true; + l1 = rowStarts[i]; + h1 = rowStarts[i + 1]; + for (j = l1; j < h1; j++) { + some = false; + all = true; + l2 = choiceStarts[j]; + h2 = choiceStarts[j + 1]; + for (k = l2; k < h2; k++) { + // Assume that only non-zero entries are stored + if (!u.get(cols[k])) { + all = false; + continue; // Stop early (already know b1 will be set to false) + } + if (v.get(cols[k])) { + some = true; + } + } + if (!(some && all)) { + b1 = false; + continue; + } + } + result.set(i, b1); + } + } + } + + @Override + public void prob1Estep(BitSet subset, BitSet u, BitSet v, BitSet result, int strat[]) + { + int i, j, k, l1, h1, l2, h2, stratCh = -1; + boolean b1, some, all; + for (i = 0; i < numStates; i++) { + if (subset.get(i)) { + b1 = false; + l1 = rowStarts[i]; + h1 = rowStarts[i + 1]; + for (j = l1; j < h1; j++) { + some = false; + all = true; + l2 = choiceStarts[j]; + h2 = choiceStarts[j + 1]; + for (k = l2; k < h2; k++) { + // Assume that only non-zero entries are stored + if (!u.get(cols[k])) { + all = false; + continue; // Stop early (already know b1 will not be set to true) + } + if (v.get(cols[k])) { + some = true; + } + } + if (some && all) { + b1 = true; + // If strategy generation is enabled, remember optimal choice + if (strat != null) + stratCh = j - l1; + continue; + } + } + // If strategy generation is enabled, store optimal choice + // (only if this the first time we add the state to S^yes) + if (strat != null & b1 & !result.get(i)) { + strat[i] = stratCh; + } + // Store result + result.set(i, b1); + } + } + } + @Override public void prob1step(BitSet subset, BitSet u, BitSet v, boolean forall, BitSet result) {