diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index abe95922..d9553805 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -54,17 +54,17 @@ public class CTMCModelChecker extends DTMCModelChecker // Model checking functions @Override - protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax) throws PrismException + protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax, BitSet statesOfInterest) throws PrismException { mainLog.println("Building embedded DTMC..."); DTMC dtmcEmb = ((CTMC)model).buildImplicitEmbeddedDTMC(); // use superclass (DTMCModelChecker) method on the embedded DTMC - return super.checkProbPathFormulaLTL(dtmcEmb, expr, qual, minMax); + return super.checkProbPathFormulaLTL(dtmcEmb, expr, qual, minMax, statesOfInterest); } @Override - protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException + protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { double lTime, uTime; // time bounds Expression exprTmp; @@ -101,9 +101,9 @@ public class CTMCModelChecker extends DTMCModelChecker uTime = -1; } - // model check operands first - b1 = checkExpression(model, expr.getOperand1()).getBitSet(); - b2 = checkExpression(model, expr.getOperand2()).getBitSet(); + // model check operands first for all states + b1 = checkExpression(model, expr.getOperand1(), null).getBitSet(); + b2 = checkExpression(model, expr.getOperand2(), null).getBitSet(); // compute probabilities diff --git a/prism/src/explicit/CTMDPModelChecker.java b/prism/src/explicit/CTMDPModelChecker.java index bee2963d..3b832e3b 100644 --- a/prism/src/explicit/CTMDPModelChecker.java +++ b/prism/src/explicit/CTMDPModelChecker.java @@ -52,7 +52,7 @@ public class CTMDPModelChecker extends MDPModelChecker // Model checking functions @Override - protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException + protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { double uTime; BitSet b1, b2; @@ -66,9 +66,9 @@ public class CTMDPModelChecker extends MDPModelChecker throw new PrismException("Invalid upper bound " + bound + " in time-bounded until formula"); } - // model check operands first - b1 = checkExpression(model, expr.getOperand1()).getBitSet(); - b2 = checkExpression(model, expr.getOperand2()).getBitSet(); + // model check operands first for all states + b1 = checkExpression(model, expr.getOperand1(), null).getBitSet(); + b2 = checkExpression(model, expr.getOperand2(), null).getBitSet(); // compute probabilities diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 98d995c8..bc94d1ca 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -59,7 +59,7 @@ public class DTMCModelChecker extends ProbModelChecker // Model checking functions @Override - protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax) throws PrismException + protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax, BitSet statesOfInterest) throws PrismException { LTLModelChecker mcLtl; StateValues probsProduct, probs; diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index b91e85ca..bb5f274c 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -82,8 +82,8 @@ public class LTLModelChecker extends PrismComponent { // A state formula if (expr.getType() instanceof TypeBool) { - // Model check - StateValues sv = mc.checkExpression(model, expr); + // Model check state formula for all states + StateValues sv = mc.checkExpression(model, expr, null); BitSet bs = sv.getBitSet(); // Detect special cases (true, false) for optimisation if (bs.isEmpty()) { diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 5868db87..1401f111 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -62,7 +62,7 @@ public class MDPModelChecker extends ProbModelChecker // Model checking functions @Override - protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax) throws PrismException + protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax, BitSet statesOfInterest) throws PrismException { LTLModelChecker mcLtl; StateValues probsProduct, probs; diff --git a/prism/src/explicit/NonProbModelChecker.java b/prism/src/explicit/NonProbModelChecker.java index c8e8180b..93dad65a 100644 --- a/prism/src/explicit/NonProbModelChecker.java +++ b/prism/src/explicit/NonProbModelChecker.java @@ -26,6 +26,8 @@ package explicit; +import java.util.BitSet; + import parser.ast.Expression; import parser.ast.ExpressionExists; import parser.ast.ExpressionForAll; @@ -46,7 +48,7 @@ public class NonProbModelChecker extends StateModelChecker } @Override - public StateValues checkExpression(Model model, Expression expr) throws PrismException + public StateValues checkExpression(Model model, Expression expr, BitSet statesOfInterest) throws PrismException { StateValues res; @@ -60,7 +62,7 @@ public class NonProbModelChecker extends StateModelChecker } // Otherwise, use the superclass else { - res = super.checkExpression(model, expr); + res = super.checkExpression(model, expr, statesOfInterest); } return res; diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 28242f22..9a7594c9 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -440,13 +440,13 @@ public class ProbModelChecker extends NonProbModelChecker // Model checking functions @Override - public StateValues checkExpression(Model model, Expression expr) throws PrismException + public StateValues checkExpression(Model model, Expression expr, BitSet statesOfInterest) throws PrismException { StateValues res; // P operator if (expr instanceof ExpressionProb) { - res = checkExpressionProb(model, (ExpressionProb) expr); + res = checkExpressionProb(model, (ExpressionProb) expr, statesOfInterest); } // R operator else if (expr instanceof ExpressionReward) { @@ -458,20 +458,21 @@ public class ProbModelChecker extends NonProbModelChecker } // <<>> operator else if (expr instanceof ExpressionStrategy) { - res = checkExpressionStrategy(model, (ExpressionStrategy) expr); + res = checkExpressionStrategy(model, (ExpressionStrategy) expr, statesOfInterest); } // Otherwise, use the superclass else { - res = super.checkExpression(model, expr); + res = super.checkExpression(model, expr, statesOfInterest); } return res; } /** - * Model check a <<>> or [[]] operator expression and return the values for all states. + * Model check a <<>> or [[]] operator expression and return the values for the statesOfInterest. + * * @param statesOfInterest the states of interest, see checkExpression() */ - protected StateValues checkExpressionStrategy(Model model, ExpressionStrategy expr) throws PrismException + protected StateValues checkExpressionStrategy(Model model, ExpressionStrategy expr, BitSet statesOfInterest) throws PrismException { // Only support <<>> right now, not [[]] if (!expr.isThereExists()) @@ -490,7 +491,7 @@ public class ProbModelChecker extends NonProbModelChecker // Pass onto relevant method: // P operator if (exprSub instanceof ExpressionProb) { - return checkExpressionProb(model, (ExpressionProb) exprSub, false, coalition); + return checkExpressionProb(model, (ExpressionProb) exprSub, false, coalition, statesOfInterest); } // R operator else if (exprSub instanceof ExpressionReward) { @@ -503,30 +504,32 @@ public class ProbModelChecker extends NonProbModelChecker } /** - * Model check a P operator expression and return the values for all states. + * Model check a P operator expression and return the values for the statesOfInterest. + * @param statesOfInterest the states of interest, see checkExpression() */ - protected StateValues checkExpressionProb(Model model, ExpressionProb expr) throws PrismException + protected StateValues checkExpressionProb(Model model, ExpressionProb expr, BitSet statesOfInterest) throws PrismException { // Use the default semantics for a standalone P operator // (i.e. quantification over all strategies, and no game-coalition info) - return checkExpressionProb(model, expr, true, null); + return checkExpressionProb(model, expr, true, null, statesOfInterest); } /** - * Model check a P operator expression and return the values for all states. + * Model check a P operator expression and return the values for the states of interest. * @param model The model * @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 coalition If relevant, info about which set of players this P operator refers to + * @param statesOfInterest the states of interest, see checkExpression() */ - protected StateValues checkExpressionProb(Model model, ExpressionProb expr, boolean forAll, Coalition coalition) throws PrismException + protected StateValues checkExpressionProb(Model model, ExpressionProb expr, boolean forAll, Coalition coalition, BitSet statesOfInterest) throws PrismException { // Get info from P operator OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues); MinMax minMax = opInfo.getMinMax(model.getModelType()); // Compute probabilities - StateValues probs = checkProbPathFormula(model, expr.getExpression(), minMax); + StateValues probs = checkProbPathFormula(model, expr.getExpression(), minMax, statesOfInterest); // Print out probabilities if (getVerbosity() > 5) { @@ -548,22 +551,23 @@ public class ProbModelChecker extends NonProbModelChecker /** * Compute probabilities for the contents of a P operator. + * @param statesOfInterest the states of interest, see checkExpression() */ - protected StateValues checkProbPathFormula(Model model, Expression expr, MinMax minMax) throws PrismException + protected StateValues checkProbPathFormula(Model model, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { // Test whether this is a simple path formula (i.e. PCTL) // and then pass control to appropriate method. if (expr.isSimplePathFormula()) { - return checkProbPathFormulaSimple(model, expr, minMax); + return checkProbPathFormulaSimple(model, expr, minMax, statesOfInterest); } else { - return checkProbPathFormulaLTL(model, expr, false, minMax); + return checkProbPathFormulaLTL(model, expr, false, minMax, statesOfInterest); } } /** * Compute probabilities for a simple, non-LTL path operator. */ - protected StateValues checkProbPathFormulaSimple(Model model, Expression expr, MinMax minMax) throws PrismException + protected StateValues checkProbPathFormulaSimple(Model model, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { StateValues probs = null; @@ -573,12 +577,12 @@ public class ProbModelChecker extends NonProbModelChecker // Parentheses if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) { // Recurse - probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), minMax); + probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), minMax, statesOfInterest); } // Negation else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) { // Compute, then subtract from 1 - probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), minMax.negate()); + probs = checkProbPathFormulaSimple(model, exprUnary.getOperand(), minMax.negate(), statesOfInterest); probs.timesConstant(-1.0); probs.plusConstant(1.0); } @@ -588,19 +592,19 @@ public class ProbModelChecker extends NonProbModelChecker ExpressionTemporal exprTemp = (ExpressionTemporal) expr; // Next if (exprTemp.getOperator() == ExpressionTemporal.P_X) { - probs = checkProbNext(model, exprTemp, minMax); + probs = checkProbNext(model, exprTemp, minMax, statesOfInterest); } // Until else if (exprTemp.getOperator() == ExpressionTemporal.P_U) { if (exprTemp.hasBounds()) { - probs = checkProbBoundedUntil(model, exprTemp, minMax); + probs = checkProbBoundedUntil(model, exprTemp, minMax, statesOfInterest); } else { - probs = checkProbUntil(model, exprTemp, minMax); + probs = checkProbUntil(model, exprTemp, minMax, statesOfInterest); } } // Anything else - convert to until and recurse else { - probs = checkProbPathFormulaSimple(model, exprTemp.convertToUntilForm(), minMax); + probs = checkProbPathFormulaSimple(model, exprTemp.convertToUntilForm(), minMax, statesOfInterest); } } @@ -613,10 +617,10 @@ public class ProbModelChecker extends NonProbModelChecker /** * Compute probabilities for a next operator. */ - protected StateValues checkProbNext(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException + protected StateValues checkProbNext(Model model, ExpressionTemporal expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { - // Model check the operand - BitSet target = checkExpression(model, expr.getOperand2()).getBitSet(); + // Model check the operand for all states + BitSet target = checkExpression(model, expr.getOperand2(), null).getBitSet(); // Compute/return the probabilities ModelCheckerResult res = null; @@ -642,7 +646,7 @@ public class ProbModelChecker extends NonProbModelChecker /** * Compute probabilities for a bounded until operator. */ - protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException + protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { // This method just handles discrete time // Continuous-time model checkers will override this method @@ -656,9 +660,9 @@ public class ProbModelChecker extends NonProbModelChecker throw new PrismException("Invalid bound " + bound + " in bounded until formula"); } - // Model check operands - BitSet remain = checkExpression(model, expr.getOperand1()).getBitSet(); - BitSet target = checkExpression(model, expr.getOperand2()).getBitSet(); + // Model check operands for all states + BitSet remain = checkExpression(model, expr.getOperand1(), null).getBitSet(); + BitSet target = checkExpression(model, expr.getOperand2(), null).getBitSet(); // Compute/return the probabilities // A trivial case: "U<=0" (prob is 1 in target states, 0 otherwise) @@ -686,11 +690,11 @@ public class ProbModelChecker extends NonProbModelChecker /** * Compute probabilities for an (unbounded) until operator. */ - protected StateValues checkProbUntil(Model model, ExpressionTemporal expr, MinMax minMax) throws PrismException + protected StateValues checkProbUntil(Model model, ExpressionTemporal expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { - // Model check operands - BitSet remain = checkExpression(model, expr.getOperand1()).getBitSet(); - BitSet target = checkExpression(model, expr.getOperand2()).getBitSet(); + // Model check operands for all states + BitSet remain = checkExpression(model, expr.getOperand1(), null).getBitSet(); + BitSet target = checkExpression(model, expr.getOperand2(), null).getBitSet(); // Compute/return the probabilities ModelCheckerResult res = null; @@ -717,7 +721,7 @@ public class ProbModelChecker extends NonProbModelChecker /** * Compute probabilities for an LTL path formula */ - protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax) throws PrismException + protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax, BitSet statesOfInterest) throws PrismException { // To be overridden by subclasses throw new PrismException("Computation not implemented yet"); @@ -822,8 +826,8 @@ public class ProbModelChecker extends NonProbModelChecker */ protected StateValues checkRewardReach(Model model, Rewards modelRewards, ExpressionTemporal expr, MinMax minMax) throws PrismException { - // Model check the operand - BitSet target = checkExpression(model, expr.getOperand2()).getBitSet(); + // Model check the operand for all states + BitSet target = checkExpression(model, expr.getOperand2(), null).getBitSet(); // Compute/return the rewards ModelCheckerResult res = null; @@ -958,8 +962,8 @@ public class ProbModelChecker extends NonProbModelChecker */ protected StateValues checkSteadyStateFormula(Model model, Expression expr, MinMax minMax) throws PrismException { - // Model check operand - BitSet b = checkExpression(model, expr).getBitSet(); + // Model check operand for all states + BitSet b = checkExpression(model, expr, null).getBitSet(); // Compute/return the probabilities ModelCheckerResult res = null; diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java index 626cb28c..b7d111ba 100644 --- a/prism/src/explicit/STPGModelChecker.java +++ b/prism/src/explicit/STPGModelChecker.java @@ -55,7 +55,7 @@ public class STPGModelChecker extends ProbModelChecker // Model checking functions @Override - protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax) throws PrismException + protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax, BitSet statesOfInterest) throws PrismException { throw new PrismException("LTL model checking not yet supported for stochastic games"); } diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index a7c4fc8e..b8e5ee4c 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -313,7 +313,8 @@ public class StateModelChecker extends PrismComponent // Do model checking and store result vector timer = System.currentTimeMillis(); - vals = checkExpression(model, expr); + // check expression for all states (null => statesOfInterest=all) + vals = checkExpression(model, expr, null); timer = System.currentTimeMillis() - timer; mainLog.println("\nTime for model checking: " + timer / 1000.0 + " seconds."); @@ -338,26 +339,28 @@ public class StateModelChecker extends PrismComponent * For other required info (labels, reward structures, etc.), use the methods * {@link #setModulesFile} and {@link #setPropertiesFile} * to attach the original model/properties files. + * @param statesOfInterest a set of states for which results should be calculated (null = all states). + * The calculated values for states not of interest are arbitrary and should to be ignored. */ - public StateValues checkExpression(Model model, Expression expr) throws PrismException + public StateValues checkExpression(Model model, Expression expr, BitSet statesOfInterest) throws PrismException { StateValues res = null; // If-then-else if (expr instanceof ExpressionITE) { - res = checkExpressionITE(model, (ExpressionITE) expr); + res = checkExpressionITE(model, (ExpressionITE) expr, statesOfInterest); } // Binary ops else if (expr instanceof ExpressionBinaryOp) { - res = checkExpressionBinaryOp(model, (ExpressionBinaryOp) expr); + res = checkExpressionBinaryOp(model, (ExpressionBinaryOp) expr, statesOfInterest); } // Unary ops else if (expr instanceof ExpressionUnaryOp) { - res = checkExpressionUnaryOp(model, (ExpressionUnaryOp) expr); + res = checkExpressionUnaryOp(model, (ExpressionUnaryOp) expr, statesOfInterest); } // Functions else if (expr instanceof ExpressionFunc) { - res = checkExpressionFunc(model, (ExpressionFunc) expr); + res = checkExpressionFunc(model, (ExpressionFunc) expr, statesOfInterest); } // Identifiers else if (expr instanceof ExpressionIdent) { @@ -376,25 +379,25 @@ public class StateModelChecker extends PrismComponent else if (expr instanceof ExpressionFormula) { // This should have been defined or expanded by now. if (((ExpressionFormula) expr).getDefinition() != null) - return checkExpression(model, ((ExpressionFormula) expr).getDefinition()); + return checkExpression(model, ((ExpressionFormula) expr).getDefinition(), statesOfInterest); else throw new PrismException("Unexpanded formula \"" + ((ExpressionFormula) expr).getName() + "\""); } // Variables else if (expr instanceof ExpressionVar) { - res = checkExpressionVar(model, (ExpressionVar) expr); + res = checkExpressionVar(model, (ExpressionVar) expr, statesOfInterest); } // Labels else if (expr instanceof ExpressionLabel) { - res = checkExpressionLabel(model, (ExpressionLabel) expr); + res = checkExpressionLabel(model, (ExpressionLabel) expr, statesOfInterest); } // Property refs else if (expr instanceof ExpressionProp) { - res = checkExpressionProp(model, (ExpressionProp) expr); + res = checkExpressionProp(model, (ExpressionProp) expr, statesOfInterest); } // Filter else if (expr instanceof ExpressionFilter) { - res = checkExpressionFilter(model, (ExpressionFilter) expr); + res = checkExpressionFilter(model, (ExpressionFilter) expr, statesOfInterest); } // Anything else - error else { @@ -406,16 +409,17 @@ public class StateModelChecker extends PrismComponent /** * Model check a binary operator. + * @param statesOfInterest the states of interest, see checkExpression() */ - protected StateValues checkExpressionITE(Model model, ExpressionITE expr) throws PrismException + protected StateValues checkExpressionITE(Model model, ExpressionITE expr, BitSet statesOfInterest) throws PrismException { StateValues res1 = null, res2 = null, res3 = null; // Check operands recursively try { - res1 = checkExpression(model, expr.getOperand1()); - res2 = checkExpression(model, expr.getOperand2()); - res3 = checkExpression(model, expr.getOperand3()); + res1 = checkExpression(model, expr.getOperand1(), statesOfInterest); + res2 = checkExpression(model, expr.getOperand2(), statesOfInterest); + res3 = checkExpression(model, expr.getOperand3(), statesOfInterest); } catch (PrismException e) { if (res1 != null) res1.clear(); @@ -434,16 +438,17 @@ public class StateModelChecker extends PrismComponent /** * Model check a binary operator. + * @param statesOfInterest the states of interest, see checkExpression() */ - protected StateValues checkExpressionBinaryOp(Model model, ExpressionBinaryOp expr) throws PrismException + protected StateValues checkExpressionBinaryOp(Model model, ExpressionBinaryOp expr, BitSet statesOfInterest) throws PrismException { StateValues res1 = null, res2 = null; int op = expr.getOperator(); // Check operands recursively try { - res1 = checkExpression(model, expr.getOperand1()); - res2 = checkExpression(model, expr.getOperand2()); + res1 = checkExpression(model, expr.getOperand1(), statesOfInterest); + res2 = checkExpression(model, expr.getOperand2(), statesOfInterest); } catch (PrismException e) { if (res1 != null) res1.clear(); @@ -459,14 +464,15 @@ public class StateModelChecker extends PrismComponent /** * Model check a unary operator. + * @param statesOfInterest the states of interest, see checkExpression() */ - protected StateValues checkExpressionUnaryOp(Model model, ExpressionUnaryOp expr) throws PrismException + protected StateValues checkExpressionUnaryOp(Model model, ExpressionUnaryOp expr, BitSet statesOfInterest) throws PrismException { StateValues res1 = null; int op = expr.getOperator(); // Check operand recursively - res1 = checkExpression(model, expr.getOperand()); + res1 = checkExpression(model, expr.getOperand(), statesOfInterest); // Parentheses are easy - nothing to do: if (op == ExpressionUnaryOp.PARENTH) @@ -480,20 +486,21 @@ public class StateModelChecker extends PrismComponent /** * Model check a function. + * @param statesOfInterest the states of interest, see checkExpression() */ - protected StateValues checkExpressionFunc(Model model, ExpressionFunc expr) throws PrismException + protected StateValues checkExpressionFunc(Model model, ExpressionFunc expr, BitSet statesOfInterest) throws PrismException { switch (expr.getNameCode()) { case ExpressionFunc.MIN: case ExpressionFunc.MAX: - return checkExpressionFuncNary(model, expr); + return checkExpressionFuncNary(model, expr, statesOfInterest); case ExpressionFunc.FLOOR: case ExpressionFunc.CEIL: - return checkExpressionFuncUnary(model, expr); + return checkExpressionFuncUnary(model, expr, statesOfInterest); case ExpressionFunc.POW: case ExpressionFunc.MOD: case ExpressionFunc.LOG: - return checkExpressionFuncBinary(model, expr); + return checkExpressionFuncBinary(model, expr, statesOfInterest); case ExpressionFunc.MULTI: throw new PrismException("Multi-objective model checking is not supported for " + model.getModelType() + "s"); default: @@ -501,13 +508,13 @@ public class StateModelChecker extends PrismComponent } } - protected StateValues checkExpressionFuncUnary(Model model, ExpressionFunc expr) throws PrismException + protected StateValues checkExpressionFuncUnary(Model model, ExpressionFunc expr, BitSet statesOfInterest) throws PrismException { StateValues res1 = null; int op = expr.getNameCode(); // Check operand recursively - res1 = checkExpression(model, expr.getOperand(0)); + res1 = checkExpression(model, expr.getOperand(0), statesOfInterest); // Apply operation try { @@ -523,15 +530,15 @@ public class StateModelChecker extends PrismComponent return res1; } - protected StateValues checkExpressionFuncBinary(Model model, ExpressionFunc expr) throws PrismException + protected StateValues checkExpressionFuncBinary(Model model, ExpressionFunc expr, BitSet statesOfInterest) throws PrismException { StateValues res1 = null, res2 = null; int op = expr.getNameCode(); // Check operands recursively try { - res1 = checkExpression(model, expr.getOperand(0)); - res2 = checkExpression(model, expr.getOperand(1)); + res1 = checkExpression(model, expr.getOperand(0), statesOfInterest); + res2 = checkExpression(model, expr.getOperand(1), statesOfInterest); } catch (PrismException e) { if (res1 != null) res1.clear(); @@ -555,19 +562,19 @@ public class StateModelChecker extends PrismComponent return res1; } - protected StateValues checkExpressionFuncNary(Model model, ExpressionFunc expr) throws PrismException + protected StateValues checkExpressionFuncNary(Model model, ExpressionFunc expr, BitSet statesOfInterest) throws PrismException { StateValues res1 = null, res2 = null; int i, n, op = expr.getNameCode(); // Check first operand recursively - res1 = checkExpression(model, expr.getOperand(0)); + res1 = checkExpression(model, expr.getOperand(0), statesOfInterest); // Go through remaining operands n = expr.getNumOperands(); for (i = 1; i < n; i++) { // Check next operand recursively try { - res2 = checkExpression(model, expr.getOperand(i)); + res2 = checkExpression(model, expr.getOperand(i), statesOfInterest); } catch (PrismException e) { if (res2 != null) res2.clear(); @@ -609,9 +616,12 @@ public class StateModelChecker extends PrismComponent /** * Model check a variable reference. + * @param statesOfInterest the states of interest, see checkExpression() */ - protected StateValues checkExpressionVar(Model model, ExpressionVar expr) throws PrismException + protected StateValues checkExpressionVar(Model model, ExpressionVar expr, BitSet statesOfInterest) throws PrismException { + // TODO (JK): optimize evaluation using statesOfInterest + int numStates = model.getNumStates(); StateValues res = new StateValues(expr.getType(), model); List statesList = model.getStatesList(); @@ -633,9 +643,12 @@ public class StateModelChecker extends PrismComponent /** * Model check a label. + * @param statesOfInterest the states of interest, see checkExpression() */ - protected StateValues checkExpressionLabel(Model model, ExpressionLabel expr) throws PrismException + protected StateValues checkExpressionLabel(Model model, ExpressionLabel expr, BitSet statesOfInterest) throws PrismException { + // TODO: optimize evaluation using statesOfInterest + LabelList ll; int i; @@ -666,19 +679,19 @@ public class StateModelChecker extends PrismComponent if (i == -1) throw new PrismException("Unknown label \"" + expr.getName() + "\" in property"); // check recursively - return checkExpression(model, ll.getLabel(i)); + return checkExpression(model, ll.getLabel(i), statesOfInterest); } } // Check property ref - protected StateValues checkExpressionProp(Model model, ExpressionProp expr) throws PrismException + protected StateValues checkExpressionProp(Model model, ExpressionProp expr, BitSet 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(model, prop.getExpression()); + return checkExpression(model, prop.getExpression(), statesOfInterest); } else { throw new PrismException("Unknown property reference " + expr); } @@ -686,7 +699,7 @@ public class StateModelChecker extends PrismComponent // Check filter - protected StateValues checkExpressionFilter(Model model, ExpressionFilter expr) throws PrismException + protected StateValues checkExpressionFilter(Model model, ExpressionFilter expr, BitSet statesOfInterest) throws PrismException { // Filter info Expression filter; @@ -712,7 +725,10 @@ public class StateModelChecker extends PrismComponent filterTrue = Expression.isTrue(filter); // Store some more info filterStatesString = filterTrue ? "all states" : "states satisfying filter"; - bsFilter = checkExpression(model, filter).getBitSet(); + + // get the BitSet of states matching the filter, without taking statesOfInterest into account + bsFilter = checkExpression(model, filter, null).getBitSet(); + // Check if filter state set is empty; we treat this as an error if (bsFilter.isEmpty()) { throw new PrismException("Filter satisfies no states"); @@ -733,8 +749,8 @@ public class StateModelChecker extends PrismComponent currentFilter = null; } - // Check operand recursively - vals = checkExpression(model, expr.getOperand()); + // Check operand recursively, using bsFilter as statesOfInterest + vals = checkExpression(model, expr.getOperand(), bsFilter); // Print out number of states satisfying filter if (!filterInit) @@ -1090,7 +1106,7 @@ public class StateModelChecker extends PrismComponent // Model check StateValues sv; try { - sv = mc.checkExpression(model, e); + sv = mc.checkExpression(model, e, null); } catch (PrismException ex) { throw new PrismLangException(ex.getMessage()); }