PrismCL passes parameters names to test code in parametric testing mode.

This potentially allows checking of "symbolic" expressions for methods/engines
other than the parametric engine. It will also allow simplification of the
mechanisms for storing results from parametric model checking, aligning it
with other parts of the code.

prism/src/param/ParamResult.java

@@ -28,6 +28,8 @@
 
 package param;
 
+import java.util.List;
+
 import parser.Values;
 import parser.ast.ConstantList;
 import parser.ast.Expression;
@@ -125,10 +127,11 @@ public class ParamResult
 	 * @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
+	 * @param params The names of any parameters, i.e., still undefined constants (null if none)
 	 * @return true if the test succeeds
 	 * @throws PrismException on test failure
 	 */
-	public boolean test(Type propertyType, String strExpected, Values constValues) throws PrismException
+	public boolean test(Type propertyType, String strExpected, Values constValues, List<String> params) throws PrismException
 	{
 		Expression exprExpected = null;
 		try {
@@ -145,7 +148,7 @@ public class ParamResult
 				// defined constants
 				ConstantList constantList = new ConstantList(constValues);
 				// and parametric constants
-				for (String p : modelBuilder.getParameterNames()) {
+				for (String p : params) {
 					constantList.addConstant(new ExpressionIdent(p), null, TypeDouble.getInstance());
 				}
 				exprExpected = (Expression) exprExpected.findAllConstants(constantList);

prism/src/parser/ast/Property.java

@@ -27,6 +27,7 @@
 package parser.ast;
 
 import java.util.HashMap;
+import java.util.List;
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 
@@ -108,13 +109,13 @@ public class Property extends ASTElement
 	/**
 	 * Tests a result against the expected result for this Property, specified by an embedded "RESULT: xxx"
 	 * string in the accompanying comment (immediately preceding it in the property specification).
-	 * Different results for different constant values are specified by e.g. "RESULT (x=1): xxx". 
+	 * Different results for different constant values are specified by e.g. "RESULT (x=1): xxx".
 	 * The result should ideally be passed in as a {@link prism.Result} object, but can also
 	 * be given directly as an object of the appropriate type: Boolean, Double, etc.)
 	 * If the test fails or something else goes wrong, an explanatory PrismException is thrown.
 	 * Otherwise, the method successfully exits, returning a boolean value that indicates
 	 * whether or not a check was actually applied (i.e. if the result specification is of the
-	 * form "RESULT: ?") then false is returned; otherwise true.   
+	 * form "RESULT: ?") then false is returned; otherwise true.
 	 * @param result The actual result
 	 * @return Whether or not the check was performed
 	 */
@@ -126,29 +127,49 @@ public class Property extends ASTElement
 	/**
 	 * Tests a result against the expected result for this Property, specified by an embedded "RESULT: xxx"
 	 * string in the accompanying comment (immediately preceding it in the property specification).
-	 * Different results for different constant values are specified by e.g. "RESULT (x=1): xxx". 
+	 * Different results for different constant values are specified by e.g. "RESULT (x=1): xxx".
 	 * The result should ideally be passed in as a {@link prism.Result} object, but can also
 	 * be given directly as an object of the appropriate type: Boolean, Double, etc.)
 	 * If the test fails or something else goes wrong, an explanatory PrismException is thrown.
 	 * Otherwise, the method successfully exits, returning a boolean value that indicates
 	 * whether or not a check was actually applied (i.e. if the result specification is of the
-	 * form "RESULT: ?") then false is returned; otherwise true.   
+	 * form "RESULT: ?") then false is returned; otherwise true.
 	 * @param result The actual result
-	 * @param constValues The values of any undefined constants (null if none)
+	 * @param constValues The values of any constants (null if none)
 	 * @return Whether or not the check was performed
 	 */
 	public boolean checkAgainstExpectedResult(Object result, Values constValues) throws PrismException
+	{
+		return checkAgainstExpectedResult(result, constValues, null);
+	}
+
+	/**
+	 * Tests a result against the expected result for this Property, specified by an embedded "RESULT: xxx"
+	 * string in the accompanying comment (immediately preceding it in the property specification).
+	 * Different results for different constant values are specified by e.g. "RESULT (x=1): xxx".
+	 * The result should ideally be passed in as a {@link prism.Result} object, but can also
+	 * be given directly as an object of the appropriate type: Boolean, Double, etc.)
+	 * If the test fails or something else goes wrong, an explanatory PrismException is thrown.
+	 * Otherwise, the method successfully exits, returning a boolean value that indicates
+	 * whether or not a check was actually applied (i.e. if the result specification is of the
+	 * form "RESULT: ?") then false is returned; otherwise true.
+	 * @param result The actual result
+	 * @param constValues The values of any constants (null if none)
+	 * @param params The names of any parameters, for "symbolic" results (null if none)
+	 * @return Whether or not the check was performed
+	 */
+	public boolean checkAgainstExpectedResult(Object result, Values constValues, List<String> params) throws PrismException
 	{
 		Result resultObj = (result instanceof Result) ? ((Result) result) : new Result(result);
 		String strExpected = getExpectedResultString(constValues);
-		return ResultTesting.checkAgainstExpectedResultString(strExpected, constValues, expr.getType(), resultObj);
+		return ResultTesting.checkAgainstExpectedResultString(strExpected, constValues, params, expr.getType(), resultObj);
 	}
 
 	/**
 	 * Get the expected result by extracting from the appropriate RESULT annotation.
 	 * This is done by finding the first RESULT whose constant values (if any) all match those
 	 * provided in {@code constValues}. A PrismException is thrown if no matching RESULT is found.
-	 * @param constValues The values of any undefined constants (null if none)
+	 * @param constValues The values of any constants (null if none)
 	 */
 	private String getExpectedResultString(Values constValues) throws PrismException
 	{
@@ -220,7 +241,7 @@ public class Property extends ASTElement
 	 * This is done by an exact string match against the provided string of constant values.
 	 * A PrismException is thrown if no matching RESULT is found.
 	 * This method actually looks at all RESULTs and complains if there multiple matches. 
-	 * @param constValues The values of any undefined constants (null or "" if none)
+	 * @param constValues The values of any constants (null or "" if none)
 	 */
 	@SuppressWarnings("unused")
 	private String getExpectedResultString(String constValues) throws PrismException

prism/src/prism/PrismCL.java

@@ -33,6 +33,8 @@ import java.io.PrintWriter;
 import java.io.StringWriter;
 import java.net.UnknownHostException;
 import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Collections;
 import java.util.List;
 
 import common.StackTraceHelper;
@@ -1005,7 +1007,8 @@ public class PrismCL implements PrismModelListener
 	{
 		try {
 			Values allConsts = new Values(mfConstants, pfConstants);
-			if (prop.checkAgainstExpectedResult(res, allConsts)) {
+			List<String> allParams = param ? Arrays.asList(paramNames) : Collections.emptyList(); 
+			if (prop.checkAgainstExpectedResult(res, allConsts, allParams)) {
 				mainLog.println("Testing result: PASS");
 			} else {
 				mainLog.println("Testing result: NOT TESTED");

prism/src/prism/ResultTesting.java

@@ -52,12 +52,13 @@ public class ResultTesting
 	 * whether or not a check was actually applied (i.e. if the result specification is of the
 	 * form "RESULT: ?") then false is returned; otherwise true.   
 	 * @param strExpected Expected result
-	 * @param constValues The values of any undefined constants (null or "" if none)
+	 * @param constValues The values of any constants (null if none)
+	 * @param params The names of any still undefined constants (null if none)
 	 * @param type The type of the property yielding this result
 	 * @param resultObj The result to check
 	 * @return Whether or not the check was performed
 	 */
-	public static boolean checkAgainstExpectedResultString(String strExpected, Values constValues, Type type, Result resultObj) throws PrismException
+	public static boolean checkAgainstExpectedResultString(String strExpected, Values constValues, List<String> params, Type type, Result resultObj) throws PrismException
 	{
 		Object result = resultObj.getResult();
 		// Check for special "don't care" case
@@ -73,7 +74,7 @@ public class ResultTesting
 		}
 		// Check result of parametric model checking
 		if (result instanceof ParamResult) {
-			return ((ParamResult) result).test(type, strExpected, constValues);
+			return ((ParamResult) result).test(type, strExpected, constValues, params);
 		}
 		// Otherwise, check depends on the type of the property  
 		// Boolean-valued properties