diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 91ed563e..2ebbda98 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -43,7 +43,6 @@ import parser.type.TypeDouble; import parser.type.TypePathBool; import parser.type.TypePathDouble; import prism.IntegerBound; -import prism.ModelType; import prism.OpRelOpBound; import prism.PrismComponent; import prism.PrismException; @@ -468,8 +467,12 @@ public class ProbModelChecker extends NonProbModelChecker { StateValues res; + // <<>> or [[]] operator + if (expr instanceof ExpressionStrategy) { + res = checkExpressionStrategy(model, (ExpressionStrategy) expr, statesOfInterest); + } // P operator - if (expr instanceof ExpressionProb) { + else if (expr instanceof ExpressionProb) { res = checkExpressionProb(model, (ExpressionProb) expr, statesOfInterest); } // R operator @@ -480,10 +483,6 @@ public class ProbModelChecker extends NonProbModelChecker else if (expr instanceof ExpressionSS) { res = checkExpressionSteadyState(model, (ExpressionSS) expr); } - // <<>> operator - else if (expr instanceof ExpressionStrategy) { - res = checkExpressionStrategy(model, (ExpressionStrategy) expr, statesOfInterest); - } // Otherwise, use the superclass else { res = super.checkExpression(model, expr, statesOfInterest); @@ -498,28 +497,36 @@ public class ProbModelChecker extends NonProbModelChecker */ protected StateValues checkExpressionStrategy(Model model, ExpressionStrategy expr, BitSet statesOfInterest) throws PrismException { - // Only support <<>> right now, not [[]] - if (!expr.isThereExists()) - throw new PrismNotSupportedException("The " + expr.getOperatorString() + " operator is not yet supported"); - - // Only support <<>> for MDPs right now + // Only support <<>>/[[]] for MDPs right now if (!(this instanceof MDPModelChecker)) throw new PrismNotSupportedException("The " + expr.getOperatorString() + " operator is only supported for MDPs currently"); + // Will we be quantifying universally or existentially over strategies/adversaries? + boolean forAll = !expr.isThereExists(); + // Extract coalition info Coalition coalition = expr.getCoalition(); - // Strip any parentheses (they might have been needless wrapped around a single P or R) + // For non-games (i.e., models with a single player), deal with the coalition operator here and then remove it + if (coalition != null && !model.getModelType().multiplePlayers()) { + if (coalition.isEmpty()) { + // An empty coalition negates the quantification ("*" has no effect) + forAll = !forAll; + } + coalition = null; + } + + // Strip any parentheses (they might have been needlessly wrapped around a single P or R) Expression exprSub = expr.getExpression(); while (Expression.isParenth(exprSub)) exprSub = ((ExpressionUnaryOp) exprSub).getOperand(); // Pass onto relevant method: // P operator if (exprSub instanceof ExpressionProb) { - return checkExpressionProb(model, (ExpressionProb) exprSub, false, coalition, statesOfInterest); + return checkExpressionProb(model, (ExpressionProb) exprSub, forAll, coalition, statesOfInterest); } // R operator else if (exprSub instanceof ExpressionReward) { - return checkExpressionReward(model, (ExpressionReward) exprSub, false, coalition, statesOfInterest); + return checkExpressionReward(model, (ExpressionReward) exprSub, forAll, coalition, statesOfInterest); } // Anything else is an error else { @@ -550,16 +557,8 @@ public class ProbModelChecker extends NonProbModelChecker { // Get info from P operator OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues); - MinMax minMax = opInfo.getMinMax(model.getModelType()); + MinMax minMax = opInfo.getMinMax(model.getModelType(), forAll); - // Deal with coalition operator, if present (just MDPs, currently) - if (coalition != null && model.getModelType() == ModelType.MDP) { - if (coalition.isEmpty()) { - // An empty coalition negates the min/max ("*" has no effect) - minMax = minMax.negate(); - } - } - // Compute probabilities StateValues probs = checkProbPathFormula(model, expr.getExpression(), minMax, statesOfInterest); @@ -827,10 +826,12 @@ public class ProbModelChecker extends NonProbModelChecker } /** - * Model check a P operator expression and return the values for all states. + * Model check an R operator expression and return the values for all states. */ protected StateValues checkExpressionReward(Model model, ExpressionReward expr, BitSet statesOfInterest) throws PrismException { + // Use the default semantics for a standalone R operator + // (i.e. quantification over all strategies, and no game-coalition info) return checkExpressionReward(model, expr, true, null, statesOfInterest); } @@ -841,7 +842,7 @@ public class ProbModelChecker extends NonProbModelChecker { // Get info from R operator OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues); - MinMax minMax = opInfo.getMinMax(model.getModelType()); + MinMax minMax = opInfo.getMinMax(model.getModelType(), forAll); // Build rewards RewardStruct rewStruct = expr.getRewardStructByIndexObject(modulesFile, constantValues); diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 4865b306..8cb58c99 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -43,11 +43,13 @@ import jdd.JDDNode; import jdd.JDDVars; import mtbdd.PrismMTBDD; import odd.ODDUtils; +import parser.ast.Coalition; import parser.ast.Expression; import parser.ast.ExpressionFunc; import parser.ast.ExpressionProb; import parser.ast.ExpressionQuant; import parser.ast.ExpressionReward; +import parser.ast.ExpressionStrategy; import parser.ast.ExpressionTemporal; import parser.ast.ExpressionUnaryOp; import parser.ast.PropertiesFile; @@ -142,8 +144,12 @@ public class NondetModelChecker extends NonProbModelChecker { StateValues res; + // <<>> or [[]] operator + if (expr instanceof ExpressionStrategy) { + res = checkExpressionStrategy((ExpressionStrategy) expr); + } // P operator - if (expr instanceof ExpressionProb) { + else if (expr instanceof ExpressionProb) { res = checkExpressionProb((ExpressionProb) expr); } // R operator @@ -174,14 +180,64 @@ public class NondetModelChecker extends NonProbModelChecker return res; } + /** + * Model check a <<>> or [[]] operator expression and return the values for all states. + */ + protected StateValues checkExpressionStrategy(ExpressionStrategy expr) throws PrismException + { + // Will we be quantifying universally or existentially over strategies/adversaries? + boolean forAll = !expr.isThereExists(); + + // Extract coalition info + Coalition coalition = expr.getCoalition(); + // Deal with the coalition operator here and then remove it + if (coalition != null) { + if (coalition.isEmpty()) { + // An empty coalition negates the quantification ("*" has no effect) + forAll = !forAll; + } + coalition = null; + } + + // Strip any parentheses (they might have been needlessly wrapped around a single P or R) + Expression exprSub = expr.getExpression(); + while (Expression.isParenth(exprSub)) + exprSub = ((ExpressionUnaryOp) exprSub).getOperand(); + // Pass onto relevant method: + // P operator + if (exprSub instanceof ExpressionProb) { + return checkExpressionProb((ExpressionProb) exprSub, forAll); + } + // R operator + else if (exprSub instanceof ExpressionReward) { + return checkExpressionReward((ExpressionReward) exprSub, forAll); + } + // Anything else is an error + else { + throw new PrismException("Unexpected operators in " + expr.getOperatorString() + " operator"); + } + } + /** * Model check a P operator expression and return the values for all states. */ protected StateValues checkExpressionProb(ExpressionProb expr) throws PrismException + { + // Use the default semantics for a standalone P operator + // (i.e. quantification over all strategies) + return checkExpressionProb(expr, true); + } + + /** + * Model check a P operator expression and return the values for all states. + * @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] + */ + protected StateValues checkExpressionProb(ExpressionProb expr, boolean forAll) throws PrismException { // Get info from P operator OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues); - MinMax minMax = opInfo.getMinMax(model.getModelType()); + MinMax minMax = opInfo.getMinMax(model.getModelType(), forAll); // Check for trivial (i.e. stupid) cases if (opInfo.isTriviallyTrue()) { @@ -220,13 +276,25 @@ public class NondetModelChecker extends NonProbModelChecker } /** - * Model check an R operator expression and return the values for all states. + * Model check n R operator expression and return the values for all states. */ protected StateValues checkExpressionReward(ExpressionReward expr) throws PrismException + { + // Use the default semantics for a standalone R operator + // (i.e. quantification over all strategies) + return checkExpressionReward(expr, true); + } + + /** + * Model check an R operator expression and return the values for all states. + * @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] + */ + protected StateValues checkExpressionReward(ExpressionReward expr, boolean forAll) throws PrismException { // Get info from R operator OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues); - MinMax minMax = opInfo.getMinMax(model.getModelType()); + MinMax minMax = opInfo.getMinMax(model.getModelType(), forAll); // Get rewards Object rs = expr.getRewardStructIndex(); diff --git a/prism/src/prism/OpRelOpBound.java b/prism/src/prism/OpRelOpBound.java index 3cd33962..3fae2822 100644 --- a/prism/src/prism/OpRelOpBound.java +++ b/prism/src/prism/OpRelOpBound.java @@ -79,16 +79,28 @@ public class OpRelOpBound } public MinMax getMinMax(ModelType modelType) throws PrismException + { + return getMinMax(modelType, true); + } + + public MinMax getMinMax(ModelType modelType, boolean forAll) throws PrismException { MinMax minMax = MinMax.blank(); if (modelType.nondeterministic()) { - if (relOp == RelOp.EQ && isNumeric()) { - throw new PrismException("Can't use \"" + op + "=?\" for nondeterministic models; use e.g. \"" + op + "min=?\" or \"" + op + "max=?\""); + if (!(modelType == ModelType.MDP || modelType == ModelType.CTMDP)) { + throw new PrismException("Don't know how to model check " + getTypeOfOperator() + " properties for " + modelType + "s"); } - if (modelType == ModelType.MDP || modelType == ModelType.CTMDP) { - minMax = (relOp.isLowerBound() || relOp.isMin()) ? MinMax.min() : MinMax.max(); + if (isNumeric()) { + if (relOp == RelOp.EQ) { + throw new PrismException("Can't use \"" + op + "=?\" for nondeterministic models; use e.g. \"" + op + "min=?\" or \"" + op + "max=?\""); + } + minMax = relOp.isMin() ? MinMax.min() : MinMax.max(); } else { - throw new PrismException("Don't know how to model check " + getTypeOfOperator() + " properties for " + modelType + "s"); + if (forAll) { + minMax = (relOp.isLowerBound() ) ? MinMax.min() : MinMax.max(); + } else { + minMax = (relOp.isLowerBound() ) ? MinMax.max() : MinMax.min(); + } } } return minMax;