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

@@ -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) {

prism/src/param/ParamResult.java

@@ -0,0 +1,194 @@
+//==============================================================================
+//	
+//	Copyright (c) 2016-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (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.
+	 * <br>
+	 * 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.
+	 * <br>
+	 * 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.
+	 * <br>
+	 * 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;
+	}
+}

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

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";