From e1105ab74aed4997fcb157802c2b8853515d170e Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 22 Jul 2016 10:37:48 +0000 Subject: [PATCH] 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 | 73 ++++++++++++++++++++++++------ 1 file changed, 60 insertions(+), 13 deletions(-) diff --git a/prism/src/parser/ast/Property.java b/prism/src/parser/ast/Property.java index 16ba7d7f..f7ea47a4 100644 --- a/prism/src/parser/ast/Property.java +++ b/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