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

Tidy of conversion to U for F/G checking/simulation. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@699 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
df49f2b833
commit
ffc6437a7e
3 changed files with 1541 additions and 1576 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. 164
      prism/src/prism/NondetModelChecker.java
  2. 178
      prism/src/prism/ProbModelChecker.java
  3. 2775
      prism/src/simulator/SimulatorEngine.java

164
prism/src/prism/NondetModelChecker.java
View File

@ -131,12 +131,11 @@ public class NondetModelChecker extends StateModelChecker
double p = 0; // probability bound (actual value)
String relOp; // relational operator
boolean min; // are we finding min (true) or max (false) probs
PathExpression pe; // path expression
JDDNode sol;
StateProbs probs = null;
// get info from prob operator
// Get info from prob operator
relOp = expr.getRelOp();
pb = expr.getProb();
if (pb != null) {
@ -145,7 +144,7 @@ public class NondetModelChecker extends StateModelChecker
throw new PrismException("Invalid probability bound " + p + " in P operator");
}
// check for trivial (i.e. stupid) cases
// Check for trivial (i.e. stupid) cases
if (pb != null) {
if ((p == 0 && relOp.equals(">=")) || (p == 1 && relOp.equals("<="))) {
mainLog.print("\nWarning: checking for probability " + relOp + " " + p
@ -159,7 +158,7 @@ public class NondetModelChecker extends StateModelChecker
}
}
// determine whether min or max probabilities needed
// Determine whether min or max probabilities needed
if (relOp.equals(">") || relOp.equals(">=") || relOp.equals("min=")) {
// min
min = true;
@ -170,42 +169,11 @@ public class NondetModelChecker extends StateModelChecker
throw new PrismException("Can't use \"P=?\" for MDPs; use \"Pmin=?\" or \"Pmax=?\"");
}
// compute probabilities
pe = expr.getPathExpression();
if (pe instanceof PathExpressionTemporal) {
if (((PathExpressionTemporal) pe).hasBounds()) {
switch (((PathExpressionTemporal) pe).getOperator()) {
case PathExpressionTemporal.P_U:
probs = checkProbBoundedUntil((PathExpressionTemporal) pe, min);
break;
case PathExpressionTemporal.P_F:
probs = checkProbBoundedFuture((PathExpressionTemporal) pe, min);
break;
case PathExpressionTemporal.P_G:
probs = checkProbBoundedGlobal((PathExpressionTemporal) pe, min);
break;
}
} else {
switch (((PathExpressionTemporal) pe).getOperator()) {
case PathExpressionTemporal.P_X:
probs = checkProbNext((PathExpressionTemporal) pe, min);
break;
case PathExpressionTemporal.P_U:
probs = checkProbUntil((PathExpressionTemporal) pe, pb, p, min);
break;
case PathExpressionTemporal.P_F:
probs = checkProbFuture((PathExpressionTemporal) pe, pb, p, min);
break;
case PathExpressionTemporal.P_G:
probs = checkProbGlobal((PathExpressionTemporal) pe, pb, p, min);
break;
}
}
}
if (probs == null)
throw new PrismException("Unrecognised path operator in P operator");
// Compute probabilities
boolean qual = pb != null && ((p == 0) || (p == 1)) && precomp;
probs = checkProbPathExpression(expr.getPathExpression(), qual, min);
// print out probabilities
// Print out probabilities
if (verbose) {
mainLog.print("\n" + (min ? "Minimum" : "Maximum") + " probabilities (non-zero only) for all states:\n");
probs.print(mainLog);
@ -332,6 +300,50 @@ public class NondetModelChecker extends StateModelChecker
}
}
// Contents of a P operator
protected StateProbs checkProbPathExpression(PathExpression pe, boolean qual, boolean min)
throws PrismException
{
StateProbs probs = null;
// Logial operators
if (pe instanceof PathExpressionLogical) {
PathExpressionLogical pel = (PathExpressionLogical) pe;
// Negation
if (pel.getOperator() == PathExpressionLogical.NOT) {
// Flip min/max, then subtract from 1
probs = checkProbPathExpression(pel.getOperand2(), qual, !min);
probs.subtractFromOne();
}
}
// Temporal operators
else if (pe instanceof PathExpressionTemporal) {
PathExpressionTemporal pet = (PathExpressionTemporal) pe;
// Next
if (pet.getOperator() == PathExpressionTemporal.P_X) {
probs = checkProbNext(pet, min);
}
// Until
else if (pet.getOperator() == PathExpressionTemporal.P_U) {
if (pet.hasBounds()) {
probs = checkProbBoundedUntil(pet, min);
} else {
probs = checkProbUntil(pet, qual, min);
}
}
// Anything else - convert to until and recurse
else {
probs = checkProbPathExpression(pet.convertToUntilForm(), qual, min);
}
}
if (probs == null)
throw new PrismException("Unrecognised path operator in P operator");
return probs;
}
// next
protected StateProbs checkProbNext(PathExpressionTemporal pe, boolean min) throws PrismException
@ -423,8 +435,7 @@ public class NondetModelChecker extends StateModelChecker
// until (unbounded)
protected StateProbs checkProbUntil(PathExpressionTemporal pe, Expression pb, double p, boolean min)
throws PrismException
protected StateProbs checkProbUntil(PathExpressionTemporal pe, boolean qual, boolean min) throws PrismException
{
Expression expr1, expr2;
JDDNode b1, b2, splus, newb1, newb2;
@ -486,11 +497,11 @@ public class NondetModelChecker extends StateModelChecker
// allDDRowVars.n()) + " states\n");
}
// if p is 0 or 1 and precomputation algorithms are enabled, compute
// probabilities qualitatively
if (pb != null && ((p == 0) || (p == 1)) && precomp) {
mainLog.print("\nWarning: probability bound in formula is " + p
+ " so exact probabilities may not be computed\n");
// if requested (i.e. when prob bound is 0 or 1 and precomputation algorithms are enabled),
// compute probabilities qualitatively
if (qual) {
mainLog.print("\nWarning: probability bound in formula is"
+ " 0/1 so exact probabilities may not be computed\n");
// for fairness, we compute max here
probs = computeUntilProbsQual(trans01, b1, b2, min && !fairness);
}
@ -520,63 +531,6 @@ public class NondetModelChecker extends StateModelChecker
return probs;
}
// bounded future (eventually)
// F<=k phi == true U<=k phi
protected StateProbs checkProbBoundedFuture(PathExpressionTemporal pe, boolean min) throws PrismException
{
PathExpressionTemporal pe2;
pe2 = new PathExpressionTemporal(PathExpressionTemporal.P_U, new PathExpressionExpr(Expression.True()), pe
.getOperand2(), pe.getLowerBound(), pe.getUpperBound());
return checkProbBoundedUntil(pe2, min);
}
// future (eventually)
// F phi == true U phi
protected StateProbs checkProbFuture(PathExpressionTemporal pe, Expression pb, double p, boolean min)
throws PrismException
{
PathExpressionTemporal pe2;
pe2 = new PathExpressionTemporal(PathExpressionTemporal.P_U, new PathExpressionExpr(Expression.True()), pe
.getOperand2());
return checkProbUntil(pe2, pb, p, min);
}
// bounded global (always)
// F<=k phi == true U<=k phi
// P(G<=k phi) == 1-P(true U<=k !phi)
// Pmin(G<=k phi) == 1-Pmax(true U<=k !phi)
protected StateProbs checkProbBoundedGlobal(PathExpressionTemporal pe, boolean min) throws PrismException
{
PathExpressionTemporal pe2;
StateProbs probs;
pe2 = new PathExpressionTemporal(PathExpressionTemporal.P_U, new PathExpressionExpr(Expression.True()),
new PathExpressionExpr(Expression.Not(((PathExpressionExpr) pe.getOperand2()).getExpression())), pe
.getLowerBound(), pe.getUpperBound());
probs = checkProbBoundedUntil(pe2, !min);
probs.subtractFromOne();
return probs;
}
// global (always)
// G phi == !(true U !phi)
// P(G phi) == 1-P(true U !phi)
// Pmin(G phi) == 1-Pmax(true U !phi)
protected StateProbs checkProbGlobal(PathExpressionTemporal pe, Expression pb, double p, boolean min)
throws PrismException
{
PathExpressionTemporal pe2;
StateProbs probs;
pe2 = new PathExpressionTemporal(PathExpressionTemporal.P_U, new PathExpressionExpr(Expression.True()),
new PathExpressionExpr(Expression.Not(((PathExpressionExpr) pe.getOperand2()).getExpression())));
probs = checkProbUntil(pe2, pb, p, !min);
probs.subtractFromOne();
return probs;
}
// inst reward
protected StateProbs checkRewardInst(PathExpressionTemporal pe, JDDNode stateRewards, JDDNode transRewards,
@ -665,8 +619,8 @@ public class NondetModelChecker extends StateModelChecker
// compute probabilities for bounded until
protected StateProbs computeBoundedUntilProbs(JDDNode tr, JDDNode tr01, JDDNode b1, JDDNode b2, int time, boolean min)
throws PrismException
protected StateProbs computeBoundedUntilProbs(JDDNode tr, JDDNode tr01, JDDNode b1, JDDNode b2, int time,
boolean min) throws PrismException
{
JDDNode yes, no, maybe;
JDDNode probsMTBDD;

178
prism/src/prism/ProbModelChecker.java
View File

@ -140,12 +140,11 @@ public class ProbModelChecker extends StateModelChecker
Expression pb; // probability bound (expression)
double p = 0; // probability bound (actual value)
String relOp; // relational operator
PathExpression pe; // path expression
JDDNode sol;
StateProbs probs = null;
// get info from prob operator
// Get info from prob operator
relOp = expr.getRelOp();
pb = expr.getProb();
if (pb != null) {
@ -154,7 +153,7 @@ public class ProbModelChecker extends StateModelChecker
throw new PrismException("Invalid probability bound " + p + " in P operator");
}
// check for trivial (i.e. stupid) cases
// Check for trivial (i.e. stupid) cases
if (pb != null) {
if ((p == 0 && relOp.equals(">=")) || (p == 1 && relOp.equals("<="))) {
mainLog.print("\nWarning: checking for probability " + relOp + " " + p
@ -168,47 +167,16 @@ public class ProbModelChecker extends StateModelChecker
}
}
// print a warning if Pmin/Pmax used
// Print a warning if Pmin/Pmax used
if (relOp.equals("min=") || relOp.equals("max=")) {
mainLog.print("\nWarning: \"Pmin=?\" and \"Pmax=?\" operators are identical to \"P=?\" for DTMCs\n");
}
// compute probabilities
pe = expr.getPathExpression();
if (pe instanceof PathExpressionTemporal) {
if (((PathExpressionTemporal) pe).hasBounds()) {
switch (((PathExpressionTemporal) pe).getOperator()) {
case PathExpressionTemporal.P_U:
probs = checkProbBoundedUntil((PathExpressionTemporal) pe);
break;
case PathExpressionTemporal.P_F:
probs = checkProbBoundedFuture((PathExpressionTemporal) pe);
break;
case PathExpressionTemporal.P_G:
probs = checkProbBoundedGlobal((PathExpressionTemporal) pe);
break;
}
} else {
switch (((PathExpressionTemporal) pe).getOperator()) {
case PathExpressionTemporal.P_X:
probs = checkProbNext((PathExpressionTemporal) pe);
break;
case PathExpressionTemporal.P_U:
probs = checkProbUntil((PathExpressionTemporal) pe, pb, p);
break;
case PathExpressionTemporal.P_F:
probs = checkProbFuture((PathExpressionTemporal) pe, pb, p);
break;
case PathExpressionTemporal.P_G:
probs = checkProbGlobal((PathExpressionTemporal) pe, pb, p);
break;
}
}
}
if (probs == null)
throw new PrismException("Unrecognised path operator in P operator");
// Compute probabilities
boolean qual = pb != null && ((p == 0) || (p == 1)) && precomp;
probs = checkProbPathExpression(expr.getPathExpression(), qual);
// print out probabilities
// Print out probabilities
if (prism.getVerbose()) {
mainLog.print("\nProbabilities (non-zero only) for all states:\n");
probs.print(mainLog);
@ -534,6 +502,49 @@ public class ProbModelChecker extends StateModelChecker
}
}
// Contents of a P operator
protected StateProbs checkProbPathExpression(PathExpression pe, boolean qual) throws PrismException
{
StateProbs probs = null;
// Logial operators
if (pe instanceof PathExpressionLogical) {
PathExpressionLogical pel = (PathExpressionLogical) pe;
// Negation
if (pel.getOperator() == PathExpressionLogical.NOT) {
// Compute, then subtract from 1
probs = checkProbPathExpression(pel.getOperand2(), qual);
probs.subtractFromOne();
}
}
// Temporal operators
else if (pe instanceof PathExpressionTemporal) {
PathExpressionTemporal pet = (PathExpressionTemporal) pe;
// Next
if (pet.getOperator() == PathExpressionTemporal.P_X) {
probs = checkProbNext(pet);
}
// Until
else if (pet.getOperator() == PathExpressionTemporal.P_U) {
if (pet.hasBounds()) {
probs = checkProbBoundedUntil(pet);
} else {
probs = checkProbUntil(pet, qual);
}
}
// Anything else - convert to until and recurse
else {
probs = checkProbPathExpression(pet.convertToUntilForm(), qual);
}
}
if (probs == null)
throw new PrismException("Unrecognised path operator in P operator");
return probs;
}
// next
protected StateProbs checkProbNext(PathExpressionTemporal pe) throws PrismException
@ -625,7 +636,7 @@ public class ProbModelChecker extends StateModelChecker
// until (unbounded)
protected StateProbs checkProbUntil(PathExpressionTemporal pe, Expression pb, double p) throws PrismException
protected StateProbs checkProbUntil(PathExpressionTemporal pe, boolean qual) throws PrismException
{
Expression expr1, expr2;
JDDNode b1, b2;
@ -654,12 +665,12 @@ public class ProbModelChecker extends StateModelChecker
// compute probabilities
// if prob bound is 0 or 1 and precomputation algorithms are enabled,
// if requested (i.e. when prob bound is 0 or 1 and precomputation algorithms are enabled),
// compute probabilities qualitatively
if (pb != null && ((p == 0) || (p == 1)) && precomp) {
mainLog.print("\nWarning: Probability bound in formula is " + p
+ " so exact probabilities may not be computed\n");
probs = computeUntilProbsQual(trans01, b1, b2, p);
if (qual) {
mainLog.print("\nWarning: probability bound in formula is"
+ " 0/1 so exact probabilities may not be computed\n");
probs = computeUntilProbsQual(trans01, b1, b2);
}
// otherwise actually compute probabilities
else {
@ -679,59 +690,6 @@ public class ProbModelChecker extends StateModelChecker
return probs;
}
// bounded future (eventually)
// F<=k phi == true U<=k phi
protected StateProbs checkProbBoundedFuture(PathExpressionTemporal pe) throws PrismException
{
PathExpressionTemporal pe2;
pe2 = new PathExpressionTemporal(PathExpressionTemporal.P_U, new PathExpressionExpr(Expression.True()), pe
.getOperand2(), pe.getLowerBound(), pe.getUpperBound());
return checkProbBoundedUntil(pe2);
}
// future (eventually)
// F phi == true U phi
protected StateProbs checkProbFuture(PathExpressionTemporal pe, Expression pb, double p) throws PrismException
{
PathExpressionTemporal pe2;
pe2 = new PathExpressionTemporal(PathExpressionTemporal.P_U, new PathExpressionExpr(Expression.True()), pe
.getOperand2());
return checkProbUntil(pe2, pb, p);
}
// bounded global (always)
// F<=k phi == true U<=k phi
// P(G<=k phi) == 1-P(true U<=k !phi)
protected StateProbs checkProbBoundedGlobal(PathExpressionTemporal pe) throws PrismException
{
PathExpressionTemporal pe2;
StateProbs probs;
pe2 = new PathExpressionTemporal(PathExpressionTemporal.P_U, new PathExpressionExpr(Expression.True()),
new PathExpressionExpr(Expression.Not(((PathExpressionExpr) pe.getOperand2()).getExpression())), pe
.getLowerBound(), pe.getUpperBound());
probs = checkProbBoundedUntil(pe2);
probs.subtractFromOne();
return probs;
}
// global (always)
// G phi == !(true U !phi)
// P(G phi) == 1-P(true U !phi)
protected StateProbs checkProbGlobal(PathExpressionTemporal pe, Expression pb, double p) throws PrismException
{
PathExpressionTemporal pe2;
StateProbs probs;
pe2 = new PathExpressionTemporal(PathExpressionTemporal.P_U, new PathExpressionExpr(Expression.True()),
new PathExpressionExpr(Expression.Not(((PathExpressionExpr) pe.getOperand2()).getExpression())));
probs = checkProbUntil(pe2, pb, p);
probs.subtractFromOne();
return probs;
}
// cumulative reward
protected StateProbs checkRewardCumul(PathExpressionTemporal pe, JDDNode stateRewards, JDDNode transRewards)
@ -1258,7 +1216,7 @@ public class ProbModelChecker extends StateModelChecker
// compute probabilities for until (for qualitative properties)
protected StateProbs computeUntilProbsQual(JDDNode tr01, JDDNode b1, JDDNode b2, double p)
protected StateProbs computeUntilProbsQual(JDDNode tr01, JDDNode b1, JDDNode b2)
{
JDDNode yes, no, maybe;
StateProbs probs = null;
@ -1304,20 +1262,18 @@ public class ProbModelChecker extends StateModelChecker
JDD.Ref(yes);
probs = new StateProbsMTBDD(yes, model);
}
// p = 0
else if (p == 0) {
// anything that's unknown but definitely > 0
// may as well be 1
JDD.Ref(yes);
JDD.Ref(maybe);
probs = new StateProbsMTBDD(JDD.Or(yes, maybe), model);
}
// p = 1
// otherwise we set the probabilities for maybe states to be 0.5
// (actual probabilities for these states are unknown but definitely >0
// and <1)
// (this is safe because the results of this function will only be used
// to compare against 0/1 bounds)
// (this is not entirely elegant but is simpler and less error prone
// than
// trying to work out whether to use 0/1 for all case of future/global, etc.)
else {
// anything that's unknown but definitely < 1
// may as well be 0
JDD.Ref(yes);
probs = new StateProbsMTBDD(yes, model);
JDD.Ref(maybe);
probs = new StateProbsMTBDD(JDD.Apply(JDD.PLUS, yes, JDD.Apply(JDD.TIMES, maybe, JDD.Constant(0.5))), model);
}
// derefs

2775
prism/src/simulator/SimulatorEngine.java
File diff suppressed because it is too large
View File

Write Preview
Loading…
Cancel
Save