Prism.modelCheck() takes Property rather than Expression objects, and thus displays property names when model checking.

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

prism/src/prism/Prism.java

@@ -2233,24 +2233,34 @@ public class Prism implements PrismSettingsListener
 	 * @param expr The property to check
 	 */
 	public Result modelCheck(PropertiesFile propertiesFile, Expression expr) throws PrismException, PrismLangException
+	{
+		return modelCheck(propertiesFile, new Property(expr));
+	}
+	
+	/**
+	 * Perform model checking of a property on the currently loaded model and return result.
+	 * @param propertiesFile Parent property file of property (for labels/constants/...)
+	 * @param expr The property to check
+	 */
+	public Result modelCheck(PropertiesFile propertiesFile, Property prop) throws PrismException, PrismLangException
 	{
 		Result res = null;
 		Values definedPFConstants = propertiesFile.getConstantValues();
 
 		if (!digital)
 			mainLog.printSeparator();
-		mainLog.println("\nModel checking: " + expr);
+		mainLog.println("\nModel checking: " + prop);
 		if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0)
 			mainLog.println("Model constants: " + currentDefinedMFConstants);
 		if (definedPFConstants != null && definedPFConstants.getNumValues() > 0)
 			mainLog.println("Property constants: " + definedPFConstants);
 
 		// Check that property is valid for the current model type
-		expr.checkValid(currentModelType);
+		prop.getExpression().checkValid(currentModelType);
 
 		// For PTAs...
 		if (currentModelType == ModelType.PTA) {
-			return modelCheckPTA(propertiesFile, expr, definedPFConstants);
+			return modelCheckPTA(propertiesFile, prop.getExpression(), definedPFConstants);
 		}
 
 		// Build model, if necessary
@@ -2272,7 +2282,7 @@ public class Prism implements PrismSettingsListener
 			default:
 				throw new PrismException("Unknown model type " + currentModelType);
 			}
-			res = mc.check(expr);
+			res = mc.check(prop.getExpression());
 		} else {
 			explicit.StateModelChecker mc = null;
 			switch (currentModelType) {
@@ -2297,7 +2307,7 @@ public class Prism implements PrismSettingsListener
 			mc.setLog(mainLog);
 			mc.setSettings(settings);
 			mc.setModulesFileAndPropertiesFile(currentModulesFile, propertiesFile);
-			res = mc.check(currentModelExpl, expr);
+			res = mc.check(currentModelExpl, prop.getExpression());
 		}
 
 		// Return result

prism/src/prism/PrismCL.java

@@ -282,7 +282,7 @@ public class PrismCL implements PrismModelListener
 							}
 							// Normal model checking
 							if (!simulate) {
-								res = prism.modelCheck(propertiesFile, propertiesToCheck.get(j).getExpression());
+								res = prism.modelCheck(propertiesFile, propertiesToCheck.get(j));
 							}
 							// Approximate (simulation-based) model checking
 							else {

prism/src/prism/PrismTest.java

@@ -65,12 +65,12 @@ public class PrismTest
 			
 			// Parse a prop, check on model 1
 			propertiesFile = prism.parsePropertiesString(modulesFile, "P=?[F<=0.1 s1=1]");
-			result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(0));
+			result = prism.modelCheck(propertiesFile, propertiesFile.getPropertyObject(0));
 			System.out.println(result.getResult());
 			
 			// Parse another prop, check on model 1
 			propertiesFile = prism.parsePropertiesString(modulesFile, "P=?[F<=0.1 s1=1]");
-			result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(0));
+			result = prism.modelCheck(propertiesFile, propertiesFile.getPropertyObject(0));
 			System.out.println(result.getResult());
 			
 			// Parse/load model 2
@@ -79,7 +79,7 @@ public class PrismTest
 			
 			// Parse a prop, check on model 2
 			propertiesFile = prism.parsePropertiesString(modulesFile, "P=?[F<=0.1 s1=1]");
-			result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(0));
+			result = prism.modelCheck(propertiesFile, propertiesFile.getPropertyObject(0));
 			System.out.println(result.getResult());
 			
 			// Close down

prism/src/userinterface/properties/GUIExperiment.java

@@ -204,7 +204,7 @@ public class GUIExperiment
 		{
 			int i, k;
 			int propertyIndex = propertiesFile.getNumProperties() - 1;
-			Expression propertyToCheck = propertiesFile.getProperty(propertyIndex);
+			Property propertyToCheck = propertiesFile.getPropertyObject(propertyIndex);
 			SimulationInformation info = null;
 			boolean reuseInfo = false, reuseInfoAsked = false;
 
@@ -242,7 +242,7 @@ public class GUIExperiment
 					if (useSimulation && !reuseInfo) {
 						try {
 							info = null;
-							info = GUISimulationPicker.defineSimulationWithDialog(guiProp.getGUI(), propertyToCheck, prism.getPRISMModel(), "("
+							info = GUISimulationPicker.defineSimulationWithDialog(guiProp.getGUI(), propertyToCheck.getExpression(), prism.getPRISMModel(), "("
 									+ definedMFConstants + ")");
 						} catch (PrismException e) {
 							// in case of error, report it (in log only), store as result, and go on to the next model
@@ -279,7 +279,7 @@ public class GUIExperiment
 								initialState = new parser.State(info.getInitialState(), prism.getPRISMModel());
 							}
 							// do simulation
-							prism.modelCheckSimulatorExperiment(propertiesFile, undefinedConstants, results, propertyToCheck, initialState,
+							prism.modelCheckSimulatorExperiment(propertiesFile, undefinedConstants, results, propertyToCheck.getExpression(), initialState,
 									info.getMaxPathLength(), info.createSimulationMethod());
 							// update progress meter
 							// (all properties simulated simultaneously so can't get more accurate feedback at the moment anyway)
@@ -319,8 +319,8 @@ public class GUIExperiment
 										initialState = new parser.State(info.getInitialState(), prism.getPRISMModel());
 									}
 									// do simulation
-									res = prism.modelCheckSimulator(propertiesFile, propertyToCheck, definedPFConstants, initialState, info.getMaxPathLength(),
-											info.createSimulationMethod());
+									res = prism.modelCheckSimulator(propertiesFile, propertyToCheck.getExpression(), definedPFConstants, initialState,
+											info.getMaxPathLength(), info.createSimulationMethod());
 								}
 							} catch (PrismException e) {
 								// in case of error, report it (in log only), store exception as the result and proceed

prism/src/userinterface/properties/computation/ModelCheckThread.java

@@ -103,7 +103,7 @@ public class ModelCheckThread extends GUIComputationThread
 
 			// Do model checking
 			try {
-				result = prism.modelCheck(propertiesFile, propertiesFile.getProperty(i));
+				result = prism.modelCheck(propertiesFile, propertiesFile.getPropertyObject(i));
 			} catch (PrismException e) {
 				result = new Result(e);
 				error(e.getMessage());