s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Improvements to strategy generation for MDP reachability in explicit engine, notably algorithms for precomputation. Also split Prob1 into Prob1A and Prob1E for efficiency reasons. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6907 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
d30e52c2a4
commit
8b6d5d17a8
4 changed files with 264 additions and 42 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 33
      prism/src/explicit/MDP.java
  2. 123
      prism/src/explicit/MDPModelChecker.java
  3. 55
      prism/src/explicit/MDPSimple.java
  4. 95
      prism/src/explicit/MDPSparse.java

33
prism/src/explicit/MDP.java
View File

@ -64,6 +64,15 @@ public interface MDP extends Model
*/
public Iterator<Entry<Integer, Double>> 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,

123
prism/src/explicit/MDPModelChecker.java
View File

@ -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;

55
prism/src/explicit/MDPSimple.java
View File

@ -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)
{

95
prism/src/explicit/MDPSparse.java
View File

@ -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)
{

Write Preview
Loading…
Cancel
Save