From 8291b5984ce62aaf9cddbf4af61a32ecb3f12f7d Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 26 Dec 2013 22:00:24 +0000 Subject: [PATCH] Refactoring wrt the way that relational operators are stored for P/R/S operators (String -> RelOp). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7766 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/dv/DoubleVector.java | 30 +++++-- prism/src/explicit/DTMCModelChecker.java | 2 - prism/src/explicit/MDPModelChecker.java | 2 - prism/src/explicit/ProbModelChecker.java | 35 ++------ prism/src/explicit/StateValues.java | 40 +++++++--- prism/src/param/ParamModelChecker.java | 86 ++++++++------------ prism/src/parser/ast/ExpressionProb.java | 21 +++-- prism/src/parser/ast/ExpressionReward.java | 17 ++-- prism/src/parser/ast/ExpressionSS.java | 13 ++- prism/src/parser/ast/RelOp.java | 93 ++++++++++++++++++++++ prism/src/parser/visitor/CheckValid.java | 15 ++++ prism/src/prism/NondetModelChecker.java | 71 +++++------------ prism/src/prism/ProbModelChecker.java | 45 ++++++----- prism/src/prism/StateValues.java | 4 +- prism/src/prism/StateValuesDV.java | 12 ++- prism/src/prism/StateValuesMTBDD.java | 29 +++++-- prism/src/prism/StateValuesVoid.java | 9 ++- prism/src/pta/PTAModelChecker.java | 2 +- prism/src/simulator/method/APMCMethod.java | 5 +- prism/src/simulator/method/CIMethod.java | 5 +- prism/src/simulator/method/SPRTMethod.java | 5 +- 21 files changed, 336 insertions(+), 205 deletions(-) create mode 100644 prism/src/parser/ast/RelOp.java diff --git a/prism/src/dv/DoubleVector.java b/prism/src/dv/DoubleVector.java index 4f308b5e..5ff58d28 100644 --- a/prism/src/dv/DoubleVector.java +++ b/prism/src/dv/DoubleVector.java @@ -26,6 +26,7 @@ package dv; +import parser.ast.RelOp; import prism.*; import jdd.*; import odd.*; @@ -277,29 +278,42 @@ public class DoubleVector * Generate BDD for states in the given interval * (interval specified as relational operator and bound) */ - public JDDNode getBDDFromInterval(String relOp, double bound, JDDVars vars, ODDNode odd) + public JDDNode getBDDFromInterval(String relOpString, double bound, JDDVars vars, ODDNode odd) + { + return getBDDFromInterval(RelOp.parseSymbol(relOpString), bound, vars, odd); + } + + /** + * Generate BDD for states in the given interval + * (interval specified as relational operator and bound) + */ + public JDDNode getBDDFromInterval(RelOp relOp, double bound, JDDVars vars, ODDNode odd) { JDDNode sol = null; - if (relOp.equals(">=")) { + switch (relOp) { + case GEQ: sol = new JDDNode( DV_BDDGreaterThanEquals(v, bound, vars.array(), vars.n(), odd.ptr()) ); - } - else if (relOp.equals(">")) { + break; + case GT: sol = new JDDNode( DV_BDDGreaterThan(v, bound, vars.array(), vars.n(), odd.ptr()) ); - } - else if (relOp.equals("<=")) { + break; + case LEQ: sol = new JDDNode( DV_BDDLessThanEquals(v, bound, vars.array(), vars.n(), odd.ptr()) ); - } - else if (relOp.equals("<")) { + break; + case LT: sol = new JDDNode( DV_BDDLessThan(v, bound, vars.array(), vars.n(), odd.ptr()) ); + break; + default: + // Don't handle } return sol; diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 699b7878..d489d0da 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -36,12 +36,10 @@ import parser.ast.Expression; import parser.ast.ExpressionTemporal; import parser.ast.ExpressionUnaryOp; import parser.type.TypeDouble; -import parser.visitor.ASTTraverse; import prism.DRA; import prism.Pair; import prism.PrismComponent; import prism.PrismException; -import prism.PrismLangException; import prism.PrismUtils; import explicit.rewards.MCRewards; diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index ce05ec6b..d4d15a63 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -36,14 +36,12 @@ import parser.ast.Expression; import parser.ast.ExpressionTemporal; import parser.ast.ExpressionUnaryOp; import parser.type.TypeDouble; -import parser.visitor.ASTTraverse; import prism.DRA; import prism.Pair; import prism.PrismComponent; import prism.PrismDevNullLog; import prism.PrismException; import prism.PrismFileLog; -import prism.PrismLangException; import prism.PrismLog; import prism.PrismUtils; import strat.MDStrategyArray; diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index c528eae5..6493dee0 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -32,6 +32,7 @@ import parser.ast.Expression; import parser.ast.ExpressionProb; import parser.ast.ExpressionReward; import parser.ast.ExpressionSS; +import parser.ast.RelOp; import parser.ast.RewardStruct; import prism.ModelType; import prism.PrismComponent; @@ -464,7 +465,7 @@ public class ProbModelChecker extends NonProbModelChecker { Expression pb; // Probability bound (expression) double p = 0; // Probability bound (actual value) - String relOp; // Relational operator + RelOp relOp; // Relational operator boolean min = false; // For nondeterministic models, are we finding min (true) or max (false) probs ModelType modelType = model.getModelType(); @@ -478,19 +479,7 @@ public class ProbModelChecker extends NonProbModelChecker 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.equals(">") || relOp.equals(">=") || relOp.equals("min=")) { - // min - min = true; - } else if (relOp.equals("<") || relOp.equals("<=") || relOp.equals("max=")) { - // max - min = false; - } else { - throw new PrismException("Can't use \"P=?\" for nondeterministic models; use \"Pmin=?\" or \"Pmax=?\""); - } - } + min = relOp.isLowerBound(); // Compute probabilities switch (modelType) { @@ -540,7 +529,7 @@ public class ProbModelChecker extends NonProbModelChecker RewardStruct rewStruct = null; // Reward struct object Expression rb; // Reward bound (expression) double r = 0; // Reward bound (actual value) - String relOp; // Relational operator + RelOp relOp; // Relational operator boolean min = false; // For nondeterministic models, are we finding min (true) or max (false) rewards ModelType modelType = model.getModelType(); StateValues rews = null; @@ -557,19 +546,7 @@ public class ProbModelChecker extends NonProbModelChecker 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.equals(">") || relOp.equals(">=") || relOp.equals("min=")) { - // min - min = true; - } else if (relOp.equals("<") || relOp.equals("<=") || relOp.equals("max=")) { - // max - min = false; - } else { - throw new PrismException("Can't use \"R=?\" for nondeterministic models; use \"Rmin=?\" or \"Rmax=?\""); - } - } + min = relOp.isLowerBound(); // Get reward info if (modulesFile == null) @@ -643,7 +620,7 @@ public class ProbModelChecker extends NonProbModelChecker { Expression pb; // Probability bound (expression) double p = 0; // Probability bound (actual value) - String relOp; // Relational operator + RelOp relOp; // Relational operator ModelType modelType = model.getModelType(); StateValues probs = null; diff --git a/prism/src/explicit/StateValues.java b/prism/src/explicit/StateValues.java index c0291915..5217de00 100644 --- a/prism/src/explicit/StateValues.java +++ b/prism/src/explicit/StateValues.java @@ -37,6 +37,7 @@ import parser.State; import parser.ast.ExpressionBinaryOp; import parser.ast.ExpressionFunc; import parser.ast.ExpressionUnaryOp; +import parser.ast.RelOp; import parser.type.Type; import parser.type.TypeBool; import parser.type.TypeDouble; @@ -205,45 +206,66 @@ public class StateValues * Generate BitSet for states in the given interval * (interval specified as relational operator and bound) */ - public BitSet getBitSetFromInterval(String relOp, double bound) + public BitSet getBitSetFromInterval(String relOpString, double bound) + { + return getBitSetFromInterval(RelOp.parseSymbol(relOpString), bound); + } + + /** + * Generate BitSet for states in the given interval + * (interval specified as relational operator and bound) + */ + public BitSet getBitSetFromInterval(RelOp relOp, double bound) { BitSet sol = new BitSet(); if (type instanceof TypeInt) { - if (relOp.equals(">=")) { + switch (relOp) { + case GEQ: for (int i = 0; i < size; i++) { sol.set(i, valuesI[i] >= bound); } - } else if (relOp.equals(">")) { + break; + case GT: for (int i = 0; i < size; i++) { sol.set(i, valuesI[i] > bound); } - } else if (relOp.equals("<=")) { + break; + case LEQ: for (int i = 0; i < size; i++) { sol.set(i, valuesI[i] <= bound); } - } else if (relOp.equals("<")) { + break; + case LT: for (int i = 0; i < size; i++) { sol.set(i, valuesI[i] < bound); } + default: + // Don't handle } } else if (type instanceof TypeDouble) { - if (relOp.equals(">=")) { + switch (relOp) { + case GEQ: for (int i = 0; i < size; i++) { sol.set(i, valuesD[i] >= bound); } - } else if (relOp.equals(">")) { + break; + case GT: for (int i = 0; i < size; i++) { sol.set(i, valuesD[i] > bound); } - } else if (relOp.equals("<=")) { + break; + case LEQ: for (int i = 0; i < size; i++) { sol.set(i, valuesD[i] <= bound); } - } else if (relOp.equals("<")) { + break; + case LT: for (int i = 0; i < size; i++) { sol.set(i, valuesD[i] < bound); } + default: + // Don't handle } } diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index 7394eed4..bda0ce85 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -54,19 +54,35 @@ package param; -import java.io.FileOutputStream; -import java.util.*; - -import edu.jas.kern.ComputerThreads; -import explicit.Model; +import java.util.BitSet; +import java.util.List; import param.Lumper.BisimType; import param.StateEliminator.EliminationOrder; import parser.State; import parser.Values; -import parser.ast.*; +import parser.ast.Expression; +import parser.ast.ExpressionBinaryOp; +import parser.ast.ExpressionConstant; +import parser.ast.ExpressionFilter; import parser.ast.ExpressionFilter.FilterOperator; -import parser.type.*; +import parser.ast.ExpressionLabel; +import parser.ast.ExpressionLiteral; +import parser.ast.ExpressionProb; +import parser.ast.ExpressionProp; +import parser.ast.ExpressionReward; +import parser.ast.ExpressionSS; +import parser.ast.ExpressionTemporal; +import parser.ast.ExpressionUnaryOp; +import parser.ast.LabelList; +import parser.ast.ModulesFile; +import parser.ast.PropertiesFile; +import parser.ast.Property; +import parser.ast.RelOp; +import parser.ast.RewardStruct; +import parser.type.TypeBool; +import parser.type.TypeDouble; +import parser.type.TypeInt; import prism.ModelType; import prism.PrismComponent; import prism.PrismException; @@ -74,6 +90,8 @@ import prism.PrismLog; import prism.PrismPrintStreamLog; import prism.PrismSettings; import prism.Result; +import edu.jas.kern.ComputerThreads; +import explicit.Model; /** * Model checker for parametric Markov models. @@ -881,7 +899,7 @@ final public class ParamModelChecker extends PrismComponent //String relOp; // Relational operator //boolean min = false; // For nondeterministic models, are we finding min (true) or max (false) probs ModelType modelType = model.getModelType(); - String relOp; + RelOp relOp; boolean min = false; RegionValues probs = null; @@ -895,19 +913,7 @@ final public class ParamModelChecker extends PrismComponent if (p.compareTo(0) == -1 || p.compareTo(1) == 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.equals(">") || relOp.equals(">=") || relOp.equals("min=")) { - // min - min = true; - } else if (relOp.equals("<") || relOp.equals("<=") || relOp.equals("max=")) { - // max - min = false; - } else { - throw new PrismException("Can't use \"P=?\" for nondeterministic models; use \"Pmin=?\" or \"Pmax=?\""); - } - } + min = relOp.isLowerBound(); // Compute probabilities if (!expr.getExpression().isSimplePathFormula()) { @@ -926,7 +932,7 @@ final public class ParamModelChecker extends PrismComponent } // Otherwise, compare against bound to get set of satisfying states else { - return probs.binaryOp(Region.getOp(relOp), p); + return probs.binaryOp(Region.getOp(relOp.toString()), p); } } @@ -1003,7 +1009,7 @@ final public class ParamModelChecker extends PrismComponent // Get info from reward operator rs = expr.getRewardStructIndex(); - String relOp = expr.getRelOp(); + RelOp relOp = expr.getRelOp(); rb = expr.getReward(); if (rb != null) { // TODO check whether actually evaluated as such, take constantValues into account @@ -1011,19 +1017,7 @@ final public class ParamModelChecker extends PrismComponent if (r.compareTo(0) == -1) 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.equals(">") || relOp.equals(">=") || relOp.equals("min=")) { - // min - min = true; - } else if (relOp.equals("<") || relOp.equals("<=") || relOp.equals("max=")) { - // max - min = false; - } else if(modelType.nondeterministic()) { - throw new PrismException("Can't use \"R=?\" for nondeterministic models; use \"Rmin=?\" or \"Rmax=?\""); - } - //} + min = relOp.isLowerBound(); // Get reward info if (modulesFile == null) @@ -1060,7 +1054,7 @@ final public class ParamModelChecker extends PrismComponent } // Otherwise, compare against bound to get set of satisfying states else { - return rews.binaryOp(Region.getOp(relOp), r); + return rews.binaryOp(Region.getOp(relOp.toString()), r); } } @@ -1162,7 +1156,7 @@ final public class ParamModelChecker extends PrismComponent //String relOp; // Relational operator //boolean min = false; // For nondeterministic models, are we finding min (true) or max (false) probs ModelType modelType = model.getModelType(); - String relOp; + RelOp relOp; boolean min = false; RegionValues probs = null; @@ -1176,19 +1170,7 @@ final public class ParamModelChecker extends PrismComponent if (p.compareTo(0) == -1 || p.compareTo(1) == 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.equals(">") || relOp.equals(">=") || relOp.equals("min=")) { - // min - min = true; - } else if (relOp.equals("<") || relOp.equals("<=") || relOp.equals("max=")) { - // max - min = false; - } else { - throw new PrismException("Can't use \"S=?\" for nondeterministic models; use \"Smin=?\" or \"Smax=?\""); - } - } + min = relOp.isLowerBound(); // Compute probabilities probs = checkProbSteadyState(model, expr.getExpression(), min, needStates); @@ -1204,7 +1186,7 @@ final public class ParamModelChecker extends PrismComponent } // Otherwise, compare against bound to get set of satisfying states else { - return probs.binaryOp(Region.getOp(relOp), p); + return probs.binaryOp(Region.getOp(relOp.toString()), p); } } diff --git a/prism/src/parser/ast/ExpressionProb.java b/prism/src/parser/ast/ExpressionProb.java index 530912fa..a5f995d4 100644 --- a/prism/src/parser/ast/ExpressionProb.java +++ b/prism/src/parser/ast/ExpressionProb.java @@ -26,13 +26,13 @@ package parser.ast; -import parser.*; -import parser.visitor.*; +import parser.EvaluateContext; +import parser.visitor.ASTVisitor; import prism.PrismLangException; public class ExpressionProb extends Expression { - String relOp = null; + RelOp relOp = null; Expression prob = null; Expression expression = null; // Note: this "old-style" filter is just for display purposes @@ -48,15 +48,20 @@ public class ExpressionProb extends Expression public ExpressionProb(Expression e, String r, Expression p) { expression = e; - relOp = r; + relOp = RelOp.parseSymbol(r); prob = p; } // Set methods + public void setRelOp(RelOp relOp) + { + this.relOp = relOp; + } + public void setRelOp(String r) { - relOp = r; + relOp = RelOp.parseSymbol(r); } public void setProb(Expression p) @@ -76,7 +81,7 @@ public class ExpressionProb extends Expression // Get methods - public String getRelOp() + public RelOp getRelOp() { return relOp; } @@ -128,9 +133,9 @@ public class ExpressionProb extends Expression { if (prob != null) return "Result"; - else if (relOp.equals("min=")) + else if (relOp == RelOp.MIN) return "Minimum probability"; - else if (relOp.equals("max=")) + else if (relOp == RelOp.MAX) return "Maximum probability"; else return "Probability"; diff --git a/prism/src/parser/ast/ExpressionReward.java b/prism/src/parser/ast/ExpressionReward.java index b20d4ab9..d34d9338 100644 --- a/prism/src/parser/ast/ExpressionReward.java +++ b/prism/src/parser/ast/ExpressionReward.java @@ -33,7 +33,7 @@ import prism.PrismLangException; public class ExpressionReward extends Expression { Object rewardStructIndex = null; - String relOp = null; + RelOp relOp = null; Expression reward = null; Expression expression = null; // Note: this "old-style" filter is just for display purposes @@ -49,7 +49,7 @@ public class ExpressionReward extends Expression public ExpressionReward(Expression e, String r, Expression p) { expression = e; - relOp = r; + relOp = RelOp.parseSymbol(r); reward = p; } @@ -60,9 +60,14 @@ public class ExpressionReward extends Expression rewardStructIndex = o; } + public void setRelOp(RelOp relOp) + { + this.relOp = relOp; + } + public void setRelOp(String r) { - relOp =r; + relOp = RelOp.parseSymbol(r); } public void setReward(Expression p) @@ -87,7 +92,7 @@ public class ExpressionReward extends Expression return rewardStructIndex; } - public String getRelOp() + public RelOp getRelOp() { return relOp; } @@ -140,8 +145,8 @@ public class ExpressionReward extends Expression // For R=? properties, use name of reward structure where applicable if (reward == null) { String s = "E"; - if (relOp.equals("min=")) s = "Minimum e"; - else if (relOp.equals("max=")) s = "Maximum e"; + if (relOp == RelOp.MIN) s = "Minimum e"; + else if (relOp == RelOp.MAX) s = "Maximum e"; else s = "E"; if (rewardStructIndex instanceof String) s += "xpected "+rewardStructIndex; // Or just call it "Expected reward" diff --git a/prism/src/parser/ast/ExpressionSS.java b/prism/src/parser/ast/ExpressionSS.java index 6f7be726..edfea2f2 100644 --- a/prism/src/parser/ast/ExpressionSS.java +++ b/prism/src/parser/ast/ExpressionSS.java @@ -32,7 +32,7 @@ import prism.PrismLangException; public class ExpressionSS extends Expression { - String relOp = null; + RelOp relOp = null; Expression prob = null; Expression expression = null; // Note: this "old-style" filter is just for display purposes @@ -48,15 +48,20 @@ public class ExpressionSS extends Expression public ExpressionSS(Expression e, String r, Expression p) { expression = e; - relOp = r; + relOp = RelOp.parseSymbol(r); prob = p; } // Set methods + public void setRelOp(RelOp relOp) + { + this.relOp = relOp; + } + public void setRelOp(String r) { - relOp =r; + relOp = RelOp.parseSymbol(r); } public void setProb(Expression p) @@ -76,7 +81,7 @@ public class ExpressionSS extends Expression // Get methods - public String getRelOp() + public RelOp getRelOp() { return relOp; } diff --git a/prism/src/parser/ast/RelOp.java b/prism/src/parser/ast/RelOp.java new file mode 100644 index 00000000..89914865 --- /dev/null +++ b/prism/src/parser/ast/RelOp.java @@ -0,0 +1,93 @@ +package parser.ast; + +import java.util.HashMap; +import java.util.Iterator; +import java.util.Map; +import java.util.Map.Entry; + +/** + * Class to represent a relational operator (or similar) found in a P/R/S operator. + */ +public enum RelOp { + + GT, GEQ, MIN, LEQ, LT, MAX, EQ; + + protected static Map symbols; + static { + symbols = new HashMap(); + symbols.put(RelOp.GT, ">"); + symbols.put(RelOp.GEQ, ">="); + symbols.put(RelOp.MIN, "min="); + symbols.put(RelOp.LT, "<"); + symbols.put(RelOp.LEQ, "<="); + symbols.put(RelOp.MAX, "max="); + symbols.put(RelOp.EQ, "="); + } + + @Override + public String toString() + { + return symbols.get(this); + } + + /** + * Returns true if this corresponds to a lower bound (e.g. >, >=, min=). + */ + public boolean isLowerBound() + { + switch (this) { + case GT: + case GEQ: + case MIN: + return true; + default: + return false; + } + } + + /** + * Returns true if this is a strict bound (i.e. < or >). + */ + public boolean isStrict() + { + switch (this) { + case GT: + case LT: + return true; + default: + return false; + } + } + + /** + * Returns true if this corresponds to an upper bound (e.g. <, <=, max=). + */ + public boolean isUpperBound() + { + switch (this) { + case LT: + case LEQ: + case MAX: + return true; + default: + return false; + } + } + + /** + * Returns the RelOp object corresponding to a (string) symbol, + * e.g. parseSymbol("<=") returns RelOp.LEQ. Returns null if invalid. + * @param symbol The symbol to look up + * @return + */ + public static RelOp parseSymbol(String symbol) + { + Iterator> it = symbols.entrySet().iterator(); + while (it.hasNext()) { + Map.Entry e = it.next(); + if (e.getValue().equals(symbol)) + return e.getKey(); + } + return null; + } +} diff --git a/prism/src/parser/visitor/CheckValid.java b/prism/src/parser/visitor/CheckValid.java index 0f811476..41a83a5a 100644 --- a/prism/src/parser/visitor/CheckValid.java +++ b/prism/src/parser/visitor/CheckValid.java @@ -28,6 +28,7 @@ package parser.visitor; import parser.ast.*; import parser.type.*; +import prism.PrismException; import prism.PrismLangException; import prism.ModelType; @@ -89,6 +90,18 @@ public class CheckValid extends ASTTraverse } } + public void visitPost(ExpressionProb e) throws PrismLangException + { + if (modelType.nondeterministic() && e.getRelOp() == RelOp.EQ) + throw new PrismLangException("Can't use \"P=?\" for nondeterministic models; use \"Pmin=?\" or \"Pmax=?\""); + } + + public void visitPost(ExpressionReward e) throws PrismLangException + { + if (modelType.nondeterministic() && e.getRelOp() == RelOp.EQ) + throw new PrismLangException("Can't use \"R=?\" for nondeterministic models; use \"Rmin=?\" or \"Rmax=?\""); + } + public void visitPost(ExpressionSS e) throws PrismLangException { // S operator only works for some models @@ -98,5 +111,7 @@ public class CheckValid extends ASTTraverse if (modelType == ModelType.PTA) { throw new PrismLangException("The S operator cannot be used for PTAs"); } + /*if (modelType.nondeterministic() && e.getRelOp() == RelOp.EQ) + throw new PrismLangException("Can't use \"S=?\" for nondeterministic models; use \"Smin=?\" or \"Smax=?\"");*/ } } diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 9ccf5378..bf99425b 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -157,7 +157,7 @@ public class NondetModelChecker extends NonProbModelChecker { Expression pb; // probability bound (expression) double p = 0; // probability bound (actual value) - String relOp; // relational operator + RelOp relOp; // relational operator boolean min; // are we finding min (true) or max (false) probs JDDNode sol; @@ -171,30 +171,20 @@ public class NondetModelChecker extends NonProbModelChecker if (p < 0 || p > 1) throw new PrismException("Invalid probability bound " + p + " in P operator"); } + min = relOp.isLowerBound(); // Check for trivial (i.e. stupid) cases if (pb != null) { - if ((p == 0 && relOp.equals(">=")) || (p == 1 && relOp.equals("<="))) { + if ((p == 0 && relOp == RelOp.GEQ) || (p == 1 && relOp == RelOp.LEQ)) { mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies all states"); JDD.Ref(reach); return new StateValuesMTBDD(reach, model); - } else if ((p == 0 && relOp.equals("<")) || (p == 1 && relOp.equals(">"))) { + } else if ((p == 0 && relOp == RelOp.LT) || (p == 1 && relOp == RelOp.GT)) { mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies no states"); return new StateValuesMTBDD(JDD.Constant(0), model); } } - // Determine whether min or max probabilities needed - if (relOp.equals(">") || relOp.equals(">=") || relOp.equals("min=")) { - // min - min = true; - } else if (relOp.equals("<") || relOp.equals("<=") || relOp.equals("max=")) { - // max - min = false; - } else { - throw new PrismException("Can't use \"P=?\" for MDPs; use \"Pmin=?\" or \"Pmax=?\""); - } - // Compute probabilities boolean qual = pb != null && ((p == 0) || (p == 1)) && precomp && prob0 && prob1; probs = checkProbPathFormula(expr.getExpression(), qual, min); @@ -229,7 +219,7 @@ public class NondetModelChecker extends NonProbModelChecker Object rs; // reward struct index Expression rb; // reward bound (expression) double r = 0; // reward bound (actual value) - String relOp; // relational operator + RelOp relOp; // relational operator boolean min; // are we finding min (true) or max (false) rewards Expression expr2; // expression @@ -246,6 +236,7 @@ public class NondetModelChecker extends NonProbModelChecker if (r < 0) throw new PrismException("Invalid reward bound " + r + " in R operator"); } + min = relOp.isLowerBound(); // get reward info if (model.getNumRewardStructs() == 0) @@ -267,27 +258,16 @@ public class NondetModelChecker extends NonProbModelChecker // check for trivial (i.e. stupid) cases if (rb != null) { - if (r == 0 && relOp.equals(">=")) { + if (r == 0 && relOp == RelOp.GEQ) { mainLog.printWarning("Checking for reward " + relOp + " " + r + " - formula trivially satisfies all states"); JDD.Ref(reach); return new StateValuesMTBDD(reach, model); - } else if (r == 0 && relOp.equals("<")) { + } else if (r == 0 && relOp == RelOp.LT) { mainLog.printWarning("Checking for reward " + relOp + " " + r + " - formula trivially satisfies no states"); return new StateValuesMTBDD(JDD.Constant(0), model); } } - // determine whether min or max rewards needed - if (relOp.equals(">") || relOp.equals(">=") || relOp.equals("min=")) { - // min - min = true; - } else if (relOp.equals("<") || relOp.equals("<=") || relOp.equals("max=")) { - // max - min = false; - } else { - throw new PrismException("Can't use \"R=?\" for MDPs; use \"Rmin=?\" or \"Rmax=?\""); - } - // compute rewards expr2 = expr.getExpression(); if (expr2 instanceof ExpressionTemporal) { @@ -332,22 +312,19 @@ public class NondetModelChecker extends NonProbModelChecker protected void extractInfoFromMultiObjectiveOperand(Expression operand, OpsAndBoundsList opsAndBounds, List rewardsIndex, List targetName, List targetExprs, boolean isFirst) throws PrismException { - String relOp; int stepBound = 0; ExpressionProb exprProb = null; ExpressionReward exprReward = null; ExpressionTemporal exprTemp; - // Only do P or R operators - if (!(operand instanceof ExpressionProb || operand instanceof ExpressionReward)) - throw new PrismException("Multiple objectives must be P or R operators"); - //if (expr.getOperand(i) instanceof ExpressionReward && i > 0) - // throw new PrismException("R operator can only be used as first argument of multi function"); + RelOp relOp; if (operand instanceof ExpressionProb) { exprProb = (ExpressionProb) operand; exprReward = null; - } else { + relOp = exprProb.getRelOp(); + } else if (operand instanceof ExpressionReward) { exprReward = (ExpressionReward) operand; exprProb = null; + relOp = exprReward.getRelOp(); Object rs = exprReward.getRewardStructIndex(); JDDNode transRewards = null; JDDNode stateRewards = null; @@ -372,6 +349,8 @@ public class NondetModelChecker extends NonProbModelChecker if (transRewards == null) throw new PrismException("Invalid reward structure index \"" + rs + "\""); rewardsIndex.add(transRewards); + } else { + throw new PrismException("Multi-objective properties can only contain P and R operators"); } // Get the cumulative step bound for reward if (exprReward != null) { @@ -405,23 +384,17 @@ public class NondetModelChecker extends NonProbModelChecker } // Get info from P/R operator - // Store relational operator as an integer - // Only do max=? or lower bounds - relOp = (exprProb != null) ? exprProb.getRelOp() : exprReward.getRelOp(); + // Store relational operator + if (relOp.isStrict()) + throw new PrismException("Multi-objective properties can not use strict inequalities on P/R operators"); Operator op; - if (relOp.equals("max=")) { + if (relOp == RelOp.MAX) { op = (exprProb != null) ? Operator.P_MAX : Operator.R_MAX; - } else if (relOp.equals(">")) // currently do not support - //relOps.add(1); - throw new PrismException("Multi-objective properties can not use strict inequalities on P/R operators"); - else if (relOp.equals(">=")) { + } else if (relOp == RelOp.GEQ) { op = (exprProb != null) ? Operator.P_GE : Operator.R_GE; - } else if (relOp.equals("min=")) { + } else if (relOp == RelOp.MIN) { op = (exprProb != null) ? Operator.P_MIN : Operator.R_MIN; - } else if (relOp.equals("<")) // currently do not support - //relOps.add(6); - throw new PrismException("Multi-objective properties can not use strict inequalities on P/R operators"); - else if (relOp.equals("<=")) { + } else if (relOp == RelOp.LEQ) { op = (exprProb != null) ? Operator.P_LE : Operator.R_LE; } else throw new PrismException("Multi-objective properties can only contain P/R operators with max/min=? or lower/upper probability bounds"); @@ -433,7 +406,7 @@ public class NondetModelChecker extends NonProbModelChecker throw new PrismException("Invalid probability bound " + p + " in P operator"); if ((exprProb == null) && (p < 0)) throw new PrismException("Invalid reward bound " + p + " in P operator"); - if (exprProb != null && relOp.equals("<=")) + if (exprProb != null && relOp == RelOp.LEQ) p = 1 - p; opsAndBounds.add(op, p, stepBound); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index a12715f0..ffed90ff 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -26,19 +26,28 @@ package prism; +import hybrid.PrismHybrid; + import java.io.File; import java.io.FileNotFoundException; import java.util.BitSet; import java.util.List; import java.util.Vector; -import jdd.*; -import dv.*; -import mtbdd.*; -import sparse.*; -import hybrid.*; -import parser.ast.*; -import parser.visitor.ASTTraverse; +import jdd.JDD; +import jdd.JDDNode; +import jdd.JDDVars; +import mtbdd.PrismMTBDD; +import parser.ast.Expression; +import parser.ast.ExpressionProb; +import parser.ast.ExpressionReward; +import parser.ast.ExpressionSS; +import parser.ast.ExpressionTemporal; +import parser.ast.ExpressionUnaryOp; +import parser.ast.PropertiesFile; +import parser.ast.RelOp; +import sparse.PrismSparse; +import dv.DoubleVector; /* * Model checker for DTMCs. @@ -144,7 +153,7 @@ public class ProbModelChecker extends NonProbModelChecker { Expression pb; // probability bound (expression) double p = 0; // probability bound (actual value) - String relOp; // relational operator + RelOp relOp; // relational operator JDDNode sol; StateValues probs = null; @@ -160,18 +169,18 @@ public class ProbModelChecker extends NonProbModelChecker // Check for trivial (i.e. stupid) cases if (pb != null) { - if ((p == 0 && relOp.equals(">=")) || (p == 1 && relOp.equals("<="))) { + if ((p == 0 && relOp == RelOp.GEQ) || (p == 1 && relOp == RelOp.LEQ)) { mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies all states"); JDD.Ref(reach); return new StateValuesMTBDD(reach, model); - } else if ((p == 0 && relOp.equals("<")) || (p == 1 && relOp.equals(">"))) { + } else if ((p == 0 && relOp == RelOp.LT) || (p == 1 && relOp == RelOp.GT)) { mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies no states"); return new StateValuesMTBDD(JDD.Constant(0), model); } } // Print a warning if Pmin/Pmax used - if (relOp.equals("min=") || relOp.equals("max=")) { + if (relOp == RelOp.MIN || relOp == RelOp.MAX) { mainLog.printWarning("\"Pmin=?\" and \"Pmax=?\" operators are identical to \"P=?\" for DTMCs/CTMCs"); } @@ -208,7 +217,7 @@ public class ProbModelChecker extends NonProbModelChecker Object rs; // reward struct index Expression rb; // reward bound (expression) double r = 0; // reward bound (actual value) - String relOp; // relational operator + RelOp relOp; // relational operator Expression expr2; // expression JDDNode stateRewards = null, transRewards = null, sol; @@ -245,18 +254,18 @@ public class ProbModelChecker extends NonProbModelChecker // check for trivial (i.e. stupid) cases if (rb != null) { - if (r == 0 && relOp.equals(">=")) { + if (r == 0 && relOp == RelOp.GEQ) { mainLog.printWarning("Checking for reward " + relOp + " " + r + " - formula trivially satisfies all states"); JDD.Ref(reach); return new StateValuesMTBDD(reach, model); - } else if (r == 0 && relOp.equals("<")) { + } else if (r == 0 && relOp == RelOp.LT) { mainLog.printWarning("Checking for reward " + relOp + " " + r + " - formula trivially satisfies no states"); return new StateValuesMTBDD(JDD.Constant(0), model); } } // print a warning if Rmin/Rmax used - if (relOp.equals("min=") || relOp.equals("max=")) { + if (relOp == RelOp.MIN || relOp == RelOp.MAX) { mainLog.printWarning("\"Rmin=?\" and \"Rmax=?\" operators are identical to \"R=?\" for DTMCs/CTMCs"); } @@ -309,7 +318,7 @@ public class ProbModelChecker extends NonProbModelChecker { Expression pb; // probability bound (expression) double p = 0; // probability bound (actual value) - String relOp; // relational operator + RelOp relOp; // relational operator // BSCC stuff List bsccs = null; @@ -332,11 +341,11 @@ public class ProbModelChecker extends NonProbModelChecker // Check for trivial (i.e. stupid) cases if (pb != null) { - if ((p == 0 && relOp.equals(">=")) || (p == 1 && relOp.equals("<="))) { + if ((p == 0 && relOp == RelOp.GEQ) || (p == 1 && relOp == RelOp.LEQ)) { mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies all states"); JDD.Ref(reach); return new StateValuesMTBDD(reach, model); - } else if ((p == 0 && relOp.equals("<")) || (p == 1 && relOp.equals(">"))) { + } else if ((p == 0 && relOp == RelOp.LT) || (p == 1 && relOp == RelOp.GT)) { mainLog.printWarning("Checking for probability " + relOp + " " + p + " - formula trivially satisfies no states"); return new StateValuesMTBDD(JDD.Constant(0), model); } diff --git a/prism/src/prism/StateValues.java b/prism/src/prism/StateValues.java index c4a7e403..a0024f42 100644 --- a/prism/src/prism/StateValues.java +++ b/prism/src/prism/StateValues.java @@ -30,6 +30,7 @@ import java.io.File; import jdd.JDDNode; import jdd.JDDVars; +import parser.ast.RelOp; // Interface for classes for state-indexed vectors of (integer or double) values @@ -54,7 +55,8 @@ public interface StateValues double sumOverBDD(JDDNode filter); double sumOverMTBDD(JDDNode mult); StateValues sumOverDDVars(JDDVars sumVars, Model newModel) throws PrismException; - JDDNode getBDDFromInterval(String relOp, double bound); + JDDNode getBDDFromInterval(String relOpString, double bound); + JDDNode getBDDFromInterval(RelOp relOp, double bound); JDDNode getBDDFromInterval(double lo, double hi); JDDNode getBDDFromCloseValue(double val, double epsilon, boolean abs); JDDNode getBDDFromCloseValueAbs(double val, double epsilon); diff --git a/prism/src/prism/StateValuesDV.java b/prism/src/prism/StateValuesDV.java index 5375883d..2bea6762 100644 --- a/prism/src/prism/StateValuesDV.java +++ b/prism/src/prism/StateValuesDV.java @@ -32,6 +32,7 @@ import dv.*; import jdd.*; import odd.*; import parser.VarList; +import parser.ast.RelOp; import parser.type.*; ; @@ -303,7 +304,16 @@ public class StateValuesDV implements StateValues * Generate BDD for states in the given interval * (interval specified as relational operator and bound) */ - public JDDNode getBDDFromInterval(String relOp, double bound) + public JDDNode getBDDFromInterval(String relOpString, double bound) + { + return getBDDFromInterval(RelOp.parseSymbol(relOpString), bound); + } + + /** + * Generate BDD for states in the given interval + * (interval specified as relational operator and bound) + */ + public JDDNode getBDDFromInterval(RelOp relOp, double bound) { return values.getBDDFromInterval(relOp, bound, vars, odd); } diff --git a/prism/src/prism/StateValuesMTBDD.java b/prism/src/prism/StateValuesMTBDD.java index eff5a9cf..38d8eb86 100644 --- a/prism/src/prism/StateValuesMTBDD.java +++ b/prism/src/prism/StateValuesMTBDD.java @@ -34,6 +34,7 @@ import java.io.IOException; import jdd.*; import odd.*; import parser.VarList; +import parser.ast.RelOp; import parser.type.*; // Class for state-indexed vectors of (integer or double) values, represented by an MTBDD @@ -408,22 +409,34 @@ public class StateValuesMTBDD implements StateValues * Generate BDD for states in the given interval * (interval specified as relational operator and bound) */ - public JDDNode getBDDFromInterval(String relOp, double bound) + public JDDNode getBDDFromInterval(String relOpString, double bound) + { + return getBDDFromInterval(RelOp.parseSymbol(relOpString), bound); + } + + /** + * Generate BDD for states in the given interval + * (interval specified as relational operator and bound) + */ + public JDDNode getBDDFromInterval(RelOp relOp, double bound) { JDDNode sol = null; JDD.Ref(values); - if (relOp.equals(">=")) { + switch (relOp) { + case GEQ: sol = JDD.GreaterThanEquals(values, bound); - } - else if (relOp.equals(">")) { + break; + case GT: sol = JDD.GreaterThan(values, bound); - } - else if (relOp.equals("<=")) { + break; + case LEQ: sol = JDD.LessThanEquals(values, bound); - } - else if (relOp.equals("<")) { + break; + case LT: sol = JDD.LessThan(values, bound); + default: + // Don't handle } return sol; diff --git a/prism/src/prism/StateValuesVoid.java b/prism/src/prism/StateValuesVoid.java index 95b14898..796c93c0 100644 --- a/prism/src/prism/StateValuesVoid.java +++ b/prism/src/prism/StateValuesVoid.java @@ -28,6 +28,8 @@ package prism; import java.io.File; +import parser.ast.RelOp; + import jdd.JDDNode; import jdd.JDDVars; @@ -148,7 +150,12 @@ public class StateValuesVoid implements StateValues throw new UnsupportedOperationException(); } - public JDDNode getBDDFromInterval(String relOp, double bound) + public JDDNode getBDDFromInterval(String relOpString, double bound) + { + throw new UnsupportedOperationException(); + } + + public JDDNode getBDDFromInterval(RelOp relOp, double bound) { throw new UnsupportedOperationException(); } diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java index 231d74e8..08e91eba 100644 --- a/prism/src/pta/PTAModelChecker.java +++ b/prism/src/pta/PTAModelChecker.java @@ -193,7 +193,7 @@ public class PTAModelChecker extends PrismComponent if (expr.getProb() != null) { throw new PrismException("PTA model checking currently only supports Pmin=? and Pmax=? properties (try the digital clocks engine instead)"); } - min = expr.getRelOp().equals("min="); + min = expr.getRelOp().isLowerBound(); // Check this is a F path property (only case allowed at the moment) if (!(expr.getExpression() instanceof ExpressionTemporal)) diff --git a/prism/src/simulator/method/APMCMethod.java b/prism/src/simulator/method/APMCMethod.java index e743b5e9..1ec1a5c1 100644 --- a/prism/src/simulator/method/APMCMethod.java +++ b/prism/src/simulator/method/APMCMethod.java @@ -30,6 +30,7 @@ package simulator.method; import parser.ast.Expression; import parser.ast.ExpressionProb; import parser.ast.ExpressionReward; +import parser.ast.RelOp; import prism.PrismException; import simulator.sampler.Sampler; @@ -91,7 +92,7 @@ public abstract class APMCMethod extends SimulationMethod public void setExpression(Expression expr) throws PrismException { Expression bound; - String relOp; + RelOp relOp; // For P properties... if (expr instanceof ExpressionProb) { @@ -113,7 +114,7 @@ public abstract class APMCMethod extends SimulationMethod prOp = 0; theta = -1.0; // junk } else { - prOp = (relOp.equals(">") || relOp.equals(">=")) ? -1 : 1; + prOp = relOp.isLowerBound() ? -1 : 1; theta = bound.evaluateDouble(); } } diff --git a/prism/src/simulator/method/CIMethod.java b/prism/src/simulator/method/CIMethod.java index 2e0dc4d0..af1e2968 100644 --- a/prism/src/simulator/method/CIMethod.java +++ b/prism/src/simulator/method/CIMethod.java @@ -30,6 +30,7 @@ package simulator.method; import parser.ast.Expression; import parser.ast.ExpressionProb; import parser.ast.ExpressionReward; +import parser.ast.RelOp; import prism.PrismException; import simulator.sampler.Sampler; @@ -91,7 +92,7 @@ public abstract class CIMethod extends SimulationMethod public void setExpression(Expression expr) throws PrismException { Expression bound; - String relOp; + RelOp relOp; // For P properties... if (expr instanceof ExpressionProb) { @@ -113,7 +114,7 @@ public abstract class CIMethod extends SimulationMethod prOp = 0; theta = -1.0; // junk } else { - prOp = (relOp.equals(">") || relOp.equals(">=")) ? -1 : 1; + prOp = relOp.isLowerBound() ? -1 : 1; theta = bound.evaluateDouble(); } } diff --git a/prism/src/simulator/method/SPRTMethod.java b/prism/src/simulator/method/SPRTMethod.java index 046ff2c6..b3a3adbc 100644 --- a/prism/src/simulator/method/SPRTMethod.java +++ b/prism/src/simulator/method/SPRTMethod.java @@ -30,6 +30,7 @@ package simulator.method; import parser.ast.Expression; import parser.ast.ExpressionProb; import parser.ast.ExpressionReward; +import parser.ast.RelOp; import prism.PrismException; import simulator.sampler.Sampler; import simulator.sampler.SamplerDouble; @@ -109,7 +110,7 @@ public final class SPRTMethod extends SimulationMethod public void setExpression(Expression expr) throws PrismException { Expression bound; - String relOp; + RelOp relOp; double theta; // For P properties... @@ -145,7 +146,7 @@ public final class SPRTMethod extends SimulationMethod } // Set p0/p1 values for two hypotheses // Default case is that H0 means probability/reward >= theta + delta - if (relOp.equals(">") || relOp.equals(">=")) { + if (relOp.isLowerBound()) { p0 = theta + delta; p1 = theta - delta; }