Disallow properties of the form R[F<=k].

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

prism/src/explicit/ProbModelChecker.java

@@ -1037,6 +1037,11 @@ public class ProbModelChecker extends NonProbModelChecker
 	 */
 	protected StateValues checkRewardReach(Model model, Rewards modelRewards, ExpressionTemporal expr, MinMax minMax, BitSet statesOfInterest) throws PrismException
 	{
+		// No time bounds allowed
+		if (expr.hasBounds()) {
+			throw new PrismNotSupportedException("R operator cannot contain a bounded F operator: " + expr);
+		}
+		
 		// Model check the operand for all states
 		BitSet target = checkExpression(model, expr.getOperand2(), null).getBitSet();
 

prism/src/parser/ast/Expression.java

@@ -725,10 +725,8 @@ public abstract class Expression extends ASTElement
 			{
 				public void visitPre(ExpressionTemporal e) throws PrismLangException
 				{
-					if (e.getLowerBound() != null)
-						throw new PrismLangException(e.getOperatorSymbol());
-					if (e.getUpperBound() != null)
-						throw new PrismLangException(e.getOperatorSymbol());
+					if (e.hasBounds())
+						throw new PrismLangException("");
 				}
 			});
 		} catch (PrismLangException e) {

prism/src/prism/NondetModelChecker.java

@@ -1202,6 +1202,11 @@ public class NondetModelChecker extends NonProbModelChecker
 		JDDNode b;
 		StateValues rewards = null;
 
+		// No time bounds allowed
+		if (expr.hasBounds()) {
+			throw new PrismNotSupportedException("R operator cannot contain a bounded F operator: " + expr);
+		}
+		
 		// model check operand first
 		b = checkExpressionDD(expr.getOperand2());
 

prism/src/prism/ProbModelChecker.java

@@ -876,6 +876,11 @@ public class ProbModelChecker extends NonProbModelChecker
 		JDDNode b;
 		StateValues rewards = null;
 
+		// No time bounds allowed
+		if (expr.hasBounds()) {
+			throw new PrismNotSupportedException("R operator cannot contain a bounded F operator: " + expr);
+		}
+		
 		// model check operand first
 		b = checkExpressionDD(expr.getOperand2());