From bae541523cc040d7b83daf4d39cfd1dfded8b99d Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 23 Mar 2018 14:53:10 +0100 Subject: [PATCH] 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 | 61 ++++++++++++++++--- prism/src/parser/ast/ModulesFile.java | 31 ++++++++-- prism/src/parser/ast/PropertiesFile.java | 36 ++++++++++- prism/src/prism/ModelInfo.java | 24 ++++++++ prism/src/prism/Prism.java | 30 +++++++-- .../simulator/ModulesFileModelGenerator.java | 10 ++- .../ModulesFileModelGeneratorSymbolic.java | 10 ++- 7 files changed, 177 insertions(+), 25 deletions(-) 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(); }