param/exact: support for ITE and functions in probability expressions

If-then-else expressions:
The if-expression can not refer to a parametric constant.

Other functions (min, max, floor, ...):
Arguments can not refer to parametric constants and evaluating
the function exactly has to be supported.


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

prism/src/param/ModelBuilder.java

@@ -35,6 +35,8 @@ import parser.ast.ConstantList;
 import parser.ast.Expression;
 import parser.ast.ExpressionBinaryOp;
 import parser.ast.ExpressionConstant;
+import parser.ast.ExpressionFunc;
+import parser.ast.ExpressionITE;
 import parser.ast.ExpressionLiteral;
 import parser.ast.ExpressionUnaryOp;
 import parser.ast.ModulesFile;
@@ -149,6 +151,41 @@ public final class ModelBuilder extends PrismComponent
 			default:
 				throw new PrismNotSupportedException("parametric analysis with rate/probability of " + expr + " not implemented");
 			}
+		} else if (expr instanceof ExpressionITE){
+			ExpressionITE iteExpr = (ExpressionITE) expr;
+			// ITE expressions where the if-expression does not
+			// depend on a parametric constant are supported
+			if (iteExpr.getOperand1().isConstant()) {
+				try {
+					// non-parametric constants and state variable values have
+					// been already partially expanded, so if this evaluation
+					// succeeds there are no parametric constants involved
+					boolean ifValue = iteExpr.getOperand1().evaluateBoolean();
+					if (ifValue) {
+						return expr2function(factory, iteExpr.getOperand2());
+					} else {
+						return expr2function(factory, iteExpr.getOperand3());
+					}
+				} catch (PrismException e) {
+					// Most likely, a parametric constant occurred.
+					// Do nothing here, exception is thrown below
+				}
+			}
+			throw new PrismNotSupportedException("parametric analysis with rate/probability of " + expr + " not implemented");
+		} else if (expr instanceof ExpressionFunc) {
+			// functions (min, max, floor, ...) are supported if
+			// they don't refer to parametric constants in their arguments
+			// and can be exactly evaluated
+			try {
+				// non-parametric constants and state variable values have
+				// been already partially expanded, so if this evaluation
+				// succeeds there are no parametric constants involved
+				BigRational value = expr.evaluateExact();
+				return factory.fromBigRational(value);
+			} catch (PrismException e) {
+				// Most likely, a parametric constant occurred.
+				throw new PrismNotSupportedException("parametric analysis with rate/probability of " + expr + " not implemented");
+			}
 		} else {
 			throw new PrismNotSupportedException("parametric analysis with rate/probability of " + expr + " not implemented");
 		}