diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java
index 69680dc0..95c049f5 100644
--- a/prism/src/prism/LTLModelChecker.java
+++ b/prism/src/prism/LTLModelChecker.java
@@ -104,7 +104,7 @@ public class LTLModelChecker extends PrismComponent
// A state formula
if (expr.getType() instanceof TypeBool) {
// Model check
- JDDNode dd = mc.checkExpressionDD(expr);
+ JDDNode dd = mc.checkExpressionDD(expr, model.getReach().copy());
// Detect special cases (true, false) for optimisation
if (dd.equals(JDD.ZERO)) {
JDD.Deref(dd);
diff --git a/prism/src/prism/ModelChecker.java b/prism/src/prism/ModelChecker.java
index 2f00cf41..f0b202aa 100644
--- a/prism/src/prism/ModelChecker.java
+++ b/prism/src/prism/ModelChecker.java
@@ -34,9 +34,32 @@ import parser.ast.*;
public interface ModelChecker
{
+ /**
+ * Model check an expression, process, print and return the result.
+ */
public Result check(Expression expr) throws PrismException;
- public StateValues checkExpression(Expression expr) throws PrismException;
- public JDDNode checkExpressionDD(Expression expr) throws PrismException;
+
+ /**
+ * Model check an expression and return a vector of result values,
+ * with valid results for at least all states of interest.
+ *
+ * @param expr the expression
+ * @param statesOfInterest the states of interest.
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ public StateValues checkExpression(Expression expr, JDDNode statesOfInterest) throws PrismException;
+
+ /**
+ * Model check expression, convert to symbolic form (if not already), return BDD.
+ *
+ * Will have valid results at least for all states of interest.
+ * @param expr the expression
+ * @param statesOfInterest the states of interest
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ public JDDNode checkExpressionDD(Expression expr, JDDNode statesOfInterest) throws PrismException;
+
+ /** Get the constant values (both from the modules file and the properties file) */
public Values getConstantValues();
}
diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java
index b124d272..6919947c 100644
--- a/prism/src/prism/Modules2MTBDD.java
+++ b/prism/src/prism/Modules2MTBDD.java
@@ -1922,7 +1922,8 @@ public class Modules2MTBDD
private JDDNode translateExpression(Expression e) throws PrismException
{
// pass this work onto the Expression2MTBDD object
- return expr2mtbdd.checkExpressionDD(e);
+ // states of interest = JDD.ONE = true = all possible states
+ return expr2mtbdd.checkExpressionDD(e, JDD.ONE.copy());
}
// build state and transition rewards
diff --git a/prism/src/prism/NonProbModelChecker.java b/prism/src/prism/NonProbModelChecker.java
index d54f403a..9c729d00 100644
--- a/prism/src/prism/NonProbModelChecker.java
+++ b/prism/src/prism/NonProbModelChecker.java
@@ -62,22 +62,22 @@ public class NonProbModelChecker extends StateModelChecker
// -----------------------------------------------------------------------------------
// Check expression (recursive)
-
- public StateValues checkExpression(Expression expr) throws PrismException
+ @Override
+ public StateValues checkExpression(Expression expr, JDDNode statesOfInterest) throws PrismException
{
StateValues res;
// E operator
if (expr instanceof ExpressionExists) {
- res = checkExpressionExists(((ExpressionExists) expr).getExpression());
+ res = checkExpressionExists(((ExpressionExists) expr).getExpression(), statesOfInterest);
}
// A operator
else if (expr instanceof ExpressionForAll) {
- res = checkExpressionForAll(((ExpressionForAll) expr).getExpression());
+ res = checkExpressionForAll(((ExpressionForAll) expr).getExpression(), statesOfInterest);
}
// Otherwise, use the superclass
else {
- res = super.checkExpression(expr);
+ res = super.checkExpression(expr, statesOfInterest);
}
// Filter out non-reachable states from solution
@@ -94,17 +94,21 @@ public class NonProbModelChecker extends StateModelChecker
/**
* Model check a CTL exists (E) operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkExpressionExists(Expression expr) throws PrismException
+ protected StateValues checkExpressionExists(Expression expr, JDDNode statesOfInterest) throws PrismException
{
StateValues res = null;
// Check whether this is a simple path formula (i.e. CTL, not LTL)
if (!expr.isSimplePathFormula()) {
+ JDD.Deref(statesOfInterest);
throw new PrismNotSupportedException("(Non-probabilistic) LTL model checking is not supported");
}
if (prism.getFairness()) {
+ JDD.Deref(statesOfInterest);
throw new PrismNotSupportedException("Non-probabilistic CTL model checking is not supported with fairness");
}
@@ -114,12 +118,12 @@ public class NonProbModelChecker extends StateModelChecker
// Parentheses
if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
// Recurse
- res = checkExpressionExists(exprUnary.getOperand());
+ res = checkExpressionExists(exprUnary.getOperand(), statesOfInterest);
}
// Negation
else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
// Compute, then negate
- res = checkExpressionForAll(exprUnary.getOperand());
+ res = checkExpressionForAll(exprUnary.getOperand(), statesOfInterest);
res.subtractFromOne();
}
}
@@ -127,23 +131,24 @@ public class NonProbModelChecker extends StateModelChecker
else if (expr instanceof ExpressionTemporal) {
ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
if (exprTemp.hasBounds()) {
+ JDD.Deref(statesOfInterest);
throw new PrismNotSupportedException("Model checking of bounded CTL operators is not supported");
}
// Next (EX)
if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
- res = checkNext(exprTemp, false);
+ res = checkNext(exprTemp, false, statesOfInterest);
}
// Until (EU)
else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
- res = checkExistsUntil(exprTemp);
+ res = checkExistsUntil(exprTemp, statesOfInterest);
}
// Globally (EG)
else if (exprTemp.getOperator() == ExpressionTemporal.P_G) {
- res = checkExistsGlobally(exprTemp);
+ res = checkExistsGlobally(exprTemp, statesOfInterest);
}
// Anything else - convert to until and recurse
else {
- res = checkExpressionExists(exprTemp.convertToUntilForm());
+ res = checkExpressionExists(exprTemp.convertToUntilForm(), statesOfInterest);
}
}
@@ -155,17 +160,21 @@ public class NonProbModelChecker extends StateModelChecker
/**
* Model check a CTL forall (A) operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkExpressionForAll(Expression expr) throws PrismException
+ protected StateValues checkExpressionForAll(Expression expr, JDDNode statesOfInterest) throws PrismException
{
StateValues res = null;
// Check whether this is a simple path formula (i.e. CTL, not LTL)
if (!expr.isSimplePathFormula()) {
+ JDD.Deref(statesOfInterest);
throw new PrismNotSupportedException("(Non-probabilistic) LTL model checking is not supported");
}
if (prism.getFairness()) {
+ JDD.Deref(statesOfInterest);
throw new PrismNotSupportedException("Non-probabilistic CTL model checking is not supported with fairness");
}
@@ -175,12 +184,12 @@ public class NonProbModelChecker extends StateModelChecker
// Parentheses
if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
// Recurse
- res = checkExpressionForAll(exprUnary.getOperand());
+ res = checkExpressionForAll(exprUnary.getOperand(), statesOfInterest);
}
// Negation
else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
// Compute, then negate
- res = checkExpressionExists(exprUnary.getOperand());
+ res = checkExpressionExists(exprUnary.getOperand(), statesOfInterest);
res.subtractFromOne();
}
}
@@ -188,11 +197,12 @@ public class NonProbModelChecker extends StateModelChecker
else if (expr instanceof ExpressionTemporal) {
ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
if (exprTemp.hasBounds()) {
+ JDD.Deref(statesOfInterest);
throw new PrismNotSupportedException("Model checking of bounded CTL operators is not supported");
}
// Next (AX)
if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
- res = checkNext(exprTemp, true);
+ res = checkNext(exprTemp, true, statesOfInterest);
}
// Until (AU)
else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
@@ -205,7 +215,7 @@ public class NonProbModelChecker extends StateModelChecker
Expression rhs = new ExpressionTemporal(ExpressionTemporal.P_G, null, notPhi2);
rhs = Expression.Not(new ExpressionExists(rhs));
Expression enf = Expression.And(lhs, rhs);
- res = checkExpression(enf);
+ res = checkExpression(enf, statesOfInterest);
}
// Eventually (AF)
else if (exprTemp.getOperator() == ExpressionTemporal.P_F) {
@@ -213,12 +223,12 @@ public class NonProbModelChecker extends StateModelChecker
ExpressionTemporal exprCopy = (ExpressionTemporal) exprTemp.deepCopy();
exprCopy.setOperator(ExpressionTemporal.P_G);
exprCopy.setOperand2(Expression.Not(exprCopy.getOperand2()));
- res = checkExpressionExists(exprCopy);
+ res = checkExpressionExists(exprCopy, statesOfInterest);
res.subtractFromOne();
}
// Anything else - convert to until and recurse
else {
- res = checkExpressionForAll(exprTemp.convertToUntilForm());
+ res = checkExpressionForAll(exprTemp.convertToUntilForm(), statesOfInterest);
}
}
@@ -230,13 +240,18 @@ public class NonProbModelChecker extends StateModelChecker
/**
* Model check a CTL exists/forall next (EX/AX) operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkNext(ExpressionTemporal expr, boolean forall) throws PrismException
+ protected StateValues checkNext(ExpressionTemporal expr, boolean forall, JDDNode statesOfInterest) throws PrismException
{
JDDNode b, transRel, pre;
- // Model check operand first
- b = checkExpressionDD(expr.getOperand2());
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
+ // Model check operands first, statesOfInterest = all
+ b = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
// Get transition relation
if (model.getModelType() == ModelType.MDP) {
@@ -265,8 +280,10 @@ public class NonProbModelChecker extends StateModelChecker
/**
* Model check a CTL exists until (EU) operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkExistsUntil(ExpressionTemporal expr) throws PrismException
+ protected StateValues checkExistsUntil(ExpressionTemporal expr, JDDNode statesOfInterest) throws PrismException
{
JDDNode b1, b2, transRel, tmp, tmp2, tmp3, init = null;
ArrayList cexDDs = null;
@@ -276,10 +293,13 @@ public class NonProbModelChecker extends StateModelChecker
int iters, i;
long l;
- // Model check operands first
- b1 = checkExpressionDD(expr.getOperand1());
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
+ // Model check operands first, statesOfInterest = all
+ b1 = checkExpressionDD(expr.getOperand1(), model.getReach().copy());
try {
- b2 = checkExpressionDD(expr.getOperand2());
+ b2 = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
} catch (PrismException e) {
JDD.Deref(b1);
throw e;
@@ -425,8 +445,10 @@ public class NonProbModelChecker extends StateModelChecker
/**
* Model check a CTL exists globally (EG) operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkExistsGlobally(ExpressionTemporal expr) throws PrismException
+ protected StateValues checkExistsGlobally(ExpressionTemporal expr, JDDNode statesOfInterest) throws PrismException
{
JDDNode b2, transRel, tmp, tmp2;
boolean done;
@@ -437,8 +459,11 @@ public class NonProbModelChecker extends StateModelChecker
JDDNode notInSCCs = null;
int numSCCs = 0;
- // Model check operand first
- b2 = checkExpressionDD(expr.getOperand2());
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
+ // Model check operand first, statesOfInterest = all
+ b2 = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
l = System.currentTimeMillis();
diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java
index 89c22da0..ec4612a6 100644
--- a/prism/src/prism/NondetModelChecker.java
+++ b/prism/src/prism/NondetModelChecker.java
@@ -143,36 +143,36 @@ public class NondetModelChecker extends NonProbModelChecker
// Model checking functions
@Override
- public StateValues checkExpression(Expression expr) throws PrismException
+ public StateValues checkExpression(Expression expr, JDDNode statesOfInterest) throws PrismException
{
StateValues res;
// <<>> or [[]] operator
if (expr instanceof ExpressionStrategy) {
- res = checkExpressionStrategy((ExpressionStrategy) expr);
+ res = checkExpressionStrategy((ExpressionStrategy) expr, statesOfInterest);
}
// P operator
else if (expr instanceof ExpressionProb) {
- res = checkExpressionProb((ExpressionProb) expr);
+ res = checkExpressionProb((ExpressionProb) expr, statesOfInterest);
}
// R operator
else if (expr instanceof ExpressionReward) {
- res = checkExpressionReward((ExpressionReward) expr);
+ res = checkExpressionReward((ExpressionReward) expr, statesOfInterest);
}
// Multi-objective
else if (expr instanceof ExpressionFunc) {
// Detect "multi" function
if (((ExpressionFunc) expr).getName().equals("multi")) {
- res = checkExpressionMultiObjective((ExpressionFunc) expr);
+ res = checkExpressionMultiObjective((ExpressionFunc) expr, statesOfInterest);
}
// For any other function, check as normal
else {
- res = super.checkExpression(expr);
+ res = super.checkExpression(expr, statesOfInterest);
}
}
// Otherwise, use the superclass
else {
- res = super.checkExpression(expr);
+ res = super.checkExpression(expr, statesOfInterest);
}
// Filter out non-reachable states from solution
@@ -184,9 +184,11 @@ public class NondetModelChecker extends NonProbModelChecker
}
/**
- * Model check a <<>> or [[]] operator expression and return the values for all states.
+ * Model check a <<>> or [[]] operator expression.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkExpressionStrategy(ExpressionStrategy expr) throws PrismException
+ protected StateValues checkExpressionStrategy(ExpressionStrategy expr, JDDNode statesOfInterest) throws PrismException
{
// Will we be quantifying universally or existentially over strategies/adversaries?
boolean forAll = !expr.isThereExists();
@@ -207,34 +209,39 @@ public class NondetModelChecker extends NonProbModelChecker
// Pass onto relevant method:
// Single P operator
if (exprs.size() == 1 && exprs.get(0) instanceof ExpressionProb) {
- return checkExpressionProb((ExpressionProb) exprs.get(0), forAll);
+ return checkExpressionProb((ExpressionProb) exprs.get(0), forAll, statesOfInterest);
}
// Single R operator
else if (exprs.size() == 1 && exprs.get(0) instanceof ExpressionReward) {
- return checkExpressionReward((ExpressionReward) exprs.get(0), forAll);
+ return checkExpressionReward((ExpressionReward) exprs.get(0), forAll, statesOfInterest);
}
// Anything else is treated as multi-objective
else {
- return checkExpressionMultiObjective(exprs, forAll);
+ return checkExpressionMultiObjective(exprs, forAll, statesOfInterest);
}
}
/**
- * Model check a P operator expression and return the values for all states.
+ * Model check a P operator expression.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkExpressionProb(ExpressionProb expr) throws PrismException
+ protected StateValues checkExpressionProb(ExpressionProb expr, JDDNode statesOfInterest) throws PrismException
{
// Use the default semantics for a standalone P operator
// (i.e. quantification over all strategies)
- return checkExpressionProb(expr, true);
+ return checkExpressionProb(expr, true, statesOfInterest);
}
/**
- * Model check a P operator expression and return the values for all states.
+ * Model check a P operator expression.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ *
* @param expr The P operator expression
- * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries]
+ * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries]
*/
- protected StateValues checkExpressionProb(ExpressionProb expr, boolean forAll) throws PrismException
+ protected StateValues checkExpressionProb(ExpressionProb expr, boolean forAll, JDDNode statesOfInterest) throws PrismException
{
// Get info from P operator
OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
@@ -244,15 +251,17 @@ public class NondetModelChecker extends NonProbModelChecker
if (opInfo.isTriviallyTrue()) {
mainLog.printWarning("Checking for probability " + opInfo.relOpBoundString() + " - formula trivially satisfies all states");
JDD.Ref(reach);
+ JDD.Deref(statesOfInterest);
return new StateValuesMTBDD(reach, model);
} else if (opInfo.isTriviallyFalse()) {
mainLog.printWarning("Checking for probability " + opInfo.relOpBoundString() + " - formula trivially satisfies no states");
+ JDD.Deref(statesOfInterest);
return new StateValuesMTBDD(JDD.Constant(0), model);
}
// Compute probabilities
boolean qual = opInfo.isQualitative() && precomp && prob0 && prob1;
- StateValues probs = checkProbPathFormula(expr.getExpression(), qual, minMax.isMin());
+ StateValues probs = checkProbPathFormula(expr.getExpression(), qual, minMax.isMin(), statesOfInterest);
// Print out probabilities
if (verbose) {
@@ -277,21 +286,26 @@ public class NondetModelChecker extends NonProbModelChecker
}
/**
- * Model check n R operator expression and return the values for all states.
+ * Model check an R operator expression.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkExpressionReward(ExpressionReward expr) throws PrismException
+ protected StateValues checkExpressionReward(ExpressionReward expr, JDDNode statesOfInterest) throws PrismException
{
// Use the default semantics for a standalone R operator
// (i.e. quantification over all strategies)
- return checkExpressionReward(expr, true);
+ return checkExpressionReward(expr, true, statesOfInterest);
}
/**
- * Model check an R operator expression and return the values for all states.
+ * Model check an R operator expression.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ *
* @param expr The R operator expression
- * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries]
+ * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries]
*/
- protected StateValues checkExpressionReward(ExpressionReward expr, boolean forAll) throws PrismException
+ protected StateValues checkExpressionReward(ExpressionReward expr, boolean forAll, JDDNode statesOfInterest) throws PrismException
{
// Get info from R operator
OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
@@ -310,17 +324,17 @@ public class NondetModelChecker extends NonProbModelChecker
switch (exprTemp.getOperator()) {
case ExpressionTemporal.R_C:
if (exprTemp.hasBounds()) {
- rewards = checkRewardCumul(exprTemp, stateRewards, transRewards, minMax.isMin());
+ rewards = checkRewardCumul(exprTemp, stateRewards, transRewards, minMax.isMin(), statesOfInterest);
} else {
- rewards = checkRewardTotal(exprTemp, stateRewards, transRewards, minMax.isMin());
+ rewards = checkRewardTotal(exprTemp, stateRewards, transRewards, minMax.isMin(), statesOfInterest);
}
break;
case ExpressionTemporal.R_I:
- rewards = checkRewardInst(exprTemp, stateRewards, transRewards, minMax.isMin());
+ rewards = checkRewardInst(exprTemp, stateRewards, transRewards, minMax.isMin(), statesOfInterest);
break;
}
} else if (expr2.getType() instanceof TypePathBool || expr2.getType() instanceof TypeBool) {
- rewards = checkRewardPathFormula(expr2, stateRewards, transRewards, minMax.isMin());
+ rewards = checkRewardPathFormula(expr2, stateRewards, transRewards, minMax.isMin(), statesOfInterest);
}
if (rewards == null)
@@ -352,13 +366,17 @@ public class NondetModelChecker extends NonProbModelChecker
* Model check a multi-objective query (from the contents of a strategy operator).
* Return the result as a StateValues object (usually this gives values for all states,
* but for a multi-objective query, we just give a single value, usually for the initial state).
+ *
+ *
[ REFS: result, DEREFS: statesOfInterest ]
* @param exprs The list of Expressions specifying the objectives
- * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries]
+ * @param forAll Are we checking "for all strategies" (true) or "there exists a strategy" (false)? [irrelevant for numerical (=?) queries]
+ * @param statesOfInterest the states of interest
*/
- protected StateValues checkExpressionMultiObjective(List exprs, boolean forAll) throws PrismException
+ protected StateValues checkExpressionMultiObjective(List exprs, boolean forAll, JDDNode statesOfInterest) throws PrismException
{
// For now, just support a single expression (which may encode a Boolean combination of objectives)
if (exprs.size() > 1) {
+ JDD.Deref(statesOfInterest);
throw new PrismException("Cannot currently check strategy operators with lists of expressions");
}
Expression exprSub = exprs.get(0);
@@ -380,6 +398,7 @@ public class NondetModelChecker extends NonProbModelChecker
prop = ((ExpressionUnaryOp) prop).getOperand();
}
if (!(prop instanceof ExpressionQuant)) {
+ JDD.Deref(statesOfInterest);
throw new PrismException("Expression " + prop + " is not allowed in a multi-objective query");
}
}
@@ -400,6 +419,7 @@ public class NondetModelChecker extends NonProbModelChecker
// Only handle a single disjunct for now
if (dnf.size() > 1) {
+ JDD.Deref(statesOfInterest);
throw new PrismException("Multi-objective model checking of multiple disjuncts not yet supported");
}
// Convert to multi(...)
@@ -409,13 +429,14 @@ public class NondetModelChecker extends NonProbModelChecker
}
// Handle negation
if (forAll) {
- return checkExpression(Expression.Not(exprMulti));
+ return checkExpression(Expression.Not(exprMulti), statesOfInterest);
} else {
- return checkExpressionMultiObjective(exprMulti);
+ return checkExpressionMultiObjective(exprMulti, statesOfInterest);
}
} else if (exprSub.getType() instanceof TypeDouble) {
- return checkExpressionMultiObjective(exprs);
+ return checkExpressionMultiObjective(exprs, statesOfInterest);
} else {
+ JDD.Deref(statesOfInterest);
throw new PrismException("Multi-objective model checking not supported for: " + exprSub);
}
}
@@ -423,8 +444,9 @@ public class NondetModelChecker extends NonProbModelChecker
/**
* Model check a multi-objective expression and return the result.
* For multi-objective queries, we only find the value for one state.
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkExpressionMultiObjective(ExpressionFunc expr) throws PrismException
+ protected StateValues checkExpressionMultiObjective(ExpressionFunc expr, JDDNode statesOfInterest) throws PrismException
{
// Extract objective list from 'multi' function
List exprs = new ArrayList();
@@ -432,14 +454,15 @@ public class NondetModelChecker extends NonProbModelChecker
for (int i = 0; i < n; i++) {
exprs.add(expr.getOperand(i));
}
- return checkExpressionMultiObjective(exprs);
+ return checkExpressionMultiObjective(exprs, statesOfInterest);
}
/**
* Model check a multi-objective expression and return the result.
* For multi-objective queries, we only find the value for one state.
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkExpressionMultiObjective(List exprs) throws PrismException
+ protected StateValues checkExpressionMultiObjective(List exprs, JDDNode statesOfInterest) throws PrismException
{
// Objective/target info
List multitargetDDs = null;
@@ -459,6 +482,10 @@ public class NondetModelChecker extends NonProbModelChecker
boolean hasMaxReward = false;
//boolean hasLTLconstraint = false;
+ // currently, ignore statesOfInterest
+ // TODO: switch singleton check below to use statesOfInterest
+ JDD.Deref(statesOfInterest);
+
// Make sure we are only expected to compute a value for a single state
// Assuming yes, determine index of state of interest and build BDD
JDDNode ddStateIndex = null;
@@ -488,6 +515,7 @@ public class NondetModelChecker extends NonProbModelChecker
//currently we do 1 numerical subject to booleans, or multiple numericals only
if (opsAndBounds.numberOfNumerical() > 1 &&
opsAndBounds.numberOfNumerical() < opsAndBounds.probSize() + opsAndBounds.rewardSize()) {
+ JDD.Deref(stateOfInterest);
throw new PrismException("Multiple min/max queries cannot be combined with boolean queries.");
}
@@ -604,7 +632,7 @@ public class NondetModelChecker extends NonProbModelChecker
// (not used currently)
// Fixme: maybe not efficient
if (pathFormulas.get(i) != null) {
- JDDNode dd = checkExpressionDD(pathFormulas.get(i));
+ JDDNode dd = checkExpressionDD(pathFormulas.get(i), model.getReach().copy());
JDD.Ref(modelProduct.getReach());
dd = JDD.And(dd, modelProduct.getReach());
targetDDs.add(dd);
@@ -847,8 +875,10 @@ public class NondetModelChecker extends NonProbModelChecker
/**
* Compute probabilities for the contents of a P operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkProbPathFormula(Expression expr, boolean qual, boolean min) throws PrismException
+ protected StateValues checkProbPathFormula(Expression expr, boolean qual, boolean min, JDDNode statesOfInterest) throws PrismException
{
// Test whether this is a simple path formula (i.e. PCTL)
// and whether we want to use the corresponding algorithms
@@ -863,16 +893,18 @@ public class NondetModelChecker extends NonProbModelChecker
}
if (useSimplePathAlgo) {
- return checkProbPathFormulaSimple(expr, qual, min);
+ return checkProbPathFormulaSimple(expr, qual, min, statesOfInterest);
} else {
- return checkProbPathFormulaLTL(expr, qual, min);
+ return checkProbPathFormulaLTL(expr, qual, min, statesOfInterest);
}
}
/**
* Compute probabilities for a simple, non-LTL path operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkProbPathFormulaSimple(Expression expr, boolean qual, boolean min) throws PrismException
+ protected StateValues checkProbPathFormulaSimple(Expression expr, boolean qual, boolean min, JDDNode statesOfInterest) throws PrismException
{
boolean negated = false;
StateValues probs = null;
@@ -892,14 +924,14 @@ public class NondetModelChecker extends NonProbModelChecker
ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
// Next
if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
- probs = checkProbNext(exprTemp, min);
+ probs = checkProbNext(exprTemp, min, statesOfInterest);
}
// Until
else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
if (exprTemp.hasBounds()) {
- probs = checkProbBoundedUntil(exprTemp, min);
+ probs = checkProbBoundedUntil(exprTemp, min, statesOfInterest);
} else {
- probs = checkProbUntil(exprTemp, qual, min);
+ probs = checkProbUntil(exprTemp, qual, min, statesOfInterest);
}
}
}
@@ -917,14 +949,19 @@ public class NondetModelChecker extends NonProbModelChecker
/**
* Compute probabilities for a next operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkProbNext(ExpressionTemporal expr, boolean min) throws PrismException
+ protected StateValues checkProbNext(ExpressionTemporal expr, boolean min, JDDNode statesOfInterest) throws PrismException
{
JDDNode b;
StateValues probs = null;
- // model check operand first
- b = checkExpressionDD(expr.getOperand2());
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
+ // model check operand first, statesOfInterest = all
+ b = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
// print out some info about num states
// mainLog.print("\nb = " + JDD.GetNumMintermsString(b,
@@ -941,8 +978,10 @@ public class NondetModelChecker extends NonProbModelChecker
/**
* Compute probabilities for a bounded until operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkProbBoundedUntil(ExpressionTemporal expr, boolean min) throws PrismException
+ protected StateValues checkProbBoundedUntil(ExpressionTemporal expr, boolean min, JDDNode statesOfInterest) throws PrismException
{
JDDNode b1, b2;
StateValues probs = null;
@@ -950,13 +989,16 @@ public class NondetModelChecker extends NonProbModelChecker
IntegerBound bounds;
int i;
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
// get and check bounds information
bounds = IntegerBound.fromExpressionTemporal(expr, constantValues, true);
- // model check operands first
- b1 = checkExpressionDD(expr.getOperand1());
+ // model check operands first, statesOfInterest = all
+ b1 = checkExpressionDD(expr.getOperand1(), model.getReach().copy());
try {
- b2 = checkExpressionDD(expr.getOperand2());
+ b2 = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
} catch (PrismException e) {
JDD.Deref(b1);
throw e;
@@ -1022,16 +1064,21 @@ public class NondetModelChecker extends NonProbModelChecker
/**
* Compute probabilities for an (unbounded) until operator.
* Note: This method is split into two steps so that the LTL model checker can use the second part directly.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkProbUntil(ExpressionTemporal expr, boolean qual, boolean min) throws PrismException
+ protected StateValues checkProbUntil(ExpressionTemporal expr, boolean qual, boolean min, JDDNode statesOfInterest) throws PrismException
{
JDDNode b1, b2;
StateValues probs = null;
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
// model check operands first
- b1 = checkExpressionDD(expr.getOperand1());
+ b1 = checkExpressionDD(expr.getOperand1(), model.getReach().copy());
try {
- b2 = checkExpressionDD(expr.getOperand2());
+ b2 = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
} catch (PrismException e) {
JDD.Deref(b1);
throw e;
@@ -1059,7 +1106,10 @@ public class NondetModelChecker extends NonProbModelChecker
}
/**
- * Compute probabilities for an (unbounded) until operator.
+ * Compute probabilities for an (unbounded) until operator (b1 U b2).
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ *
* @param b1 Remain in these states
* @param b2 Target states
* @param qual True if only qualititative (0/1) results are needed
@@ -1141,8 +1191,10 @@ public class NondetModelChecker extends NonProbModelChecker
/**
* Compute probabilities for an LTL path formula
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkProbPathFormulaLTL(Expression expr, boolean qual, boolean min) throws PrismException
+ protected StateValues checkProbPathFormulaLTL(Expression expr, boolean qual, boolean min, JDDNode statesOfInterest) throws PrismException
{
LTLModelChecker mcLtl;
StateValues probsProduct = null, probs = null;
@@ -1155,6 +1207,9 @@ public class NondetModelChecker extends NonProbModelChecker
int i;
long l;
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
// For min probabilities, need to negate the formula
// (But check fairness setting since this may affect min/max)
// (add parentheses to allow re-parsing if required)
@@ -1260,12 +1315,17 @@ public class NondetModelChecker extends NonProbModelChecker
/**
* Compute rewards for a cumulative reward operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkRewardCumul(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
+ protected StateValues checkRewardCumul(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min, JDDNode statesOfInterest) throws PrismException
{
int time; // time
StateValues rewards = null;
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
// check that there is an upper time bound
if (expr.getUpperBound() == null) {
throw new PrismException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries");
@@ -1294,21 +1354,30 @@ public class NondetModelChecker extends NonProbModelChecker
/**
* Compute rewards for a total reward operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkRewardTotal(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
+ protected StateValues checkRewardTotal(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min, JDDNode statesOfInterest) throws PrismException
{
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
StateValues rewards = computeTotalRewards(trans, trans01, transActions, stateRewards, transRewards, min);
return rewards;
}
/**
* Compute rewards for an instantaneous reward operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
+ protected StateValues checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min, JDDNode statesOfInterest) throws PrismException
{
int time; // time bound
StateValues rewards = null;
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
// get info from bounded until
time = expr.getUpperBound().evaluateInt(constantValues);
if (time < 0) {
@@ -1322,33 +1391,42 @@ public class NondetModelChecker extends NonProbModelChecker
}
/**
- * Compute rewards for a reachability reward operator.
+ * Compute rewards for a reachability reward operator (either simple reachability or co-safe LTL).
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
+ protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min, JDDNode statesOfInterest) throws PrismException
{
if (Expression.isReach(expr)) {
- return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards, min);
+ return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards, min, statesOfInterest);
}
else if (Expression.isCoSafeLTLSyntactic(expr, true)) {
- return checkRewardCoSafeLTL(expr, stateRewards, transRewards, min);
+ return checkRewardCoSafeLTL(expr, stateRewards, transRewards, min, statesOfInterest);
}
+ JDD.Deref(statesOfInterest);
throw new PrismException("R operator contains a path formula that is not syntactically co-safe: " + expr);
}
-
- // reach reward
- protected StateValues checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
+ /**
+ * Compute rewards for a reachability reward operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min, JDDNode statesOfInterest) throws PrismException
{
JDDNode b;
StateValues rewards = null;
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
// No time bounds allowed
if (expr.hasBounds()) {
throw new PrismNotSupportedException("R operator cannot contain a bounded F operator: " + expr);
}
- // model check operand first
- b = checkExpressionDD(expr.getOperand2());
+ // model check operand first, statesOfInterest = all
+ b = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
// print out some info about num states
// mainLog.print("\nb = " + JDD.GetNumMintermsString(b,
@@ -1368,9 +1446,12 @@ public class NondetModelChecker extends NonProbModelChecker
return rewards;
}
- // co-safe LTL reward
-
- protected StateValues checkRewardCoSafeLTL(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
+ /**
+ * Compute rewards for a co-safe LTL reward operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkRewardCoSafeLTL(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min, JDDNode statesOfInterest) throws PrismException
{
LTLModelChecker mcLtl;
StateValues rewardsProduct = null, rewards = null;
@@ -1384,6 +1465,9 @@ public class NondetModelChecker extends NonProbModelChecker
int i;
long l;
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
if (Expression.containsTemporalTimeBounds(expr)) {
if (model.getModelType().continuousTime()) {
throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java
index 82289243..5a014871 100644
--- a/prism/src/prism/ProbModelChecker.java
+++ b/prism/src/prism/ProbModelChecker.java
@@ -124,26 +124,26 @@ public class ProbModelChecker extends NonProbModelChecker
// -----------------------------------------------------------------------------------
// Check expression (recursive)
-
- public StateValues checkExpression(Expression expr) throws PrismException
+ @Override
+ public StateValues checkExpression(Expression expr, JDDNode statesOfInterest) throws PrismException
{
StateValues res;
// P operator
if (expr instanceof ExpressionProb) {
- res = checkExpressionProb((ExpressionProb) expr);
+ res = checkExpressionProb((ExpressionProb) expr, statesOfInterest);
}
// R operator
else if (expr instanceof ExpressionReward) {
- res = checkExpressionReward((ExpressionReward) expr);
+ res = checkExpressionReward((ExpressionReward) expr, statesOfInterest);
}
// S operator
else if (expr instanceof ExpressionSS) {
- res = checkExpressionSteadyState((ExpressionSS) expr);
+ res = checkExpressionSteadyState((ExpressionSS) expr, statesOfInterest);
}
// Otherwise, use the superclass
else {
- res = super.checkExpression(expr);
+ res = super.checkExpression(expr, statesOfInterest);
}
// Filter out non-reachable states from solution
@@ -160,7 +160,12 @@ public class ProbModelChecker extends NonProbModelChecker
// P operator
- protected StateValues checkExpressionProb(ExpressionProb expr) throws PrismException
+ /**
+ * Check a P (probability) operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionProb(ExpressionProb expr, JDDNode statesOfInterest) throws PrismException
{
// Get info from P operator
OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
@@ -169,9 +174,11 @@ public class ProbModelChecker extends NonProbModelChecker
if (opInfo.isTriviallyTrue()) {
mainLog.printWarning("Checking for probability " + opInfo.relOpBoundString() + " - formula trivially satisfies all states");
JDD.Ref(reach);
+ JDD.Deref(statesOfInterest);
return new StateValuesMTBDD(reach, model);
} else if (opInfo.isTriviallyFalse()) {
mainLog.printWarning("Checking for probability " + opInfo.relOpBoundString() + " - formula trivially satisfies no states");
+ JDD.Deref(statesOfInterest);
return new StateValuesMTBDD(JDD.Constant(0), model);
}
@@ -182,7 +189,7 @@ public class ProbModelChecker extends NonProbModelChecker
// Compute probabilities
boolean qual = opInfo.isQualitative() && precomp && prob0 && prob1;
- StateValues probs = checkProbPathFormula(expr.getExpression(), qual);
+ StateValues probs = checkProbPathFormula(expr.getExpression(), qual, statesOfInterest);
// Print out probabilities
if (prism.getVerbose()) {
@@ -207,8 +214,13 @@ public class ProbModelChecker extends NonProbModelChecker
}
// R operator
-
- protected StateValues checkExpressionReward(ExpressionReward expr) throws PrismException
+
+ /**
+ * Check an R (reward) operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionReward(ExpressionReward expr, JDDNode statesOfInterest) throws PrismException
{
// Get info from R operator
OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
@@ -231,20 +243,20 @@ public class ProbModelChecker extends NonProbModelChecker
switch (exprTemp.getOperator()) {
case ExpressionTemporal.R_C:
if (exprTemp.hasBounds()) {
- rewards = checkRewardCumul(exprTemp, stateRewards, transRewards);
+ rewards = checkRewardCumul(exprTemp, stateRewards, transRewards, statesOfInterest);
} else {
- rewards = checkRewardTotal(exprTemp, stateRewards, transRewards);
+ rewards = checkRewardTotal(exprTemp, stateRewards, transRewards, statesOfInterest);
}
break;
case ExpressionTemporal.R_I:
- rewards = checkRewardInst(exprTemp, stateRewards, transRewards);
+ rewards = checkRewardInst(exprTemp, stateRewards, transRewards, statesOfInterest);
break;
case ExpressionTemporal.R_S:
- rewards = checkRewardSS(exprTemp, stateRewards, transRewards);
+ rewards = checkRewardSS(exprTemp, stateRewards, transRewards, statesOfInterest);
break;
}
} else if (expr2.getType() instanceof TypePathBool || expr2.getType() instanceof TypeBool) {
- rewards = checkRewardPathFormula(expr2, stateRewards, transRewards);
+ rewards = checkRewardPathFormula(expr2, stateRewards, transRewards, statesOfInterest);
}
if (rewards == null)
@@ -274,7 +286,12 @@ public class ProbModelChecker extends NonProbModelChecker
// S operator
- protected StateValues checkExpressionSteadyState(ExpressionSS expr) throws PrismException
+ /**
+ * Check an S (steady-state) operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionSteadyState(ExpressionSS expr, JDDNode statesOfInterest) throws PrismException
{
// BSCC stuff
List bsccs = null;
@@ -286,6 +303,8 @@ public class ProbModelChecker extends NonProbModelChecker
int i, numBSCCs = 0;
double d, probBSCCs[];
+ JDD.Deref(statesOfInterest);
+
// Get info from S operator
OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
@@ -300,8 +319,8 @@ public class ProbModelChecker extends NonProbModelChecker
}
try {
- // Model check argument
- b = checkExpressionDD(expr.getExpression());
+ // Model check argument with stateOfInterest = all
+ b = checkExpressionDD(expr.getExpression(), model.getReach().copy());
// Compute bottom strongly connected components (BSCCs)
if (bsccComp) {
@@ -438,7 +457,14 @@ public class ProbModelChecker extends NonProbModelChecker
// Contents of a P operator
- protected StateValues checkProbPathFormula(Expression expr, boolean qual) throws PrismException
+ /**
+ * Check a P operator path formula.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
+ * @param qual perform qualitative model checking
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkProbPathFormula(Expression expr, boolean qual, JDDNode statesOfInterest) throws PrismException
{
// Test whether this is a simple path formula (i.e. PCTL)
// and whether we want to use the corresponding algorithms
@@ -453,13 +479,20 @@ public class ProbModelChecker extends NonProbModelChecker
}
if (useSimplePathAlgo) {
- return checkProbPathFormulaSimple(expr, qual);
+ return checkProbPathFormulaSimple(expr, qual, statesOfInterest);
} else {
- return checkProbPathFormulaLTL(expr, qual);
+ return checkProbPathFormulaLTL(expr, qual, statesOfInterest);
}
}
- protected StateValues checkProbPathFormulaSimple(Expression expr, boolean qual) throws PrismException
+ /**
+ * Check a P operator simple path formula (single, non-nested temporal operator).
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
+ * @param qual perform qualitative model checking
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkProbPathFormulaSimple(Expression expr, boolean qual, JDDNode statesOfInterest) throws PrismException
{
boolean negated = false;
StateValues probs = null;
@@ -477,14 +510,14 @@ public class ProbModelChecker extends NonProbModelChecker
ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
// Next
if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
- probs = checkProbNext(exprTemp);
+ probs = checkProbNext(exprTemp, statesOfInterest);
}
// Until
else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
if (exprTemp.hasBounds()) {
- probs = checkProbBoundedUntil(exprTemp);
+ probs = checkProbBoundedUntil(exprTemp, statesOfInterest);
} else {
- probs = checkProbUntil(exprTemp, qual);
+ probs = checkProbUntil(exprTemp, qual, statesOfInterest);
}
}
}
@@ -500,9 +533,14 @@ public class ProbModelChecker extends NonProbModelChecker
return probs;
}
- // LTL-like path formula for P operator
-
- protected StateValues checkProbPathFormulaLTL(Expression expr, boolean qual) throws PrismException
+ /**
+ * Check a P operator LTL-like path formula.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
+ * @param qual perform qualitative model checking
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkProbPathFormulaLTL(Expression expr, boolean qual, JDDNode statesOfInterest) throws PrismException
{
LTLModelChecker mcLtl;
StateValues probsProduct = null, probs = null;
@@ -514,6 +552,9 @@ public class ProbModelChecker extends NonProbModelChecker
JDDVars daDDRowVars, daDDColVars;
int i;
+ // TODO: take statesOfInterest into account for product construction
+ JDD.Deref(statesOfInterest);
+
AcceptanceType[] allowedAcceptance = {
AcceptanceType.RABIN,
AcceptanceType.REACH,
@@ -587,15 +628,20 @@ public class ProbModelChecker extends NonProbModelChecker
return probs;
}
- // next
-
- protected StateValues checkProbNext(ExpressionTemporal expr) throws PrismException
+ /**
+ * Check a P operator with a next operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkProbNext(ExpressionTemporal expr, JDDNode statesOfInterest) throws PrismException
{
JDDNode b;
StateValues probs = null;
- // model check operand first
- b = checkExpressionDD(expr.getOperand2());
+ JDD.Deref(statesOfInterest);
+
+ // model check operand first, stateOfInterest = all
+ b = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
// print out some info about num states
// mainLog.print("\nb = " + JDD.GetNumMintermsString(b,
@@ -610,9 +656,12 @@ public class ProbModelChecker extends NonProbModelChecker
return probs;
}
- // bounded until
-
- protected StateValues checkProbBoundedUntil(ExpressionTemporal expr) throws PrismException
+ /**
+ * Check a P operator with a bounded until operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkProbBoundedUntil(ExpressionTemporal expr, JDDNode statesOfInterest) throws PrismException
{
JDDNode b1, b2;
StateValues probs = null;
@@ -620,13 +669,16 @@ public class ProbModelChecker extends NonProbModelChecker
IntegerBound bounds;
int i;
+ // currently, we ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
// get and check bounds information
bounds = IntegerBound.fromExpressionTemporal(expr, constantValues, true);
- // model check operands first
- b1 = checkExpressionDD(expr.getOperand1());
+ // model check operands first, statesOfInterest = all
+ b1 = checkExpressionDD(expr.getOperand1(), model.getReach().copy());
try {
- b2 = checkExpressionDD(expr.getOperand2());
+ b2 = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
} catch (PrismException e) {
JDD.Deref(b1);
throw e;
@@ -689,19 +741,24 @@ public class ProbModelChecker extends NonProbModelChecker
return probs;
}
- // until (unbounded)
-
+ /**
+ * Check a P operator with an unbounded until operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
// this method is split into two steps so that the LTL model checker can use the second part directly
-
- protected StateValues checkProbUntil(ExpressionTemporal expr, boolean qual) throws PrismException
+ protected StateValues checkProbUntil(ExpressionTemporal expr, boolean qual, JDDNode statesOfInterest) throws PrismException
{
JDDNode b1, b2;
StateValues probs = null;
- // model check operands first
- b1 = checkExpressionDD(expr.getOperand1());
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
+ // model check operands first, statesOfInterest = all
+ b1 = checkExpressionDD(expr.getOperand1(), model.getReach().copy());
try {
- b2 = checkExpressionDD(expr.getOperand2());
+ b2 = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
} catch (PrismException e) {
JDD.Deref(b1);
throw e;
@@ -728,8 +785,11 @@ public class ProbModelChecker extends NonProbModelChecker
return probs;
}
- // until (unbounded): b1/b2 are bdds for until operands
-
+ /**
+ * Check a P operator with an unbounded until operator (b1 U b2)
+ * @param qual perform qualitative model checking?
+ *
[ REFS: result, DEREFS: none ]
+ */
protected StateValues checkProbUntil(JDDNode b1, JDDNode b2, boolean qual) throws PrismException
{
StateValues probs = null;
@@ -750,13 +810,19 @@ public class ProbModelChecker extends NonProbModelChecker
return probs;
}
- // cumulative reward
-
- protected StateValues checkRewardCumul(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+ /**
+ * Check a cumulative reward operator (C<=t).
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkRewardCumul(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException
{
int time; // time
StateValues rewards = null;
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
// check that there is an upper time bound
if (expr.getUpperBound() == null) {
throw new PrismException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries");
@@ -785,21 +851,33 @@ public class ProbModelChecker extends NonProbModelChecker
return rewards;
}
- // cumulative reward
-
- protected StateValues checkRewardTotal(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+ /**
+ * Check a total reward operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkRewardTotal(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException
{
+ // currently, we ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
StateValues rewards = computeTotalRewards(trans, trans01, stateRewards, transRewards);
return rewards;
}
- // inst reward
-
- protected StateValues checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+ /**
+ * Check an instantaneous reward operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException
{
int time; // time
StateValues rewards = null;
+ // currently, we ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
// get info from inst reward
time = expr.getUpperBound().evaluateInt(constantValues);
if (time < 0) {
@@ -813,33 +891,42 @@ public class ProbModelChecker extends NonProbModelChecker
}
/**
- * Compute rewards for a reachability reward operator.
+ * Check a reachability reward operator (either simple or using co-safety LTL).
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
*/
- protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+ protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException
{
if (Expression.isReach(expr)) {
- return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards);
+ return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards, statesOfInterest);
}
else if (Expression.isCoSafeLTLSyntactic(expr, true)) {
- return checkRewardCoSafeLTL(expr, stateRewards, transRewards);
+ return checkRewardCoSafeLTL(expr, stateRewards, transRewards, statesOfInterest);
}
+ JDD.Deref(statesOfInterest);
throw new PrismException("R operator contains a path formula that is not syntactically co-safe: " + expr);
}
-
- // reach reward
- protected StateValues checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+ /**
+ * Check a reachability reward operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException
{
JDDNode b;
StateValues rewards = null;
+ // currently, we ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
// No time bounds allowed
if (expr.hasBounds()) {
throw new PrismNotSupportedException("R operator cannot contain a bounded F operator: " + expr);
}
// model check operand first
- b = checkExpressionDD(expr.getOperand2());
+ b = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
// print out some info about num states
// mainLog.print("\nb = " + JDD.GetNumMintermsString(b,
@@ -859,9 +946,12 @@ public class ProbModelChecker extends NonProbModelChecker
return rewards;
}
- // co-safe LTL reward
-
- protected StateValues checkRewardCoSafeLTL(Expression expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+ /**
+ * Check a co-safe LTL reward operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkRewardCoSafeLTL(Expression expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException
{
LTLModelChecker mcLtl;
StateValues rewardsProduct = null, rewards = null;
@@ -875,6 +965,9 @@ public class ProbModelChecker extends NonProbModelChecker
int i;
long l;
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
if (Expression.containsTemporalTimeBounds(expr)) {
if (model.getModelType().continuousTime()) {
throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
@@ -995,9 +1088,12 @@ public class ProbModelChecker extends NonProbModelChecker
return rewards;
}
- // steady state reward
-
- protected StateValues checkRewardSS(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+ /**
+ * Check a steady-state reward operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkRewardSS(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException
{
// bscc stuff
List vectBSCCs;
@@ -1009,6 +1105,9 @@ public class ProbModelChecker extends NonProbModelChecker
int i, numBSCCs;
double d, rewBSCCs[];
+ // currently, ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
// compute rewards corresponding to each state
JDD.Ref(trans);
JDD.Ref(transRewards);
diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index 57f3642e..b6cb8110 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/prism/src/prism/StateModelChecker.java
@@ -191,9 +191,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
model.clear();
}
- /**
- * Model check an expression, process and return the result.
- */
+ @Override
public Result check(Expression expr) throws PrismException
{
long timer = 0;
@@ -217,7 +215,8 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
// Do model checking and store result vector
timer = System.currentTimeMillis();
- vals = checkExpression(expr);
+ // check expression, statesOfInterest = all reachable states
+ vals = checkExpression(expr, model.getReach().copy());
timer = System.currentTimeMillis() - timer;
mainLog.println("\nTime for model checking: " + timer / 1000.0 + " seconds.");
@@ -235,28 +234,26 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
return result;
}
- /**
- * Model check an expression and return a vector result values over all states.
- */
- public StateValues checkExpression(Expression expr) throws PrismException
+ @Override
+ public StateValues checkExpression(Expression expr, JDDNode statesOfInterest) throws PrismException
{
StateValues res;
// If-then-else
if (expr instanceof ExpressionITE) {
- res = checkExpressionITE((ExpressionITE) expr);
+ res = checkExpressionITE((ExpressionITE) expr, statesOfInterest);
}
// Binary ops
else if (expr instanceof ExpressionBinaryOp) {
- res = checkExpressionBinaryOp((ExpressionBinaryOp) expr);
+ res = checkExpressionBinaryOp((ExpressionBinaryOp) expr, statesOfInterest);
}
// Unary ops
else if (expr instanceof ExpressionUnaryOp) {
- res = checkExpressionUnaryOp((ExpressionUnaryOp) expr);
+ res = checkExpressionUnaryOp((ExpressionUnaryOp) expr, statesOfInterest);
}
// Functions
else if (expr instanceof ExpressionFunc) {
- res = checkExpressionFunc((ExpressionFunc) expr);
+ res = checkExpressionFunc((ExpressionFunc) expr, statesOfInterest);
}
// Identifiers
else if (expr instanceof ExpressionIdent) {
@@ -265,38 +262,39 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
}
// Literals
else if (expr instanceof ExpressionLiteral) {
- res = checkExpressionLiteral((ExpressionLiteral) expr);
+ res = checkExpressionLiteral((ExpressionLiteral) expr, statesOfInterest);
}
// Constants
else if (expr instanceof ExpressionConstant) {
- res = checkExpressionConstant((ExpressionConstant) expr);
+ res = checkExpressionConstant((ExpressionConstant) expr, statesOfInterest);
}
// Formulas
else if (expr instanceof ExpressionFormula) {
// This should have been defined or expanded by now.
if (((ExpressionFormula) expr).getDefinition() != null)
- return checkExpression(((ExpressionFormula) expr).getDefinition());
+ return checkExpression(((ExpressionFormula) expr).getDefinition(), statesOfInterest);
else
throw new PrismException("Unexpanded formula \"" + ((ExpressionFormula) expr).getName() + "\"");
}
// Variables
else if (expr instanceof ExpressionVar) {
- res = checkExpressionVar((ExpressionVar) expr);
+ res = checkExpressionVar((ExpressionVar) expr, statesOfInterest);
}
// Labels
else if (expr instanceof ExpressionLabel) {
- res = checkExpressionLabel((ExpressionLabel) expr);
+ res = checkExpressionLabel((ExpressionLabel) expr, statesOfInterest);
}
// Property refs
else if (expr instanceof ExpressionProp) {
- res = checkExpressionProp((ExpressionProp) expr);
+ res = checkExpressionProp((ExpressionProp) expr, statesOfInterest);
}
// Filter
else if (expr instanceof ExpressionFilter) {
- res = checkExpressionFilter((ExpressionFilter) expr);
+ res = checkExpressionFilter((ExpressionFilter) expr, statesOfInterest);
}
// Anything else - error
else {
+ JDD.Deref(statesOfInterest);
throw new PrismException("Couldn't check " + expr.getClass());
}
@@ -309,11 +307,10 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
return res;
}
- // Check expression, convert to symbolic form (if not already), return BDD
-
- public JDDNode checkExpressionDD(Expression expr) throws PrismException
+ @Override
+ public JDDNode checkExpressionDD(Expression expr, JDDNode statesOfInterest) throws PrismException
{
- return checkExpression(expr).convertToStateValuesMTBDD().getJDDNode();
+ return checkExpression(expr, statesOfInterest).convertToStateValuesMTBDD().getJDDNode();
}
// -----------------------------------------------------------------------------------
@@ -348,8 +345,12 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
* properties, the vector will be stored symbolically since values are Booleans.
*/
- // Check an 'if-then-else'
- protected StateValues checkExpressionITE(ExpressionITE expr) throws PrismException
+ /**
+ * Check an 'if-then-else' expression.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionITE(ExpressionITE expr, JDDNode statesOfInterest) throws PrismException
{
StateValues res1 = null, res2 = null, res3 = null;
JDDNode dd, dd1, dd2, dd3;
@@ -357,15 +358,17 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
// Check operands recursively
try {
- res1 = checkExpression(expr.getOperand1());
- res2 = checkExpression(expr.getOperand2());
- res3 = checkExpression(expr.getOperand3());
+ res1 = checkExpression(expr.getOperand1(), statesOfInterest.copy());
+ res2 = checkExpression(expr.getOperand2(), statesOfInterest.copy());
+ res3 = checkExpression(expr.getOperand3(), statesOfInterest.copy());
} catch (PrismException e) {
if (res1 != null)
res1.clear();
if (res2 != null)
res2.clear();
throw e;
+ } finally {
+ JDD.Deref(statesOfInterest);
}
// Operand 1 is boolean so should be symbolic
@@ -392,9 +395,12 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
}
}
- // Check a binary operator
-
- protected StateValues checkExpressionBinaryOp(ExpressionBinaryOp expr) throws PrismException
+ /**
+ * Check a binary operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionBinaryOp(ExpressionBinaryOp expr, JDDNode statesOfInterest) throws PrismException
{
StateValues res1 = null, res2 = null;
JDDNode dd, dd1, dd2;
@@ -404,17 +410,19 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
// Optimisations are possible for relational operators
// (note dubious use of knowledge that op IDs are consecutive)
if (op >= ExpressionBinaryOp.EQ && op <= ExpressionBinaryOp.LE) {
- return checkExpressionRelOp(op, expr.getOperand1(), expr.getOperand2());
+ return checkExpressionRelOp(op, expr.getOperand1(), expr.getOperand2(), statesOfInterest);
}
// Check operands recursively
try {
- res1 = checkExpression(expr.getOperand1());
- res2 = checkExpression(expr.getOperand2());
+ res1 = checkExpression(expr.getOperand1(), statesOfInterest.copy());
+ res2 = checkExpression(expr.getOperand2(), statesOfInterest.copy());
} catch (PrismException e) {
if (res1 != null)
res1.clear();
throw e;
+ } finally {
+ JDD.Deref(statesOfInterest);
}
// If both operands are symbolic, result will be symbolic
@@ -490,9 +498,12 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
}
}
- // Check a relational operator (=, !=, >, >=, < <=)
-
- protected StateValues checkExpressionRelOp(int op, Expression expr1, Expression expr2) throws PrismException
+ /**
+ * Check a relational operator (=, !=, >, >=, < <=).
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionRelOp(int op, Expression expr1, Expression expr2, JDDNode statesOfInterest) throws PrismException
{
StateValues res1 = null, res2 = null;
JDDNode dd, dd1, dd2;
@@ -503,6 +514,8 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
// var relop int
if (expr1 instanceof ExpressionVar && expr2.isConstant() && expr2.getType() instanceof TypeInt) {
+ JDD.Deref(statesOfInterest);
+
ExpressionVar e1;
Expression e2;
int i, j, l, h, v;
@@ -553,6 +566,8 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
}
// int relop var
else if (expr1.isConstant() && expr1.getType() instanceof TypeInt && expr2 instanceof ExpressionVar) {
+ JDD.Deref(statesOfInterest);
+
Expression e1;
ExpressionVar e2;
int i, j, l, h, v;
@@ -607,12 +622,14 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
// just convert both operands to MTBDDs first. Optimisations would be possible here.
// Check operands recursively
try {
- res1 = checkExpression(expr1);
- res2 = checkExpression(expr2);
+ res1 = checkExpression(expr1, statesOfInterest.copy());
+ res2 = checkExpression(expr2, statesOfInterest.copy());
} catch (PrismException e) {
if (res1 != null)
res1.clear();
throw e;
+ } finally {
+ JDD.Deref(statesOfInterest);
}
dd1 = res1.convertToStateValuesMTBDD().getJDDNode();
dd2 = res2.convertToStateValuesMTBDD().getJDDNode();
@@ -641,9 +658,12 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
return new StateValuesMTBDD(dd, model);
}
- // Check a unary operator
-
- protected StateValues checkExpressionUnaryOp(ExpressionUnaryOp expr) throws PrismException
+ /**
+ * Check a unary operator.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionUnaryOp(ExpressionUnaryOp expr, JDDNode statesOfInterest) throws PrismException
{
StateValues res1 = null;
JDDNode dd, dd1;
@@ -651,7 +671,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
int i, n, op = expr.getOperator();
// Check operand recursively
- res1 = checkExpression(expr.getOperand());
+ res1 = checkExpression(expr.getOperand(), statesOfInterest);
// Parentheses are easy - nothing to do:
if (op == ExpressionUnaryOp.PARENTH)
@@ -693,29 +713,39 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
}
}
- // Check a 'function'
-
- protected StateValues checkExpressionFunc(ExpressionFunc expr) throws PrismException
+ /**
+ * Check a 'function'.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionFunc(ExpressionFunc expr, JDDNode statesOfInterest) throws PrismException
{
switch (expr.getNameCode()) {
case ExpressionFunc.MIN:
case ExpressionFunc.MAX:
- return checkExpressionFuncNary(expr);
+ return checkExpressionFuncNary(expr, statesOfInterest);
case ExpressionFunc.FLOOR:
case ExpressionFunc.CEIL:
- return checkExpressionFuncUnary(expr);
+ return checkExpressionFuncUnary(expr, statesOfInterest);
case ExpressionFunc.POW:
case ExpressionFunc.MOD:
case ExpressionFunc.LOG:
- return checkExpressionFuncBinary(expr);
+ return checkExpressionFuncBinary(expr, statesOfInterest);
case ExpressionFunc.MULTI:
+ JDD.Deref(statesOfInterest);
throw new PrismException("Multi-objective model checking is not supported for " + model.getModelType() + "s");
default:
+ JDD.Deref(statesOfInterest);
throw new PrismException("Unrecognised function \"" + expr.getName() + "\"");
}
}
- protected StateValues checkExpressionFuncUnary(ExpressionFunc expr) throws PrismException
+ /**
+ * Check a unary 'function'.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionFuncUnary(ExpressionFunc expr, JDDNode statesOfInterest) throws PrismException
{
StateValues res1 = null;
JDDNode dd1;
@@ -723,7 +753,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
int i, n, op = expr.getNameCode();
// Check operand recursively
- res1 = checkExpression(expr.getOperand(0));
+ res1 = checkExpression(expr.getOperand(0), statesOfInterest);
// Symbolic
if (res1 instanceof StateValuesMTBDD) {
dd1 = ((StateValuesMTBDD) res1).getJDDNode();
@@ -759,7 +789,12 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
}
}
- protected StateValues checkExpressionFuncBinary(ExpressionFunc expr) throws PrismException
+ /**
+ * Check a binary 'function'.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionFuncBinary(ExpressionFunc expr, JDDNode statesOfInterest) throws PrismException
{
StateValues res1 = null, res2 = null;
JDDNode dd = null, dd1, dd2;
@@ -769,12 +804,14 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
// Check operands recursively
try {
- res1 = checkExpression(expr.getOperand(0));
- res2 = checkExpression(expr.getOperand(1));
+ res1 = checkExpression(expr.getOperand(0), statesOfInterest.copy());
+ res2 = checkExpression(expr.getOperand(1), statesOfInterest.copy());
} catch (PrismException e) {
if (res1 != null)
res1.clear();
throw e;
+ } finally {
+ JDD.Deref(statesOfInterest);
}
// If both operands are symbolic, result will be symbolic
if (res1 instanceof StateValuesMTBDD && res2 instanceof StateValuesMTBDD) {
@@ -849,7 +886,12 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
}
}
- protected StateValues checkExpressionFuncNary(ExpressionFunc expr) throws PrismException
+ /**
+ * Check an n-ary 'function'.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionFuncNary(ExpressionFunc expr, JDDNode statesOfInterest) throws PrismException
{
StateValues res1 = null, res2 = null;
JDDNode dd1, dd2;
@@ -858,17 +900,18 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
boolean symbolic;
// Check first operand recursively
- res1 = checkExpression(expr.getOperand(0));
+ res1 = checkExpression(expr.getOperand(0), statesOfInterest.copy());
// Go through remaining operands
// Switch to explicit as soon as an operand is explicit
n = expr.getNumOperands();
symbolic = (res1 instanceof StateValuesMTBDD);
for (i = 1; i < n; i++) {
try {
- res2 = checkExpression(expr.getOperand(i));
+ res2 = checkExpression(expr.getOperand(i), statesOfInterest.copy());
} catch (PrismException e) {
if (res2 != null)
res2.clear();
+ JDD.Deref(statesOfInterest);
throw e;
}
// Explicit
@@ -906,14 +949,24 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
}
}
+ JDD.Deref(statesOfInterest);
return res1;
}
- // Check a literal
-
- protected StateValues checkExpressionLiteral(ExpressionLiteral expr) throws PrismException
+ /**
+ * Check a literal.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionLiteral(ExpressionLiteral expr, JDDNode statesOfInterest) throws PrismException
{
JDDNode dd;
+
+ // it's more efficient to return the constant node
+ // instead of a MTBDD function for ITE(statesOfInterest, value, 0),
+ // so we ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
try {
dd = JDD.Constant(expr.evaluateDouble());
} catch (PrismLangException e) {
@@ -922,13 +975,21 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
return new StateValuesMTBDD(dd, model);
}
- // Check a constant
-
- protected StateValues checkExpressionConstant(ExpressionConstant expr) throws PrismException
+ /**
+ * Check a constant.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionConstant(ExpressionConstant expr, JDDNode statesOfInterest) throws PrismException
{
int i;
JDDNode dd;
+ // it's more efficient to return the constant node
+ // instead of a MTBDD function for ITE(statesOfInterest, value, 0),
+ // so we ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
i = constantValues.getIndexOf(expr.getName());
if (i == -1)
throw new PrismException("Couldn't evaluate constant \"" + expr.getName() + "\"");
@@ -941,14 +1002,21 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
return new StateValuesMTBDD(dd, model);
}
- // Check a variable reference
-
- protected StateValues checkExpressionVar(ExpressionVar expr) throws PrismException
+ /**
+ * Check a variable reference.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionVar(ExpressionVar expr, JDDNode statesOfInterest) throws PrismException
{
String s;
int v, l, h, i;
JDDNode dd;
+ // it's generally more efficient not to restrict to statesOfInterest here
+ // so we ignore statesOfInterest
+ JDD.Deref(statesOfInterest);
+
s = expr.getName();
// get the variable's index
v = varList.getIndex(s);
@@ -967,9 +1035,12 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
return new StateValuesMTBDD(dd, model);
}
- // Check label
-
- protected StateValues checkExpressionLabel(ExpressionLabel expr) throws PrismException
+ /**
+ * Check a label.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionLabel(ExpressionLabel expr, JDDNode statesOfInterest) throws PrismException
{
LabelList ll;
JDDNode dd;
@@ -977,14 +1048,17 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
// treat special cases
if (expr.isDeadlockLabel()) {
+ JDD.Deref(statesOfInterest);
dd = model.getDeadlocks();
JDD.Ref(dd);
return new StateValuesMTBDD(dd, model);
} else if (expr.isInitLabel()) {
+ JDD.Deref(statesOfInterest);
dd = start;
JDD.Ref(dd);
return new StateValuesMTBDD(dd, model);
} else if (model.hasLabelDD(expr.getName())) {
+ JDD.Deref(statesOfInterest);
dd = model.getLabelDD(expr.getName());
return new StateValuesMTBDD(dd.copy(), model);
} else {
@@ -996,27 +1070,35 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
if (i == -1)
throw new PrismException("Unknown label \"" + expr.getName() + "\" in property");
// check recursively
- return checkExpression(ll.getLabel(i));
+ return checkExpression(ll.getLabel(i), statesOfInterest);
}
}
- // Check property ref
- protected StateValues checkExpressionProp(ExpressionProp expr) throws PrismException
+ /**
+ * Check a property reference.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionProp(ExpressionProp expr, JDDNode statesOfInterest) throws PrismException
{
// Look up property and check recursively
Property prop = propertiesFile.lookUpPropertyObjectByName(expr.getName());
if (prop != null) {
mainLog.println("\nModel checking : " + prop);
- return checkExpression(prop.getExpression());
+ return checkExpression(prop.getExpression(), statesOfInterest);
} else {
+ JDD.Deref(statesOfInterest);
throw new PrismException("Unknown property reference " + expr);
}
}
- // Check filter
-
- protected StateValues checkExpressionFilter(ExpressionFilter expr) throws PrismException
+ /**
+ * Check a filter.
+ * The result will have valid results at least for the states of interest (use model.getReach().copy() for all reachable states)
+ *
[ REFS: result, DEREFS: statesOfInterest ]
+ */
+ protected StateValues checkExpressionFilter(ExpressionFilter expr, JDDNode statesOfInterest) throws PrismException
{
// Translate filter
Expression filter = expr.getFilter();
@@ -1027,7 +1109,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
boolean filterTrue = Expression.isTrue(filter);
// Store some more info
String filterStatesString = filterTrue ? "all states" : "states satisfying filter";
- JDDNode ddFilter = checkExpressionDD(filter);
+ JDDNode ddFilter = checkExpressionDD(filter, statesOfInterest.copy());
StateListMTBDD statesFilter = new StateListMTBDD(ddFilter, model);
// Check if filter state set is empty; we treat this as an error
if (ddFilter.equals(JDD.ZERO)) {
@@ -1057,10 +1139,11 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
StateValues vals = null;
try {
- // Check operand recursively
- vals = checkExpression(expr.getOperand());
+ // Check operand recursively, using the filter as the states of interest
+ vals = checkExpression(expr.getOperand(), ddFilter.copy());
} catch (PrismException e) {
JDD.Deref(ddFilter);
+ JDD.Deref(statesOfInterest);
throw e;
}
@@ -1364,6 +1447,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
}
// Other derefs
JDD.Deref(ddFilter);
+ JDD.Deref(statesOfInterest);
return resVals;
}
@@ -1416,7 +1500,6 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
return transRewards;
}
- /** Get the constant values (both from the modules file and the properties file) */
@Override
public Values getConstantValues()
{
@@ -1466,7 +1549,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
int numLabels = labelNames.size();
JDDNode labels[] = new JDDNode[numLabels];
for (int i = 0; i < numLabels; i++) {
- labels[i] = checkExpressionDD(new ExpressionLabel(labelNames.get(i)));
+ labels[i] = checkExpressionDD(new ExpressionLabel(labelNames.get(i)), model.getReach().copy());
}
// Export them using the MTBDD engine
diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java
index 66af2465..edd5ddec 100644
--- a/prism/src/prism/StochModelChecker.java
+++ b/prism/src/prism/StochModelChecker.java
@@ -78,14 +78,16 @@ public class StochModelChecker extends ProbModelChecker
// -----------------------------------------------------------------------------------
// bounded until
-
- protected StateValues checkProbBoundedUntil(ExpressionTemporal expr) throws PrismException
+ @Override
+ protected StateValues checkProbBoundedUntil(ExpressionTemporal expr, JDDNode statesOfInterest) throws PrismException
{
double lTime, uTime; // time bounds
Expression exprTmp;
JDDNode b1, b2, tmp;
StateValues tmpProbs = null, probs = null;
+ JDD.Deref(statesOfInterest);
+
// get info from bounded until
// lower bound is 0 if not specified
@@ -115,10 +117,10 @@ public class StochModelChecker extends ProbModelChecker
uTime = -1;
}
- // model check operands first
- b1 = checkExpressionDD(expr.getOperand1());
+ // model check operands first, statesOfInterest = all
+ b1 = checkExpressionDD(expr.getOperand1(), model.getReach().copy());
try {
- b2 = checkExpressionDD(expr.getOperand2());
+ b2 = checkExpressionDD(expr.getOperand2(), model.getReach().copy());
} catch (PrismException e) {
JDD.Deref(b1);
throw e;
@@ -228,13 +230,15 @@ public class StochModelChecker extends ProbModelChecker
}
// cumulative reward
-
- protected StateValues checkRewardCumul(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards)
+ @Override
+ protected StateValues checkRewardCumul(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest)
throws PrismException
{
double time; // time
StateValues rewards = null;
+ JDD.Deref(statesOfInterest);
+
// get info from inst reward
time = expr.getUpperBound().evaluateDouble(constantValues);
if (time < 0) {
@@ -260,12 +264,15 @@ public class StochModelChecker extends ProbModelChecker
// inst reward
- protected StateValues checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards)
+ @Override
+ protected StateValues checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest)
throws PrismException
{
double time; // time
StateValues sr = null, rewards = null;
+ JDD.Deref(statesOfInterest);
+
// get info from inst reward
time = expr.getUpperBound().evaluateDouble(constantValues);
if (time < 0) {
@@ -391,7 +398,7 @@ public class StochModelChecker extends ProbModelChecker
// -----------------------------------------------------------------------------------
// compute probabilities for next
-
+ @Override
protected StateValues computeNextProbs(JDDNode tr, JDDNode b)
{
JDDNode diags, emb;
@@ -491,7 +498,7 @@ public class StochModelChecker extends ProbModelChecker
}
// compute probabilities for until (general case)
-
+ @Override
protected StateValues computeUntilProbs(JDDNode tr, JDDNode tr01, JDDNode b1, JDDNode b2) throws PrismException
{
JDDNode diags, emb;
@@ -555,6 +562,7 @@ public class StochModelChecker extends ProbModelChecker
// compute total rewards
+ @Override
protected StateValues computeTotalRewards(JDDNode tr, JDDNode tr01, JDDNode sr, JDDNode trr) throws PrismException
{
JDDNode diags, emb, srNew;
@@ -587,7 +595,7 @@ public class StochModelChecker extends ProbModelChecker
}
// compute rewards for reach reward
-
+ @Override
protected StateValues computeReachRewards(JDDNode tr, JDDNode tr01, JDDNode sr, JDDNode trr, JDDNode b)
throws PrismException
{