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.

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

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 ]

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

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

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 ]

prism-tests/functionality/verify/exact/exact-const-2.prism.props.args

@@ -0,0 +1,2 @@
+-const x=0 -exact
+-param x=0:1

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

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 ]

prism-tests/functionality/verify/exact/exact-eval-1.prism.props.args

@@ -0,0 +1,2 @@
+-exact -const x=0
+-param x=0:1

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

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 ]
+

prism-tests/functionality/verify/exact/exact-literal.prism.exact.props.args

@@ -0,0 +1 @@
+--exact --const x=0

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);
 		}
 	}
 

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()}.
 	 * <br>
 	 * Constant values are evaluated using standard (integer, floating-point) arithmetic.
 	 */

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();

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);

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);

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;

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) {

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();

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