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:
*
+ * - {@link #isPropertyOKForSimulation}
*
- {@link #checkPropertyForSimulation}
*
- {@link #modelCheckSingleProperty}
*
- {@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();
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()