imported patch rewardcounter-CTMC-extra-check-TODO.patch

prism/src/explicit/CTMCModelChecker.java

@@ -55,6 +55,9 @@ public class CTMCModelChecker extends ProbModelChecker
 	@Override
 	protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax, BitSet statesOfInterest) throws PrismException
 	{
+		if (Expression.containsTemporalRewardBounds(expr)) {
+			throw new PrismNotSupportedException("LTL formulas with reward bounds not supported for CTMCs");
+		}
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			throw new PrismNotSupportedException("LTL formulas with time bounds not supported for CTMCs");
 		}
@@ -77,6 +80,9 @@ public class CTMCModelChecker extends ProbModelChecker
 	@Override
 	protected StateValues checkRewardCoSafeLTL(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException
 	{
+		if (Expression.containsTemporalRewardBounds(expr)) {
+			throw new PrismNotSupportedException("LTL formulas with reward bounds not supported for CTMCs");
+		}
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			throw new PrismNotSupportedException("LTL formulas with time bounds not supported for CTMCs");
 		}
@@ -105,6 +111,9 @@ public class CTMCModelChecker extends ProbModelChecker
 	@Override
 	protected StateValues checkExistsLTL(Model model, Expression expr, BitSet statesOfInterest) throws PrismException
 	{
+		if (Expression.containsTemporalRewardBounds(expr)) {
+			throw new PrismNotSupportedException("LTL formulas with reward bounds not supported for CTMCs");
+		}
 		if (Expression.containsTemporalTimeBounds(expr)) {
 			throw new PrismNotSupportedException("LTL formulas with time bounds not supported for CTMCs");
 		}