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