From 6c0294923ec565bc8900e6c8051842367db7fc07 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 23 Mar 2018 14:55:40 +0100 Subject: [PATCH] Use exact evaluation of constant expressions in exact and parametric mode Using the infrastructure from the previous commit, we request exact evaluation of constants in exact and parametric model checking mode. Additionally, note where we deliberately choose non-exact evaluation mode. Add corresponding test cases. --- .../verify/exact/exact-const-1.prism | 13 +++++++++++++ .../verify/exact/exact-const-1.prism.props | 11 +++++++++++ .../exact/exact-const-1.prism.props.args | 3 +++ .../verify/exact/exact-const-2.prism | 13 +++++++++++++ .../verify/exact/exact-const-2.prism.props | 11 +++++++++++ .../exact/exact-const-2.prism.props.args | 2 ++ .../verify/exact/exact-eval-1.prism | 13 +++++++++++++ .../verify/exact/exact-eval-1.prism.props | 5 +++++ .../exact/exact-eval-1.prism.props.args | 2 ++ .../verify/exact/exact-literal.prism | 15 +++++++++++++++ .../exact/exact-literal.prism.exact.props | 6 ++++++ .../exact-literal.prism.exact.props.args | 1 + prism/src/parser/ast/ModulesFile.java | 4 +++- prism/src/parser/ast/PropertiesFile.java | 7 +++++-- prism/src/prism/Prism.java | 3 ++- prism/src/prism/PrismCL.java | 12 +++++++++--- prism/src/simulator/SimulatorEngine.java | 3 ++- .../model/GUIMultiModelHandler.java | 12 ++++++++---- .../properties/GUIExperiment.java | 9 +++++++-- .../properties/GUIMultiProperties.java | 19 +++++++++++++------ .../userinterface/simulator/GUISimulator.java | 10 +++++----- 21 files changed, 149 insertions(+), 25 deletions(-) create mode 100644 prism-tests/functionality/verify/exact/exact-const-1.prism create mode 100644 prism-tests/functionality/verify/exact/exact-const-1.prism.props create mode 100644 prism-tests/functionality/verify/exact/exact-const-1.prism.props.args create mode 100644 prism-tests/functionality/verify/exact/exact-const-2.prism create mode 100644 prism-tests/functionality/verify/exact/exact-const-2.prism.props create mode 100644 prism-tests/functionality/verify/exact/exact-const-2.prism.props.args create mode 100644 prism-tests/functionality/verify/exact/exact-eval-1.prism create mode 100644 prism-tests/functionality/verify/exact/exact-eval-1.prism.props create mode 100644 prism-tests/functionality/verify/exact/exact-eval-1.prism.props.args create mode 100644 prism-tests/functionality/verify/exact/exact-literal.prism create mode 100644 prism-tests/functionality/verify/exact/exact-literal.prism.exact.props create mode 100644 prism-tests/functionality/verify/exact/exact-literal.prism.exact.props.args diff --git a/prism-tests/functionality/verify/exact/exact-const-1.prism b/prism-tests/functionality/verify/exact/exact-const-1.prism new file mode 100644 index 00000000..e7fd1ca0 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-const-1.prism @@ -0,0 +1,13 @@ +// test case for setting exact external constants + +dtmc + +const double p; +const double x; // dummy for parametric + +module M1 + s: [0..2] init 0; + + [] s=0 -> p:(s'=1) + 1-p:(s'=2); + [] s>=1 -> true; +endmodule diff --git a/prism-tests/functionality/verify/exact/exact-const-1.prism.props b/prism-tests/functionality/verify/exact/exact-const-1.prism.props new file mode 100644 index 00000000..b5cf34ea --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-const-1.prism.props @@ -0,0 +1,11 @@ +// RESULT: 1/3 +P=?[ F s=1 ] + +// RESULT: false +P>1/3[ F s=1 ] + +// RESULT: true +P>=1/3[ F s=1 ] + +// RESULT: false +P<1/3[ F s=1 ] diff --git a/prism-tests/functionality/verify/exact/exact-const-1.prism.props.args b/prism-tests/functionality/verify/exact/exact-const-1.prism.props.args new file mode 100644 index 00000000..3ea357a9 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-const-1.prism.props.args @@ -0,0 +1,3 @@ +-const p=1/3,x=0 -exact +-const p=1/3 -param x=0:1 +-const p=1/1/3,x=0 -exact diff --git a/prism-tests/functionality/verify/exact/exact-const-2.prism b/prism-tests/functionality/verify/exact/exact-const-2.prism new file mode 100644 index 00000000..1f9fb878 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-const-2.prism @@ -0,0 +1,13 @@ +// test case for exact constant evaluation + +dtmc + +const double p = 1/3; +const double x; // dummy for parametric + +module M1 + s: [0..2] init 0; + + [] s=0 -> p:(s'=1) + 1-p:(s'=2); + [] s>=1 -> true; +endmodule diff --git a/prism-tests/functionality/verify/exact/exact-const-2.prism.props b/prism-tests/functionality/verify/exact/exact-const-2.prism.props new file mode 100644 index 00000000..b5cf34ea --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-const-2.prism.props @@ -0,0 +1,11 @@ +// RESULT: 1/3 +P=?[ F s=1 ] + +// RESULT: false +P>1/3[ F s=1 ] + +// RESULT: true +P>=1/3[ F s=1 ] + +// RESULT: false +P<1/3[ F s=1 ] diff --git a/prism-tests/functionality/verify/exact/exact-const-2.prism.props.args b/prism-tests/functionality/verify/exact/exact-const-2.prism.props.args new file mode 100644 index 00000000..7bea457c --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-const-2.prism.props.args @@ -0,0 +1,2 @@ +-const x=0 -exact +-param x=0:1 diff --git a/prism-tests/functionality/verify/exact/exact-eval-1.prism b/prism-tests/functionality/verify/exact/exact-eval-1.prism new file mode 100644 index 00000000..c846f44f --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-eval-1.prism @@ -0,0 +1,13 @@ +// test case, check if double constants are evaluated exactly in exact / parametric mode + +dtmc + +const double p = (1/3 = 0.333333333333333333333333 ? 1/2 : 0); +const double x; // dummy for parametric + +module M1 + s: [0..2] init 0; + + [] s=0 -> p:(s'=1) + 1-p:(s'=2); + [] s>=1 -> true; +endmodule diff --git a/prism-tests/functionality/verify/exact/exact-eval-1.prism.props b/prism-tests/functionality/verify/exact/exact-eval-1.prism.props new file mode 100644 index 00000000..2ae9248a --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-eval-1.prism.props @@ -0,0 +1,5 @@ +// RESULT: 0 +P=?[ F s=1 ] + +// RESULT: false +P>0[ F s=1 ] diff --git a/prism-tests/functionality/verify/exact/exact-eval-1.prism.props.args b/prism-tests/functionality/verify/exact/exact-eval-1.prism.props.args new file mode 100644 index 00000000..3ef43ee0 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-eval-1.prism.props.args @@ -0,0 +1,2 @@ +-exact -const x=0 +-param x=0:1 diff --git a/prism-tests/functionality/verify/exact/exact-literal.prism b/prism-tests/functionality/verify/exact/exact-literal.prism new file mode 100644 index 00000000..586457e1 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-literal.prism @@ -0,0 +1,15 @@ +// test case for exact handling of floating point literals + +dtmc + +// in exact mode, this literal should be kept with full precision +// and not be approximated by 0.5, which would happen if it's converted to a double first +const double p = 0.500000000000000000000000000000001; + +const double x; // dummy, for parametric mode + +module M1 + s: [0..2] init 0; + + [] s=0 -> p:(s'=1) + (1-p):(s'=2); +endmodule diff --git a/prism-tests/functionality/verify/exact/exact-literal.prism.exact.props b/prism-tests/functionality/verify/exact/exact-literal.prism.exact.props new file mode 100644 index 00000000..555d24c4 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-literal.prism.exact.props @@ -0,0 +1,6 @@ +// RESULT: 500000000000000000000000000000001/1000000000000000000000000000000000 +P=?[ F s=1 ] + +// RESULT: true +P>1/2[ F s=1 ] + diff --git a/prism-tests/functionality/verify/exact/exact-literal.prism.exact.props.args b/prism-tests/functionality/verify/exact/exact-literal.prism.exact.props.args new file mode 100644 index 00000000..60f9ca93 --- /dev/null +++ b/prism-tests/functionality/verify/exact/exact-literal.prism.exact.props.args @@ -0,0 +1 @@ +--exact --const x=0 diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 91f2f956..7e2bc2f7 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -686,7 +686,9 @@ public class ModulesFile extends ASTElement implements ModelInfo // NB: Can't call setUndefinedConstants if there are undefined constants // because semanticCheckAfterConstants may fail. if (getUndefinedConstants().isEmpty()) { - setUndefinedConstants(null); + // we use non-exact constant evaluation by default, + // for exact mode constants will be reevaluated later on + setUndefinedConstants(null, false); } } diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index 27178f77..5d0a46d1 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/prism/src/parser/ast/PropertiesFile.java @@ -305,7 +305,10 @@ public class PropertiesFile extends ASTElement // Set up some values for constants // (without assuming any info about undefined constants) - setSomeUndefinedConstants(null); + // + // we use non-exact constant evaluation by default, + // for exact mode constants will be reevaluated later on + setSomeUndefinedConstants(null, false); } // check formula identifiers @@ -532,7 +535,7 @@ public class PropertiesFile extends ASTElement * 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()}. *
* Constant values are evaluated using standard (integer, floating-point) arithmetic. */ diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 9aa6f2f1..380dfc77 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2991,7 +2991,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener DigitalClocks dc = new DigitalClocks(this); dc.translate(oldModulesFile, propertiesFile, expr); currentModulesFile = dc.getNewModulesFile(); - currentModulesFile.setUndefinedConstants(oldModulesFile.getConstantValues()); + // evaluate constants (use exact evaluation if we are in exact computation mode) + currentModulesFile.setUndefinedConstants(oldModulesFile.getConstantValues(), settings.getBoolean(PrismSettings.PRISM_EXACT_ENABLED)); currentModelType = ModelType.MDP; currentModelGenerator = new ModulesFileModelGenerator(currentModulesFile, this); clearBuiltModel(); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 67a552dc..98a808e2 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -201,6 +201,7 @@ public class PrismCL implements PrismModelListener private String[] paramUpperBounds = null; private String[] paramNames = null; + private boolean exactConstants = false; /** * Entry point: call run method, catch CuddOutOfMemoryException @@ -252,6 +253,9 @@ public class PrismCL implements PrismModelListener errorAndExit("Parametric model checking requires at least one property to check"); } + // evaluate constants exactly if we are in param or exact computation mode + exactConstants = param || prism.getSettings().getBoolean(PrismSettings.PRISM_EXACT_ENABLED); + // process info about undefined constants try { // first, see which constants are undefined @@ -260,9 +264,11 @@ public class PrismCL implements PrismModelListener undefinedMFConstants = new UndefinedConstants(modulesFile, propertiesFile, true); else undefinedMFConstants = new UndefinedConstants(modulesFile, null); + undefinedMFConstants.setExactMode(exactConstants); undefinedConstants = new UndefinedConstants[numPropertiesToCheck]; for (i = 0; i < numPropertiesToCheck; i++) { undefinedConstants[i] = new UndefinedConstants(modulesFile, propertiesFile, propertiesToCheck.get(i)); + undefinedConstants[i].setExactMode(exactConstants); } // may need to remove some constants if they are used for parametric methods if (param) { @@ -292,7 +298,7 @@ public class PrismCL implements PrismModelListener // set values for ModulesFile constants try { definedMFConstants = undefinedMFConstants.getMFConstantValues(); - prism.setPRISMModelConstants(definedMFConstants); + prism.setPRISMModelConstants(definedMFConstants, exactConstants); } catch (PrismException e) { // in case of error, report it, store as result for any properties, and go on to the next model // (might happen for example if overflow or another numerical problem is detected at this stage) @@ -366,7 +372,7 @@ public class PrismCL implements PrismModelListener // Set values for PropertiesFile constants if (propertiesFile != null) { definedPFConstants = undefinedConstants[j].getPFConstantValues(); - propertiesFile.setSomeUndefinedConstants(definedPFConstants); + propertiesFile.setSomeUndefinedConstants(definedPFConstants, exactConstants); } // Normal model checking if (!simulate && !param) { @@ -809,7 +815,7 @@ public class PrismCL implements PrismModelListener try { if (propertiesFile != null) { definedPFConstants = undefinedMFConstants.getPFConstantValues(); - propertiesFile.setSomeUndefinedConstants(definedPFConstants); + propertiesFile.setSomeUndefinedConstants(definedPFConstants, exactConstants); } File f = (exportLabelsFilename.equals("stdout")) ? null : new File(exportLabelsFilename); prism.exportLabelsToFile(propertiesFile, exportType, f); diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 38c4bc44..bd3ca88b 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -1608,7 +1608,8 @@ public class SimulatorEngine extends PrismComponent for (int i = 0; i < n; i++) { definedPFConstants = undefinedConstants.getPFConstantValues(); pfcs[i] = definedPFConstants; - propertiesFile.setSomeUndefinedConstants(definedPFConstants); + // for simulation, use non-exact constant evaluation + propertiesFile.setSomeUndefinedConstants(definedPFConstants, false); try { checkPropertyForSimulation(expr); indices[i] = addProperty(expr, propertiesFile); diff --git a/prism/src/userinterface/model/GUIMultiModelHandler.java b/prism/src/userinterface/model/GUIMultiModelHandler.java index 8588c495..3cc90440 100644 --- a/prism/src/userinterface/model/GUIMultiModelHandler.java +++ b/prism/src/userinterface/model/GUIMultiModelHandler.java @@ -627,7 +627,8 @@ public class GUIMultiModelHandler extends JPanel implements PrismModelListener lastMFConstants = unC.getMFConstantValues(); } try { - prism.setPRISMModelConstants(unC.getMFConstantValues()); + // currently, don't evaluate constants exactly + prism.setPRISMModelConstants(unC.getMFConstantValues(), false); } catch (PrismException e) { theModel.error(e.getMessage()); return; @@ -724,7 +725,8 @@ public class GUIMultiModelHandler extends JPanel implements PrismModelListener lastMFConstants = unC.getMFConstantValues(); } try { - prism.setPRISMModelConstants(unC.getMFConstantValues()); + // currently, don't evaluate constants exactly + prism.setPRISMModelConstants(unC.getMFConstantValues(), false); } catch (PrismException e) { theModel.error(e.getMessage()); return; @@ -762,7 +764,8 @@ public class GUIMultiModelHandler extends JPanel implements PrismModelListener lastMFConstants = unC.getMFConstantValues(); } try { - prism.setPRISMModelConstants(unC.getMFConstantValues()); + // for steady-state, currently don't evaluate constants exactly + prism.setPRISMModelConstants(unC.getMFConstantValues(), false); } catch (PrismException e) { theModel.error(e.getMessage()); return; @@ -800,7 +803,8 @@ public class GUIMultiModelHandler extends JPanel implements PrismModelListener lastMFConstants = unC.getMFConstantValues(); } try { - prism.setPRISMModelConstants(unC.getMFConstantValues()); + // for transient computation, currently don't evaluate constants exactly + prism.setPRISMModelConstants(unC.getMFConstantValues(), false); } catch (PrismException e) { theModel.error(e.getMessage()); return; diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java index dcdef5ba..4a78246d 100644 --- a/prism/src/userinterface/properties/GUIExperiment.java +++ b/prism/src/userinterface/properties/GUIExperiment.java @@ -224,12 +224,17 @@ public class GUIExperiment } }); + // are we in exact mode? + boolean exact = prism.getSettings().getBoolean(PrismSettings.PRISM_EXACT_ENABLED); + // for simulation, don't use exact mode... + exact &= !useSimulation; + for (i = 0; i < undefinedConstants.getNumModelIterations(); i++) { // set values for ModulesFile constants try { definedMFConstants = undefinedConstants.getMFConstantValues(); - prism.setPRISMModelConstants(definedMFConstants); + prism.setPRISMModelConstants(definedMFConstants, exact); } catch (Exception e) { // in case of error, report it (in log only), store as result, and go on to the next model errorLog(e); @@ -302,7 +307,7 @@ public class GUIExperiment // Set values for PropertiesFile constants if (propertiesFile != null) { definedPFConstants = undefinedConstants.getPFConstantValues(); - propertiesFile.setSomeUndefinedConstants(definedPFConstants); + propertiesFile.setSomeUndefinedConstants(definedPFConstants, exact); } // Normal model checking if (!useSimulation) { diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index 978a6d04..7b6a44a3 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -269,6 +269,9 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List verifyAfterReceiveParseNotification = false; try { + // are we in exact mode? + boolean exact = getPrism().getSettings().getBoolean(PrismSettings.PRISM_EXACT_ENABLED); + // Get valid/selected properties String propertiesString = getLabelsString() + "\n" + getConstantsString() + "\n" + propList.getValidSelectedAndReferencedString(); // Get PropertiesFile for valid/selected properties @@ -281,6 +284,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List for (int i = 0; i < n; i++) validProperties.add(parsedProperties.getPropertyObject(i)); uCon = new UndefinedConstants(parsedModel, parsedProperties, validProperties); + uCon.setExactMode(exact); if (uCon.getMFNumUndefined() + uCon.getPFNumUndefined() > 0) { // Use previous constant values as defaults in dialog int result = GUIConstantsPicker.defineConstantsWithDialog(this.getGUI(), uCon, mfConstants, pfConstants); @@ -290,8 +294,8 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List // Store model/property constants mfConstants = uCon.getMFConstantValues(); pfConstants = uCon.getPFConstantValues(); - getPrism().setPRISMModelConstants(mfConstants); - parsedProperties.setSomeUndefinedConstants(pfConstants); + getPrism().setPRISMModelConstants(mfConstants, exact); + parsedProperties.setSomeUndefinedConstants(pfConstants, exact); // Store properties to be verified propertiesToBeVerified = validGUIProperties; for (GUIProperty gp : propertiesToBeVerified) @@ -361,8 +365,9 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List // Store model/property constants mfConstants = uCon.getMFConstantValues(); pfConstants = uCon.getPFConstantValues(); - getPrism().setPRISMModelConstants(mfConstants); - parsedProperties.setSomeUndefinedConstants(pfConstants); + // currently, evaluate constants non-exact for simulation + getPrism().setPRISMModelConstants(mfConstants, false); + parsedProperties.setSomeUndefinedConstants(pfConstants, false); for (GUIProperty gp : simulatableGUIProperties) gp.setConstants(mfConstants, pfConstants); @@ -433,6 +438,7 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List // sort out undefined constants UndefinedConstants uCon = new UndefinedConstants(parsedModel, parsedProperties, props); + uCon.setExactMode(getPrism().getSettings().getBoolean(PrismSettings.PRISM_EXACT_ENABLED)); boolean showGraphDialog = false; boolean useSimulation = false; if (uCon.getMFNumUndefined() + uCon.getPFNumUndefined() == 0) { @@ -1131,8 +1137,9 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List // Store model/property constants mfConstants = uCon.getMFConstantValues(); pfConstants = uCon.getPFConstantValues(); - getPrism().setPRISMModelConstants(mfConstants); - parsedProperties.setSomeUndefinedConstants(pfConstants); + // currently, evaluate constants non-exact for model building + getPrism().setPRISMModelConstants(mfConstants, false); + parsedProperties.setSomeUndefinedConstants(pfConstants, false); // If export is being done to log, switch view to log if (exportFile == null) logToFront(); diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index bcd79a16..1b9a4756 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -406,9 +406,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // remember constant values for next time lastConstants = uCon.getMFConstantValues(); lastPropertyConstants = uCon.getPFConstantValues(); - // store constants - parsedModel.setUndefinedConstants(lastConstants); - pf.setSomeUndefinedConstants(lastPropertyConstants); + // store constants (currently, compute non-exact for simulation) + parsedModel.setUndefinedConstants(lastConstants, false); + pf.setSomeUndefinedConstants(lastPropertyConstants, false); // check here for possibility of multiple initial states // (not supported yet) to avoid problems below @@ -782,8 +782,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } // remember constant values for next time lastConstants = uCon.getMFConstantValues(); - // store constants - parsedModel.setUndefinedConstants(lastConstants); + // store constants (currently, compute non-exact for simulation) + parsedModel.setUndefinedConstants(lastConstants, false); // do we need to ask for an initial state for simulation? // no: just use default/random