From 72c2d1602ea3e449ade0fc70d525c5ccee51ebe1 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 28 Dec 2014 23:22:12 +0000 Subject: [PATCH] Refactoring of extraction of info from P/R/S operators (in explicit engine). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9458 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/ProbModelChecker.java | 97 ++++------------------ prism/src/parser/ast/ExpressionProb.java | 20 +++++ prism/src/parser/ast/ExpressionReward.java | 20 ++++- prism/src/parser/ast/ExpressionSS.java | 24 +++++- prism/src/prism/OpRelOpBound.java | 69 +++++++++++++++ 5 files changed, 147 insertions(+), 83 deletions(-) create mode 100644 prism/src/prism/OpRelOpBound.java diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index c3aad5e0..d1107652 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -36,10 +36,9 @@ 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.OpRelOpBound; import prism.PrismComponent; import prism.PrismException; import prism.PrismSettings; @@ -522,37 +521,13 @@ public class ProbModelChecker extends NonProbModelChecker */ protected StateValues checkExpressionProb(Model model, ExpressionProb expr, boolean forAll, Coalition 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 - relOp = expr.getRelOp(); - pb = expr.getProb(); - if (pb != null) { - p = pb.evaluateDouble(constantValues); - if (p < 0 || p > 1) - 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"); - } - } + OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues); + MinMax minMax = opInfo.getMinMax(model.getModelType()); // Compute probabilities - probs = checkProbPathFormula(model, expr.getExpression(), minMax); + StateValues probs = checkProbPathFormula(model, expr.getExpression(), minMax); // Print out probabilities if (getVerbosity() > 5) { @@ -561,12 +536,12 @@ public class ProbModelChecker extends NonProbModelChecker } // For =? properties, just return values - if (pb == null) { + if (opInfo.isNumeric()) { return probs; } // Otherwise, compare against bound to get set of satisfying states else { - BitSet sol = probs.getBitSetFromInterval(relOp, p); + BitSet sol = probs.getBitSetFromInterval(expr.getRelOp(), opInfo.getBound()); probs.clear(); return StateValues.createFromBitSet(sol, model); } @@ -762,42 +737,17 @@ public class ProbModelChecker extends NonProbModelChecker */ protected StateValues checkExpressionReward(Model model, ExpressionReward expr, boolean forAll, Coalition 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; - // Get info from R operator - RewardStruct rewStruct = expr.getRewardStructByIndexObject(modulesFile, constantValues); - relOp = expr.getRelOp(); - rb = expr.getReward(); - if (rb != null) { - r = rb.evaluateDouble(constantValues); - if (r < 0) - 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"); - } - } + OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues); + MinMax minMax = opInfo.getMinMax(model.getModelType()); // Build rewards + RewardStruct rewStruct = expr.getRewardStructByIndexObject(modulesFile, constantValues); mainLog.println("Building reward structure..."); - rewards = constructRewards(model, rewStruct); + Rewards rewards = constructRewards(model, rewStruct); // Compute rewards - rews = checkRewardFormula(model, rewards, expr.getExpression(), minMax); + StateValues rews = checkRewardFormula(model, rewards, expr.getExpression(), minMax); // Print out rewards if (getVerbosity() > 5) { @@ -806,12 +756,12 @@ public class ProbModelChecker extends NonProbModelChecker } // For =? properties, just return values - if (rb == null) { + if (opInfo.isNumeric()) { return rews; } // Otherwise, compare against bound to get set of satisfying states else { - BitSet sol = rews.getBitSetFromInterval(relOp, r); + BitSet sol = rews.getBitSetFromInterval(expr.getRelOp(), opInfo.getBound()); rews.clear(); return StateValues.createFromBitSet(sol, model); } @@ -979,23 +929,12 @@ public class ProbModelChecker extends NonProbModelChecker */ protected StateValues checkExpressionSteadyState(Model model, ExpressionSS expr) throws PrismException { - Expression pb; // Probability bound (expression) - double p = 0; // Probability bound (actual value) - RelOp relOp; // Relational operator - StateValues probs = null; - // Get info from S operator - relOp = expr.getRelOp(); - pb = expr.getProb(); - if (pb != null) { - p = pb.evaluateDouble(constantValues); - if (p < 0 || p > 1) - throw new PrismException("Invalid probability bound " + p + " in P operator"); - } + OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues); + MinMax minMax = opInfo.getMinMax(model.getModelType()); // Compute probabilities - MinMax minMax = (relOp.isLowerBound() || relOp.isMin()) ? MinMax.min() : MinMax.max(); - probs = checkSteadyStateFormula(model, expr.getExpression(), minMax); + StateValues probs = checkSteadyStateFormula(model, expr.getExpression(), minMax); // Print out probabilities if (getVerbosity() > 5) { @@ -1004,12 +943,12 @@ public class ProbModelChecker extends NonProbModelChecker } // For =? properties, just return values - if (pb == null) { + if (opInfo.isNumeric()) { return probs; } // Otherwise, compare against bound to get set of satisfying states else { - BitSet sol = probs.getBitSetFromInterval(relOp, p); + BitSet sol = probs.getBitSetFromInterval(expr.getRelOp(), opInfo.getBound()); probs.clear(); return StateValues.createFromBitSet(sol, model); } diff --git a/prism/src/parser/ast/ExpressionProb.java b/prism/src/parser/ast/ExpressionProb.java index baac5ebe..84b7b10c 100644 --- a/prism/src/parser/ast/ExpressionProb.java +++ b/prism/src/parser/ast/ExpressionProb.java @@ -27,7 +27,10 @@ package parser.ast; import parser.EvaluateContext; +import parser.Values; import parser.visitor.ASTVisitor; +import prism.OpRelOpBound; +import prism.PrismException; import prism.PrismLangException; public class ExpressionProb extends Expression @@ -112,6 +115,23 @@ public class ExpressionProb extends Expression return s; } + /** + * Get info about the operator and bound. + * Does some checks, e.g., throws an exception if probability is out of range. + * @param constantValues Values for constants in order to evaluate any bound + */ + public OpRelOpBound getRelopBoundInfo(Values constantValues) throws PrismException + { + if (prob != null) { + double bound = prob.evaluateDouble(constantValues); + if (bound < 0 || bound > 1) + throw new PrismException("Invalid probability bound " + bound + " in P operator"); + return new OpRelOpBound("P", relOp, bound); + } else { + return new OpRelOpBound("P", relOp, null); + } + } + // Methods required for Expression: /** diff --git a/prism/src/parser/ast/ExpressionReward.java b/prism/src/parser/ast/ExpressionReward.java index 92343300..af7dacf0 100644 --- a/prism/src/parser/ast/ExpressionReward.java +++ b/prism/src/parser/ast/ExpressionReward.java @@ -26,8 +26,10 @@ package parser.ast; -import parser.*; -import parser.visitor.*; +import parser.EvaluateContext; +import parser.Values; +import parser.visitor.ASTVisitor; +import prism.OpRelOpBound; import prism.PrismException; import prism.PrismLangException; @@ -172,6 +174,20 @@ public class ExpressionReward extends Expression } + /** + * Get info about the operator and bound. + * @param constantValues Values for constants in order to evaluate any bound + */ + public OpRelOpBound getRelopBoundInfo(Values constantValues) throws PrismException + { + if (reward != null) { + double bound = reward.evaluateDouble(constantValues); + return new OpRelOpBound("R", relOp, bound); + } else { + return new OpRelOpBound("R", relOp, null); + } + } + // Methods required for Expression: /** diff --git a/prism/src/parser/ast/ExpressionSS.java b/prism/src/parser/ast/ExpressionSS.java index edfea2f2..2b44034d 100644 --- a/prism/src/parser/ast/ExpressionSS.java +++ b/prism/src/parser/ast/ExpressionSS.java @@ -26,8 +26,11 @@ package parser.ast; -import parser.*; -import parser.visitor.*; +import parser.EvaluateContext; +import parser.Values; +import parser.visitor.ASTVisitor; +import prism.OpRelOpBound; +import prism.PrismException; import prism.PrismLangException; public class ExpressionSS extends Expression @@ -101,6 +104,23 @@ public class ExpressionSS extends Expression return filter; } + /** + * Get info about the operator and bound. + * Does some checks, e.g., throws an exception if probability is out of range. + * @param constantValues Values for constants in order to evaluate any bound + */ + public OpRelOpBound getRelopBoundInfo(Values constantValues) throws PrismException + { + if (prob != null) { + double bound = prob.evaluateDouble(constantValues); + if (bound < 0 || bound > 1) + throw new PrismException("Invalid probability bound " + bound + " in P operator"); + return new OpRelOpBound("P", relOp, bound); + } else { + return new OpRelOpBound("P", relOp, null); + } + } + // Methods required for Expression: /** diff --git a/prism/src/prism/OpRelOpBound.java b/prism/src/prism/OpRelOpBound.java new file mode 100644 index 00000000..1eaf5c94 --- /dev/null +++ b/prism/src/prism/OpRelOpBound.java @@ -0,0 +1,69 @@ +package prism; + +import parser.ast.RelOp; +import explicit.MinMax; + +/** + * Class to represent info (operator, relational operator, bound, etc.) found in a P/R/S operator. + */ +public class OpRelOpBound +{ + protected String op; + protected RelOp relOp; + protected boolean numeric; + protected double bound; + + public OpRelOpBound(String op, RelOp relOp, Double boundObject) + { + this.op = op; + this.relOp = relOp; + numeric = (boundObject == null); + if (boundObject != null) + bound = boundObject.doubleValue(); + } + + public RelOp getRelOp() + { + return relOp; + } + + public boolean isNumeric() + { + return numeric; + } + + public double getBound() + { + return bound; + } + + public MinMax getMinMax(ModelType modelType) 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) { + minMax = (relOp.isLowerBound() || relOp.isMin()) ? MinMax.min() : MinMax.max(); + } else { + throw new PrismException("Don't know how to model check " + getTypeOfOperator() + " properties for " + modelType + "s"); + } + } + return minMax; + } + + public String getTypeOfOperator() + { + String s = ""; + s += op + relOp; + s += isNumeric() ? "?" : "p"; // TODO: always "p"? + return s; + } + + @Override + public String toString() + { + return relOp.toString() + bound; + } +}