From 23d86799313b4b8e279b6dfe0296b18e4f1a19c0 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 13 Jul 2017 17:00:31 +0000 Subject: [PATCH] Symbolic model checkers: Change the checkXYZ methods to take a stateOfInterest argument Additionally, provide more consistent JavaDoc/@Override annotations for these methods. Often, we are only interested in a subset of the states. E.g., for the top-level expression, PRISM by default only reports on the initial states; for filters, only the filtered states are of interest, etc. By providing a statesOfInterest set to the check methods, they can in principle exploit this knowledge. One prominent candidate is the automata-based LTL model checking, which can start the product construction only from the states of interest instead of from all states. The statesOfInterest information is merely a hint, i.e., a checkXYZ method can return values for more states than those specified as the states of interest. However, the caller should not rely on any results beyond those for the statesOfInterest. This commit only provides the basic infrastructure, i.e., adding the stateOfInterest argument to the method signatures, passing this set to recursive method calls where appropriate, etc, but does not yet exploit this information. Subsequent commits will then begin to exploit this information. The called checkXYZ method is responsible for dereferencing the JDDNode for the statesOfInterest set. Generally, care should be taken that statesOfInterest is indeed an MTBDD over the row-variables of the model and that it is a subset of the reachable states of the model. If one is interested in results for all states, use model.getReach().copy() as the statesOfInterest. An analoguous mechanism already exists for the explicit engine. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12032 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 2 +- prism/src/prism/ModelChecker.java | 27 ++- prism/src/prism/Modules2MTBDD.java | 3 +- prism/src/prism/NonProbModelChecker.java | 83 +++++--- prism/src/prism/NondetModelChecker.java | 228 ++++++++++++++------- prism/src/prism/ProbModelChecker.java | 241 +++++++++++++++------- prism/src/prism/StateModelChecker.java | 245 +++++++++++++++-------- prism/src/prism/StochModelChecker.java | 30 ++- 8 files changed, 591 insertions(+), 268 deletions(-) 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 {