From b030d707eb2f1495b01dd0a32b2bc5cfc584692b Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 17 Aug 2016 17:09:51 +0000 Subject: [PATCH] param: Wrap result as ParamResult, support testing (for single region result) We wrap the RegionValues returned by ParamModelChecker in a ParamResult object, which stores additional meta-information that allow for the result to be tested. In test mode, if there is only a single region, tests against the given expected RESULT expression. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11639 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/param/ParamModelChecker.java | 2 +- prism/src/param/ParamResult.java | 194 +++++++++++++++++++++++++ prism/src/parser/ast/Property.java | 6 + prism/src/prism/Prism.java | 20 +-- 4 files changed, 204 insertions(+), 18 deletions(-) create mode 100644 prism/src/param/ParamResult.java diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index e8a93fa5..e02c01ed 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -245,7 +245,7 @@ final public class ParamModelChecker extends PrismComponent // Store result result = new Result(); vals.clearExceptInit(); - result.setResult(vals); + result.setResult(new ParamResult(vals, modelBuilder, functionFactory)); /* // Output plot to tex file if (paramLower.length == 2) { diff --git a/prism/src/param/ParamResult.java b/prism/src/param/ParamResult.java new file mode 100644 index 00000000..2f0dedd7 --- /dev/null +++ b/prism/src/param/ParamResult.java @@ -0,0 +1,194 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * Dave Parker (University of Birmingham/Oxford) +// * Joachim Klein (TU Dresden) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + + +package param; + +import parser.Values; +import parser.ast.ConstantList; +import parser.ast.Expression; +import parser.ast.ExpressionIdent; +import parser.type.Type; +import parser.type.TypeBool; +import parser.type.TypeDouble; +import prism.Prism; +import prism.PrismException; +import prism.PrismLangException; +import prism.PrismNotSupportedException; + +/** + * Stores the result of a ParamModelChecker run (a RegionValues object) + * as well as additional information (ModelBuilder, FunctionFactory) + * that is needed to test the actual result against an expected result + * (test mode). + */ +public class ParamResult +{ + /** The actual result */ + private RegionValues regionValues; + /** The model builder (for accessing expr2func) */ + private ModelBuilder modelBuilder; + /** The function factory used for model checking */ + private FunctionFactory factory; + + /** + * Constructor + * @param regionValues the actual result + * @param modelBuilder the model builder used during checking + * @param factory the function factory used during checking + */ + public ParamResult(RegionValues regionValues, ModelBuilder modelBuilder, FunctionFactory factory) + { + this.regionValues = regionValues; + this.modelBuilder = modelBuilder; + this.factory = factory; + } + + /** + * Get the region values result. + */ + public RegionValues getRegionValues() + { + return regionValues; + } + + /** + * Returns the result (region values) as a String. + */ + @Override + public String toString() + { + return regionValues.toString(); + } + + /** + * If ParamModelChecker ran in exact mode (no parametric constants), + * the result will consist of a single region and a single value instead + * of a function. + *
+ * This method returns this single value (either a Boolean or a BigRational). + * @param propertyType the type of the checked property + * @return Boolean/BigRational result (for the initial state) + * @throws PrismException if there are multiple regions or the value is a function + */ + public Object getSimpleResult(Type propertyType) throws PrismException + { + if (regionValues.getNumRegions() != 1) + throw new PrismException("Unexpected result from parametric model checker"); + + if (propertyType.equals(TypeBool.getInstance())) { + // boolean result + boolean boolResult = regionValues.getResult(0).getInitStateValueAsBoolean(); + return boolResult; + } else { + // numeric result + param.Function func = regionValues.getResult(0).getInitStateValueAsFunction(); + // Evaluate the function at an arbitrary point (should not depend on parameter values) + BigRational rat = func.evaluate(new param.Point(new BigRational[] { new BigRational(0) })); + return rat; + } + } + + /** + * Test the result against the given expected result string. + *
+ * Returns true if the test succeeds, throws a PrismException + * with an explanation otherwise. + * @param propertyType the type of the checked property + * @param strExpected the expected result (as a String) + * @param constValues the model/property constants used during the checking + * @return true if the test succeeds + * @throws PrismException on test failure + */ + public boolean test(Type propertyType, String strExpected, Values constValues) throws PrismException + { + Expression exprExcepted = null; + try { + exprExcepted = Prism.parseSingleExpressionString(strExpected); + + // the constants that can be used in the expected result expression: + // defined constants + ConstantList constantList = new ConstantList(constValues); + // and parametric constants + for (String p : modelBuilder.getParameterNames()) { + constantList.addConstant(new ExpressionIdent(p), null, TypeDouble.getInstance()); + } + exprExcepted.findAllConstants(constantList); + exprExcepted.typeCheck(); + + // replace constants in the expression that have a value + // with the value + exprExcepted = (Expression) exprExcepted.evaluatePartially(constValues, null); + } catch (PrismLangException e) { + throw new PrismException("Invalid RESULT specification \"" + strExpected + "\" for property: " + e.getMessage()); + } + return test(propertyType, exprExcepted, strExpected); + } + + /** + * Test the result against the given expression. + *
+ * Returns true if the test succeeds, throws a PrismException + * with an explanation otherwise. + * @param expected expression for the expected result + * @param strExpected the expected result (as a String, for display in error messages) + * @param propertyType the type of the checked property + * @return true if the test succeeds + * @throws PrismException on test failure + */ + private boolean test(Type propertyType, Expression expected, String strExpected) throws PrismException + { + if (regionValues.getNumRegions() != 1) { + throw new PrismNotSupportedException("Testing parametric results with multiple regions not supported"); + } + + if (propertyType.equals(TypeBool.getInstance())) { + // boolean result + boolean boolResult = regionValues.getResult(0).getInitStateValueAsBoolean(); + boolean boolExpected = expected.evaluateBoolean(); + + if (boolResult != boolExpected) { + throw new PrismException("Wrong result (expected " + strExpected + ", got " + boolResult + ")"); + } + } else { + // numeric result + Function funcExpected; + try { + funcExpected = modelBuilder.expr2function(factory, expected); + } catch (PrismException e) { + throw new PrismException("Invalid (or unsupported) RESULT specification \"" + strExpected + "\" for parametric property"); + } + param.Function func = regionValues.getResult(0).getInitStateValueAsFunction(); + + if (!func.equals(funcExpected)) { + throw new PrismException("Wrong result (expected " + strExpected + " = " + funcExpected + ", got " + func + ")"); + } + } + + return true; + } +} diff --git a/prism/src/parser/ast/Property.java b/prism/src/parser/ast/Property.java index 54c8e986..06d247e2 100644 --- a/prism/src/parser/ast/Property.java +++ b/prism/src/parser/ast/Property.java @@ -33,6 +33,7 @@ import java.util.regex.Matcher; import java.util.regex.Pattern; import param.BigRational; +import param.ParamResult; import parser.Values; import parser.type.*; import parser.visitor.*; @@ -300,6 +301,11 @@ public class Property extends ASTElement // Check expected/actual result Type type = expr.getType(); + if (result instanceof param.ParamResult) { + ParamResult paramResult = (param.ParamResult)result; + return paramResult.test(type, strExpected, constValues); + } + // Boolean-valued properties if (type instanceof TypeBool) { // Parse expected result diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 03fbd854..92a1f93d 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -43,6 +43,7 @@ import odd.ODDUtils; import param.BigRational; import param.ModelBuilder; import param.ParamModelChecker; +import param.ParamResult; import param.RegionValues; import parser.ExplicitFiles2ModulesFile; import parser.PrismParser; @@ -3059,23 +3060,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener // Convert result of parametric model checking to a single value, // either boolean for boolean properties or a rational for numeric properties // There should be just one region since no parameters are used - RegionValues regVals = (RegionValues) result.getResult(); - if (regVals.getNumRegions() != 1) - throw new PrismException("Unexpected result from paramteric model checker"); - - if (prop.getType().equals(TypeBool.getInstance())) { - // boolean result - boolean boolResult = regVals.getResult(0).getInitStateValueAsBoolean(); - // Restore in result object - result.setResult(boolResult); - } else { - // numeric result - param.Function func = regVals.getResult(0).getInitStateValueAsFunction(); - // Evaluate the function at an arbitrary point (should not depend on parameter values) - BigRational rat = func.evaluate(new param.Point(new BigRational[] { new BigRational(0) })); - // Restore in result object - result.setResult(rat); - } + ParamResult paramResult = (ParamResult) result.getResult(); + result.setResult(paramResult.getSimpleResult(prop.getType())); // Print result to log String resultString = "Result";