Tweak/move error messages for non-supported R[C] operator.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6222 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/prism/ProbModelChecker.java

@@ -788,9 +788,9 @@ public class ProbModelChecker extends NonProbModelChecker
 		int time; // time
 		StateValues rewards = null;
 
-		//check that there is an upper time bound
+		// check that there is an upper time bound
 		if (expr.getUpperBound() == null) {
-			throw new PrismException("Cumulative reward without any time bound is only allowed for multi-objective queries.");
+			throw new PrismException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries");
 		}
 
 		// get info from inst reward

prism/src/simulator/SimulatorEngine.java

@@ -1306,6 +1306,17 @@ public class SimulatorEngine
 		} catch (PrismException e) {
 			return "Simulator cannot handle this property: " + e.getMessage();
 		}
+		// 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";
+					}
+				}
+			}
+		}
 		// No errors
 		return null;
 	}

prism/src/simulator/sampler/Sampler.java

@@ -238,11 +238,6 @@ public abstract class Sampler
 		ExpressionTemporal exprTemp = (ExpressionTemporal) expr.getExpression();
 		switch (exprTemp.getOperator()) {
 		case ExpressionTemporal.R_C:
-			//first check that there is an upper time bound
-			if (exprTemp.getUpperBound() == null) {
-				throw new PrismException("Cumulative reward without any time bound is only allowed for multi-objective queries.");
-			}
-			
 			if (mf.getModelType().continuousTime()) {
 				// Continuous-time cumulative reward
 				return new SamplerRewardCumulCont(exprTemp, rsi);

prism/src/simulator/sampler/SamplerRewardCumulCont.java

@@ -48,11 +48,6 @@ public class SamplerRewardCumulCont extends SamplerDouble
 		if (expr.getOperator() != ExpressionTemporal.R_C)
 			throw new PrismException("Error creating Sampler");
 		
-		//check that there is an upper time bound
-		if (expr.getUpperBound() == null) {
-			throw new PrismException("Cumulative reward without any time bound is only allowed for multi-objective queries.");
-		}
-		
 		timeBound = expr.getUpperBound().evaluateDouble();
 		this.rewardStructIndex = rewardStructIndex;
 		// Initialise sampler info

prism/src/simulator/sampler/SamplerRewardCumulDisc.java

@@ -48,11 +48,6 @@ public class SamplerRewardCumulDisc extends SamplerDouble
 		if (expr.getOperator() != ExpressionTemporal.R_C)
 			throw new PrismException("Error creating Sampler");
 		
-		//Check that there is an upper time bound
-		if (expr.getUpperBound() == null) {
-			throw new PrismException("Cumulative reward without any time bound is only allowed for multi-objective queries.");
-		}
-		
 		timeBound = expr.getUpperBound().evaluateInt();
 		this.rewardStructIndex = rewardStructIndex;
 		// Initialise sampler info