Bugfix: missing type checking in properties: P/S/R operators were allowed to contain arbitrary types.

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

prism/src/parser/visitor/TypeCheck.java

@@ -463,9 +463,11 @@ public class TypeCheck extends ASTTraverse
 
 	public void visitPost(ExpressionProb e) throws PrismLangException
 	{
+		// Check prob bound
 		if (e.getProb() != null && !TypeDouble.getInstance().canAssign(e.getProb().getType())) {
 			throw new PrismLangException("Type error: P operator probability bound is not a double", e.getProb());
 		}
+		// Check filter
 		if (e.getFilter() != null && !(e.getFilter().getExpression().getType() instanceof TypeBool)) {
 			throw new PrismLangException("Type error: P operator filter is not a Boolean", e.getFilter().getExpression());
 		}
@@ -475,21 +477,28 @@ public class TypeCheck extends ASTTraverse
 				throw new PrismLangException("Type error: Cannot use min/max filters in Boolean-valued properties");
 			}
 		}
+		// Check path operator
+		if (!(e.getExpression().getType() instanceof TypePathBool)) {
+			throw new PrismLangException("Type error: Contents of P operator is not a path formula", e.getExpression());
+		}
 		// Set type
 		e.setType(e.getProb() == null ? TypeDouble.getInstance() : TypeBool.getInstance());
 	}
 
 	public void visitPost(ExpressionReward e) throws PrismLangException
 	{
+		// Check reward struct ref
 		if (e.getRewardStructIndex() != null && e.getRewardStructIndex() instanceof Expression) {
 			Expression rsi = (Expression) e.getRewardStructIndex();
 			if (!(rsi.getType() instanceof TypeInt)) {
 				throw new PrismLangException("Type error: Reward structure index must be string or integer", rsi);
 			}
 		}
+		// Check reward bound
 		if (e.getReward() != null && !TypeDouble.getInstance().canAssign(e.getReward().getType())) {
 			throw new PrismLangException("Type error: R operator reward bound is not a double", e.getReward());
 		}
+		// Check filter
 		if (e.getFilter() != null && !(e.getFilter().getExpression().getType() instanceof TypeBool)) {
 			throw new PrismLangException("Type error: R operator filter is not a Boolean", e.getFilter().getExpression());
 		}
@@ -499,15 +508,21 @@ public class TypeCheck extends ASTTraverse
 				throw new PrismLangException("Type error: Cannot use min/max filters in Boolean-valued properties");
 			}
 		}
+		// Check argument
+		if (!(e.getExpression().getType() instanceof TypePathDouble)) {
+			throw new PrismLangException("Type error: Contents of R operator is invalid", e.getExpression());
+		}
 		// Set type
 		e.setType(e.getReward() == null ? TypeDouble.getInstance() : TypeBool.getInstance());
 	}
 
 	public void visitPost(ExpressionSS e) throws PrismLangException
 	{
+		// Check probability bound
 		if (e.getProb() != null && !TypeDouble.getInstance().canAssign(e.getProb().getType())) {
 			throw new PrismLangException("Type error: S operator probability bound is not a double", e.getProb());
 		}
+		// Check filter
 		if (e.getFilter() != null && !(e.getFilter().getExpression().getType() instanceof TypeBool)) {
 			throw new PrismLangException("Type error: P operator filter is not a Boolean", e.getFilter().getExpression());
 		}
@@ -517,6 +532,10 @@ public class TypeCheck extends ASTTraverse
 				throw new PrismLangException("Type error: Cannot use min/max filters in Boolean-valued properties");
 			}
 		}
+		// Check argument
+		if (!(e.getExpression().getType() instanceof TypePathBool)) {
+			throw new PrismLangException("Type error: Contents of S operator is not a Boolean-valued expression", e.getExpression());
+		}
 		// Set type
 		e.setType(e.getProb() == null ? TypeDouble.getInstance() : TypeBool.getInstance());
 	}