imported patch rewardcounter-reward-bound-checks.patch

prism/src/explicit/ProbModelChecker.java

@@ -683,6 +683,10 @@ public class ProbModelChecker extends NonProbModelChecker
 	 */
 	protected StateValues checkProbNext(Model model, ExpressionTemporal expr, MinMax minMax, BitSet statesOfInterest) throws PrismException
 	{
+		if (expr.getBounds().hasRewardBounds()) {
+			throw new PrismException("Reachability reward operator with reward bounds is not supported.");
+		}
+
 		// Model check the operand for all states
 		BitSet target = checkExpression(model, expr.getOperand2(), null).getBitSet();
 

prism/src/prism/NondetModelChecker.java

@@ -942,8 +942,17 @@ public class NondetModelChecker extends NonProbModelChecker
 		StateValues probs = null;
 
 		expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
+		ExpressionTemporal exprTemp = Expression.getTemporalOperatorForSimplePathFormula(expr);
+		if (exprTemp.getBounds().hasRewardBounds()) {
+			throw new PrismException("Reward bounds are currently not supported with the symbolic engine");
+		}
+
+		if (exprTemp.getBounds().countTimeBoundsDiscrete() > 1) {
+			throw new PrismException("Multiple time / step bounds are currently not supported with the symbolic engine");
+		}
 
-		// Negation
+		
+		// Negation		
 		if (expr instanceof ExpressionUnaryOp &&
 		    ((ExpressionUnaryOp)expr).getOperator() == ExpressionUnaryOp.NOT) {
 			// mark as negated, switch from min to max and vice versa
@@ -953,7 +962,7 @@ public class NondetModelChecker extends NonProbModelChecker
 		}
 
 		if (expr instanceof ExpressionTemporal) {
-			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
+			exprTemp = (ExpressionTemporal) expr;
 			// Next
 			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
 				probs = checkProbNext(exprTemp, min, statesOfInterest);
@@ -1360,6 +1369,10 @@ public class NondetModelChecker extends NonProbModelChecker
 		// currently, ignore statesOfInterest
 		JDD.Deref(statesOfInterest);
 
+		if (expr.getBounds().hasRewardBounds()) {
+			throw new PrismException("Cumulative reward operator does not support reward bounds");
+		}
+		
 		// check that there is an upper time bound
 		if (!expr.hasBounds() || !expr.getBounds().getStepBoundForDiscreteTime().hasUpperBound()) {
 			throw new PrismException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries");
@@ -1412,6 +1425,10 @@ public class NondetModelChecker extends NonProbModelChecker
 		// currently, ignore statesOfInterest
 		JDD.Deref(statesOfInterest);
 
+		if (expr.getBounds().hasRewardBounds()) {
+			throw new PrismException("Instantaneous reward operator does not support reward bounds");
+		}
+		
 		// get info from bounded until
 		time = expr.getBounds().getStepBoundForDiscreteTime().getUpperBound().evaluateInt(constantValues);
 		if (time < 0) {

prism/src/prism/ProbModelChecker.java

@@ -502,8 +502,16 @@ public class ProbModelChecker extends NonProbModelChecker
 		StateValues probs = null;
 
 		expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
-
-		// Negation
+		ExpressionTemporal exprTemp = Expression.getTemporalOperatorForSimplePathFormula(expr);
+		if (exprTemp.getBounds().hasRewardBounds()) {
+			throw new PrismException("Reward bounds are currently not supported with the symbolic engine");
+		}
+		
+		if (exprTemp.getBounds().countTimeBoundsDiscrete() > 1) {
+			throw new PrismException("Multiple time / step bounds are currently not supported with the symbolic engine");
+		}
+		
+		// Negation		
 		if (expr instanceof ExpressionUnaryOp &&
 		    ((ExpressionUnaryOp)expr).getOperator() == ExpressionUnaryOp.NOT) {
 			negated = true;
@@ -511,7 +519,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		}
 
 		if (expr instanceof ExpressionTemporal) {
-			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
+			exprTemp = (ExpressionTemporal) expr;
 			// Next
 			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
 				probs = checkProbNext(exprTemp, statesOfInterest);
@@ -828,6 +836,10 @@ public class ProbModelChecker extends NonProbModelChecker
 	{
 		int time; // time
 		StateValues rewards = null;
+		
+		if (expr.getBounds().hasRewardBounds()) {
+			throw new PrismException("Cumulative reward operator does not support reward bounds");
+		}
 
 		// currently, ignore statesOfInterest
 		JDD.Deref(statesOfInterest);
@@ -887,6 +899,10 @@ public class ProbModelChecker extends NonProbModelChecker
 		// currently, we ignore statesOfInterest
 		JDD.Deref(statesOfInterest);
 
+		if (expr.getBounds().hasRewardBounds()) {
+			throw new PrismException("Instantaneous reward operator does not support reward bounds");
+		}
+
 		// get info from inst reward
 		time = expr.getBounds().getStepBoundForDiscreteTime().getUpperBound().evaluateInt(constantValues);
 		if (time < 0) {
@@ -970,6 +986,12 @@ public class ProbModelChecker extends NonProbModelChecker
 		ProbModelChecker mcProduct;
 		long l;
 
+
+		if (Expression.containsTemporalRewardBounds(expr)) {
+			JDD.Deref(statesOfInterest);
+			throw new PrismException("Can not handle reward bounds via deterministic automata.");
+		}
+
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			if (model.getModelType().continuousTime()) {
 				JDD.Deref(statesOfInterest);

prism/src/simulator/sampler/SamplerRewardCumulDisc.java

@@ -48,6 +48,10 @@ public class SamplerRewardCumulDisc extends SamplerDouble
 		if (expr.getOperator() != ExpressionTemporal.R_C)
 			throw new PrismException("Error creating Sampler");
 		
+		if (expr.getBounds().hasRewardBounds()) {
+			throw new PrismException("Cumulative reward operator does not support reward bounds");
+		}
+		
 		timeBound = expr.getBounds().getStepBoundForDiscreteTime().getUpperBound().evaluateInt();
 		this.rewardStructIndex = rewardStructIndex;
 		// Initialise sampler info

prism/src/simulator/sampler/SamplerRewardInstDisc.java

@@ -47,6 +47,11 @@ public class SamplerRewardInstDisc extends SamplerDouble
 		// Then extract other required info
 		if (expr.getOperator() != ExpressionTemporal.R_I)
 			throw new PrismException("Error creating Sampler");
+		
+		if (expr.getBounds().hasRewardBounds()) {
+			throw new PrismException("Instantaneous reward operator does not support reward bounds");
+		}
+
 		time = expr.getBounds().getStepBoundForDiscreteTime().getUpperBound().evaluateInt();
 		this.rewardStructIndex = rewardStructIndex;
 		// Initialise sampler info