From 0bb55587be13e97f20182d87f0d21b62d354f055 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 26 Dec 2014 23:53:28 +0000 Subject: [PATCH] Allow <<>> to be used for MDPs (explicit engine only). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9444 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MinMax.java | 5 ++ prism/src/explicit/ProbModelChecker.java | 96 +++++++++++++++++++++- prism/src/parser/ast/ExpressionProb.java | 11 +++ prism/src/parser/ast/ExpressionReward.java | 11 +++ 4 files changed, 120 insertions(+), 3 deletions(-) diff --git a/prism/src/explicit/MinMax.java b/prism/src/explicit/MinMax.java index 97313463..c38371bf 100644 --- a/prism/src/explicit/MinMax.java +++ b/prism/src/explicit/MinMax.java @@ -84,6 +84,11 @@ public class MinMax // Utility methods to create instances of this class + public static MinMax blank() + { + return new MinMax(); + } + public static MinMax min() { MinMax minMax = new MinMax(); diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 47583de0..3939694b 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -27,16 +27,19 @@ package explicit; import java.util.BitSet; +import java.util.List; import parser.ast.Expression; import parser.ast.ExpressionProb; import parser.ast.ExpressionReward; import parser.ast.ExpressionSS; +import parser.ast.ExpressionStrategy; import parser.ast.ExpressionTemporal; import parser.ast.ExpressionUnaryOp; import parser.ast.RelOp; import parser.ast.RewardStruct; import parser.type.TypeDouble; +import prism.ModelType; import prism.PrismComponent; import prism.PrismException; import prism.PrismSettings; @@ -454,6 +457,10 @@ 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); + } // Otherwise, use the superclass else { res = super.checkExpression(model, expr); @@ -462,14 +469,65 @@ public class ProbModelChecker extends NonProbModelChecker return res; } + /** + * Model check a <<>> or [[]] operator expression and return the values for all states. + */ + protected StateValues checkExpressionStrategy(Model model, ExpressionStrategy expr) throws PrismException + { + // Only support <<>> right now, not [[]] + if (!expr.isThereExists()) + throw new PrismException("The " + expr.getOperatorString() + " operator is not yet supported"); + + // Only support <<>> for MDPs right now + if (!(this instanceof MDPModelChecker)) + throw new PrismException("The " + expr.getOperatorString() + " operator is only supported for MDPs currently"); + + // Extract coalition info + List coalition = expr.getCoalition(); + // Strip any parentheses (they might have been needless 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); + } + // R operator + else if (exprSub instanceof ExpressionReward) { + return checkExpressionReward(model, (ExpressionReward) exprSub, false, coalition); + } + // 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(Model model, ExpressionProb expr) 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); + } + + /** + * Model check a P operator expression and return the values for all states. + * @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 + */ + protected StateValues checkExpressionProb(Model model, ExpressionProb expr, boolean forAll, List coalition) throws PrismException { Expression pb; // Probability bound (expression) double p = 0; // Probability bound (actual value) RelOp relOp; // Relational operator + MinMax minMax = MinMax.blank(); + ModelType modelType = model.getModelType(); + StateValues probs = null; // Get info from P operator @@ -481,8 +539,19 @@ public class ProbModelChecker extends NonProbModelChecker throw new PrismException("Invalid probability bound " + p + " in P operator"); } + // For nondeterministic models, determine whether min or max probabilities needed + if (modelType.nondeterministic()) { + if (relOp == RelOp.EQ && pb == null) { + throw new PrismException("Can't use \"P=?\" for nondeterministic models; use \"Pmin=?\" or \"Pmax=?\""); + } + if (modelType == ModelType.MDP || modelType == ModelType.CTMDP) { + minMax = (relOp.isLowerBound() || relOp.isMin()) ? MinMax.min() : MinMax.max(); + } else { + throw new PrismException("Don't know how to model check " + expr.getTypeOfPOperator() + " properties for " + modelType + "s"); + } + } + // Compute probabilities - MinMax minMax = (relOp.isLowerBound() || relOp.isMin()) ? MinMax.min() : MinMax.max(); probs = checkProbPathFormula(model, expr.getExpression(), minMax); // Print out probabilities @@ -681,13 +750,23 @@ public class ProbModelChecker extends NonProbModelChecker } /** - * Model check an R operator expression and return the values for all states. + * Model check a P operator expression and return the values for all states. */ protected StateValues checkExpressionReward(Model model, ExpressionReward expr) throws PrismException + { + return checkExpressionReward(model, expr, true, null); + } + + /** + * Model check an R operator expression and return the values for all states. + */ + protected StateValues checkExpressionReward(Model model, ExpressionReward expr, boolean forAll, List coalition) throws PrismException { Expression rb; // Reward bound (expression) double r = 0; // Reward bound (actual value) RelOp relOp; // Relational operator + MinMax minMax = MinMax.blank(); + ModelType modelType = model.getModelType(); StateValues rews = null; Rewards rewards = null; @@ -701,12 +780,23 @@ public class ProbModelChecker extends NonProbModelChecker throw new PrismException("Invalid reward bound " + r + " in R[] formula"); } + // For nondeterministic models, determine whether min or max rewards needed + if (modelType.nondeterministic()) { + if (relOp == RelOp.EQ && rb == null) { + throw new PrismException("Can't use \"R=?\" for nondeterministic models; use \"Rmin=?\" or \"Rmax=?\""); + } + if (modelType == ModelType.MDP || modelType == ModelType.CTMDP) { + minMax = (relOp.isLowerBound() || relOp.isMin()) ? MinMax.min() : MinMax.max(); + } else { + throw new PrismException("Don't know how to model check " + expr.getTypeOfROperator() + " properties for " + modelType + "s"); + } + } + // Build rewards mainLog.println("Building reward structure..."); rewards = constructRewards(model, rewStruct); // Compute rewards - MinMax minMax = (relOp.isLowerBound() || relOp.isMin()) ? MinMax.min() : MinMax.max(); rews = checkRewardFormula(model, rewards, expr.getExpression(), minMax); // Print out rewards diff --git a/prism/src/parser/ast/ExpressionProb.java b/prism/src/parser/ast/ExpressionProb.java index a5f995d4..baac5ebe 100644 --- a/prism/src/parser/ast/ExpressionProb.java +++ b/prism/src/parser/ast/ExpressionProb.java @@ -101,6 +101,17 @@ public class ExpressionProb extends Expression return filter; } + /** + * Get a string describing the type of P operator, e.g. "P=?" or "P