From ead22700e86c63b9e16c6f8d35c97ca626044f70 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 28 Feb 2012 10:46:09 +0000
Subject: [PATCH] New SimulatorEngine/Prism method
 prism.isPropertyOKForSimulation().

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4741 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/Prism.java                    |  9 ++++
 prism/src/simulator/SimulatorEngine.java      | 42 +++++++++++++++----
 .../properties/GUIMultiProperties.java        |  5 +--
 .../userinterface/properties/GUIProperty.java |  9 +---
 4 files changed, 45 insertions(+), 20 deletions(-)

diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
index a76623e6..ea556278 100644
--- a/prism/src/prism/Prism.java
+++ b/prism/src/prism/Prism.java
@@ -2372,6 +2372,15 @@ public class Prism implements PrismSettingsListener
 		}
 	}
 
+	/**
+	 * Check whether a property is suitable for approximate model checking using the simulator.
+	 * @param expr The property to check.
+	 */
+	public boolean isPropertyOKForSimulation(Expression expr)
+	{
+		return getSimulator().isPropertyOKForSimulation(expr);
+	}
+	
 	/**
 	 * Check if a property is suitable for analysis with the simulator.
 	 * If not, an explanatory exception is thrown.
diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java
index d41e85b7..8219bfcf 100644
--- a/prism/src/simulator/SimulatorEngine.java
+++ b/prism/src/simulator/SimulatorEngine.java
@@ -67,6 +67,7 @@ import prism.*;
  * 
  * For sampling-based approximate model checking, use:
  * <UL>
+ * <LI> {@link #isPropertyOKForSimulation}
  * <LI> {@link #checkPropertyForSimulation}
  * <LI> {@link #modelCheckSingleProperty}
  * <LI> {@link #modelCheckMultipleProperties}
@@ -1196,24 +1197,49 @@ public class SimulatorEngine
 	// Model checking (approximate)
 	// ------------------------------------------------------------------------------
 
+	/**
+	 * Check whether a property is suitable for approximate model checking using the simulator.
+	 */
+	public boolean isPropertyOKForSimulation(Expression expr)
+	{
+		return isPropertyOKForSimulationString(expr) == null;
+	}
+	
 	/**
 	 * Check whether a property is suitable for approximate model checking using the simulator.
 	 * If not, an explanatory error message is thrown as an exception.
 	 */
-	public void checkPropertyForSimulation(Expression prop) throws PrismException
+	public void checkPropertyForSimulation(Expression expr) throws PrismException
+	{
+		String errMsg = isPropertyOKForSimulationString(expr);
+		if (errMsg != null)
+			throw new PrismException(errMsg);
+	}
+	
+	/**
+	 * Check whether a property is suitable for approximate model checking using the simulator.
+	 * If yes, return null; if not, return an explanatory error message.
+	 */
+	private String isPropertyOKForSimulationString(Expression expr)
 	{
 		// Simulator can only be applied to P or R properties (without filters)
-		if (!(prop instanceof ExpressionProb || prop instanceof ExpressionReward)) {
-			if (prop instanceof ExpressionFilter) {
-				if (((ExpressionFilter) prop).getOperand() instanceof ExpressionProb || ((ExpressionFilter) prop).getOperand() instanceof ExpressionReward)
-					throw new PrismException("Simulator cannot handle P or R properties with filters");
+		if (!(expr instanceof ExpressionProb || expr instanceof ExpressionReward)) {
+			if (expr instanceof ExpressionFilter) {
+				if (((ExpressionFilter) expr).getOperand() instanceof ExpressionProb || ((ExpressionFilter) expr).getOperand() instanceof ExpressionReward)
+					return "Simulator cannot handle P or R properties with filters";
 			}
-			throw new PrismException("Simulator can only handle P or R properties");
+			return "Simulator can only handle P or R properties";
 		}
 		// Check that there are no nested probabilistic operators
-		if (prop.computeProbNesting() > 1) {
-			throw new PrismException("Simulator cannot handle nested P, R or S operators");
+		try {
+			if (expr.computeProbNesting() > 1) {
+				return "Simulator cannot handle nested P, R or S operators";
+			}
+		} catch (PrismException e) {
+			return "Simulator cannot handle this property: " + e.getMessage();
 		}
+		// No errors
+		return null;
 	}
 
 	/**
diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java
index 15c21f78..95b463e0 100644
--- a/prism/src/userinterface/properties/GUIMultiProperties.java
+++ b/prism/src/userinterface/properties/GUIMultiProperties.java
@@ -309,13 +309,10 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List
 		simulatableExprs = new ArrayList<Expression>();
 		for (int i = 0; i < validGUIProperties.size(); i++) {
 			GUIProperty guiP = validGUIProperties.get(i);
-			try {
-				getPrism().checkPropertyForSimulation(guiP.getProperty());
+			if (getPrism().isPropertyOKForSimulation(guiP.getProperty())) {
 				simulatableGUIProperties.add(guiP);
 				simulatableProperties.add(parsedProperties.getPropertyObject(i));
 				simulatableExprs.add(guiP.getProperty());
-			} catch (PrismException e) {
-				// do nothing
 			}
 		}
 		if (simulatableGUIProperties.size() == 0) {
diff --git a/prism/src/userinterface/properties/GUIProperty.java b/prism/src/userinterface/properties/GUIProperty.java
index 3baf8278..0c332a26 100644
--- a/prism/src/userinterface/properties/GUIProperty.java
+++ b/prism/src/userinterface/properties/GUIProperty.java
@@ -220,14 +220,7 @@ public class GUIProperty
 	 */
 	public boolean isValidForSimulation()
 	{
-		if (!isValid())
-			return false;
-		try {
-			prism.checkPropertyForSimulation(expr);
-		} catch (PrismException e) {
-			return false;
-		}
-		return true;
+		return isValid() && prism.isPropertyOKForSimulation(expr);
 	}
 
 	public Result getResult()