diff --git a/prism/src/parser/ast/ConstantList.java b/prism/src/parser/ast/ConstantList.java
index c10f9a04..a84a842d 100644
--- a/prism/src/parser/ast/ConstantList.java
+++ b/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
+ *
+ * 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
+ *
+ * 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);
}
}
diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java
index 9faaf519..91f2f956 100644
--- a/prism/src/parser/ast/ModulesFile.java
+++ b/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.
+ *
+ * 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.
+ *
+ * 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();
}
diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java
index 050bf4aa..27178f77 100644
--- a/prism/src/parser/ast/PropertiesFile.java
+++ b/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()}.
+ *
+ * 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()}.
+ *
+ * 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()}.
+ *
+ * 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()}.
+ *
+ * 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
}
diff --git a/prism/src/prism/ModelInfo.java b/prism/src/prism/ModelInfo.java
index aab27378..e69b5250 100644
--- a/prism/src/prism/ModelInfo.java
+++ b/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()}.
+ *
+ * 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()}.
+ *
+ * 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)}.
diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
index 5267a590..9aa6f2f1 100644
--- a/prism/src/prism/Prism.java
+++ b/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).
+ *
+ * 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
diff --git a/prism/src/simulator/ModulesFileModelGenerator.java b/prism/src/simulator/ModulesFileModelGenerator.java
index 4e70b8a7..7cd5153a 100644
--- a/prism/src/simulator/ModulesFileModelGenerator.java
+++ b/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();
}
diff --git a/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java b/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java
index d8da5ca1..69c9907e 100644
--- a/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java
+++ b/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();
}