imported patch rewardcounter-TemporalOperatorBound-use.patch

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) {

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");
 		}
 

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);

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");
 		}
 

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();
 }
 {
-	( ( <LE> ( LOOKAHEAD(IdentifierExpression() <LPARENTH>) uBound = IdentifierExpression() | uBound = Expression(false, false) ) { exprTemp.setUpperBound(uBound, false); } )
-	| ( <LT> ( LOOKAHEAD(IdentifierExpression() <LPARENTH>) uBound = IdentifierExpression() | uBound = Expression(false, false) ) { exprTemp.setUpperBound(uBound, true); } )
-	| ( <GE> ( LOOKAHEAD(IdentifierExpression() <LPARENTH>) lBound = IdentifierExpression() | lBound = Expression(false, false) ) { exprTemp.setLowerBound(lBound, false); } )
-	| ( <GT> ( LOOKAHEAD(IdentifierExpression() <LPARENTH>) lBound = IdentifierExpression() | lBound = Expression(false, false) ) { exprTemp.setLowerBound(lBound, true); } )
-	| ( <LBRACKET> lBound = Expression(false, false) <COMMA> uBound = Expression(false, false) <RBRACKET> { exprTemp.setLowerBound(lBound, false); exprTemp.setUpperBound(uBound, false); } )
-	| ( <EQ> lBound = Expression(false, false) { exprTemp.setEqualBounds(lBound); } )
+	( ( <LE> ( LOOKAHEAD(IdentifierExpression() <LPARENTH>) uBound = IdentifierExpression() | uBound = Expression(false, false) ) { bound.setUpperBound(uBound, false); } )
+	| ( <LT> ( LOOKAHEAD(IdentifierExpression() <LPARENTH>) uBound = IdentifierExpression() | uBound = Expression(false, false) ) { bound.setUpperBound(uBound, true); } )
+	| ( <GE> ( LOOKAHEAD(IdentifierExpression() <LPARENTH>) lBound = IdentifierExpression() | lBound = Expression(false, false) ) { bound.setLowerBound(lBound, false); } )
+	| ( <GT> ( LOOKAHEAD(IdentifierExpression() <LPARENTH>) lBound = IdentifierExpression() | lBound = Expression(false, false) ) { bound.setLowerBound(lBound, true); } )
+	| ( <LBRACKET> lBound = Expression(false, false) <COMMA> uBound = Expression(false, false) <RBRACKET> { bound.setLowerBound(lBound, false); bound.setUpperBound(uBound, false); } )
+	| ( <EQ> 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) :
 	| <S> { ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null); }
 	
 	// Normal reward operators (excluding S; see above)
-	| LOOKAHEAD(<C> <LE>) begin = <C> <LE> expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; }
+	| LOOKAHEAD(<C> <LE>) begin = <C> <LE> expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); b.setUpperBound(expr); exprTemp.setBound(b); ret = exprTemp; }
 	| <C> { ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); }
-	| <I> <EQ> expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; }
+	| <I> <EQ> 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; }

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 &gt;= 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 &gt;= e or &gt; 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 &lt;= 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 &lt;= e or &lt; 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;
 	}
 

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;
 	}

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;
 	}

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");
 		}
 	}

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) {

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:

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()) {

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");
 		}

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");
 		}

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");
 		}

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));
 			}
 		}
 		

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 <T)
-			timeBound = exprTemp.getUpperBound().evaluateInt(constantValues);
-			timeBoundStrict = exprTemp.upperBoundIsStrict();
+			timeBound = exprTemp.bound.getUpperBound().evaluateInt(constantValues);
+			timeBoundStrict = exprTemp.bound.upperBoundIsStrict();
 			// Check for non-allowed time bounds (negative)
 			if (timeBound < (timeBoundStrict ? 1 : 0)) {
 				throw new PrismLangException("Negative bound in " + exprTemp);

prism/src/simulator/SimulatorEngine.java

@@ -1526,12 +1526,12 @@ public class SimulatorEngine extends PrismComponent
 		}
 		// Simulator cannot handle cumulative reward properties without a time bound
 		if (expr instanceof ExpressionReward) {
-			Expression exprTemp = ((ExpressionReward) expr).getExpression();
-			if (exprTemp instanceof ExpressionTemporal) {
-				if (((ExpressionTemporal) exprTemp).getOperator() == ExpressionTemporal.R_C) {
-					if (((ExpressionTemporal) exprTemp).getUpperBound() == null) {
-						return "Simulator cannot handle cumulative reward properties without time bounds";
-					}
+			Expression expr_ = ((ExpressionReward) expr).getExpression();
+			if (expr_ instanceof ExpressionTemporal) {
+				ExpressionTemporal exprTemp = (ExpressionTemporal)expr_;
+				if (exprTemp.getOperator() == ExpressionTemporal.R_C &&
+				    (exprTemp.bound==null || exprTemp.bound.getUpperBound() == null)) {
+					return "Simulator cannot handle cumulative reward properties without time bounds";
 				}
 			}
 		}

prism/src/simulator/sampler/SamplerBoundedUntilCont.java

@@ -56,17 +56,17 @@ public class SamplerBoundedUntilCont extends SamplerBoolean
 		left = expr.getOperand1();
 		right = expr.getOperand2();
 
-		lb = expr.getLowerBound() == null ? 0.0 : expr.getLowerBound().evaluateDouble();
+		lb = expr.getBound().getLowerBound() == null ? 0.0 : expr.getBound().getLowerBound().evaluateDouble();
 		if (lb < 0) {
 			throw new PrismException("Invalid lower bound " + lb + " in time-bounded until formula");
 		}
 
-		if (expr.getUpperBound() == null) {
+		if (expr.getBound().getUpperBound() == null) {
 			ub = Double.POSITIVE_INFINITY;
 		} else {
-			ub = expr.getUpperBound().evaluateDouble();
-			if (ub < 0 || (ub == 0 && expr.upperBoundIsStrict())) {
-				String bound = (expr.upperBoundIsStrict() ? "<" : "<=") + ub;
+			ub = expr.getBound().getUpperBound().evaluateDouble();
+			if (ub < 0 || (ub == 0 && expr.getBound().upperBoundIsStrict())) {
+				String bound = (expr.getBound().upperBoundIsStrict() ? "<" : "<=") + ub;
 				throw new PrismException("Invalid upper bound " + bound + " in time-bounded until formula");
 			}
 			if (ub < lb) {

prism/src/simulator/sampler/SamplerBoundedUntilDisc.java

@@ -54,9 +54,9 @@ public class SamplerBoundedUntilDisc extends SamplerBoolean
 		left = expr.getOperand1();
 		right = expr.getOperand2();
 		// Lower bound
-		if (expr.getLowerBound() != null) {
-			lb = expr.getLowerBound().evaluateInt();
-			if (expr.lowerBoundIsStrict()) {
+		if (expr.getBound().hasLowerBound()) {
+			lb = expr.getBound().getLowerBound().evaluateInt();
+			if (expr.getBound().lowerBoundIsStrict()) {
 				// Convert to non-strict bound:  >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  <=>  <=ub-1
 				ub = ub - 1;
 			}

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();

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();

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();

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();