Better handling of errors in simulator calls from GUI.

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

prism/src/simulator/GenerateSimulationPath.java

@@ -463,7 +463,8 @@ public class GenerateSimulationPath
 			try {
 				generateAndPlotSimulationPath(modulesFile, initialState, details, maxPathLength, graphModel);
 			} catch (PrismException e) {
-				// Just ignore problems
+				// Just report errors passively to log
+				mainLog.printWarning("Error occured during path plot: " + e.getMessage());
 			}
 		}
 	}

prism/src/simulator/SimulatorEngine.java

@@ -169,6 +169,22 @@ public class SimulatorEngine
 	// Path creation and modification
 	// ------------------------------------------------------------------------------
 
+	/**
+	 * Check whether a model is suitable for exploration/analysis using the simulator.
+	 * If not, an explanatory error message is thrown as an exception.
+	 */
+	public void checkModelForSimulation(ModulesFile modulesFile) throws PrismException
+	{
+		// No support for PTAs yet
+		if (modulesFile.getModelType() == ModelType.PTA) {
+			throw new PrismException("Sorry - the simulator does not currently support PTAs");
+		}
+		// No support for system...endsystem yet
+		if (modulesFile.getSystemDefn() != null) {
+			throw new PrismException("Sorry - the simulator does not currently handle the system...endsystem construct");
+		}
+	}
+	
 	/**
 	 * Create a new path for a model.
 	 * Note: All constants in the model must have already been defined.
@@ -644,15 +660,8 @@ public class SimulatorEngine
 		modelType = modulesFile.getModelType();
 		this.mfConstants = modulesFile.getConstantValues();
 
-		// Check for PTAs
-		if (modulesFile.getModelType() == ModelType.PTA) {
-			throw new PrismException("Sorry - the simulator does not currently support PTAs");
-		}
-
-		// Check for presence of system...endsystem
-		if (modulesFile.getSystemDefn() != null) {
-			throw new PrismException("Sorry - the simulator does not currently handle the system...endsystem construct");
-		}
+		// Check model is simulate-able
+		checkModelForSimulation(modulesFile);
 
 		// Get variable list (symbol table) for model 
 		varList = modulesFile.createVarList();

prism/src/userinterface/simulator/GUISimulator.java

@@ -318,6 +318,10 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 	{
 		Values initialState;
 		try {
+			// Check model is simulate-able
+			// (bail out now else causes problems below)
+			engine.checkModelForSimulation(parsedModel);
+			
 			// get properties constants/labels
 			PropertiesFile pf;
 			try {
@@ -693,6 +697,10 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 	{
 		Values initialState;
 		try {
+			// Check model is simulate-able
+			// (bail out now else causes problems below)
+			engine.checkModelForSimulation(parsedModel);
+			
 			// if necessary, get values for undefined constants from user
 			UndefinedConstants uCon = new UndefinedConstants(parsedModel, null);
 			if (uCon.getMFNumUndefined() > 0) {
@@ -705,12 +713,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 			// store constants
 			parsedModel.setUndefinedConstants(lastConstants);
 
-			// check here for possibility of multiple initial states
-			// (not supported yet) to avoid problems below
-			if (parsedModel.getInitialStates() != null) {
-				throw new PrismException("The simulator does not not yet handle models with multiple states");
-			}
-
 			// do we need to ask for an initial state for simulation?
 			// no: just use default/random
 			if (!chooseInitialState) {