Move path plot thread to GUI to allow display of warnings/errors.

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

prism/src/simulator/GenerateSimulationPath.java

@@ -28,10 +28,14 @@ package simulator;
 
 import java.io.File;
 import java.util.ArrayList;
-
-import prism.*;
-import parser.*;
-import parser.ast.*;
+import java.util.List;
+
+import parser.State;
+import parser.VarList;
+import parser.ast.ModulesFile;
+import prism.PrismException;
+import prism.PrismFileLog;
+import prism.PrismLog;
 import userinterface.graph.Graph;
 
 public class GenerateSimulationPath
@@ -39,6 +43,9 @@ public class GenerateSimulationPath
 	// The simulator engine and a log for output
 	private SimulatorEngine engine;
 	private PrismLog mainLog;
+	
+	// Store warnings
+	private List<String> warnings = new ArrayList<String>();
 
 	// Enums
 	private enum PathType {
@@ -64,6 +71,26 @@ public class GenerateSimulationPath
 	private boolean simPathSnapshots = false;
 	private double simPathSnapshotTime = 0.0;
 
+	public int getNumWarnings()
+	{
+		return warnings.size();
+	}
+	
+	public List<String> getWarnings()
+	{
+		return warnings;
+	}
+	
+	/**
+	 * Send a warning messages to the log;
+	 * also, store a copy for later retrieval.
+	 */
+	private void warning(String msg)
+	{
+		mainLog.printWarning(msg + ".");
+		warnings.add(msg);
+	}
+	
 	public GenerateSimulationPath(SimulatorEngine engine, PrismLog mainLog)
 	{
 		this.engine = engine;
@@ -83,6 +110,7 @@ public class GenerateSimulationPath
 		this.initialState = initialState;
 		this.maxPathLength = maxPathLength;
 		this.file = file;
+		warnings.clear();
 
 		parseDetails(details);
 		PathDisplayer displayer = generateDisplayerForExport();
@@ -367,10 +395,10 @@ public class GenerateSimulationPath
 
 		// Display warnings if needed
 		if (simLoopCheck && engine.isPathLooping()) {
-			mainLog.printWarning("Deterministic loop detected after " + engine.getPathSize() + " steps (use loopcheck=false option to extend path).");
+			warning("Deterministic loop detected after " + engine.getPathSize() + " steps (use loopcheck=false option to extend path)");
 		}
 		if (simPathType == PathType.SIM_PATH_TIME && path.getTotalTime() < simPathTime) {
-			mainLog.printWarning("Path terminated before time " + simPathTime + " because maximum path length (" + maxPathLength + ") was reached.");
+			warning("Path terminated before time " + simPathTime + " because maximum path length (" + maxPathLength + ") was reached");
 		}
 
 		// Print summary of path

prism/src/userinterface/simulator/GUISimulator.java

@@ -738,10 +738,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 			guiProp.tabToFront();
 			Graph graphModel = new Graph();
 			guiProp.getGraphHandler().addGraph(graphModel);
-			GenerateSimulationPath genPath = new GenerateSimulationPath(engine, getGUI().getLog());
 			int maxPathLength = getPrism().getSettings().getInteger(PrismSettings.SIMULATOR_DEFAULT_MAX_PATH);
-			State initialStateObject = initialState == null ? null : new parser.State(initialState, parsedModel);
-			genPath.generateAndPlotSimulationPathInThread(parsedModel, initialStateObject, simPathDetails, maxPathLength, graphModel);
+			parser.State initialStateObject = initialState == null ? null : new parser.State(initialState, parsedModel);
+			new SimPathPlotThread(this, engine, parsedModel, initialStateObject, simPathDetails, maxPathLength, graphModel).start();
 			setComputing(false);
 
 			// store initial state for next time

prism/src/userinterface/simulator/SimPathPlotThread.java

@@ -0,0 +1,71 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package userinterface.simulator;
+
+import parser.ast.ModulesFile;
+import prism.PrismException;
+import simulator.GenerateSimulationPath;
+import simulator.SimulatorEngine;
+import userinterface.GUIComputationThread;
+import userinterface.graph.Graph;
+
+public class SimPathPlotThread extends GUIComputationThread
+{
+	private SimulatorEngine engine;
+	private ModulesFile modulesFile;
+	private parser.State initialState;
+	private String simPathDetails;
+	private int maxPathLength;
+	private Graph graphModel;
+
+	public SimPathPlotThread(GUISimulator guiSim, SimulatorEngine engine, ModulesFile modulesFile, parser.State initialState, String simPathDetails,
+			int maxPathLength, Graph graphModel)
+	{
+		super(guiSim);
+		this.engine = engine;
+		this.modulesFile = modulesFile;
+		this.initialState = initialState;
+		this.simPathDetails = simPathDetails;
+		this.maxPathLength = maxPathLength;
+		this.graphModel = graphModel;
+	}
+
+	public void run()
+	{
+		try {
+			GenerateSimulationPath genPath = new GenerateSimulationPath(engine, prism.getMainLog());
+			genPath.generateAndPlotSimulationPath(modulesFile, initialState, simPathDetails, maxPathLength, graphModel);
+			if (genPath.getNumWarnings() > 0) {
+				for (String msg : genPath.getWarnings()) {
+					plug.warning(msg);
+				}
+			}
+		} catch (PrismException e) {
+			error(e.getMessage());
+		}
+	}
+}