diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index a41c889a..d08f0722 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -137,7 +137,7 @@ public class CTMCModelChecker extends ProbModelChecker // lower bound is 0 if not specified // (i.e. if until is of form U<=t) - exprTmp = expr.getLowerBound(); + exprTmp = expr.bound == null ? null : expr.bound.getLowerBound(); if (exprTmp != null) { lTime = exprTmp.evaluateDouble(constantValues); if (lTime < 0) { @@ -148,11 +148,11 @@ public class CTMCModelChecker extends ProbModelChecker } // upper bound is -1 if not specified // (i.e. if until is of form U>=t) - exprTmp = expr.getUpperBound(); + exprTmp = expr.bound == null ? null : expr.bound.getUpperBound(); if (exprTmp != null) { uTime = exprTmp.evaluateDouble(constantValues); - if (uTime < 0 || (uTime == 0 && expr.upperBoundIsStrict())) { - String bound = (expr.upperBoundIsStrict() ? "<" : "<=") + uTime; + if (uTime < 0 || (uTime == 0 && expr.bound.upperBoundIsStrict())) { + String bound = (expr.bound.upperBoundIsStrict() ? "<" : "<=") + uTime; throw new PrismException("Invalid upper bound " + bound + " in time-bounded until formula"); } if (uTime < lTime) { diff --git a/prism/src/explicit/CTMDPModelChecker.java b/prism/src/explicit/CTMDPModelChecker.java index 2f06113e..ce970439 100644 --- a/prism/src/explicit/CTMDPModelChecker.java +++ b/prism/src/explicit/CTMDPModelChecker.java @@ -65,9 +65,9 @@ public class CTMDPModelChecker extends ProbModelChecker ModelCheckerResult res = null; // get info from bounded until - uTime = expr.getUpperBound().evaluateDouble(constantValues); - if (uTime < 0 || (uTime == 0 && expr.upperBoundIsStrict())) { - String bound = (expr.upperBoundIsStrict() ? "<" : "<=") + uTime; + uTime = expr.bound == null ? null : expr.bound.getUpperBound().evaluateDouble(constantValues); + if (uTime < 0 || (uTime == 0 && expr.bound.upperBoundIsStrict())) { + String bound = (expr.bound.upperBoundIsStrict() ? "<" : "<=") + uTime; throw new PrismException("Invalid upper bound " + bound + " in time-bounded until formula"); } diff --git a/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java b/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java index c477a2fe..16e49455 100644 --- a/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java +++ b/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java @@ -143,13 +143,13 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent } double timeLower = 0.0; - if (exprTemp.getLowerBound() != null) { - timeLower = exprTemp.getLowerBound().evaluateDouble(constantValues); + if (exprTemp.bound != null && exprTemp.bound.getLowerBound() != null) { + timeLower = exprTemp.bound.getLowerBound().evaluateDouble(constantValues); } - if (exprTemp.getUpperBound() == null) { + if (exprTemp.bound == null || exprTemp.bound.getUpperBound() == null) { throw new PrismNotSupportedException("Fast adaptive uniformisation window model checking currently requires an upper time bound"); } - double timeUpper = exprTemp.getUpperBound().evaluateDouble(constantValues); + double timeUpper = exprTemp.bound.getUpperBound().evaluateDouble(constantValues); if (!exprTemp.hasBounds()) { throw new PrismNotSupportedException("Fast adaptive uniformisation window model checking currently only supports timed properties"); @@ -237,7 +237,7 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent default: throw new PrismNotSupportedException("Currently only instantaneous or cumulative rewards are allowed."); } - double time = temporal.getUpperBound().evaluateDouble(constantValues); + double time = temporal.bound.getUpperBound().evaluateDouble(constantValues); RewardStruct rewStruct = modulesFile.getRewardStruct(expr.getRewardStructIndexByIndexObject(modulesFile.getRewardStructNames(), constantValues)); fau.setRewardStruct(rewStruct); fau.setConstantValues(constantValues); diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 68c8c20c..9eb1682e 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -988,17 +988,17 @@ public class ProbModelChecker extends NonProbModelChecker ModelCheckerResult res = null; switch (model.getModelType()) { case DTMC: { - int k = expr.getUpperBound().evaluateInt(constantValues); + int k = expr.bound.getUpperBound().evaluateInt(constantValues); res = ((DTMCModelChecker) this).computeInstantaneousRewards((DTMC) model, (MCRewards) modelRewards, k, statesOfInterest); break; } case CTMC: { - double t = expr.getUpperBound().evaluateDouble(constantValues); + double t = expr.bound.getUpperBound().evaluateDouble(constantValues); res = ((CTMCModelChecker) this).computeInstantaneousRewards((CTMC) model, (MCRewards) modelRewards, t); break; } case MDP: { - int k = expr.getUpperBound().evaluateInt(constantValues); + int k = expr.bound.getUpperBound().evaluateInt(constantValues); res = ((MDPModelChecker) this).computeInstantaneousRewards((MDP) model, (MDPRewards) modelRewards, k, minMax.isMin()); break; } @@ -1019,18 +1019,18 @@ public class ProbModelChecker extends NonProbModelChecker double timeDouble = -1; // Check that there is an upper time bound - if (expr.getUpperBound() == null) { + if (expr.bound == null || expr.bound.getUpperBound() == null) { throw new PrismNotSupportedException("This is not a cumulative reward operator"); } // Get time bound if (model.getModelType().continuousTime()) { - timeDouble = expr.getUpperBound().evaluateDouble(constantValues); + timeDouble = expr.bound.getUpperBound().evaluateDouble(constantValues); if (timeDouble < 0) { throw new PrismException("Invalid time bound " + timeDouble + " in cumulative reward formula"); } } else { - timeInt = expr.getUpperBound().evaluateInt(constantValues); + timeInt = expr.bound.getUpperBound().evaluateInt(constantValues); if (timeInt < 0) { throw new PrismException("Invalid time bound " + timeInt + " in cumulative reward formula"); } @@ -1069,7 +1069,7 @@ public class ProbModelChecker extends NonProbModelChecker protected StateValues checkRewardTotal(Model model, Rewards modelRewards, ExpressionTemporal expr, MinMax minMax) throws PrismException { // Check that there is no upper time bound - if (expr.getUpperBound() != null) { + if (expr.getBound().getUpperBound() != null) { throw new PrismException("This is not a total reward operator"); } diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index 96ca0351..417fbfd1 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -1228,15 +1228,19 @@ Expression ExpressionTemporalUnary(boolean prop, boolean pathprop) : void TimeBound(ExpressionTemporal exprTemp) : { Expression lBound, uBound; + TemporalOperatorBound bound = new TemporalOperatorBound(); } { - ( ( ( LOOKAHEAD(IdentifierExpression() ) uBound = IdentifierExpression() | uBound = Expression(false, false) ) { exprTemp.setUpperBound(uBound, false); } ) - | ( ( LOOKAHEAD(IdentifierExpression() ) uBound = IdentifierExpression() | uBound = Expression(false, false) ) { exprTemp.setUpperBound(uBound, true); } ) - | ( ( LOOKAHEAD(IdentifierExpression() ) lBound = IdentifierExpression() | lBound = Expression(false, false) ) { exprTemp.setLowerBound(lBound, false); } ) - | ( ( LOOKAHEAD(IdentifierExpression() ) lBound = IdentifierExpression() | lBound = Expression(false, false) ) { exprTemp.setLowerBound(lBound, true); } ) - | ( lBound = Expression(false, false) uBound = Expression(false, false) { exprTemp.setLowerBound(lBound, false); exprTemp.setUpperBound(uBound, false); } ) - | ( lBound = Expression(false, false) { exprTemp.setEqualBounds(lBound); } ) + ( ( ( LOOKAHEAD(IdentifierExpression() ) uBound = IdentifierExpression() | uBound = Expression(false, false) ) { bound.setUpperBound(uBound, false); } ) + | ( ( LOOKAHEAD(IdentifierExpression() ) uBound = IdentifierExpression() | uBound = Expression(false, false) ) { bound.setUpperBound(uBound, true); } ) + | ( ( LOOKAHEAD(IdentifierExpression() ) lBound = IdentifierExpression() | lBound = Expression(false, false) ) { bound.setLowerBound(lBound, false); } ) + | ( ( LOOKAHEAD(IdentifierExpression() ) lBound = IdentifierExpression() | lBound = Expression(false, false) ) { bound.setLowerBound(lBound, true); } ) + | ( lBound = Expression(false, false) uBound = Expression(false, false) { bound.setLowerBound(lBound, false); bound.setUpperBound(uBound, false); } ) + | ( lBound = Expression(false, false) { bound.setEqualBounds(lBound); } ) ) + { + exprTemp.setBound(bound); + } } // Expression: if-then-else, i.e. "cond ? then : else" @@ -1813,6 +1817,7 @@ Expression ExpressionRewardContents(boolean prop, boolean pathprop) : ExpressionTemporal exprTemp = null; Expression ret = null; Token begin; + TemporalOperatorBound b = new TemporalOperatorBound(); } { { begin = getToken(1); } @@ -1822,9 +1827,9 @@ Expression ExpressionRewardContents(boolean prop, boolean pathprop) : | { ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null); } // Normal reward operators (excluding S; see above) - | LOOKAHEAD( ) begin = expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; } + | LOOKAHEAD( ) begin = expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); b.setUpperBound(expr); exprTemp.setBound(b); ret = exprTemp; } | { ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); } - | expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; } + | expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); b.setUpperBound(expr); exprTemp.setBound(b); ret = exprTemp; } // Path formula (including F "target") | expr = Expression(prop, true) { ret = expr; } diff --git a/prism/src/parser/ast/ExpressionTemporal.java b/prism/src/parser/ast/ExpressionTemporal.java index 21564b4d..b96ca510 100644 --- a/prism/src/parser/ast/ExpressionTemporal.java +++ b/prism/src/parser/ast/ExpressionTemporal.java @@ -56,14 +56,9 @@ public class ExpressionTemporal extends Expression /** RHS of operator, null for nullary operators (e.g., S) */ protected Expression operand2 = null; - // Optional (time) bounds - protected Expression lBound = null; // None if null, i.e. zero - protected Expression uBound = null; // None if null, i.e. infinity - // Strictness of (time) bounds - protected boolean lBoundStrict = false; // true: >, false: >= - protected boolean uBoundStrict = false; // true: <, false: <= - // Display as =T rather than [T,T] ? - protected boolean equals = false; + + // optional bound + public TemporalOperatorBound bound; // Constructors @@ -105,65 +100,13 @@ public class ExpressionTemporal extends Expression operand2 = e2; } - /** - * Set lower time bound to be of form >= e - * (null denotes no lower bound, i.e. zero) - */ - public void setLowerBound(Expression e) - { - setLowerBound(e, false); - } - - /** - * Set lower time bound to be of form >= e or > e - * (null denotes no lower bound, i.e. zero) - */ - public void setLowerBound(Expression e, boolean strict) - { - lBound = e; - lBoundStrict = strict; - } - - /** - * Set upper time bound to be of form <= e - * (null denotes no upper bound, i.e. infinity) - */ - public void setUpperBound(Expression e) - { - setUpperBound(e, false); - } - - /** - * Set upper time bound to be of form <= e or < e - * (null denotes no upper bound, i.e. infinity) - */ - public void setUpperBound(Expression e, boolean strict) - { - uBound = e; - uBoundStrict = strict; - } - - /** - * Set both lower/upper time bound to e, i.e. "=e". - */ - public void setEqualBounds(Expression e) - { - lBound = e; - lBoundStrict = false; - uBound = e; - uBoundStrict = false; - equals = true; - } - /** * Take the bounds information from the other ExpressionTemporal * and store them in this ExpressionTemporal (no deep copy). */ public void setBoundsFrom(ExpressionTemporal exprTemp) { - setLowerBound(exprTemp.getLowerBound(), exprTemp.lowerBoundIsStrict()); - setUpperBound(exprTemp.getUpperBound(), exprTemp.upperBoundIsStrict()); - equals = exprTemp.equals; + bound = exprTemp.getBound(); } // Get methods @@ -200,38 +143,16 @@ public class ExpressionTemporal extends Expression return (operand1 == null) ? 1 : 2; } - public boolean hasBounds() + public TemporalOperatorBound getBound() { - return lBound != null || uBound != null; + return bound; } - public Expression getLowerBound() - { - return lBound; - } - - public boolean lowerBoundIsStrict() - { - return lBoundStrict; - } - - public Expression getUpperBound() + public boolean hasBounds() { - return uBound; + return bound != null; } - public boolean upperBoundIsStrict() - { - return uBoundStrict; - } - - /** - * Returns true if lower/upper bound are equal and should be displayed as =T - */ - public boolean getEquals() - { - return equals; - } // Methods required for Expression: @@ -282,13 +203,17 @@ public class ExpressionTemporal extends Expression expr.setOperand1(operand1.deepCopy()); if (operand2 != null) expr.setOperand2(operand2.deepCopy()); - expr.setLowerBound(lBound == null ? null : lBound.deepCopy(), lBoundStrict); - expr.setUpperBound(uBound == null ? null : uBound.deepCopy(), uBoundStrict); - expr.equals = equals; + if (bound != null) { + expr.setBound((TemporalOperatorBound) bound.deepCopy()); + } expr.setType(type); expr.setPosition(this); return expr; } + + public void setBound(TemporalOperatorBound bound) { + this.bound = bound; + } // Standard methods @@ -299,21 +224,23 @@ public class ExpressionTemporal extends Expression if (operand1 != null) s += operand1 + " "; s += opSymbols[op]; - if (lBound == null) { - if (uBound != null) { - if (op != R_I) - s += "<" + (uBoundStrict ? "" : "=") + uBound; - else - s += "=" + uBound; - } - } else { - if (uBound == null) { - s += ">" + (lBoundStrict ? "" : "=") + lBound; + if (bound != null) { + if (bound.getLowerBound() == null) { + if (bound.getUpperBound() != null) { + if (op != R_I) + s += "<" + (bound.upperBoundIsStrict() ? "" : "=") + bound.getUpperBound(); + else + s += "=" + bound.getUpperBound(); + } } else { - if (equals) - s += "=" + lBound; - else - s += "[" + lBound + "," + uBound + "]"; + if (bound.getUpperBound() == null) { + s += ">" + (bound.lowerBoundIsStrict() ? "" : "=") + bound.getLowerBound(); + } else { + if (bound.getEquals()) + s += "=" + bound.getLowerBound(); + else + s += "[" + bound.getLowerBound() + "," + bound.getUpperBound() + "]"; + } } } if (operand2 != null) @@ -326,14 +253,10 @@ public class ExpressionTemporal extends Expression { final int prime = 31; int result = 1; - result = prime * result + (equals ? 1231 : 1237); - result = prime * result + ((lBound == null) ? 0 : lBound.hashCode()); - result = prime * result + (lBoundStrict ? 1231 : 1237); + result = prime * result + ((bound == null) ? 0 : bound.hashCode()); result = prime * result + op; result = prime * result + ((operand1 == null) ? 0 : operand1.hashCode()); result = prime * result + ((operand2 == null) ? 0 : operand2.hashCode()); - result = prime * result + ((uBound == null) ? 0 : uBound.hashCode()); - result = prime * result + (uBoundStrict ? 1231 : 1237); return result; } @@ -344,17 +267,13 @@ public class ExpressionTemporal extends Expression return true; if (obj == null) return false; - if (getClass() != obj.getClass()) + if (!(obj instanceof ExpressionTemporal)) return false; ExpressionTemporal other = (ExpressionTemporal) obj; - if (equals != other.equals) - return false; - if (lBound == null) { - if (other.lBound != null) + if (bound == null) { + if (other.bound != null) return false; - } else if (!lBound.equals(other.lBound)) - return false; - if (lBoundStrict != other.lBoundStrict) + } else if (!bound.equals(other.bound)) return false; if (op != other.op) return false; @@ -368,13 +287,6 @@ public class ExpressionTemporal extends Expression return false; } else if (!operand2.equals(other.operand2)) return false; - if (uBound == null) { - if (other.uBound != null) - return false; - } else if (!uBound.equals(other.uBound)) - return false; - if (uBoundStrict != other.uBoundStrict) - return false; return true; } diff --git a/prism/src/parser/visitor/ASTTraverse.java b/prism/src/parser/visitor/ASTTraverse.java index 4ee886b9..107b9355 100644 --- a/prism/src/parser/visitor/ASTTraverse.java +++ b/prism/src/parser/visitor/ASTTraverse.java @@ -426,8 +426,7 @@ public class ASTTraverse implements ASTVisitor visitPre(e); if (e.getOperand1() != null) e.getOperand1().accept(this); if (e.getOperand2() != null) e.getOperand2().accept(this); - if (e.getLowerBound() != null) e.getLowerBound().accept(this); - if (e.getUpperBound() != null) e.getUpperBound().accept(this); + if (e.bound != null) e.bound.accept(this); visitPost(e); return null; } diff --git a/prism/src/parser/visitor/ASTTraverseModify.java b/prism/src/parser/visitor/ASTTraverseModify.java index 24269b7c..aaa7bb9b 100644 --- a/prism/src/parser/visitor/ASTTraverseModify.java +++ b/prism/src/parser/visitor/ASTTraverseModify.java @@ -438,8 +438,7 @@ public class ASTTraverseModify implements ASTVisitor visitPre(e); if (e.getOperand1() != null) e.setOperand1((Expression)(e.getOperand1().accept(this))); if (e.getOperand2() != null) e.setOperand2((Expression)(e.getOperand2().accept(this))); - if (e.getLowerBound() != null) e.setLowerBound((Expression)(e.getLowerBound().accept(this)), e.lowerBoundIsStrict()); - if (e.getUpperBound() != null) e.setUpperBound((Expression)(e.getUpperBound().accept(this)), e.upperBoundIsStrict()); + if (e.getBound() != null) e.setBound((TemporalOperatorBound) e.bound.accept(this)); visitPost(e); return e; } diff --git a/prism/src/parser/visitor/CheckValid.java b/prism/src/parser/visitor/CheckValid.java index 260b145e..86487b1f 100644 --- a/prism/src/parser/visitor/CheckValid.java +++ b/prism/src/parser/visitor/CheckValid.java @@ -59,15 +59,15 @@ public class CheckValid extends ASTTraverse } } // PTA only support upper time bounds - if (e.getLowerBound() != null) { + if (e.bound != null && e.bound.getLowerBound() != null) { if (modelType == ModelType.PTA || modelType == ModelType.POPTA) { throw new PrismLangException("Only upper time bounds are allowed on the " + e.getOperatorSymbol() + " operator for " + modelType + "s"); } } // Apart from CTMCs, we only support integer time bounds - if ((e.getUpperBound() != null && !(e.getUpperBound().getType() instanceof TypeInt)) || - (e.getLowerBound() != null && !(e.getLowerBound().getType() instanceof TypeInt))) { + if ((e.bound != null && e.bound.getUpperBound() != null && !(e.bound.getUpperBound().getType() instanceof TypeInt)) || + (e.bound != null && e.bound.getLowerBound() != null && !(e.bound.getLowerBound().getType() instanceof TypeInt))) { if (modelType == ModelType.DTMC) { throw new PrismLangException("Time bounds on the " + e.getOperatorSymbol() + " operator must be integers for DTMCs"); @@ -82,7 +82,7 @@ public class CheckValid extends ASTTraverse } } // Don't allow lower bounds on weak until - does not have intuitive semantics - if (e.getOperator() == ExpressionTemporal.P_W && e.getLowerBound() != null) { + if (e.getOperator() == ExpressionTemporal.P_W && e.getBound().hasLowerBound()) { throw new PrismLangException("The weak until operator (W) with lower bounds is not yet supported"); } } diff --git a/prism/src/parser/visitor/PropertiesSemanticCheck.java b/prism/src/parser/visitor/PropertiesSemanticCheck.java index 2709fced..8d8debb1 100644 --- a/prism/src/parser/visitor/PropertiesSemanticCheck.java +++ b/prism/src/parser/visitor/PropertiesSemanticCheck.java @@ -38,6 +38,7 @@ import parser.ast.FormulaList; import parser.ast.LabelList; import parser.ast.ModulesFile; import parser.ast.PropertiesFile; +import parser.ast.TemporalOperatorBound; import prism.ModelInfo; import prism.PrismLangException; @@ -116,8 +117,8 @@ public class PropertiesSemanticCheck extends SemanticCheck int op = e.getOperator(); Expression operand1 = e.getOperand1(); Expression operand2 = e.getOperand2(); - Expression lBound = e.getLowerBound(); - Expression uBound = e.getUpperBound(); + Expression lBound = e.bound.getLowerBound(); + Expression uBound = e.bound.getUpperBound(); if (lBound != null && !lBound.isConstant()) { throw new PrismLangException("Lower bound in " + e.getOperatorSymbol() + " operator is not constant", lBound); } @@ -140,6 +141,18 @@ public class PropertiesSemanticCheck extends SemanticCheck } } + public void visitPost(TemporalOperatorBound e) throws PrismLangException + { + Expression lBound = e.getLowerBound(); + Expression uBound = e.getUpperBound(); + if (lBound != null && !lBound.isConstant()) { + throw new PrismLangException("Lower bound " + e + " is not constant", lBound); + } + if (uBound != null && !uBound.isConstant()) { + throw new PrismLangException("Upper bound " + e + " not constant", uBound); + } + } + public void visitPost(ExpressionProb e) throws PrismLangException { if (e.getModifier() != null) { diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index 44abc3dc..8478f155 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/prism/src/parser/visitor/TypeCheck.java @@ -168,11 +168,11 @@ public class TypeCheck extends ASTTraverse public void visitPost(ExpressionTemporal e) throws PrismLangException { Type type; - if (e.getLowerBound() != null && !TypeDouble.getInstance().canAssign(e.getLowerBound().getType())) { - throw new PrismLangException("Type error: Lower bound in " + e.getOperatorSymbol() + " operator must be an int or double", e.getLowerBound()); + if (e.bound != null && e.bound.getLowerBound() != null && !TypeDouble.getInstance().canAssign(e.bound.getLowerBound().getType())) { + throw new PrismLangException("Type error: Lower bound in " + e.getOperatorSymbol() + " operator must be an int or double", e.bound.getLowerBound()); } - if (e.getUpperBound() != null && !TypeDouble.getInstance().canAssign(e.getUpperBound().getType())) { - throw new PrismLangException("Type error: Upper bound in " + e.getOperatorSymbol() + " operator must be an int or double", e.getUpperBound()); + if (e.bound != null && e.bound.getUpperBound() != null && !TypeDouble.getInstance().canAssign(e.bound.getUpperBound().getType())) { + throw new PrismLangException("Type error: Upper bound in " + e.getOperatorSymbol() + " operator must be an int or double", e.bound.getUpperBound()); } switch (e.getOperator()) { case ExpressionTemporal.P_X: diff --git a/prism/src/prism/IntegerBound.java b/prism/src/prism/IntegerBound.java index 8640bc05..48ae6b39 100644 --- a/prism/src/prism/IntegerBound.java +++ b/prism/src/prism/IntegerBound.java @@ -28,6 +28,7 @@ package prism; import parser.Values; import parser.ast.ExpressionTemporal; +import parser.ast.TemporalOperatorBound; /** * Canonical representation of an integer bound, with strict/non-strict lower and upper bound. @@ -93,10 +94,16 @@ public class IntegerBound */ public static IntegerBound fromExpressionTemporal(ExpressionTemporal expression, Values constantValues, boolean check) throws PrismException { - IntegerBound bounds = new IntegerBound(expression.getLowerBound() == null ? null : expression.getLowerBound().evaluateInt(constantValues), - expression.lowerBoundIsStrict(), - expression.getUpperBound() == null ? null : expression.getUpperBound().evaluateInt(constantValues), - expression.upperBoundIsStrict()); + TemporalOperatorBound eBound = expression.bound; + IntegerBound bounds; + if (eBound == null) { + bounds = new IntegerBound(null, false, null, false); + } else { + bounds = new IntegerBound(eBound.getLowerBound() == null ? null : eBound.getLowerBound().evaluateInt(constantValues), + eBound.lowerBoundIsStrict(), + eBound.getUpperBound() == null ? null : eBound.getUpperBound().evaluateInt(constantValues), + eBound.upperBoundIsStrict()); + } if (check) { if (bounds.hasNegativeBound()) { diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 2d485d5d..0d893234 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -782,11 +782,11 @@ public class NondetModelChecker extends NonProbModelChecker Expression expr = exprProb.getExpression(); if (expr.isSimplePathFormula() && Expression.isReach(expr)) { ExpressionTemporal exprTemp = ((ExpressionTemporal) expr); - if (exprTemp.getLowerBound() != null) { + if (exprTemp.bound != null && exprTemp.bound.getLowerBound() != null) { throw new PrismException("Lower time bounds are not supported in multi-objective queries"); } - if (exprTemp.getUpperBound() != null) { - stepBound = exprTemp.getUpperBound().evaluateInt(constantValues); + if (exprTemp.bound != null && exprTemp.bound.getUpperBound() != null) { + stepBound = exprTemp.bound.getUpperBound().evaluateInt(constantValues); } else { stepBound = -1; } @@ -806,8 +806,8 @@ public class NondetModelChecker extends NonProbModelChecker + exprTemp.getOperatorSymbol() + ")"); } // R [ C<=k ] - if (exprTemp.getUpperBound() != null) { - stepBound = exprTemp.getUpperBound().evaluateInt(constantValues); + if (exprTemp.bound != null && exprTemp.bound.getUpperBound() != null) { + stepBound = exprTemp.bound.getUpperBound().evaluateInt(constantValues); } // R [ C ] else { @@ -1345,12 +1345,12 @@ public class NondetModelChecker extends NonProbModelChecker JDD.Deref(statesOfInterest); // check that there is an upper time bound - if (expr.getUpperBound() == null) { + if (expr.bound == null || expr.bound.getUpperBound() == null) { throw new PrismException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries"); } // get info from inst reward - time = expr.getUpperBound().evaluateInt(constantValues); + time = expr.bound.getUpperBound().evaluateInt(constantValues); if (time < 0) { throw new PrismException("Invalid time bound " + time + " in cumulative reward formula"); } @@ -1397,7 +1397,7 @@ public class NondetModelChecker extends NonProbModelChecker JDD.Deref(statesOfInterest); // get info from bounded until - time = expr.getUpperBound().evaluateInt(constantValues); + time = expr.bound.getUpperBound().evaluateInt(constantValues); if (time < 0) { throw new PrismException("Invalid bound " + time + " in instantaneous reward property"); } diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 8e61c0eb..d79e3833 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -833,12 +833,12 @@ public class ProbModelChecker extends NonProbModelChecker JDD.Deref(statesOfInterest); // check that there is an upper time bound - if (expr.getUpperBound() == null) { + if (expr.bound == null || expr.bound.getUpperBound() == null) { throw new PrismException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries"); } // get info from inst reward - time = expr.getUpperBound().evaluateInt(constantValues); + time = expr.bound.getUpperBound().evaluateInt(constantValues); if (time < 0) { throw new PrismException("Invalid time bound " + time + " in cumulative reward formula"); } @@ -888,7 +888,7 @@ public class ProbModelChecker extends NonProbModelChecker JDD.Deref(statesOfInterest); // get info from inst reward - time = expr.getUpperBound().evaluateInt(constantValues); + time = expr.bound.getUpperBound().evaluateInt(constantValues); if (time < 0) { throw new PrismException("Invalid bound " + time + " in instantaneous reward property"); } diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java index d7fd13d8..4ad35fd2 100644 --- a/prism/src/prism/StochModelChecker.java +++ b/prism/src/prism/StochModelChecker.java @@ -92,7 +92,7 @@ public class StochModelChecker extends ProbModelChecker // lower bound is 0 if not specified // (i.e. if until is of form U<=t) - exprTmp = expr.getLowerBound(); + exprTmp = expr.bound == null ? null : expr.bound.getLowerBound(); if (exprTmp != null) { lTime = exprTmp.evaluateDouble(constantValues); if (lTime < 0) { @@ -103,11 +103,11 @@ public class StochModelChecker extends ProbModelChecker } // upper bound is -1 if not specified // (i.e. if until is of form U>=t) - exprTmp = expr.getUpperBound(); + exprTmp = expr.bound == null ? null : expr.bound.getUpperBound(); if (exprTmp != null) { uTime = exprTmp.evaluateDouble(constantValues); - if (uTime < 0 || (uTime == 0 && expr.upperBoundIsStrict())) { - String bound = (expr.upperBoundIsStrict() ? "<" : "<=") + uTime; + if (uTime < 0 || (uTime == 0 && expr.bound.upperBoundIsStrict())) { + String bound = (expr.bound.upperBoundIsStrict() ? "<" : "<=") + uTime; throw new PrismException("Invalid upper bound " + bound + " in time-bounded until formula"); } if (uTime < lTime) { @@ -240,7 +240,7 @@ public class StochModelChecker extends ProbModelChecker JDD.Deref(statesOfInterest); // get info from inst reward - time = expr.getUpperBound().evaluateDouble(constantValues); + time = expr.bound.getUpperBound().evaluateDouble(constantValues); if (time < 0) { throw new PrismException("Invalid time bound " + time + " in cumulative reward formula"); } @@ -274,7 +274,7 @@ public class StochModelChecker extends ProbModelChecker JDD.Deref(statesOfInterest); // get info from inst reward - time = expr.getUpperBound().evaluateDouble(constantValues); + time = expr.bound.getUpperBound().evaluateDouble(constantValues); if (time < 0) { throw new PrismException("Invalid bound " + time + " in instantaneous reward property"); } diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java index 1d67a4f5..3758f452 100644 --- a/prism/src/pta/DigitalClocks.java +++ b/prism/src/pta/DigitalClocks.java @@ -383,7 +383,7 @@ public class DigitalClocks public Object visit(ExpressionTemporal e) throws PrismLangException { // Push (new) time bound into target - e.setUpperBound(null); + e.bound.setUpperBound(null); Expression targetNew = Expression.And(e.getOperand2().deepCopy(), boundNew); e.setOperand2(targetNew); return e; @@ -437,14 +437,14 @@ public class DigitalClocks { public void visitPost(ExpressionTemporal e) throws PrismLangException { - if (e.getLowerBound() != null) { + if (e.bound != null && e.bound.getLowerBound() != null) { throw new PrismLangException("The digital clocks method does not yet support lower time bounds"); } - if (e.getUpperBound() != null) { + if (e.bound != null && e.bound.getUpperBound() != null) { if (!ExpressionTemporal.isFinally(e)) { throw new PrismLangException("The digital clocks method only ssupport time bounds on F"); } - timeBound = e.getUpperBound().evaluateInt(constantValues); + timeBound = e.bound.getUpperBound().evaluateInt(constantValues); } } }); @@ -715,11 +715,11 @@ public class DigitalClocks // (so just evaluate directly) // We also don't care about the max value - this is done elsewhere; // we just want to make sure that the values is used to compute the GCD - if (e.getLowerBound() != null) { - allClockVals.add(e.getLowerBound().evaluateInt(constantValues)); + if (e.bound.getLowerBound() != null) { + allClockVals.add(e.bound.getLowerBound().evaluateInt(constantValues)); } - if (e.getUpperBound() != null) { - allClockVals.add(e.getUpperBound().evaluateInt(constantValues)); + if (e.bound.getUpperBound() != null) { + allClockVals.add(e.bound.getUpperBound().evaluateInt(constantValues)); } } diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java index 93b8af5f..997c587a 100644 --- a/prism/src/pta/PTAModelChecker.java +++ b/prism/src/pta/PTAModelChecker.java @@ -213,8 +213,8 @@ public class PTAModelChecker extends PrismComponent if (exprTemp.hasBounds()) { mainLog.println("Modifying PTA to encode time bound from property..."); // Get time bound info (is always of form <=T or lb <=> >=lb+1 lb = lb + 1; } @@ -68,10 +68,10 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean throw new PrismException("Invalid lower bound in "+expr); } // Upper bound - if (expr.getUpperBound() != null) { + if (expr.getBound().getUpperBound() != null) { haveUpperBound = true; - ub = expr.getUpperBound().evaluateInt(); - if (expr.upperBoundIsStrict()) { + ub = expr.getBound().getUpperBound().evaluateInt(); + if (expr.getBound().upperBoundIsStrict()) { // Convert to non-strict bound: <=ub-1 ub = ub - 1; } diff --git a/prism/src/simulator/sampler/SamplerRewardCumulCont.java b/prism/src/simulator/sampler/SamplerRewardCumulCont.java index 4f6b4b5b..a5759f13 100644 --- a/prism/src/simulator/sampler/SamplerRewardCumulCont.java +++ b/prism/src/simulator/sampler/SamplerRewardCumulCont.java @@ -48,7 +48,7 @@ public class SamplerRewardCumulCont extends SamplerDouble if (expr.getOperator() != ExpressionTemporal.R_C) throw new PrismException("Error creating Sampler"); - timeBound = expr.getUpperBound().evaluateDouble(); + timeBound = expr.bound.getUpperBound().evaluateDouble(); this.rewardStructIndex = rewardStructIndex; // Initialise sampler info reset(); diff --git a/prism/src/simulator/sampler/SamplerRewardCumulDisc.java b/prism/src/simulator/sampler/SamplerRewardCumulDisc.java index be5b5a01..9864166e 100644 --- a/prism/src/simulator/sampler/SamplerRewardCumulDisc.java +++ b/prism/src/simulator/sampler/SamplerRewardCumulDisc.java @@ -48,7 +48,7 @@ public class SamplerRewardCumulDisc extends SamplerDouble if (expr.getOperator() != ExpressionTemporal.R_C) throw new PrismException("Error creating Sampler"); - timeBound = expr.getUpperBound().evaluateInt(); + timeBound = expr.bound.getUpperBound().evaluateInt(); this.rewardStructIndex = rewardStructIndex; // Initialise sampler info reset(); diff --git a/prism/src/simulator/sampler/SamplerRewardInstCont.java b/prism/src/simulator/sampler/SamplerRewardInstCont.java index 9c72cff5..97853907 100644 --- a/prism/src/simulator/sampler/SamplerRewardInstCont.java +++ b/prism/src/simulator/sampler/SamplerRewardInstCont.java @@ -47,7 +47,7 @@ public class SamplerRewardInstCont extends SamplerDouble // Then extract other required info if (expr.getOperator() != ExpressionTemporal.R_I) throw new PrismException("Error creating Sampler"); - time = expr.getUpperBound().evaluateDouble(); + time = expr.bound.getUpperBound().evaluateDouble(); this.rewardStructIndex = rewardStructIndex; // Initialise sampler info reset(); diff --git a/prism/src/simulator/sampler/SamplerRewardInstDisc.java b/prism/src/simulator/sampler/SamplerRewardInstDisc.java index 9fc6f9f5..ce1bba93 100644 --- a/prism/src/simulator/sampler/SamplerRewardInstDisc.java +++ b/prism/src/simulator/sampler/SamplerRewardInstDisc.java @@ -47,7 +47,7 @@ public class SamplerRewardInstDisc extends SamplerDouble // Then extract other required info if (expr.getOperator() != ExpressionTemporal.R_I) throw new PrismException("Error creating Sampler"); - time = expr.getUpperBound().evaluateInt(); + time = expr.bound.getUpperBound().evaluateInt(); this.rewardStructIndex = rewardStructIndex; // Initialise sampler info reset();