diff --git a/prism/src/explicit/MinMax.java b/prism/src/explicit/MinMax.java index c38371bf..7ee2ccab 100644 --- a/prism/src/explicit/MinMax.java +++ b/prism/src/explicit/MinMax.java @@ -82,6 +82,24 @@ public class MinMax return neg; } + public String toString() + { + if (min) { + return "min"; + } else { + return "max"; + } + } + + public MinMax clone() + { + MinMax result = new MinMax(); + result.min = min; + result.min1 = min1; + result.min2 = min2; + return result; + } + // Utility methods to create instances of this class public static MinMax blank() diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index d05f5a62..86640c90 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -91,6 +91,7 @@ import parser.type.TypeInt; import parser.type.TypePathBool; import parser.type.TypePathDouble; import prism.ModelType; +import prism.OpRelOpBound; import prism.PrismComponent; import prism.PrismException; import prism.PrismSettings; @@ -918,7 +919,9 @@ 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"); } - min = relOp.isLowerBound() || relOp.isMin(); + // Get info from P operator + OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues); + min = opInfo.getMinMax(modelType).isMin(); // Compute probabilities if (!expr.getExpression().isSimplePathFormula()) { @@ -1029,7 +1032,9 @@ final public class ParamModelChecker extends PrismComponent if (r.compareTo(0) == -1) throw new PrismException("Invalid reward bound " + r + " in R[] formula"); } - min = relOp.isLowerBound() || relOp.isMin(); + // Get info from R operator + OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues); + min = opInfo.getMinMax(model.getModelType()).isMin(); ParamRewardStruct rew = constructRewards(model, rewStruct, constantValues); mainLog.println("Building reward structure..."); @@ -1186,7 +1191,9 @@ 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"); } - min = relOp.isLowerBound() || relOp.isMin(); + // Get info from SS operator + OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues); + min = opInfo.getMinMax(modelType).isMin(); // Compute probabilities probs = checkProbSteadyState(model, expr.getExpression(), min, needStates); diff --git a/prism/src/parser/ast/ExpressionProb.java b/prism/src/parser/ast/ExpressionProb.java index 515ce219..5254a0b0 100644 --- a/prism/src/parser/ast/ExpressionProb.java +++ b/prism/src/parser/ast/ExpressionProb.java @@ -86,9 +86,9 @@ public class ExpressionProb extends ExpressionQuant double boundVal = getBound().evaluateDouble(constantValues); if (boundVal < 0 || boundVal > 1) throw new PrismLangException("Invalid probability bound " + boundVal + " in P operator"); - return new OpRelOpBound("P", getRelOp(), boundVal); + return new OpRelOpBound("P", minMax, getRelOp(), boundVal); } else { - return new OpRelOpBound("P", getRelOp(), null); + return new OpRelOpBound("P", minMax, getRelOp(), null); } } @@ -123,12 +123,16 @@ public class ExpressionProb extends ExpressionQuant { if (getBound() != null) return "Result"; - else if (getRelOp() == RelOp.MIN) - return "Minimum probability"; - else if (getRelOp() == RelOp.MAX) - return "Maximum probability"; - else - return "Probability"; + else if (getRelOp() == RelOp.EQ) { + if (minMax != null) { + if (minMax.isMin()) { + return "Minimum probability"; + } else { + return "Maximum probability"; + } + } + } + return "Probability"; } @Override @@ -150,6 +154,7 @@ public class ExpressionProb extends ExpressionQuant { ExpressionProb expr = new ExpressionProb(); expr.setExpression(getExpression() == null ? null : getExpression().deepCopy()); + expr.setMinMax(minMax != null ? minMax.clone() : null); expr.setRelOp(getRelOp()); expr.setBound(getBound() == null ? null : getBound().deepCopy()); expr.setFilter(getFilter() == null ? null : (Filter)getFilter().deepCopy()); @@ -165,7 +170,9 @@ public class ExpressionProb extends ExpressionQuant { String s = ""; - s += "P" + getModifierString() + getRelOp(); + s += "P" + getModifierString(); + s += (minMax != null ? minMax : ""); + s+= getRelOp(); s += (getBound() == null) ? "?" : getBound().toString(); s += " [ " + getExpression(); if (getFilter() != null) diff --git a/prism/src/parser/ast/ExpressionQuant.java b/prism/src/parser/ast/ExpressionQuant.java index 20d2c904..8d6056e3 100644 --- a/prism/src/parser/ast/ExpressionQuant.java +++ b/prism/src/parser/ast/ExpressionQuant.java @@ -26,6 +26,7 @@ package parser.ast; +import explicit.MinMax; import parser.Values; import prism.OpRelOpBound; import prism.PrismException; @@ -38,6 +39,8 @@ public abstract class ExpressionQuant extends Expression { /** Optional "modifier" to specify variants of the P/R/S operator */ protected String modifier = null; + /** The attached min/max operator, if it exists */ + protected MinMax minMax = null; /** The attached relational operator (e.g. "<" in "P<0.1"). */ protected RelOp relOp = null; /** The attached (probability/reward) bound, as an expression (e.g. "p" in "P<p"). Null if absent (e.g. "P=?"). */ @@ -58,6 +61,23 @@ public abstract class ExpressionQuant extends Expression this.modifier = modifier; } + public void setMinMax(MinMax minMax) + { + this.minMax = minMax; + } + + /** Set the attached min/max operator */ + public void setMinMax(String minMaxString) throws PrismException + { + if (minMaxString.equals("min")) { + minMax = MinMax.min(); + } else if (minMaxString.equals("max")) { + minMax = MinMax.max(); + } else { + throw new PrismException("Min/Max has to be either min or max"); + } + } + /** * Set the attached relational operator (e.g. "<" in "P<0.1"). * Uses the enum {@link RelOp}. For example: {@code setRelOp(RelOp.GT);} @@ -119,6 +139,12 @@ public abstract class ExpressionQuant extends Expression return modifier == null ? "" : "(" + modifier + ")"; } + /** Get the optional MinMax operator */ + public MinMax getMinMax() + { + return minMax; + } + /** * Get the attached relational operator (e.g. "<" in "P<0.1"), as a {@link RelOp}. */ diff --git a/prism/src/parser/ast/ExpressionReward.java b/prism/src/parser/ast/ExpressionReward.java index 9a5b8251..788ab3eb 100644 --- a/prism/src/parser/ast/ExpressionReward.java +++ b/prism/src/parser/ast/ExpressionReward.java @@ -197,9 +197,9 @@ public class ExpressionReward extends ExpressionQuant { if (getBound() != null) { double boundValue = getBound().evaluateDouble(constantValues); - return new OpRelOpBound("R", getRelOp(), boundValue); + return new OpRelOpBound("R", minMax, getRelOp(), boundValue); } else { - return new OpRelOpBound("R", getRelOp(), null); + return new OpRelOpBound("R", minMax, getRelOp(), null); } } @@ -246,8 +246,10 @@ public class ExpressionReward extends ExpressionQuant // For R=? properties, use name of reward structure where applicable if (getBound() == null) { String s = "E"; - if (getRelOp() == RelOp.MIN) s = "Minimum e"; - else if (getRelOp() == RelOp.MAX) s = "Maximum e"; + if (minMax != null) { + if (minMax.isMin()) s = "Minimum e"; + else s = "Maximum e"; + } else s = "E"; if (rewardStructIndex instanceof String) { if (rewardStructIndexDiv instanceof String) @@ -287,6 +289,7 @@ public class ExpressionReward extends ExpressionQuant ExpressionReward expr = new ExpressionReward(); expr.setExpression(getExpression() == null ? null : getExpression().deepCopy()); expr.setRelOp(getRelOp()); + expr.setMinMax(minMax == null ? null : minMax.clone() ); expr.setBound(getBound() == null ? null : getBound().deepCopy()); if (rewardStructIndex != null && rewardStructIndex instanceof Expression) expr.setRewardStructIndex(((Expression)rewardStructIndex).deepCopy()); else expr.setRewardStructIndex(rewardStructIndex); @@ -315,6 +318,7 @@ public class ExpressionReward extends ExpressionQuant else if (rewardStructIndexDiv instanceof String) s += "{\""+rewardStructIndexDiv+"\"}"; } } + s += (getMinMax()==null) ? "" : getMinMax(); s += getRelOp(); s += (getBound()==null) ? "?" : getBound().toString(); s += " [ " + getExpression(); diff --git a/prism/src/parser/ast/ExpressionSS.java b/prism/src/parser/ast/ExpressionSS.java index 5a3bd4b3..7d224d20 100644 --- a/prism/src/parser/ast/ExpressionSS.java +++ b/prism/src/parser/ast/ExpressionSS.java @@ -80,9 +80,9 @@ public class ExpressionSS extends ExpressionQuant double boundValue = getBound().evaluateDouble(constantValues); if (boundValue < 0 || boundValue > 1) throw new PrismException("Invalid probability bound " + boundValue + " in P operator"); - return new OpRelOpBound("S", getRelOp(), boundValue); + return new OpRelOpBound("S", minMax, getRelOp(), boundValue); } else { - return new OpRelOpBound("S", getRelOp(), null); + return new OpRelOpBound("S", minMax, getRelOp(), null); } } diff --git a/prism/src/parser/ast/RelOp.java b/prism/src/parser/ast/RelOp.java index b38897cd..4c112798 100644 --- a/prism/src/parser/ast/RelOp.java +++ b/prism/src/parser/ast/RelOp.java @@ -39,19 +39,6 @@ public enum RelOp return (keepStrictness ? LEQ : LT); } }, - MIN("min=") { - @Override - public boolean isMin() - { - return true; - } - - @Override - public RelOp negate(boolean keepStrictness) throws PrismLangException - { - return MAX; - } - }, LT("<") { @Override public boolean isUpperBound() @@ -84,19 +71,6 @@ public enum RelOp return (keepStrictness ? GEQ : GT); } }, - MAX("max=") { - @Override - public boolean isMax() - { - return true; - } - - @Override - public RelOp negate(boolean keepStrictness) throws PrismLangException - { - return MIN; - } - }, EQ("=") { @Override public RelOp negate(boolean keepStrictness) throws PrismLangException @@ -120,7 +94,6 @@ public enum RelOp /** * Returns true if this corresponds to a lower bound (i.e. >, >=). - * NB: "min=?" does not return true for this. */ public boolean isLowerBound() { @@ -129,7 +102,6 @@ public enum RelOp /** * Returns true if this corresponds to an upper bound (i.e. <, <=). - * NB: "max=?" does not return true for this. */ public boolean isUpperBound() { @@ -144,22 +116,6 @@ public enum RelOp return false; } - /** - * Returns true if this corresponds to minimum (min=?). - */ - public boolean isMin() - { - return false; - } - - /** - * Returns true if this corresponds to maximum (max=?). - */ - public boolean isMax() - { - return false; - } - /** * Returns the negated form of this operator. *
diff --git a/prism/src/parser/visitor/CheckValid.java b/prism/src/parser/visitor/CheckValid.java index a5adb299..be07a016 100644 --- a/prism/src/parser/visitor/CheckValid.java +++ b/prism/src/parser/visitor/CheckValid.java @@ -99,13 +99,13 @@ public class CheckValid extends ASTTraverse public void visitPost(ExpressionProb e) throws PrismLangException { - if (modelType.nondeterministic() && e.getRelOp() == RelOp.EQ) + if (modelType.nondeterministic() && e.getRelOp() == RelOp.EQ && e.getMinMax() == null) 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) + if (modelType.nondeterministic() && e.getRelOp() == RelOp.EQ && e.getMinMax() == null) throw new PrismLangException("Can't use \"R=?\" for nondeterministic models; use \"Rmin=?\" or \"Rmax=?\""); if (e.getRewardStructIndexDiv() != null) throw new PrismLangException("No support for ratio reward objectives yet"); diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index b06b5ac7..823dae6e 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/prism/src/prism/MultiObjModelChecker.java @@ -42,6 +42,7 @@ import jdd.JDDVars; import mtbdd.PrismMTBDD; import parser.ast.Expression; import parser.ast.RelOp; +import explicit.MinMax; import sparse.NDSparseMatrix; import sparse.PrismSparse; import acceptance.AcceptanceRabin; @@ -271,7 +272,7 @@ public class MultiObjModelChecker extends PrismComponent opsAndBounds.getProbStepBound(i), i); } } - tmpOpsAndBounds.add(new OpRelOpBound("R", RelOp.MAX, -1.0), Operator.R_MAX, -1.0, -1, opsAndBounds.probSize()); + tmpOpsAndBounds.add(new OpRelOpBound("R", MinMax.max(), RelOp.EQ, -1.0), Operator.R_MAX, -1.0, -1, opsAndBounds.probSize()); ArrayList tmprewards = new ArrayList(1); tmprewards.add(rtarget); diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 8788d971..20f299c6 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -838,16 +838,21 @@ public class NondetModelChecker extends NonProbModelChecker if (relOp.isStrict()) { throw new PrismException("Multi-objective properties can not use strict inequalities on P/R operators"); } - Operator op; - if (relOp == RelOp.MAX) { - op = (exprProb != null) ? Operator.P_MAX : Operator.R_MAX; + Operator op = null; + if (relOp == RelOp.EQ) { + if (exprQuant.getMinMax() != null) { + if (exprQuant.getMinMax().isMax()) { + op = (exprProb != null) ? Operator.P_MAX : Operator.R_MAX; + } else { + op = (exprProb != null) ? Operator.P_MIN : Operator.R_MIN; + } + } } else if (relOp == RelOp.GEQ) { op = (exprProb != null) ? Operator.P_GE : Operator.R_GE; - } else if (relOp == RelOp.MIN) { - op = (exprProb != null) ? Operator.P_MIN : Operator.R_MIN; } else if (relOp == RelOp.LEQ) { op = (exprProb != null) ? Operator.P_LE : Operator.R_LE; - } else { + } + if (op == null) { throw new PrismException("Multi-objective properties can only contain P/R operators with max/min=? or lower/upper probability bounds"); } // Find bound @@ -876,7 +881,7 @@ public class NondetModelChecker extends NonProbModelChecker for (JDDNode set : tmpecs) acceptingStates = JDD.Or(acceptingStates, set); targetDDs.add(acceptingStates); - OpRelOpBound opInfo = new OpRelOpBound("P", RelOp.GEQ, 0.0); + OpRelOpBound opInfo = new OpRelOpBound("P", null, RelOp.GEQ, 0.0); opsAndBounds.add(opInfo, Operator.P_GE, 0.0, -1, -1); } diff --git a/prism/src/prism/OpRelOpBound.java b/prism/src/prism/OpRelOpBound.java index b22398ae..fb4b14b6 100644 --- a/prism/src/prism/OpRelOpBound.java +++ b/prism/src/prism/OpRelOpBound.java @@ -36,12 +36,14 @@ public class OpRelOpBound { protected String op; protected RelOp relOp; + protected MinMax minMax; protected boolean numeric; protected double bound; - public OpRelOpBound(String op, RelOp relOp, Double boundObject) + public OpRelOpBound(String op, MinMax minMax, RelOp relOp, Double boundObject) { this.op = op; + this.minMax = minMax; this.relOp = relOp; numeric = (boundObject == null); if (boundObject != null) @@ -73,6 +75,11 @@ public class OpRelOpBound return bound; } + public boolean hasExplicitMinMax() + { + return minMax != null; + } + public boolean isQualitative() { return !isNumeric() && op.equals("P") && (bound == 0 || bound == 1); @@ -111,7 +118,12 @@ public class OpRelOpBound public MinMax getMinMax(ModelType modelType, boolean forAll) throws PrismLangException { + if (this.minMax != null) { + return this.minMax; + } + MinMax minMax = MinMax.blank(); + if (modelType.nondeterministic()) { if (!(modelType == ModelType.MDP || modelType == ModelType.POMDP || modelType == ModelType.CTMDP)) { throw new PrismLangException("Don't know how to model check " + getTypeOfOperator() + " properties for " + modelType + "s"); @@ -120,7 +132,6 @@ public class OpRelOpBound if (relOp == RelOp.EQ) { throw new PrismLangException("Can't use \"" + op + "=?\" for nondeterministic models; use e.g. \"" + op + "min=?\" or \"" + op + "max=?\""); } - minMax = relOp.isMin() ? MinMax.min() : MinMax.max(); } else { if (forAll) { minMax = (relOp.isLowerBound() ) ? MinMax.min() : MinMax.max(); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 4e775e73..8017a2fa 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -187,7 +187,7 @@ public class ProbModelChecker extends NonProbModelChecker } // Print a warning if Pmin/Pmax used - if (opInfo.getRelOp() == RelOp.MIN || opInfo.getRelOp() == RelOp.MAX) { + if (opInfo.hasExplicitMinMax()) { mainLog.printWarning("\"Pmin=?\" and \"Pmax=?\" operators are identical to \"P=?\" for DTMCs/CTMCs"); } @@ -235,7 +235,7 @@ public class ProbModelChecker extends NonProbModelChecker JDDNode transRewards = getTransitionRewardsByIndexObject(rs, model, constantValues); // Print a warning if Rmin/Rmax used - if (opInfo.getRelOp() == RelOp.MIN || opInfo.getRelOp() == RelOp.MAX) { + if (opInfo.hasExplicitMinMax()) { mainLog.printWarning("\"Rmin=?\" and \"Rmax=?\" operators are identical to \"R=?\" for DTMCs/CTMCs"); } diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java index 9e31d670..cc2a80fe 100644 --- a/prism/src/pta/PTAModelChecker.java +++ b/prism/src/pta/PTAModelChecker.java @@ -194,7 +194,9 @@ 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 = relOp.isLowerBound() || relOp.isMin(); + // Get info from P operator + OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues); + min = opInfo.getMinMax(ModelType.PTA).isMin(); // Check this is a F path property (only case allowed at the moment) if (!(expr.getExpression() instanceof ExpressionTemporal))