Refactor constant evaluation: support exact evaluation mode

Previously, constants that are defined via an expression
were evaluated using standard (integer or floating point) arithmetic,
even in parametric or exact model checking mode.

This commit provides the infrastructure for requesting that constant
expressions are evaluated using exact arithmetic.

To keep the API backward compatible, we introduce additional methods that
offer an 'exact' flag, but keep the old methods as well. Those default to
normal arithmetic.

TypeDouble constants are kept as rational numbers, while int and boolean
constants are converted to Java data types. For int, an exception is raised
if the value can't be exactly represented by Java int.

prism/src/parser/ast/ConstantList.java

@@ -30,6 +30,7 @@ import java.util.HashMap;
 import java.util.Map;
 import java.util.Vector;
 
+import param.BigRational;
 import parser.*;
 import parser.visitor.*;
 import prism.PrismLangException;
@@ -232,37 +233,66 @@ public class ConstantList extends ASTElement
 			return false;
 		return (getConstant(i) != null);
 	}
-	
+
 	/**
 	 * Set values for *all* undefined constants, evaluate values for *all* constants
 	 * and return a Values object with values for *all* constants.
 	 * Argument 'someValues' contains values for undefined ones, can be null if all already defined
 	 * Argument 'otherValues' contains any other values which may be needed, null if none
+	 * <br>
+	 * Uses standard (integer, floating-point) arithmetic for evaluating constants.
 	 */
 	public Values evaluateConstants(Values someValues, Values otherValues) throws PrismLangException
 	{
-		return evaluateSomeOrAllConstants(someValues, otherValues, true);
+		return evaluateConstants(someValues, otherValues, false);
 	}
-	
+
+	/**
+	 * Set values for *all* undefined constants, evaluate values for *all* constants
+	 * and return a Values object with values for *all* constants.
+	 * Argument 'someValues' contains values for undefined ones, can be null if all already defined
+	 * Argument 'otherValues' contains any other values which may be needed, null if none
+	 * If argument 'exact' is true, constants are evaluated using exact arithmetic (BigRational)
+	 */
+	public Values evaluateConstants(Values someValues, Values otherValues, boolean exact) throws PrismLangException
+	{
+		return evaluateSomeOrAllConstants(someValues, otherValues, true, exact);
+	}
+
 	/**
 	 * Set values for *some* undefined constants, evaluate values for constants where possible
 	 * and return a Values object with values for all constants that could be evaluated.
 	 * Argument 'someValues' contains values for undefined ones, can be null if all already defined
 	 * Argument 'otherValues' contains any other values which may be needed, null if none
+	 * <br>
+	 * Uses standard (integer, floating-point) arithmetic for evaluating constants.
 	 */
 	public Values evaluateSomeConstants(Values someValues, Values otherValues) throws PrismLangException
 	{
-		return evaluateSomeOrAllConstants(someValues, otherValues, false);
+		return evaluateSomeConstants(someValues, otherValues, false);
 	}
-	
+
+	/**
+	 * Set values for *some* undefined constants, evaluate values for constants where possible
+	 * and return a Values object with values for all constants that could be evaluated.
+	 * Argument 'someValues' contains values for undefined ones, can be null if all already defined
+	 * Argument 'otherValues' contains any other values which may be needed, null if none
+	 * If argument 'exact' is true, constants are evaluated using exact arithmetic (BigRational)
+	 */
+	public Values evaluateSomeConstants(Values someValues, Values otherValues, boolean exact) throws PrismLangException
+	{
+		return evaluateSomeOrAllConstants(someValues, otherValues, false, exact);
+	}
+
 	/**
 	 * Set values for *some* or *all* undefined constants, evaluate values for constants where possible
 	 * and return a Values object with values for all constants that could be evaluated.
 	 * Argument 'someValues' contains values for undefined ones, can be null if all already defined.
 	 * Argument 'otherValues' contains any other values which may be needed, null if none.
 	 * If argument 'all' is true, an exception is thrown if any undefined constant is not defined.
+	 * If argument 'exact' is true, constants are evaluated using exact arithmetic (BigRational)
 	 */
-	private Values evaluateSomeOrAllConstants(Values someValues, Values otherValues, boolean all) throws PrismLangException
+	private Values evaluateSomeOrAllConstants(Values someValues, Values otherValues, boolean all, boolean exact) throws PrismLangException
 	{
 		ConstantList cl;
 		Expression e;
@@ -322,8 +352,23 @@ public class ConstantList extends ASTElement
 		// Evaluate constants and store in new Values object (again, ignoring 'otherValues' ones)		
 		allValues = new Values();
 		for (i = 0; i < numToEvaluate; i++) {
-			if (cl.getConstant(i) != null) {
-				val = cl.getConstant(i).evaluate(null, otherValues);
+			Expression constant = cl.getConstant(i);
+			if (constant != null) {
+				if (exact) {
+					BigRational r = constant.evaluateExact(null, otherValues);
+					// handle differently, depending on constant type
+					if (constant.getType() instanceof TypeDouble) {
+						// we keep as BigRational for TypeDouble
+						val = r;
+					} else {
+						// we convert to Java int / boolean for TypeInt and TypeBool
+						// Note: throws exception if value can't be precisely represented
+						// using the corresponding Java data type
+						val = constant.getType().castFromBigRational(r);
+					}
+				} else {
+					val = constant.evaluate(null, otherValues);
+				}
 				allValues.addValue(cl.getConstantName(i), val);
 			}
 		}

prism/src/parser/ast/ModulesFile.java

@@ -1011,24 +1011,43 @@ public class ModulesFile extends ASTElement implements ModelInfo
 	 * The current constant values (if set) are available via {@link #getConstantValues()}. 
 	 * Calling this method also triggers some additional semantic checks
 	 * that can only be done once constant values have been specified.
+	 * <br>
+	 * Constant values are evaluated using standard (integer, floating-point) arithmetic.
 	 */
 	public void setUndefinedConstants(Values someValues) throws PrismLangException
 	{
-		undefinedConstantValues = someValues == null ? null : new Values(someValues);
-		constantValues = constantList.evaluateConstants(someValues, null);
-		doSemanticChecksAfterConstants();
+		setUndefinedConstants(someValues, false);
 	}
 
 	/**
-	 * Set values for *some* undefined constants and then evaluate all constants where possible.
+	 * Set values for *all* undefined constants and then evaluate all constants.
 	 * If there are no undefined constants, {@code someValues} can be null.
 	 * Undefined constants can be subsequently redefined to different values with the same method.
-	 * The current constant values (if set) are available via {@link #getConstantValues()}.
+	 * The current constant values (if set) are available via {@link #getConstantValues()}. 
+	 * Calling this method also triggers some additional semantic checks
+	 * that can only be done once constant values have been specified.
+	 * <br>
+	 * Constant values are evaluated using either standard (integer, floating-point) arithmetic
+	 * or exact arithmetic, depending on the value of the {@code exact} flag.
 	 */
+	public void setUndefinedConstants(Values someValues, boolean exact) throws PrismLangException
+	{
+		undefinedConstantValues = someValues == null ? null : new Values(someValues);
+		constantValues = constantList.evaluateConstants(someValues, null, exact);
+		doSemanticChecksAfterConstants();
+	}
+
+	@Override
 	public void setSomeUndefinedConstants(Values someValues) throws PrismLangException
+	{
+		setSomeUndefinedConstants(someValues, false);
+	}
+
+	@Override
+	public void setSomeUndefinedConstants(Values someValues, boolean exact) throws PrismLangException
 	{
 		undefinedConstantValues = someValues == null ? null : new Values(someValues);
-		constantValues = constantList.evaluateSomeConstants(someValues, null);
+		constantValues = constantList.evaluateSomeConstants(someValues, null, exact);
 		doSemanticChecksAfterConstants();
 	}
 

prism/src/parser/ast/PropertiesFile.java

@@ -533,11 +533,27 @@ public class PropertiesFile extends ASTElement
 	 * If there are no undefined constants, {@code someValues} can be null.
 	 * Undefined constants can be subsequently redefined to different values with the same method.
 	 * The current constant values (if set) are available via {@link #getConstantValues()}. 
+	 * <br>
+	 * Constant values are evaluated using standard (integer, floating-point) arithmetic.
 	 */
 	public void setUndefinedConstants(Values someValues) throws PrismLangException
+	{
+		setUndefinedConstants(someValues, false);
+	}
+
+	/**
+	 * Set values for *all* undefined constants and then evaluate all constants.
+	 * If there are no undefined constants, {@code someValues} can be null.
+	 * Undefined constants can be subsequently redefined to different values with the same method.
+	 * The current constant values (if set) are available via {@link #getConstantValues()}.
+	 * <br>
+	 * Constant values are evaluated using either standard (integer, floating-point) arithmetic
+	 * or exact arithmetic, depending on the value of the {@code exact} flag.
+	 */
+	public void setUndefinedConstants(Values someValues, boolean exact) throws PrismLangException
 	{
 		// Might need values for ModulesFile constants too
-		constantValues = constantList.evaluateConstants(someValues, modulesFile.getConstantValues());
+		constantValues = constantList.evaluateConstants(someValues, modulesFile.getConstantValues(), exact);
 		// Note: unlike ModulesFile, we don't trigger any semantic checks at this point
 		// This will usually be done on a per-property basis later
 	}
@@ -547,11 +563,27 @@ public class PropertiesFile extends ASTElement
 	 * If there are no undefined constants, {@code someValues} can be null.
 	 * Undefined constants can be subsequently redefined to different values with the same method.
 	 * The current constant values (if set) are available via {@link #getConstantValues()}.
+	 * <br>
+	 * Constant values are evaluated using standard (integer, floating-point) arithmetic.
 	 */
 	public void setSomeUndefinedConstants(Values someValues) throws PrismLangException
+	{
+		setSomeUndefinedConstants(someValues, false);
+	}
+
+	/**
+	 * Set values for *some* undefined constants and then evaluate all constants where possible.
+	 * If there are no undefined constants, {@code someValues} can be null.
+	 * Undefined constants can be subsequently redefined to different values with the same method.
+	 * The current constant values (if set) are available via {@link #getConstantValues()}.
+	 * <br>
+	 * Constant values are evaluated using either standard (integer, floating-point) arithmetic
+	 * or exact arithmetic, depending on the value of the {@code exact} flag.
+	 */
+	public void setSomeUndefinedConstants(Values someValues, boolean exact) throws PrismLangException
 	{
 		// Might need values for ModulesFile constants too
-		constantValues = constantList.evaluateSomeConstants(someValues, modulesFile.getConstantValues());
+		constantValues = constantList.evaluateSomeConstants(someValues, modulesFile.getConstantValues(), exact);
 		// Note: unlike ModulesFile, we don't trigger any semantic checks at this point
 		// This will usually be done on a per-property basis later
 	}

prism/src/prism/ModelInfo.java

@@ -50,6 +50,8 @@ public interface ModelInfo
 	 * If there are no undefined constants, {@code someValues} can be null.
 	 * Undefined constants can be subsequently redefined to different values with the same method.
 	 * The current constant values (if set) are available via {@link #getConstantValues()}.
+	 * <br>
+	 * Constant values are evaluated using standard (integer, floating-point) arithmetic.
 	 */
 	public default void setSomeUndefinedConstants(Values someValues) throws PrismException
 	{
@@ -58,6 +60,28 @@ public interface ModelInfo
 			throw new PrismException("This model has no constants to set");
 	}
 
+	/**
+	 * Set values for *some* undefined constants.
+	 * If there are no undefined constants, {@code someValues} can be null.
+	 * Undefined constants can be subsequently redefined to different values with the same method.
+	 * The current constant values (if set) are available via {@link #getConstantValues()}.
+	 * <br>
+	 * Constant values are evaluated using either using standard (integer, floating-point) arithmetic
+	 * or exact arithmetic, depending on the value of the {@code exact} flag.
+	 */
+	public default void setSomeUndefinedConstants(Values someValues, boolean exact) throws PrismException
+	{
+		// default implementation: use implementation for setSomeUndefinedConstants(Values)
+		// for non-exact, error for exact
+		//
+		// implementers should override both this method and setSomeUndefinedConstants(Values)
+		// above
+		if (!exact)
+			setSomeUndefinedConstants(someValues);
+		else
+			throw new PrismException("This model can not set constants in exact mode");
+	}
+
 	/**
 	 * Get access to the values for all constants in the model, including the 
 	 * undefined constants set previously via the method {@link #setUndefinedConstants(Values)}.

prism/src/prism/Prism.java

@@ -262,6 +262,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 	private ModelGenerator currentModelGenerator = null;
 	// Constants to be defined for PRISM model
 	private Values currentDefinedMFConstants = null;
+	// Was currentDefinedMFConstants evaluated exactly?
+	private boolean currentDefinedMFConstantsAreExact = false;
 	// Built model storage - symbolic or explicit - at most one is non-null
 	private Model currentModel = null;
 	private explicit.Model currentModelExpl = null;
@@ -1770,28 +1772,46 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		// TODO: print more info 
 		//mainLog.println();
 	}
-	
+
 	/**
 	 * Set (some or all) undefined constants for the currently loaded PRISM model
 	 * (assuming they have changed since the last time this was called).
+	 * <br>
+	 * Constants are evaluated using standard (integer, floating-point) arithmetic.
 	 * @param definedMFConstants The constant values
 	 */
 	public void setPRISMModelConstants(Values definedMFConstants) throws PrismException
 	{
-		if (currentDefinedMFConstants == null && definedMFConstants == null)
+		setPRISMModelConstants(definedMFConstants, false);
+	}
+
+	/**
+	 * Set (some or all) undefined constants for the currently loaded PRISM model
+	 * (assuming they have changed since the last time this was called).
+	 * @param definedMFConstants The constant values
+	 * @param exact if true, do exact evaluation of constants (using BigRational)
+	 */
+	public void setPRISMModelConstants(Values definedMFConstants, boolean exact) throws PrismException
+	{
+		if (currentDefinedMFConstants == null && definedMFConstants == null && currentDefinedMFConstantsAreExact == exact)
 			return;
-		if (currentDefinedMFConstants != null && currentDefinedMFConstants.equals(definedMFConstants))
+		if (currentDefinedMFConstants != null &&
+		    currentDefinedMFConstants.equals(definedMFConstants) &&
+		    currentDefinedMFConstantsAreExact == exact) {
+			// no change in constants and evaluation mode, nothing to do
 			return;
+		}
 
 		// Clear any existing built model(s)
 		clearBuiltModel();
 		// Store constants here and in ModulesFile
 		currentDefinedMFConstants = definedMFConstants;
+		currentDefinedMFConstantsAreExact = exact;
 		if (currentModulesFile != null) {
-			currentModulesFile.setSomeUndefinedConstants(definedMFConstants);
+			currentModulesFile.setSomeUndefinedConstants(definedMFConstants, exact);
 		}
 		if (currentModelGenerator != null) {
-			currentModelGenerator.setSomeUndefinedConstants(definedMFConstants);
+			currentModelGenerator.setSomeUndefinedConstants(definedMFConstants, exact);
 		}
 
 		// If required, export parsed PRISM model, with constants expanded

prism/src/simulator/ModulesFileModelGenerator.java

@@ -110,9 +110,15 @@ public class ModulesFileModelGenerator implements ModelGenerator
 	{
 		return modelType;
 	}
-	
+
 	@Override
 	public void setSomeUndefinedConstants(Values someValues) throws PrismException
+	{
+		setSomeUndefinedConstants(someValues, false);
+	}
+
+	@Override
+	public void setSomeUndefinedConstants(Values someValues, boolean exact) throws PrismException
 	{
 		// We start again with a copy of the original modules file
 		// and set the constants in the copy.
@@ -121,7 +127,7 @@ public class ModulesFileModelGenerator implements ModelGenerator
 		// start again at a place where references to constants have not
 		// yet been replaced.
 		modulesFile = (ModulesFile) originalModulesFile.deepCopy();
-		modulesFile.setSomeUndefinedConstants(someValues);
+		modulesFile.setSomeUndefinedConstants(someValues, exact);
 		mfConstants = modulesFile.getConstantValues();
 		initialise();
 	}

prism/src/simulator/ModulesFileModelGeneratorSymbolic.java

@@ -134,9 +134,15 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
 	{
 		return modelType;
 	}
-	
+
 	@Override
 	public void setSomeUndefinedConstants(Values someValues) throws PrismException
+	{
+		setSomeUndefinedConstants(someValues, false);
+	}
+
+	@Override
+	public void setSomeUndefinedConstants(Values someValues, boolean exact) throws PrismException
 	{
 		// We start again with a copy of the original modules file
 		// and set the constants in the copy.
@@ -145,7 +151,7 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
 		// start again at a place where references to constants have not
 		// yet been replaced.
 		modulesFile = (ModulesFile) originalModulesFile.deepCopy();
-		modulesFile.setSomeUndefinedConstants(someValues);
+		modulesFile.setSomeUndefinedConstants(someValues, exact);
 		mfConstants = modulesFile.getConstantValues();
 		initialise();
 	}