Property.checkAgainstExpectedResultString: handle complex expressions

Instead of before, where only
// RESULT: integer
or
// RESULT: numerator/denominator
were allowed for result expressions, we now support arbitrary expressions
over the model/property parameters, e.g.,

// RESULT: 4.3*floor(q*3)

Caveat: Currently, there can be no whitespace in the expression...

Additionally, when model checking in exact mode, the expected value is
also computed using Expression.evaluateExact.



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

prism/src/parser/ast/Property.java

@@ -41,6 +41,7 @@ import prism.PrismLangException;
 import prism.PrismNotSupportedException;
 import prism.PrismUtils;
 import prism.Point;
+import prism.Prism;
 import prism.TileList;
 
 /**
@@ -140,7 +141,7 @@ public class Property extends ASTElement
 	public boolean checkAgainstExpectedResult(Object result, Values constValues) throws PrismException
 	{
 		String strExpected = getExpectedResultString(constValues);
-		return checkAgainstExpectedResultString(strExpected, result);
+		return checkAgainstExpectedResultString(strExpected, constValues, result);
 	}
 
 	/**
@@ -254,7 +255,7 @@ public class Property extends ASTElement
 	 * @param result The actual result
 	 * @return Whether or not the check was performed
 	 */
-	private boolean checkAgainstExpectedResultString(String strExpected, Object result) throws PrismException
+	private boolean checkAgainstExpectedResultString(String strExpected, Values constValues, Object result) throws PrismException
 	{
 		// Check for special "don't case" case
 		if (strExpected.equals("?")) {
@@ -295,30 +296,53 @@ public class Property extends ASTElement
 		if (type instanceof TypeBool) {
 			// Parse expected result
 			boolean boolExp;
+			boolean simple = true;  // is the expectation string a simple expression?
 			strExpected = strExpected.toLowerCase();
 			if (strExpected.equals("true"))
 				boolExp = true;
 			else if (strExpected.equals("false"))
 				boolExp = false;
-			else
-				throw new PrismException("Invalid RESULT specification \"" + strExpected + "\" for boolean-valued property");
+			else {
+				// complex expression?
+				Expression expectedExpr = null;
+				try {
+					expectedExpr = Prism.parseSingleExpressionString(strExpected);
+					expectedExpr.findAllConstants(new ConstantList(constValues));
+					expectedExpr.typeCheck();
+					boolExp = expectedExpr.evaluateBoolean(constValues);
+					simple = false;  // complex expression
+				} catch (PrismLangException e2) {
+					throw new PrismException("Invalid RESULT specification \"" + strExpected + "\" for boolean-valued property: " + e2.getMessage());
+				}
+			}
 			// Parse actual result
 			boolean boolRes;
 			if (!(result instanceof Boolean))
 				throw new PrismException("Result is wrong type for (boolean-valued) property");
 			boolRes = ((Boolean) result).booleanValue();
 			if (boolRes != boolExp)
-				throw new PrismException("Wrong result (expected " + boolExp + ", got " + boolRes + ")");
+				throw new PrismException("Wrong result (expected " + (simple ? "" : strExpected + " = ") + boolExp + ", got " + boolRes + ")");
 		}
 
 		// Integer-valued properties
 		else if (type instanceof TypeInt) {
 			// Parse expected result
 			int intExp;
+			boolean simple = true;  // is the expectation string a simple expression?
 			try {
 				intExp = Integer.parseInt(strExpected);
 			} catch (NumberFormatException e) {
-				throw new PrismException("Invalid RESULT specification \"" + strExpected + "\" for integer-valued property");
+				// complex expression?
+				Expression expectedExpr = null;
+				try {
+					expectedExpr = Prism.parseSingleExpressionString(strExpected);
+					expectedExpr.findAllConstants(new ConstantList(constValues));
+					expectedExpr.typeCheck();
+					intExp = expectedExpr.evaluateInt(constValues);
+					simple = false;  // complex expression
+				} catch (PrismLangException e2) {
+					throw new PrismException("Invalid RESULT specification \"" + strExpected + "\" for integer-valued property: " + e2.getMessage());
+				}
 			}
 			// Parse actual result
 			int intRes;
@@ -326,13 +350,14 @@ public class Property extends ASTElement
 				throw new PrismException("Result is wrong type for (integer-valued) property");
 			intRes = ((Integer) result).intValue();
 			if (intRes != intExp)
-				throw new PrismException("Wrong result (expected " + intExp + ", got " +intRes + ")");
+				throw new PrismException("Wrong result (expected " + (simple ? "" : strExpected + " = ") + intExp + ", got " +intRes + ")");
 		}
 
 		// Double-valued properties (non-exact mode)
 		else if (type instanceof TypeDouble && !(result instanceof BigRational)) {
 			// Parse expected result
 			double doubleExp;
+			boolean simple = true;  // is the expectation string a simple expression?
 			try {
 				// See if it's NaN
 				if (strExpected.equals("NaN")) {
@@ -343,13 +368,24 @@ public class Property extends ASTElement
 					int numer = Integer.parseInt(strExpected.substring(0, strExpected.indexOf('/')));
 					int denom = Integer.parseInt(strExpected.substring(strExpected.indexOf('/') + 1));
 					doubleExp = ((double) numer) / denom;
+					simple = false;  // complex expression
 				}
-				// Otherwise, just a double
+				// Otherwise, see if it's just a double
 				else {
 					doubleExp = Double.parseDouble(strExpected);
 				}
 			} catch (NumberFormatException e) {
-				throw new PrismException("Invalid RESULT specification \"" + strExpected + "\" for double-valued property");
+				// complex expression?
+				Expression expectedExpr = null;
+				try {
+					expectedExpr = Prism.parseSingleExpressionString(strExpected);
+					expectedExpr.findAllConstants(new ConstantList(constValues));
+					expectedExpr.typeCheck();
+					doubleExp = expectedExpr.evaluateDouble(constValues);
+					simple = false;  // complex expression
+				} catch (PrismLangException e2) {
+					throw new PrismException("Invalid RESULT specification \"" + strExpected + "\" for double-valued property: " + e2.getMessage());
+				}
 			}
 			// Parse actual result
 			if (!(result instanceof Double))
@@ -358,10 +394,10 @@ public class Property extends ASTElement
 			// Compare results
 			if (Double.isNaN(doubleRes)) {
 				if (!Double.isNaN(doubleExp))
-					throw new PrismException("Wrong result (expected " + doubleExp + ", got NaN)");
+					throw new PrismException("Wrong result (expected " + (simple ? "" : strExpected + " = ") + doubleExp + ", got NaN)");
 			} else {
 				if (!PrismUtils.doublesAreCloseRel(doubleExp, doubleRes, 1e-5))
-					throw new PrismException("Wrong result (expected " + doubleExp + ", got " + doubleRes + ")");
+					throw new PrismException("Wrong result (expected " + (simple ? "" : strExpected + " = ") + doubleExp + ", got " + doubleRes + ")");
 			}
 		}
 
@@ -370,6 +406,7 @@ public class Property extends ASTElement
 			// Parse expected result
 			BigRational rationalRes = (BigRational) result;
 			BigRational rationalExp = null;
+			boolean simple = true;  // is the expectation string a simple expression?
 			try {
 				// See if it's NaN
 				if (strExpected.equals("NaN")) {
@@ -381,11 +418,21 @@ public class Property extends ASTElement
 					rationalExp = new BigRational(strExpected);
 				}
 			} catch (NumberFormatException e) {
-				throw new PrismException("Invalid RESULT specification \"" + strExpected + "\" for rational-valued property");
+				// complex expression?
+				Expression expectedExpr = null;
+				try {
+					expectedExpr = Prism.parseSingleExpressionString(strExpected);
+					expectedExpr.findAllConstants(new ConstantList(constValues));
+					expectedExpr.typeCheck();
+					rationalExp = expectedExpr.evaluateExact(constValues);
+					simple = false;  // complex expression
+				} catch (PrismLangException e2) {
+					throw new PrismException("Invalid RESULT specification \"" + strExpected + "\" for rational-valued property: " + e2.getMessage());
+				}
 			}
 			// Compare results
 			if (!rationalRes.equals(rationalExp))
-				throw new PrismException("Wrong result (expected " + rationalExp + ", got " + rationalRes + ")");
+				throw new PrismException("Wrong result (expected " + (simple ? "" : strExpected + " = ") + rationalExp + ", got " + rationalRes + ")");
 		}
 		else if (type instanceof TypeVoid && result instanceof TileList) { //Pareto curve