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

update checkProbBoundedUntil() in the model checkers to handle lower bounds as well. [Joachim Klein] 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9572 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
e77138a79f
commit
5dc15ad61b
3 changed files with 159 additions and 52 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. 91
      prism/src/explicit/ProbModelChecker.java
  2. 49
      prism/src/prism/NondetModelChecker.java
  3. 49
      prism/src/prism/ProbModelChecker.java

91
prism/src/explicit/ProbModelChecker.java
View File

@ -38,6 +38,7 @@ import parser.ast.ExpressionTemporal;
import parser.ast.ExpressionUnaryOp;
import parser.ast.RewardStruct;
import parser.type.TypeDouble;
import prism.IntegerBound;
import prism.OpRelOpBound;
import prism.PrismComponent;
import prism.PrismException;
@ -652,39 +653,99 @@ public class ProbModelChecker extends NonProbModelChecker
// Continuous-time model checkers will override this method
// Get info from bounded until
int time = expr.getUpperBound().evaluateInt(constantValues);
if (expr.upperBoundIsStrict())
time--;
if (time < 0) {
String bound = expr.upperBoundIsStrict() ? "<" + (time + 1) : "<=" + time;
throw new PrismException("Invalid bound " + bound + " in bounded until formula");
}
Integer lowerBound;
IntegerBound bounds;
int i;
// get and check bounds information
bounds = IntegerBound.fromExpressionTemporal(expr, constantValues, true);
// Model check operands for all states
BitSet remain = checkExpression(model, expr.getOperand1(), null).getBitSet();
BitSet target = checkExpression(model, expr.getOperand2(), null).getBitSet();
// Compute/return the probabilities
// A trivial case: "U<=0" (prob is 1 in target states, 0 otherwise)
if (time == 0) {
return StateValues.createFromBitSetAsDoubles(target, model);
if (bounds.hasLowerBound()) {
lowerBound = bounds.getLowestInteger();
} else {
lowerBound = 0;
}
Integer windowSize = null; // unbounded
if (bounds.hasUpperBound()) {
windowSize = bounds.getHighestInteger() - lowerBound;
}
// compute probabilities for Until<=windowSize
StateValues sv = null;
if (windowSize == null) {
// unbounded
ModelCheckerResult res = null;
switch (model.getModelType()) {
case DTMC:
res = ((DTMCModelChecker) this).computeUntilProbs((DTMC) model, remain, target);
break;
case MDP:
res = ((MDPModelChecker) this).computeUntilProbs((MDP) model, remain, target, minMax.isMin());
break;
case STPG:
res = ((STPGModelChecker) this).computeUntilProbs((STPG) model, remain, target, minMax.isMin1(), minMax.isMin2());
break;
default:
throw new PrismException("Cannot model check " + expr + " for " + model.getModelType() + "s");
}
sv = StateValues.createFromDoubleArray(res.soln, model);
} else if (windowSize == 0) {
// A trivial case: windowSize=0 (prob is 1 in target states, 0 otherwise)
sv = StateValues.createFromBitSetAsDoubles(target, model);
} else {
// Otherwise: numerical solution
ModelCheckerResult res = null;
switch (model.getModelType()) {
case DTMC:
res = ((DTMCModelChecker) this).computeBoundedUntilProbs((DTMC) model, remain, target, time);
res = ((DTMCModelChecker) this).computeBoundedUntilProbs((DTMC) model, remain, target, windowSize);
break;
case MDP:
res = ((MDPModelChecker) this).computeBoundedUntilProbs((MDP) model, remain, target, time, minMax.isMin());
res = ((MDPModelChecker) this).computeBoundedUntilProbs((MDP) model, remain, target, windowSize, minMax.isMin());
break;
case STPG:
res = ((STPGModelChecker) this).computeBoundedUntilProbs((STPG) model, remain, target, time, minMax.isMin1(), minMax.isMin2());
res = ((STPGModelChecker) this).computeBoundedUntilProbs((STPG) model, remain, target, windowSize, minMax.isMin1(), minMax.isMin2());
break;
default:
throw new PrismException("Cannot model check " + expr + " for " + model.getModelType() + "s");
}
return StateValues.createFromDoubleArray(res.soln, model);
sv = StateValues.createFromDoubleArray(res.soln, model);
}
// perform lowerBound restricted next-step computations to
// deal with lower bound.
if (lowerBound > 0) {
double[] probs = sv.getDoubleArray();
for (i = 0; i < lowerBound; i++) {
switch (model.getModelType()) {
case DTMC:
probs = ((DTMCModelChecker) this).computeRestrictedNext((DTMC) model, remain, probs);
break;
case MDP:
probs = ((MDPModelChecker) this).computeRestrictedNext((MDP) model, remain, probs, minMax.isMin());
break;
case STPG:
// TODO (JK): Figure out if we can handle lower bounds for STPG in the same way
throw new PrismException("Lower bounds not yet supported for STPGModelChecker");
default:
throw new PrismException("Cannot model check " + expr + " for " + model.getModelType() + "s");
}
}
sv = StateValues.createFromDoubleArray(probs, model);
}
return sv;
}
/**

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

@ -739,18 +739,14 @@ public class NondetModelChecker extends NonProbModelChecker
*/
protected StateValues checkProbBoundedUntil(ExpressionTemporal expr, boolean min) throws PrismException
{
int time;
JDDNode b1, b2;
StateValues probs = null;
Integer lowerBound;
IntegerBound bounds;
int i;
// get info from bounded until
time = expr.getUpperBound().evaluateInt(constantValues);
if (expr.upperBoundIsStrict())
time--;
if (time < 0) {
String bound = expr.upperBoundIsStrict() ? "<" + (time + 1) : "<=" + time;
throw new PrismException("Invalid bound " + bound + " in bounded until formula");
}
// get and check bounds information
bounds = IntegerBound.fromExpressionTemporal(expr, constantValues, true);
// model check operands first
b1 = checkExpressionDD(expr.getOperand1());
@ -767,16 +763,35 @@ public class NondetModelChecker extends NonProbModelChecker
// mainLog.print(" states, b2 = " + JDD.GetNumMintermsString(b2,
// allDDRowVars.n()) + " states\n");
// compute probabilities
if (bounds.hasLowerBound()) {
lowerBound = bounds.getLowestInteger();
} else {
lowerBound = 0;
}
// a trivial case: "U<=0"
if (time == 0) {
Integer windowSize = null; // unbounded
if (bounds.hasUpperBound()) {
windowSize = bounds.getHighestInteger() - lowerBound;
}
// compute probabilities for Until<=windowSize
if (windowSize == null) {
// unbounded
try {
probs = checkProbUntil(b1, b2, false, min);
} catch (PrismException e) {
JDD.Deref(b1);
JDD.Deref(b2);
throw e;
}
} else if (windowSize == 0) {
// the trivial case: windowSize = 0
// prob is 1 in b2 states, 0 otherwise
JDD.Ref(b2);
probs = new StateValuesMTBDD(b2, model);
} else {
try {
probs = computeBoundedUntilProbs(trans, trans01, b1, b2, time, min);
probs = computeBoundedUntilProbs(trans, trans01, b1, b2, windowSize, min);
} catch (PrismException e) {
JDD.Deref(b1);
JDD.Deref(b2);
@ -784,6 +799,14 @@ public class NondetModelChecker extends NonProbModelChecker
}
}
// perform lowerBound restricted next-step computations to
// deal with lower bound.
if (lowerBound > 0) {
for (i = 0; i < lowerBound; i++) {
probs = computeRestrictedNext(trans, b1, probs, min);
}
}
// derefs
JDD.Deref(b1);
JDD.Deref(b2);

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

@ -618,18 +618,14 @@ public class ProbModelChecker extends NonProbModelChecker
protected StateValues checkProbBoundedUntil(ExpressionTemporal expr) throws PrismException
{
int time;
JDDNode b1, b2;
StateValues probs = null;
Integer lowerBound;
IntegerBound bounds;
int i;
// get info from bounded until
time = expr.getUpperBound().evaluateInt(constantValues);
if (expr.upperBoundIsStrict())
time--;
if (time < 0) {
String bound = expr.upperBoundIsStrict() ? "<" + (time + 1) : "<=" + time;
throw new PrismException("Invalid bound " + bound + " in bounded until formula");
}
// get and check bounds information
bounds = IntegerBound.fromExpressionTemporal(expr, constantValues, true);
// model check operands first
b1 = checkExpressionDD(expr.getOperand1());
@ -646,16 +642,35 @@ public class ProbModelChecker extends NonProbModelChecker
// mainLog.print(" states, b2 = " + JDD.GetNumMintermsString(b2,
// allDDRowVars.n()) + " states\n");
// compute probabilities
if (bounds.hasLowerBound()) {
lowerBound = bounds.getLowestInteger();
} else {
lowerBound = 0;
}
// a trivial case: "U<=0"
if (time == 0) {
Integer windowSize = null; // unbounded
if (bounds.hasUpperBound()) {
windowSize = bounds.getHighestInteger() - lowerBound;
}
// compute probabilities for Until<=windowSize
if (windowSize == null) {
// unbounded
try {
probs = computeUntilProbs(trans, trans01, b1, b2);
} catch (PrismException e) {
JDD.Deref(b1);
JDD.Deref(b2);
throw e;
}
} else if (windowSize == 0) {
// the trivial case: windowSize = 0
// prob is 1 in b2 states, 0 otherwise
JDD.Ref(b2);
probs = new StateValuesMTBDD(b2, model);
} else {
try {
probs = computeBoundedUntilProbs(trans, trans01, b1, b2, time);
probs = computeBoundedUntilProbs(trans, trans01, b1, b2, windowSize);
} catch (PrismException e) {
JDD.Deref(b1);
JDD.Deref(b2);
@ -663,6 +678,14 @@ public class ProbModelChecker extends NonProbModelChecker
}
}
// perform lowerBound restricted next-step computations to
// deal with lower bound.
if (lowerBound > 0) {
for (i = 0; i < lowerBound; i++) {
probs = computeRestrictedNext(trans, b1, probs);
}
}
// derefs
JDD.Deref(b1);
JDD.Deref(b2);

Write Preview
Loading…
Cancel
Save