diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index 5951e9bf..60387270 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -126,18 +126,26 @@ public class CTMCModelChecker extends ProbModelChecker protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { double lTime, uTime; // time bounds - Expression exprTmp; BitSet b1, b2, tmp; StateValues probs = null; ModelCheckerResult tmpRes = null, res = null; // get info from bounded until + if (expr.getBounds().hasStepBounds() || + expr.getBounds().hasRewardBounds()){ + throw new PrismNotSupportedException("Step or reward-bounds are not supported for CTMCs."); + } + + if (expr.getBounds().countTimeBounds() > 1) { + throw new PrismNotSupportedException("Conjunctions of time bounds are not supported for CTMCs."); + } + + TemporalOperatorBound bound = expr.getBounds().getTimeBoundForContinuousTime(); // lower bound is 0 if not specified // (i.e. if until is of form U<=t) - exprTmp = expr.bound == null ? null : expr.bound.getLowerBound(); - if (exprTmp != null) { - lTime = exprTmp.evaluateDouble(constantValues); + if (bound != null && bound.hasLowerBound()) { + lTime = bound.getLowerBound().evaluateDouble(constantValues); if (lTime < 0) { throw new PrismException("Invalid lower bound " + lTime + " in time-bounded until formula"); } @@ -146,12 +154,11 @@ public class CTMCModelChecker extends ProbModelChecker } // upper bound is -1 if not specified // (i.e. if until is of form U>=t) - exprTmp = expr.bound == null ? null : expr.bound.getUpperBound(); - if (exprTmp != null) { - uTime = exprTmp.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"); + if (bound != null && bound.hasUpperBound()) { + uTime = bound.getUpperBound().evaluateDouble(constantValues); + if (uTime < 0 || (uTime == 0 && bound.upperBoundIsStrict())) { + String s = (bound.upperBoundIsStrict() ? "<" : "<=") + uTime; + throw new PrismException("Invalid upper bound " + s + " in time-bounded until formula"); } if (uTime < lTime) { throw new PrismException("Upper bound must exceed lower bound in time-bounded until formula"); diff --git a/prism/src/explicit/CTMDPModelChecker.java b/prism/src/explicit/CTMDPModelChecker.java index ce970439..40c0965e 100644 --- a/prism/src/explicit/CTMDPModelChecker.java +++ b/prism/src/explicit/CTMDPModelChecker.java @@ -31,6 +31,7 @@ import java.util.List; import java.util.Map; import parser.ast.ExpressionTemporal; +import parser.ast.TemporalOperatorBound; import prism.PrismComponent; import prism.PrismException; import prism.PrismNotSupportedException; @@ -65,10 +66,22 @@ public class CTMDPModelChecker extends ProbModelChecker ModelCheckerResult res = null; // get info from bounded until - 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"); + // get info from bounded until + if (expr.getBounds().hasStepBounds() || + expr.getBounds().hasRewardBounds()){ + throw new PrismNotSupportedException("Step or reward-bounds are not supported for CTMDPs."); + } + + if (expr.getBounds().countTimeBounds() > 1) { + throw new PrismNotSupportedException("Conjunctions of time bounds are not supported for CTMDPs."); + } + + TemporalOperatorBound bound = expr.getBounds().getTimeBoundForContinuousTime(); + + uTime = bound == null ? null : bound.getUpperBound().evaluateDouble(constantValues); + if (uTime < 0 || (uTime == 0 && bound.upperBoundIsStrict())) { + String s = (bound.upperBoundIsStrict() ? "<" : "<=") + uTime; + throw new PrismException("Invalid upper bound " + s + " in time-bounded until formula"); } // model check operands first for all states diff --git a/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java b/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java index 9ec4b230..933c3b1a 100644 --- a/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java +++ b/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java @@ -36,6 +36,7 @@ import parser.ast.LabelList; import parser.ast.ModulesFile; import parser.ast.PropertiesFile; import parser.ast.RewardStruct; +import parser.ast.TemporalOperatorBound; import prism.PrismComponent; import prism.PrismException; import prism.PrismNotSupportedException; @@ -142,14 +143,25 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent throw new PrismNotSupportedException("Fast adaptive uniformisation window model checking currently only supports simple until operators"); } + if (exprTemp.getBounds().hasStepBounds() || + exprTemp.getBounds().hasRewardBounds()){ + throw new PrismNotSupportedException("Step or reward-bounds are not supported for CTMCs."); + } + + if (exprTemp.getBounds().countTimeBounds() > 1) { + throw new PrismNotSupportedException("Conjunctions of time bounds are not supported for CTMCs."); + } + + TemporalOperatorBound bound = exprTemp.getBounds().getTimeBoundForContinuousTime(); + double timeLower = 0.0; - if (exprTemp.bound != null && exprTemp.bound.getLowerBound() != null) { - timeLower = exprTemp.bound.getLowerBound().evaluateDouble(constantValues); + if (bound != null && bound.hasLowerBound()) { + timeLower = bound.getLowerBound().evaluateDouble(constantValues); } - if (exprTemp.bound == null || exprTemp.bound.getUpperBound() == null) { + if (bound == null || !bound.hasUpperBound()) { throw new PrismNotSupportedException("Fast adaptive uniformisation window model checking currently requires an upper time bound"); } - double timeUpper = exprTemp.bound.getUpperBound().evaluateDouble(constantValues); + double timeUpper = bound.getUpperBound().evaluateDouble(constantValues); if (!exprTemp.hasBounds()) { throw new PrismNotSupportedException("Fast adaptive uniformisation window model checking currently only supports timed properties"); @@ -237,7 +249,7 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent default: throw new PrismNotSupportedException("Currently only instantaneous or cumulative rewards are allowed."); } - double time = temporal.bound.getUpperBound().evaluateDouble(constantValues); + double time = temporal.getBounds().getTimeBoundForContinuousTime().getUpperBound().evaluateDouble(constantValues); RewardStruct rewStruct = expr.getRewardStructByIndexObject(modulesFile, constantValues); fau.setRewardStruct(rewStruct); fau.setConstantValues(constantValues); diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 90188bad..0ec0d147 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -230,9 +230,13 @@ public class LTLModelChecker extends PrismComponent DA da; long time; + if (Expression.containsTemporalRewardBounds(expr)) { + throw new PrismNotSupportedException("Can not handle reward bounds via deterministic automata."); + } + if (Expression.containsTemporalTimeBounds(expr)) { if (model.getModelType().continuousTime()) { - throw new PrismException("Automaton construction for time-bounded operators not supported for " + model.getModelType()+"."); + throw new PrismNotSupportedException("Automaton construction for time-bounded operators not supported for " + model.getModelType()+"."); } if (!expr.isSimplePathFormula()) { diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 68483d72..5d355981 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -44,6 +44,7 @@ import parser.ast.ExpressionStrategy; import parser.ast.ExpressionTemporal; import parser.ast.ExpressionUnaryOp; import parser.ast.RewardStruct; +import parser.ast.TemporalOperatorBound; import parser.type.TypeBool; import parser.type.TypeDouble; import parser.type.TypePathBool; @@ -634,6 +635,10 @@ public class ProbModelChecker extends NonProbModelChecker boolean negated = false; StateValues probs = null; + if (Expression.containsTemporalRewardBounds(expr)) { + throw new PrismNotSupportedException("Can not handle reward bounds."); + } + expr = Expression.convertSimplePathFormulaToCanonicalForm(expr); // Negation @@ -1001,21 +1006,25 @@ public class ProbModelChecker extends NonProbModelChecker */ protected StateValues checkRewardInstantaneous(Model model, Rewards modelRewards, ExpressionTemporal expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { + if (expr.getBounds().hasRewardBounds()) { + throw new PrismNotSupportedException("Instantaneous reward operator with reward bounds is not supported."); + } + // Compute/return the rewards ModelCheckerResult res = null; switch (model.getModelType()) { case DTMC: { - int k = expr.bound.getUpperBound().evaluateInt(constantValues); + int k = expr.getBounds().getStandardBound(model.getModelType()).getUpperBound().evaluateInt(constantValues); res = ((DTMCModelChecker) this).computeInstantaneousRewards((DTMC) model, (MCRewards) modelRewards, k, statesOfInterest); break; } case CTMC: { - double t = expr.bound.getUpperBound().evaluateDouble(constantValues); + double t = expr.getBounds().getStandardBound(model.getModelType()).getUpperBound().evaluateDouble(constantValues); res = ((CTMCModelChecker) this).computeInstantaneousRewards((CTMC) model, (MCRewards) modelRewards, t); break; } case MDP: { - int k = expr.bound.getUpperBound().evaluateInt(constantValues); + int k = expr.getBounds().getStandardBound(model.getModelType()).getUpperBound().evaluateInt(constantValues); res = ((MDPModelChecker) this).computeInstantaneousRewards((MDP) model, (MDPRewards) modelRewards, k, minMax.isMin()); break; } @@ -1035,19 +1044,23 @@ public class ProbModelChecker extends NonProbModelChecker int timeInt = -1; double timeDouble = -1; - // Check that there is an upper time bound - if (expr.bound == null || expr.bound.getUpperBound() == null) { - throw new PrismNotSupportedException("This is not a cumulative reward operator"); + if (expr.getBounds().hasRewardBounds()) { + throw new PrismNotSupportedException("Cumulative reward operator with reward bounds is not supported."); + } + + TemporalOperatorBound bound = expr.getBounds().getStandardBound(model.getModelType()); + if (bound == null || bound.getUpperBound() == null) { + throw new PrismException("This is not a cumulative reward operator"); } // Get time bound if (model.getModelType().continuousTime()) { - timeDouble = expr.bound.getUpperBound().evaluateDouble(constantValues); + timeDouble = bound.getUpperBound().evaluateDouble(constantValues); if (timeDouble < 0) { throw new PrismException("Invalid time bound " + timeDouble + " in cumulative reward formula"); } } else { - timeInt = expr.bound.getUpperBound().evaluateInt(constantValues); + timeInt = bound.getUpperBound().evaluateInt(constantValues); if (timeInt < 0) { throw new PrismException("Invalid time bound " + timeInt + " in cumulative reward formula"); } @@ -1083,8 +1096,11 @@ 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.getBound().getUpperBound() != null) { + if (expr.getBounds().hasRewardBounds()) { + throw new PrismNotSupportedException("Cumulative reward operator with reward bounds is not supported."); + } + + if (expr.hasBounds()) { 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 03a7102a..b625fcaf 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -511,6 +511,7 @@ TOKEN : | < PRIME: "'" > | < RENAME: "<-" > | < QMARK: "?" > +| < CARET: "^" > // Regular expressions | < REG_INT: (["1"-"9"](["0"-"9"])*)|("0") > | < REG_DOUBLE: (["0"-"9"])*(".")?(["0"-"9"])+(["e","E"](["-","+"])?(["0"-"9"])+)? > @@ -1124,7 +1125,7 @@ Expression Expression(boolean prop, boolean pathprop) : // that does not really help since this is done post-parsing. // To prevent (very common) cases such as "F<=t (b)", "F<=t (b)&(c)", etc. // being mis-parsed ("t(b)" would always be taken over "t"), we catch this case -// separately (see TimeBound() production below for details). +// separately (see BoundExpression() production below for details). // This means that more complex time-bounds, especially those that // start/end with an identifier should be parenthesised, e.g. "F<=(t1+t2)". @@ -1136,6 +1137,8 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) : { Expression ret, expr; ExpressionTemporal exprTemp; + TemporalOperatorBound defaultBound = null; + TemporalOperatorBounds bounds = null; Token begin = null; } { @@ -1147,7 +1150,9 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) : ( { exprTemp.setOperator(ExpressionTemporal.P_U); } | { exprTemp.setOperator(ExpressionTemporal.P_W); } | { exprTemp.setOperator(ExpressionTemporal.P_R); } ) - ( TimeBound(exprTemp) )? + ( (defaultBound = BoundExpression() { exprTemp.getBounds().setDefaultBound(defaultBound); }) + | (bounds = TemporalOpBounds() { exprTemp.setBounds(bounds); }) + )? expr = ExpressionTemporalUnary(prop, pathprop) { exprTemp.setOperand2(expr); exprTemp.setPosition(begin, getToken(0)); ret = exprTemp; } ] @@ -1158,6 +1163,8 @@ Expression ExpressionTemporalUnary(boolean prop, boolean pathprop) : { Expression ret, expr; ExpressionTemporal exprTemp; + TemporalOperatorBound defaultBound = null; + TemporalOperatorBounds bounds = null; Token begin = null; } { @@ -1168,7 +1175,9 @@ Expression ExpressionTemporalUnary(boolean prop, boolean pathprop) : ( { exprTemp.setOperator(ExpressionTemporal.P_X); } | { exprTemp.setOperator(ExpressionTemporal.P_F); } | { exprTemp.setOperator(ExpressionTemporal.P_G); } ) - ( TimeBound(exprTemp) )? + ( (defaultBound = BoundExpression() { exprTemp.getBounds().setDefaultBound(defaultBound); }) + | (bounds = TemporalOpBounds() { exprTemp.setBounds(bounds); }) + )? expr = ExpressionTemporalUnary(prop, pathprop) { exprTemp.setOperand2(expr); exprTemp.setPosition(begin, getToken(0)); ret = exprTemp; } | @@ -1177,10 +1186,10 @@ Expression ExpressionTemporalUnary(boolean prop, boolean pathprop) : { return ret; } } -// Time bound for temporal operators +// Bound expression for temporal operators // (see ExpressionTemporal production for lookahead explanation) -void TimeBound(ExpressionTemporal exprTemp) : +TemporalOperatorBound BoundExpression() : { Expression lBound, uBound; TemporalOperatorBound bound = new TemporalOperatorBound(); @@ -1194,10 +1203,43 @@ void TimeBound(ExpressionTemporal exprTemp) : | ( lBound = Expression(false, false) { bound.setEqualBounds(lBound); } ) ) { - exprTemp.setBound(bound); + return bound; } } +TemporalOperatorBounds TemporalOpBounds() : +{ + TemporalOperatorBounds bounds = new TemporalOperatorBounds(); + TemporalOperatorBound bound; +} +{ + ()? + + bound = TemporalOpBound() {bounds.addBound(bound);} + ( bound = TemporalOpBound() {bounds.addBound(bound);})* + + {return bounds;} +} + +TemporalOperatorBound TemporalOpBound() : +{ + TemporalOperatorBound bound = null; + Object rewardIndex = null; +} +{ + ( (LOOKAHEAD({ getToken(1).kind==REG_IDENT && getToken(1).image.equals("time") }) Identifier() bound = BoundExpression() {bound.setBoundType(TemporalOperatorBound.BoundType.TIME_BOUND);}) + | (LOOKAHEAD({ getToken(1).kind==REG_IDENT && getToken(1).image.equals("steps") }) Identifier() bound = BoundExpression() {bound.setBoundType(TemporalOperatorBound.BoundType.STEP_BOUND);}) + | (LOOKAHEAD({ getToken(1).kind==REG_IDENT && getToken(1).image.equals("reward") }) Identifier() + (rewardIndex = RewardIndex())? + bound = BoundExpression() + { + bound.setBoundType(TemporalOperatorBound.BoundType.REWARD_BOUND); + bound.setRewardStructureIndex(rewardIndex); + }) + ) + {return bound;} +} + // Expression: if-then-else, i.e. "cond ? then : else" Expression ExpressionITE(boolean prop, boolean pathprop) : @@ -1711,7 +1753,7 @@ Expression ExpressionReward(boolean prop, boolean pathprop) : // Various options for "R" keyword and attached symbols (( begin = ( modifier = IdentifierExpression() )? - (RewardIndex(ret))? + (RewardSpecification(ret))? (( r = LtGt() rew = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; } ) |( { relOp = "="; isBool = false; } ) |( { relOp = "min="; isBool = false; } ) @@ -1740,18 +1782,17 @@ Expression ExpressionReward(boolean prop, boolean pathprop) : } } -// Reward struct index for R operator +// Reward specification for R operator -void RewardIndex(ExpressionReward exprRew) : +void RewardSpecification(ExpressionReward exprRew) : { Object index = null; Object indexDiv = null; } { - // Lookahead here is to ensure that "id" is not misdetected as an ExpressionLabel - ( ( LOOKAHEAD(QuotedIdentifier()) ( index = QuotedIdentifier()) | index = Expression(false, false) ) ) + index = RewardIndex() // Optional second reward structure index (for ratio objectives) - ( ( ( LOOKAHEAD(QuotedIdentifier()) ( indexDiv = QuotedIdentifier() ) | indexDiv = Expression(false, false) ) ))? + ( indexDiv = RewardIndex() )? { exprRew.setRewardStructIndex(index); if (indexDiv != null) { @@ -1760,6 +1801,19 @@ void RewardIndex(ExpressionReward exprRew) : } } +Object RewardIndex() : +{ + Object index = null; +} +{ + // Lookahead here is to ensure that "id" is not misdetected as an ExpressionLabel + ( ( LOOKAHEAD(QuotedIdentifier()) ( index = QuotedIdentifier()) | index = Expression(false, false) ) ) + { + return index; + } +} + + // Contents of an R operator // JavaCC warns about lookahead for this function. This is because there is a possible conflict between @@ -1782,9 +1836,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); b.setUpperBound(expr); exprTemp.setBound(b); ret = exprTemp; } + | LOOKAHEAD( ) begin = expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); b.setUpperBound(expr); exprTemp.getBounds().setDefaultBound(b); ret = exprTemp; } | { ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); } - | expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); b.setUpperBound(expr); exprTemp.setBound(b); ret = exprTemp; } + | expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); b.setUpperBound(expr); exprTemp.getBounds().setDefaultBound(b); ret = exprTemp; } // Path formula (including F "target") | expr = Expression(prop, true) { ret = expr; } diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index c8992166..c2fafa2f 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -846,7 +846,7 @@ public abstract class Expression extends ASTElement } /** - * Test if an expression contains time bounds on temporal operators + * Test if an expression contains time/step bounds on temporal operators */ public static boolean containsTemporalTimeBounds(Expression expr) { @@ -856,8 +856,35 @@ public abstract class Expression extends ASTElement { public void visitPre(ExpressionTemporal e) throws PrismLangException { - if (e.hasBounds()) + if (e.hasBounds()) { + TemporalOperatorBounds bounds = e.getBounds(); + if (bounds.hasTimeBounds() || + bounds.hasStepBounds() || + bounds.hasDefaultBound()) { + throw new PrismLangException(""); + } + } + } + }); + } catch (PrismLangException e) { + return true; + } + return false; + } + + /** + * Test if an expression contains reward bounds on temporal operators + */ + public static boolean containsTemporalRewardBounds(Expression expr) { + try { + // check for reward bounds, don't recurse in P/R subformulas + expr.accept(new ExpressionTraverseNonNested() + { + public void visitPre(ExpressionTemporal e) throws PrismLangException + { + if (e.getBounds().hasRewardBounds()) { throw new PrismLangException(""); + } } }); } catch (PrismLangException e) { diff --git a/prism/src/parser/ast/ExpressionTemporal.java b/prism/src/parser/ast/ExpressionTemporal.java index b96ca510..28a8ea89 100644 --- a/prism/src/parser/ast/ExpressionTemporal.java +++ b/prism/src/parser/ast/ExpressionTemporal.java @@ -57,8 +57,8 @@ public class ExpressionTemporal extends Expression protected Expression operand2 = null; - // optional bound - public TemporalOperatorBound bound; + // the bounds + protected TemporalOperatorBounds bounds = new TemporalOperatorBounds(); // Constructors @@ -106,7 +106,7 @@ public class ExpressionTemporal extends Expression */ public void setBoundsFrom(ExpressionTemporal exprTemp) { - bound = exprTemp.getBound(); + bounds = exprTemp.getBounds(); } // Get methods @@ -143,14 +143,9 @@ public class ExpressionTemporal extends Expression return (operand1 == null) ? 1 : 2; } - public TemporalOperatorBound getBound() - { - return bound; - } - public boolean hasBounds() { - return bound != null; + return bounds.hasBounds(); } @@ -203,16 +198,19 @@ public class ExpressionTemporal extends Expression expr.setOperand1(operand1.deepCopy()); if (operand2 != null) expr.setOperand2(operand2.deepCopy()); - if (bound != null) { - expr.setBound((TemporalOperatorBound) bound.deepCopy()); - } + expr.setBounds(bounds.deepCopy()); + expr.setType(type); expr.setPosition(this); return expr; } - public void setBound(TemporalOperatorBound bound) { - this.bound = bound; + public void setBounds(TemporalOperatorBounds bounds) { + this.bounds = bounds; + } + + public TemporalOperatorBounds getBounds() { + return bounds; } // Standard methods @@ -224,24 +222,16 @@ public class ExpressionTemporal extends Expression if (operand1 != null) s += operand1 + " "; s += opSymbols[op]; - if (bound != null) { - if (bound.getLowerBound() == null) { - if (bound.getUpperBound() != null) { - if (op != R_I) - s += "<" + (bound.upperBoundIsStrict() ? "" : "=") + bound.getUpperBound(); - else - s += "=" + bound.getUpperBound(); - } + + if (op == R_I && bounds.hasDefaultBound()) { + TemporalOperatorBound bound = bounds.getDefaultBound(); + if (!bound.hasLowerBound() && bound.hasUpperBound()) { + s += "<" + (bound.upperBoundIsStrict() ? "" : "=") + bound.getUpperBound(); } else { - if (bound.getUpperBound() == null) { - s += ">" + (bound.lowerBoundIsStrict() ? "" : "=") + bound.getLowerBound(); - } else { - if (bound.getEquals()) - s += "=" + bound.getLowerBound(); - else - s += "[" + bound.getLowerBound() + "," + bound.getUpperBound() + "]"; - } + s+=bound.toString(); } + } else if (bounds.hasBounds()) { + s+=bounds.toString(); } if (operand2 != null) s += " " + operand2; @@ -253,7 +243,7 @@ public class ExpressionTemporal extends Expression { final int prime = 31; int result = 1; - result = prime * result + ((bound == null) ? 0 : bound.hashCode()); + result = prime * result + ((bounds == null) ? 0 : bounds.hashCode()); result = prime * result + op; result = prime * result + ((operand1 == null) ? 0 : operand1.hashCode()); result = prime * result + ((operand2 == null) ? 0 : operand2.hashCode()); @@ -270,10 +260,10 @@ public class ExpressionTemporal extends Expression if (!(obj instanceof ExpressionTemporal)) return false; ExpressionTemporal other = (ExpressionTemporal) obj; - if (bound == null) { - if (other.bound != null) + if (bounds == null) { + if (other.bounds != null) return false; - } else if (!bound.equals(other.bound)) + } else if (!bounds.equals(other.bounds)) return false; if (op != other.op) return false; diff --git a/prism/src/parser/visitor/ASTTraverse.java b/prism/src/parser/visitor/ASTTraverse.java index 16ab7e1c..1bcda819 100644 --- a/prism/src/parser/visitor/ASTTraverse.java +++ b/prism/src/parser/visitor/ASTTraverse.java @@ -386,7 +386,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.bound != null) e.bound.accept(this); + e.getBounds().accept(this); visitPost(e); return null; } diff --git a/prism/src/parser/visitor/ASTTraverseModify.java b/prism/src/parser/visitor/ASTTraverseModify.java index 4d76f815..a4a4197f 100644 --- a/prism/src/parser/visitor/ASTTraverseModify.java +++ b/prism/src/parser/visitor/ASTTraverseModify.java @@ -397,7 +397,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.getBound() != null) e.setBound((TemporalOperatorBound) e.bound.accept(this)); + e.setBounds((TemporalOperatorBounds) e.getBounds().accept(this)); visitPost(e); return e; } diff --git a/prism/src/parser/visitor/ASTVisitor.java b/prism/src/parser/visitor/ASTVisitor.java index 6f959105..d3a276b1 100644 --- a/prism/src/parser/visitor/ASTVisitor.java +++ b/prism/src/parser/visitor/ASTVisitor.java @@ -86,5 +86,6 @@ public interface ASTVisitor public Object visit(Filter e) throws PrismLangException; public Object visit(ForLoop e) throws PrismLangException; public Object visit(TemporalOperatorBound e) throws PrismLangException; + public Object visit(TemporalOperatorBounds temporalOperatorBounds) throws PrismLangException; } diff --git a/prism/src/parser/visitor/CheckValid.java b/prism/src/parser/visitor/CheckValid.java index 182cdb64..4fb7f20d 100644 --- a/prism/src/parser/visitor/CheckValid.java +++ b/prism/src/parser/visitor/CheckValid.java @@ -59,32 +59,42 @@ public class CheckValid extends ASTTraverse } } // PTA only support upper time bounds - if (e.bound != null && e.bound.getLowerBound() != null) { - if (modelType == ModelType.PTA) { - throw new PrismLangException("Only upper time bounds are allowed on the " + e.getOperatorSymbol() - + " operator for PTAs"); + if (modelType == ModelType.PTA) { + if (e.hasBounds()) { + if (e.getBounds().countBounds() > 1 || !e.getBounds().hasDefaultBound() || + e.getBounds().getDefaultBound().hasLowerBound()) { + throw new PrismLangException("Only upper time bounds are allowed on the " + e.getOperatorSymbol() + + " operator for PTAs"); + } + } + } + + // Don't allow lower bounds on weak until - does not have intuitive semantics + if (e.getOperator() == ExpressionTemporal.P_W) { + for (TemporalOperatorBound bound : e.getBounds().getBounds()) { + if (bound.hasLowerBound()) { + throw new PrismLangException("The weak until operator (W) with lower bounds is not yet supported"); + } } } + } + + public void visitPost(TemporalOperatorBound e) throws PrismLangException { // Apart from CTMCs, we only support integer time bounds - 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 (!e.isIntegerValued() && !e.isRewardBound()) { if (modelType == ModelType.DTMC) { - throw new PrismLangException("Time bounds on the " + e.getOperatorSymbol() - + " operator must be integers for DTMCs"); + throw new PrismLangException("Time bounds " + e + + " must be integers for DTMCs"); } if (modelType == ModelType.MDP) { - throw new PrismLangException("Time bounds on the " + e.getOperatorSymbol() - + " operator must be integers for MDPs"); + throw new PrismLangException("Time bounds " + e + + " must be integers for MDPs"); } if (modelType == ModelType.PTA) { - throw new PrismLangException("Time bounds on the " + e.getOperatorSymbol() - + " operator must be integers for PTAs"); + throw new PrismLangException("Time bounds " + e + + " must be integers for PTAs"); } } - // Don't allow lower bounds on weak until - does not have intuitive semantics - if (e.getOperator() == ExpressionTemporal.P_W && e.getBound().hasLowerBound()) { - throw new PrismLangException("The weak until operator (W) with lower bounds is not yet supported"); - } } public void visitPost(ExpressionProb e) throws PrismLangException diff --git a/prism/src/parser/visitor/PropertiesSemanticCheck.java b/prism/src/parser/visitor/PropertiesSemanticCheck.java index 8d8debb1..3fdb0e06 100644 --- a/prism/src/parser/visitor/PropertiesSemanticCheck.java +++ b/prism/src/parser/visitor/PropertiesSemanticCheck.java @@ -117,26 +117,38 @@ public class PropertiesSemanticCheck extends SemanticCheck int op = e.getOperator(); Expression operand1 = e.getOperand1(); Expression operand2 = e.getOperand2(); - 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); - } - if (uBound != null && !uBound.isConstant()) { - throw new PrismLangException("Upper bound in " + e.getOperatorSymbol() + " operator is not constant", uBound); - } + boolean hasBounds = e.getBounds().countBounds() > 0; + // Other checks (which parser should never allow to occur anyway) - if (op == ExpressionTemporal.P_X && (operand1 != null || operand2 == null || lBound != null || uBound != null)) { + if (op == ExpressionTemporal.P_X && (operand1 != null || operand2 == null || hasBounds)) { throw new PrismLangException("Cannot attach bounds to " + e.getOperatorSymbol() + " operator", e); } - if (op == ExpressionTemporal.R_C && (operand1 != null || operand2 != null || lBound != null)) { - // NB: upper bound is optional (e.g. multi-objective allows R...[C] operator) - throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e); - } - if (op == ExpressionTemporal.R_I && (operand1 != null || operand2 != null || lBound != null || uBound == null)) { - throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e); + if (op == ExpressionTemporal.R_C) { + boolean malformed = false; + if (operand1 != null || operand2 != null) { malformed = true;} + if (e.hasBounds()) { + if (e.getBounds().countBounds() > 1 || !e.getBounds().hasDefaultBound()) { malformed = true; } + else if (e.getBounds().getDefaultBound().hasLowerBound()) { + // NB: upper bound is optional (e.g. multi-objective allows R...[C] operator) + malformed = true; + } + } + if (malformed) + throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e); + } + if (op == ExpressionTemporal.R_I) { + boolean malformed = false; + if (operand1 != null || operand2 != null) {malformed = true;} + if (e.hasBounds()) { + if (e.getBounds().countBounds() > 1 || !e.getBounds().hasDefaultBound()) { malformed = true; } + else if (e.getBounds().getDefaultBound().hasLowerBound() || !e.getBounds().getDefaultBound().hasUpperBound()) { + malformed = true; + } + } + if (malformed) + throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e); } - if (op == ExpressionTemporal.R_S && (operand1 != null || operand2 != null || lBound != null || uBound != null)) { + if (op == ExpressionTemporal.R_S && (operand1 != null || operand2 != null || hasBounds)) { throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e); } } diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index 787360ad..3efdbaed 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/prism/src/parser/visitor/TypeCheck.java @@ -168,12 +168,6 @@ public class TypeCheck extends ASTTraverse public void visitPost(ExpressionTemporal e) throws PrismLangException { Type type; - 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.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: case ExpressionTemporal.P_U: @@ -682,4 +676,13 @@ public class TypeCheck extends ASTTraverse break; } } + + public void visitPost(TemporalOperatorBound e) throws PrismLangException { + if (e.hasLowerBound() && !TypeDouble.getInstance().canAssign(e.getLowerBound().getType())) { + throw new PrismLangException("Type error: Lower bound in " + e + " must be an int or double", e.getLowerBound()); + } + if (e.hasUpperBound() && !TypeDouble.getInstance().canAssign(e.getUpperBound().getType())) { + throw new PrismLangException("Type error: Upper bound in " + e + " operator must be an int or double", e.getUpperBound()); + } + } } diff --git a/prism/src/prism/IntegerBound.java b/prism/src/prism/IntegerBound.java index 48ae6b39..29b76f34 100644 --- a/prism/src/prism/IntegerBound.java +++ b/prism/src/prism/IntegerBound.java @@ -94,7 +94,7 @@ public class IntegerBound */ public static IntegerBound fromExpressionTemporal(ExpressionTemporal expression, Values constantValues, boolean check) throws PrismException { - TemporalOperatorBound eBound = expression.bound; + TemporalOperatorBound eBound = expression.getBounds().getStepBoundForDiscreteTime(); IntegerBound bounds; if (eBound == null) { bounds = new IntegerBound(null, false, null, false); diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index f8fdebcc..67294570 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -316,6 +316,10 @@ public class LTLModelChecker extends PrismComponent */ public DA constructDAForLTLFormula(StateModelChecker mc, Model model, Expression expr, Vector labelDDs, AcceptanceType... allowedAcceptance) throws PrismException { + if (Expression.containsTemporalRewardBounds(expr)) { + throw new PrismNotSupportedException("Can not handle reward bounds via deterministic automata."); + } + if (Expression.containsTemporalTimeBounds(expr)) { if (model.getModelType().continuousTime()) { throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+"."); diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 58cce2fe..806a1410 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -56,6 +56,7 @@ import parser.ast.ExpressionTemporal; import parser.ast.ExpressionUnaryOp; import parser.ast.PropertiesFile; import parser.ast.RelOp; +import parser.ast.TemporalOperatorBound; import parser.type.TypeBool; import parser.type.TypeDouble; import parser.type.TypePathBool; @@ -776,22 +777,31 @@ public class NondetModelChecker extends NonProbModelChecker // Check that the temporal/reward operator is supported, and store step bounds if present int stepBound = 0; + if (exprProb != null) { // F<=k is allowed Expression expr = exprProb.getExpression(); if (expr.isSimplePathFormula() && Expression.isReach(expr)) { ExpressionTemporal exprTemp = ((ExpressionTemporal) expr); - if (exprTemp.bound != null && exprTemp.bound.getLowerBound() != null) { - throw new PrismException("Lower time bounds are not supported in multi-objective queries"); + if (exprTemp.getBounds().hasRewardBounds()) { + throw new PrismNotSupportedException("Reward bounds are not supported in multi-objective queries"); + } + // Get single bound, throws exception if there are multiple + TemporalOperatorBound bound = exprTemp.getBounds().getStepBoundForDiscreteTime(); + if (bound != null && bound.getLowerBound() != null) { + throw new PrismNotSupportedException("Lower time bounds are not supported in multi-objective queries"); } - if (exprTemp.bound != null && exprTemp.bound.getUpperBound() != null) { - stepBound = exprTemp.bound.getUpperBound().evaluateInt(constantValues); + if (bound != null) { + stepBound = bound.getUpperBound().evaluateInt(constantValues); } else { stepBound = -1; } } else { + if (Expression.containsTemporalRewardBounds(expr)) { + throw new PrismNotSupportedException("Reward bounds in multi-objective queries are not supported"); + } if (Expression.containsTemporalTimeBounds(expr)) { - throw new PrismException("Time bounds in multi-objective queries can only be on F or C operators"); + throw new PrismNotSupportedException("Time bounds in multi-objective queries can only be on F or C operators"); } else { stepBound = -1; } @@ -804,9 +814,16 @@ public class NondetModelChecker extends NonProbModelChecker throw new PrismException("Only the C and C>=k reward operators are currently supported for multi-objective properties (not " + exprTemp.getOperatorSymbol() + ")"); } + if (exprTemp.getBounds().hasRewardBounds()) { + throw new PrismNotSupportedException("Reward bounds are not supported in multi-objective queries"); + } // R [ C<=k ] - if (exprTemp.bound != null && exprTemp.bound.getUpperBound() != null) { - stepBound = exprTemp.bound.getUpperBound().evaluateInt(constantValues); + TemporalOperatorBound bound = exprTemp.getBounds().getStepBoundForDiscreteTime(); + if (bound != null && bound.getLowerBound() != null) { + throw new PrismNotSupportedException("Reward operator C with lower bound is not supported for multi-objective properties"); + } + if (bound != null && bound.getUpperBound() != null) { + stepBound = bound.getUpperBound().evaluateInt(constantValues); } // R [ C ] else { @@ -1344,12 +1361,12 @@ public class NondetModelChecker extends NonProbModelChecker JDD.Deref(statesOfInterest); // check that there is an upper time bound - if (expr.bound == null || expr.bound.getUpperBound() == null) { + if (!expr.hasBounds() || !expr.getBounds().getStepBoundForDiscreteTime().hasUpperBound()) { throw new PrismException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries"); } // get info from inst reward - time = expr.bound.getUpperBound().evaluateInt(constantValues); + time = expr.getBounds().getStepBoundForDiscreteTime().getUpperBound().evaluateInt(constantValues); if (time < 0) { throw new PrismException("Invalid time bound " + time + " in cumulative reward formula"); } @@ -1396,7 +1413,7 @@ public class NondetModelChecker extends NonProbModelChecker JDD.Deref(statesOfInterest); // get info from bounded until - time = expr.bound.getUpperBound().evaluateInt(constantValues); + time = expr.getBounds().getStepBoundForDiscreteTime().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 2b88c958..dfd4b07c 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.bound == null || expr.bound.getUpperBound() == null) { + if (!expr.hasBounds() || !expr.getBounds().getStepBoundForDiscreteTime().hasUpperBound()) { throw new PrismException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries"); } // get info from inst reward - time = expr.bound.getUpperBound().evaluateInt(constantValues); + time = expr.getBounds().getStepBoundForDiscreteTime().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.bound.getUpperBound().evaluateInt(constantValues); + time = expr.getBounds().getStepBoundForDiscreteTime().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 4ad35fd2..aa1ebd2a 100644 --- a/prism/src/prism/StochModelChecker.java +++ b/prism/src/prism/StochModelChecker.java @@ -82,19 +82,27 @@ public class StochModelChecker extends ProbModelChecker protected StateValues checkProbBoundedUntil(ExpressionTemporal expr, JDDNode statesOfInterest) throws PrismException { double lTime, uTime; // time bounds - Expression exprTmp; JDDNode b1, b2, tmp; StateValues tmpProbs = null, probs = null; JDD.Deref(statesOfInterest); // get info from bounded until + if (expr.getBounds().hasStepBounds() || + expr.getBounds().hasRewardBounds()){ + throw new PrismNotSupportedException("Step or reward-bounds are not supported for CTMCs."); + } + + if (expr.getBounds().countTimeBounds() > 1) { + throw new PrismNotSupportedException("Conjunctions of time bounds are not supported for CTMCs."); + } + + TemporalOperatorBound bound = expr.getBounds().getTimeBoundForContinuousTime(); // lower bound is 0 if not specified // (i.e. if until is of form U<=t) - exprTmp = expr.bound == null ? null : expr.bound.getLowerBound(); - if (exprTmp != null) { - lTime = exprTmp.evaluateDouble(constantValues); + if (bound != null && bound.hasLowerBound()) { + lTime = bound.getLowerBound().evaluateDouble(constantValues); if (lTime < 0) { throw new PrismException("Invalid lower bound " + lTime + " in time-bounded until formula"); } @@ -103,12 +111,11 @@ public class StochModelChecker extends ProbModelChecker } // upper bound is -1 if not specified // (i.e. if until is of form U>=t) - exprTmp = expr.bound == null ? null : expr.bound.getUpperBound(); - if (exprTmp != null) { - uTime = exprTmp.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"); + if (bound != null && bound.hasUpperBound()) { + uTime = bound.getUpperBound().evaluateDouble(constantValues); + if (uTime < 0 || (uTime == 0 && bound.upperBoundIsStrict())) { + String s = (bound.upperBoundIsStrict() ? "<" : "<=") + uTime; + throw new PrismException("Invalid upper bound " + s + " in time-bounded until formula"); } if (uTime < lTime) { throw new PrismException("Upper bound must exceed lower bound in time-bounded until formula"); @@ -240,7 +247,7 @@ public class StochModelChecker extends ProbModelChecker JDD.Deref(statesOfInterest); // get info from inst reward - time = expr.bound.getUpperBound().evaluateDouble(constantValues); + time = expr.getBounds().getTimeBoundForContinuousTime().getUpperBound().evaluateDouble(constantValues); if (time < 0) { throw new PrismException("Invalid time bound " + time + " in cumulative reward formula"); } @@ -274,7 +281,7 @@ public class StochModelChecker extends ProbModelChecker JDD.Deref(statesOfInterest); // get info from inst reward - time = expr.bound.getUpperBound().evaluateDouble(constantValues); + time = expr.getBounds().getTimeBoundForContinuousTime().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 e7566b65..d3b13551 100644 --- a/prism/src/pta/DigitalClocks.java +++ b/prism/src/pta/DigitalClocks.java @@ -340,7 +340,7 @@ public class DigitalClocks { public void visitPost(ExpressionTemporal e) throws PrismLangException { - if (e.bound != null) + if (e.hasBounds()) throw new PrismLangException("The digital clocks method does not yet support bounded properties"); } }); diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java index 997c587a..9e31d670 100644 --- a/prism/src/pta/PTAModelChecker.java +++ b/prism/src/pta/PTAModelChecker.java @@ -213,8 +213,9 @@ 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 +71,10 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean throw new PrismException("Invalid lower bound in "+expr); } // Upper bound - if (expr.getBound().getUpperBound() != null) { + if (bound != null && bound.getUpperBound() != null) { haveUpperBound = true; - ub = expr.getBound().getUpperBound().evaluateInt(); - if (expr.getBound().upperBoundIsStrict()) { + ub = bound.getUpperBound().evaluateInt(); + if (bound.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 6f08e8a8..c84d7a9b 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.bound.getUpperBound().evaluateDouble(); + timeBound = expr.getBounds().getTimeBoundForContinuousTime().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 d3cfc47f..c3f4af8c 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.bound.getUpperBound().evaluateInt(); + timeBound = expr.getBounds().getStepBoundForDiscreteTime().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 fcaeeb62..984dfc9f 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.bound.getUpperBound().evaluateDouble(); + time = expr.getBounds().getTimeBoundForContinuousTime().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 630c4546..820a2d94 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.bound.getUpperBound().evaluateInt(); + time = expr.getBounds().getStepBoundForDiscreteTime().getUpperBound().evaluateInt(); this.rewardStructIndex = rewardStructIndex; // Initialise sampler info reset();