Add option (switch -exact from command-line) to enable exact model checking via parametric model checking.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9388 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/prism/Prism.java

@@ -2719,6 +2719,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 			return modelCheckPTA(propertiesFile, prop.getExpression(), definedPFConstants);
 		}
 
+		// For exact model checking
+		if (settings.getBoolean(PrismSettings.PRISM_EXACT_ENABLED)) {
+			return modelCheckExact(propertiesFile, prop);
+		}
 		// For fast adaptive uniformisation
 		if (currentModelType == ModelType.CTMC && settings.getString(PrismSettings.PRISM_TRANSIENT_METHOD).equals("Fast adaptive uniformisation")) {
 			FastAdaptiveUniformisationModelChecker fauMC;
@@ -2965,15 +2969,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		if (!(currentModelType == ModelType.DTMC || currentModelType == ModelType.CTMC || currentModelType == ModelType.MDP))
 			throw new PrismException("Exact model checking is only supported for DTMCs, CTMCs and MDPs");
 
-		// Print info
-		mainLog.printSeparator();
-		mainLog.println("\nExact model checking: " + prop);
-		if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0)
-			mainLog.println("Model constants: " + currentDefinedMFConstants);
-		Values definedPFConstants = propertiesFile.getConstantValues();
-		if (definedPFConstants != null && definedPFConstants.getNumValues() > 0)
-			mainLog.println("Property constants: " + definedPFConstants);
-
 		// Set up a dummy parameter (not used)
 		String[] paramNames = new String[] { "dummy" };
 		String[] paramLowerBounds = new String[] { "0" };

prism/src/prism/PrismSettings.java

@@ -109,6 +109,8 @@ public class PrismSettings implements Observer
 	public static final	String PRISM_PARETO_EPSILON					= "prism.paretoEpsilon";
 	public static final	String PRISM_EXPORT_PARETO_FILENAME			= "prism.exportParetoFileName";
 	
+	public static final	String PRISM_EXACT_ENABLED					= "prism.exact.enabled";
+	
 	public static final	String PRISM_PARAM_ENABLED					= "prism.param.enabled";
 	public static final	String PRISM_PARAM_PRECISION				= "prism.param.precision";
 	public static final	String PRISM_PARAM_SPLIT					= "prism.param.split";
@@ -293,6 +295,10 @@ public class PrismSettings implements Observer
 			{ STRING_TYPE,		PRISM_EXPORT_ADV_FILENAME,				"Adversary export filename",			"3.3",			"adv.tra",																	"",															
 																			"Name of file for MDP adversary export (if enabled)" },
 																		
+			// EXACT MODEL CHECKING
+			{ BOOLEAN_TYPE,		PRISM_EXACT_ENABLED,					"Do exact model checking",			"4.2.1",			new Boolean(false),															"",
+																			"Perform exact model checking." },
+			
 			// PARAMETRIC MODEL CHECKING
 			{ BOOLEAN_TYPE,		PRISM_PARAM_ENABLED,					"Do parametric model checking",			"4.1",			new Boolean(false),															"",
 																			"Perform parametric model checking." },
@@ -1213,6 +1219,12 @@ public class PrismSettings implements Observer
 			}
 		}
 		
+		// EXACT MODEL CHECKING:
+		
+		else if (sw.equals("exact")) {
+			set(PRISM_EXACT_ENABLED, true);
+		}
+		
 		// PARAMETRIC MODEL CHECKING:
 		
 		else if (sw.equals("param")) {

prism/src/userinterface/graph/GraphResultListener.java

@@ -28,6 +28,7 @@
 
 package userinterface.graph;
 
+import param.BigRational;
 import parser.*;
 import prism.*;
 
@@ -80,6 +81,8 @@ public class GraphResultListener implements ResultListener
 				x = ((Integer)xObj).intValue(); // Use integer value.  	
 			} else if(xObj instanceof Double) {
 				x = ((Double)xObj).doubleValue(); // Use double value.
+			} else if(xObj instanceof BigRational) {
+				x = ((BigRational)xObj).doubleValue(); // Use double value.
 			} else return; // Cancel if non integer/double			
 			
 			// Cancel if x = +/- infinity or NaN
@@ -93,6 +96,9 @@ public class GraphResultListener implements ResultListener
 			} else if (result instanceof Integer) {
 				y = ((Integer) result).intValue();
 				graph.addPointToSeries(seriesKey, new XYDataItem(x, y));
+			} else if (result instanceof BigRational) {
+				y = ((BigRational) result).doubleValue();
+				graph.addPointToSeries(seriesKey, new XYDataItem(x, y));
 			} else if (result instanceof Interval) {
 				Interval interval = (Interval) result;
 				if (interval.lower instanceof Double) {

prism/src/userinterface/properties/GUIProperty.java

@@ -34,6 +34,7 @@ import java.util.Vector;
 import javax.swing.*;
 
 import userinterface.GUIPrism;
+import param.BigRational;
 import parser.*;
 import parser.ast.*;
 import parser.type.TypeVoid;
@@ -318,6 +319,8 @@ public class GUIProperty
 			setStatus(STATUS_RESULT_NUMBER);
 		} else if (result.getResult() instanceof Double) {
 			setStatus(STATUS_RESULT_NUMBER);
+		} else if (result.getResult() instanceof BigRational) {
+			setStatus(STATUS_RESULT_NUMBER);
 		} else if (result.getResult() instanceof Interval) {
 			setStatus(STATUS_RESULT_NUMBER);
 		} else if (result.getResult() instanceof Exception) {