From e1e6267210b16efa33d30b2bc5c934009ab26e07 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 2 Jul 2012 08:16:58 +0000 Subject: [PATCH] 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 --- .../src/simulator/GenerateSimulationPath.java | 40 +++++++++-- .../userinterface/simulator/GUISimulator.java | 5 +- .../simulator/SimPathPlotThread.java | 71 +++++++++++++++++++ 3 files changed, 107 insertions(+), 9 deletions(-) create mode 100644 prism/src/userinterface/simulator/SimPathPlotThread.java diff --git a/prism/src/simulator/GenerateSimulationPath.java b/prism/src/simulator/GenerateSimulationPath.java index 617668d4..0a941805 100644 --- a/prism/src/simulator/GenerateSimulationPath.java +++ b/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 warnings = new ArrayList(); // 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 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 diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index b49ccbbf..4cd1432c 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/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 diff --git a/prism/src/userinterface/simulator/SimPathPlotThread.java b/prism/src/userinterface/simulator/SimPathPlotThread.java new file mode 100644 index 00000000..37b5e2af --- /dev/null +++ b/prism/src/userinterface/simulator/SimPathPlotThread.java @@ -0,0 +1,71 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (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()); + } + } +}