From 992c0864dc868d0ce22366203e1ae8c414bdf8c3 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 27 Jun 2012 10:04:58 +0000 Subject: [PATCH] New/improved simulation path plotting functionality. For -simpath switch: * paths are generated on-the-fly for efficiency where possible * rewards are not displayed by default, use 'rewards' option to show * new 'snapshot' option to only show states at certain time-points For GUI simulator: * basic functionality to plot existing paths or create new plots directly git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5384 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../src/simulator/GenerateSimulationPath.java | 293 ++++++++++++++---- prism/src/simulator/Path.java | 34 +- prism/src/simulator/PathDisplayer.java | 166 ++++++++++ prism/src/simulator/PathFull.java | 220 +++++++------ prism/src/simulator/PathFullPrefix.java | 30 ++ prism/src/simulator/PathOnTheFly.java | 44 ++- prism/src/simulator/PathToGraph.java | 121 ++++++++ prism/src/simulator/PathToText.java | 272 ++++++++++++++++ prism/src/simulator/SimulatorEngine.java | 25 +- .../simulator/GUIPathPlotDialog.java | 191 ++++++++++++ .../userinterface/simulator/GUISimulator.java | 239 ++++++++++---- 11 files changed, 1413 insertions(+), 222 deletions(-) create mode 100644 prism/src/simulator/PathDisplayer.java create mode 100644 prism/src/simulator/PathToGraph.java create mode 100644 prism/src/simulator/PathToText.java create mode 100644 prism/src/userinterface/simulator/GUIPathPlotDialog.java diff --git a/prism/src/simulator/GenerateSimulationPath.java b/prism/src/simulator/GenerateSimulationPath.java index f9d74c47..5349fca3 100644 --- a/prism/src/simulator/GenerateSimulationPath.java +++ b/prism/src/simulator/GenerateSimulationPath.java @@ -32,6 +32,7 @@ import java.util.ArrayList; import prism.*; import parser.*; import parser.ast.*; +import userinterface.graph.Graph; public class GenerateSimulationPath { @@ -49,7 +50,7 @@ public class GenerateSimulationPath private State initialState; private int maxPathLength; private File file; - + // Path configuration options private PathType simPathType = null; private int simPathLength = 0; @@ -58,6 +59,9 @@ public class GenerateSimulationPath private ArrayList simVars = null; private boolean simLoopCheck = true; private int simPathRepeat = 1; + private boolean simPathShowRewards = false; + private boolean simPathSnapshots = false; + private double simPathSnapshotTime = 0.0; public GenerateSimulationPath(SimulatorEngine engine, PrismLog mainLog) { @@ -72,15 +76,52 @@ public class GenerateSimulationPath * @param details Information about the path to be generated * @param file File to output the path to (stdout if null) */ - public void generateSimulationPath(ModulesFile modulesFile, State initialState, String details, int maxPathLength, - File file) throws PrismException + public void generateSimulationPath(ModulesFile modulesFile, State initialState, String details, int maxPathLength, File file) throws PrismException { this.modulesFile = modulesFile; this.initialState = initialState; this.maxPathLength = maxPathLength; this.file = file; + parseDetails(details); - generatePath(); + PathDisplayer displayer = generateDisplayerForExport(); + if (simPathType == PathType.SIM_PATH_DEADLOCK) + generateMultiplePaths(displayer); + else + generatePath(displayer); + } + + /** + * Generate and plot a random path through a model with the simulator. + * @param modulesFile The model + * @param initialState Initial state (if null, is selected randomly) + * @param details Information about the path to be generated + */ + public void generateAndPlotSimulationPath(ModulesFile modulesFile, State initialState, String details, int maxPathLength, Graph graphModel) + throws PrismException + { + this.modulesFile = modulesFile; + this.initialState = initialState; + this.maxPathLength = maxPathLength; + + parseDetails(details); + PathDisplayer displayer = generateDisplayerForPlotting(graphModel); + if (simPathType == PathType.SIM_PATH_DEADLOCK) + generateMultiplePaths(displayer); + else + generatePath(displayer); + } + + /** + * Generate and plot a random path through a model with the simulator, in a separate thread. + * @param modulesFile The model + * @param initialState Initial state (if null, is selected randomly) + * @param details Information about the path to be generated + */ + public void generateAndPlotSimulationPathInThread(ModulesFile modulesFile, State initialState, String details, int maxPathLength, Graph graphModel) + throws PrismException + { + new GenerateAndPlotThread(modulesFile, initialState, details, maxPathLength, graphModel).start(); } /** @@ -173,6 +214,19 @@ public class GenerateSimulationPath } catch (NumberFormatException e) { throw new PrismException("Value for \"repeat\" option must be a positive integer"); } + } else if (ss[i].indexOf("snapshot=") == 0) { + // print timed snapshots of path + try { + simPathSnapshots = true; + simPathSnapshotTime = Double.parseDouble(ss[i].substring(9)); + if (simPathSnapshotTime <= 0) + throw new NumberFormatException(); + } catch (NumberFormatException e) { + throw new PrismException("Value for \"snapshot\" option must be a positive double"); + } + } else if (ss[i].equals("rewards")) { + // display rewards + simPathShowRewards = true; } else { // path of fixed number of steps simPathType = PathType.SIM_PATH_NUM_STEPS; @@ -181,25 +235,71 @@ public class GenerateSimulationPath if (simPathLength < 0) throw new NumberFormatException(); } catch (NumberFormatException e) { - throw new PrismException("Invalid path length \"" + ss[i] + "\""); + throw new PrismException("Invalid path option \"" + ss[i] + "\""); } } } if (simPathType == null) throw new PrismException("Invalid path details \"" + details + "\""); + + // Display warning if attempt to use "repeat=" option and not "deadlock" option + if (simPathRepeat > 1 && simPathType != PathType.SIM_PATH_DEADLOCK) { + simPathRepeat = 1; + mainLog.printWarning("Ignoring \"repeat\" option - it is only valid when looking for deadlocks."); + } } /** - * Generate a random path using the simulator. + * Create a PathDisplayer object for file export */ - private void generatePath() throws PrismException + private PathDisplayer generateDisplayerForExport() throws PrismException { - int i = 0, j = 0; + PrismLog log; + PathToText displayer; + + if (file != null) { + log = new PrismFileLog(file.getPath()); + if (!log.ready()) { + throw new PrismException("Could not open file \"" + file + "\" for output"); + } + } else { + log = mainLog; + } + displayer = new PathToText(log, modulesFile); + displayer.setColSep(simPathSep); + displayer.setVarsToShow(simVars); + displayer.setShowRewards(simPathShowRewards); + if (simPathSnapshots) + displayer.setToShowSnapShots(simPathSnapshotTime); + + return displayer; + } + + /** + * Create a PathDisplayer object for graph plotting + */ + private PathDisplayer generateDisplayerForPlotting(Graph graphModel) throws PrismException + { + PathToGraph displayer; + + displayer = new PathToGraph(graphModel, modulesFile); + displayer.setShowRewards(simPathShowRewards); + if (simPathSnapshots) + displayer.setToShowSnapShots(simPathSnapshotTime); + + return displayer; + } + + /** + * Generate a random (on-the-fly) path using the simulator. + */ + private void generatePath(PathDisplayer displayer) throws PrismException + { + Path path = null; + int i = 0; boolean done; - double t = 0.0; - boolean stochastic = (modulesFile.getModelType() == ModelType.CTMC); - // print details + // Print details switch (simPathType) { case SIM_PATH_NUM_STEPS: mainLog.println("\nGenerating random path of length " + simPathLength + " steps..."); @@ -207,83 +307,164 @@ public class GenerateSimulationPath case SIM_PATH_TIME: mainLog.println("\nGenerating random path with time limit " + simPathTime + "..."); break; - case SIM_PATH_DEADLOCK: - mainLog.println("\nGenerating random path until deadlock state..."); - break; } + if (displayer instanceof PathToText && file == null) + mainLog.println(); - // display warning if attempt to use "repeat=" option and not "deadlock" option - if (simPathRepeat > 1 && simPathType != PathType.SIM_PATH_DEADLOCK) { - simPathRepeat = 1; - mainLog.printWarning("Ignoring \"repeat\" option - it is only valid when looking for deadlocks."); + // Create path + engine.createNewOnTheFlyPath(modulesFile); + // Build path + path = engine.getPath(); + engine.initialisePath(initialState); + displayer.start(path.getCurrentState(), path.getCurrentStateRewards()); + i = 0; + done = false; + while (!done) { + // Generate a single step of path + engine.automaticTransition(); + i++; + if (simPathType != PathType.SIM_PATH_DEADLOCK) { + displayer.step(path.getTimeInPreviousState(), path.getTotalTime(), path.getPreviousModuleOrAction(), path.getPreviousTransitionRewards(), + path.getCurrentState(), path.getCurrentStateRewards()); + } + // Check for termination (depending on type) + switch (simPathType) { + case SIM_PATH_NUM_STEPS: + if (i >= simPathLength || engine.queryIsDeadlock()) + done = true; + break; + case SIM_PATH_TIME: + if (path.getTotalTime() >= simPathTime || i >= maxPathLength || engine.queryIsDeadlock()) + done = true; + break; + } + // Stop if a loop was found (and loop checking was not disabled) + if (simLoopCheck && engine.isPathLooping()) + break; + } + displayer.end(); + + // Display warnings if needed + if (simLoopCheck && engine.isPathLooping()) { + mainLog.printWarning("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."); + } + + // Print summary of path + mainLog.print("\nGenerated path: " + path.size() + " step" + (path.size() == 1 ? "" : "s")); + if (modulesFile.getModelType().continuousTime()) { + mainLog.print(", total time " + path.getTotalTime()); + } + if (file != null) { + mainLog.println(" (exported to " + file + ")"); + } else { + mainLog.println(); + } + } + + /** + * Generate multiple random paths using the simulator. + * Note: these are not on-the-fly paths since we don't in advance if they are to be displayed. + */ + private void generateMultiplePaths(PathDisplayer displayer) throws PrismException + { + Path path = null; + int i = 0, j = 0; + boolean done; + + // Print details + switch (simPathType) { + case SIM_PATH_DEADLOCK: + mainLog.println("\nGenerating random path(s) until deadlock state..."); + break; } - // generate path + // Create path engine.createNewPath(modulesFile); + // Build path for (j = 0; j < simPathRepeat; j++) { + path = engine.getPath(); engine.initialisePath(initialState); i = 0; - t = 0.0; done = false; while (!done) { - // generate a single step of path - // (no need to do any loop detection: this is done below) + // Generate a single step of path engine.automaticTransition(); - if (stochastic) - t += engine.getTimeSpentInPathStep(i++); - else - t = ++i; - // check for termination (depending on type) + i++; + // Check for termination (depending on type) switch (simPathType) { - case SIM_PATH_NUM_STEPS: - if (i >= simPathLength || engine.queryIsDeadlock()) - done = true; - break; - case SIM_PATH_TIME: - if (t >= simPathTime || i >= maxPathLength || engine.queryIsDeadlock()) - done = true; - break; case SIM_PATH_DEADLOCK: if (engine.queryIsDeadlock() || i >= maxPathLength) done = true; break; } - // stop if a loop was found (and loop checking was not disabled) + // Stop if a loop was found (and loop checking was not disabled) if (simLoopCheck && engine.isPathLooping()) break; } - - // if we are generating multiple paths (to find a deadlock) only stop if deadlock actually found - if (simPathType == PathType.SIM_PATH_DEADLOCK && engine.queryIsDeadlock()) + // Stop generating paths if done + if (engine.queryIsDeadlock()) break; } if (j < simPathRepeat) j++; - // display warning if a deterministic loop was detected (but not in case where multiple paths generated) - if (simLoopCheck && engine.isPathLooping() && simPathRepeat == 1) { - mainLog.printWarning("Deterministic loop detected after " + i - + " steps (use loopcheck=false option to extend path)."); - } - - // if we needed multiple paths to find a deadlock, say how many - if (simPathRepeat > 1 && j > 1) - mainLog.println("\n" + j + " paths were generated."); - - // export path - if (simPathType == PathType.SIM_PATH_DEADLOCK && !engine.queryIsDeadlock()) { + // Bail out if we didn't build a suitable path + if (!engine.queryIsDeadlock()) { mainLog.print("\nNo deadlock state found within " + maxPathLength + " steps"); if (simPathRepeat > 1) mainLog.print(" (generated " + simPathRepeat + " paths)"); mainLog.println("."); + return; + } + + // Display path + if (file == null) + mainLog.println(); + engine.getPathFull().display(displayer); + + // Print summary of path(s) + if (simPathRepeat > 1 && j > 1) + mainLog.print("\nGenerated " + j + " paths. Final path: "); + else + mainLog.print("\nGenerated path: "); + mainLog.print(path.size() + " steps"); + if (modulesFile.getModelType().continuousTime()) { + mainLog.print(", total time " + path.getTotalTime()); + } + if (file != null) { + mainLog.println(" (exported to " + file + ")"); } else { - engine.exportPath(file, true, simPathSep, simVars); + mainLog.println(); + } + } + + class GenerateAndPlotThread extends Thread + { + private ModulesFile modulesFile; + private parser.State initialState; + private String details; + private int maxPathLength; + private Graph graphModel; + + public GenerateAndPlotThread(ModulesFile modulesFile, parser.State initialState, String details, int maxPathLength, Graph graphModel) + { + this.modulesFile = modulesFile; + this.initialState = initialState; + this.details = details; + this.maxPathLength = maxPathLength; + this.graphModel = graphModel; } - // warning if stopped early - if (simPathType == PathType.SIM_PATH_TIME && t < simPathTime) { - mainLog.printWarning("Path terminated before time " + simPathTime + " because maximum path length (" - + maxPathLength + ") reached."); + public void run() + { + try { + generateAndPlotSimulationPath(modulesFile, initialState, details, maxPathLength, graphModel); + } catch (PrismException e) { + // Just ignore problems + } } } } diff --git a/prism/src/simulator/Path.java b/prism/src/simulator/Path.java index 1a049de1..01f6ceed 100644 --- a/prism/src/simulator/Path.java +++ b/prism/src/simulator/Path.java @@ -76,9 +76,20 @@ public abstract class Path public abstract State getCurrentState(); /** - * For paths with continuous-time info, get the total time elapsed so far - * (where zero time has been spent in the current (final) state). - * For discrete-time models, just returns 0.0. + * Get the index i of the action taken in the previous step. + * If i>0, then i-1 is the index of an action label (0-indexed) + * If i<0, then -i-1 is the index of a module (0-indexed) + */ + public abstract int getPreviousModuleOrActionIndex(); + + /** + * Get a string describing the action/module of the previous step. + */ + public abstract String getPreviousModuleOrAction(); + + /** + * Get the total time elapsed so far (where zero time has been spent in the current (final) state). + * For discrete-time models, this is just the number of steps (but returned as a double). */ public abstract double getTotalTime(); @@ -101,12 +112,23 @@ public abstract class Path */ public abstract double getPreviousStateReward(int rsi); + /** + * Get the state rewards for the previous state. + * (For continuous-time models, need to multiply these by time spent in the state.) + */ + public abstract double[] getPreviousStateRewards(); + /** * Get the transition reward for the transition between the previous and current states. * @param rsi Reward structure index */ public abstract double getPreviousTransitionReward(int rsi); + /** + * Get the transition rewards for the transition between the previous and current states. + */ + public abstract double[] getPreviousTransitionRewards(); + /** * Get the state reward for the current state. * (For continuous-time models, need to multiply this by time spent in the state.) @@ -114,6 +136,12 @@ public abstract class Path */ public abstract double getCurrentStateReward(int rsi); + /** + * Get the state rewards for the current state. + * (For continuous-time models, need to multiply these by time spent in the state.) + */ + public abstract double[] getCurrentStateRewards(); + /** * Does the path contain a deterministic loop? */ diff --git a/prism/src/simulator/PathDisplayer.java b/prism/src/simulator/PathDisplayer.java new file mode 100644 index 00000000..e095ce29 --- /dev/null +++ b/prism/src/simulator/PathDisplayer.java @@ -0,0 +1,166 @@ +//============================================================================== +// +// 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 simulator; + +import java.util.ArrayList; +import java.util.List; + +import parser.State; + +/** + * Abstract class for classes that "display" a simulation path. + */ +public abstract class PathDisplayer +{ + /** Should we display (timed) snapshots, rather than steps? */ + protected boolean showSnapshots = false; + /** If we are displaying snapshots, how often? */ + protected double snapshotTimeStep = 0.0; + /** If we are displaying snapshots, when is the next one due? */ + protected double nextTime = 0.0; + + /** Indices of variables to show (null = all) */ + protected List varsToShow = null; + + /** Should we display rewards? */ + protected boolean showRewards = false; + + // Getters for config + + /** + * Should we display (timed) snapshots, rather than steps? + */ + public boolean getShowSnapshots() + { + return showSnapshots; + } + + /** + * If we are displaying snapshots, how often? + */ + public double getSnapshotTimeStep() + { + return snapshotTimeStep; + } + + /** + * Set (indices of) vars to show values of (null = all). + */ + public void setVarsToShow(List varsToShow) + { + // Take a copy of var index list + this.varsToShow = varsToShow == null ? null : new ArrayList(varsToShow); + } + + /** + * Should we display rewards? + */ + public boolean getShowRewards() + { + return showRewards; + } + + // Setters for config + + /** + * Set to display (timed) snapshots, rather than steps. + */ + public void setToShowSteps() + { + this.showSnapshots = false; + } + + /** + * Set to display steps, rather than (timed) snapshots. + */ + public void setToShowSnapShots(double timeStep) + { + this.showSnapshots = true; + this.snapshotTimeStep = timeStep; + } + + /** + * Set whether we we display rewards. + */ + public void setShowRewards(boolean showRewards) + { + this.showRewards = showRewards; + } + + // Methods called by path owner + + public void start(State initialState, double[] initialStateRewards) + { + startDisplay(initialState, initialStateRewards); + if (showSnapshots) { + nextTime = snapshotTimeStep; + } + } + + public void step(double timeSpent, double timeCumul, Object action, double[] transitionRewards, State newState, double[] newStateRewards) + { + if (showSnapshots) { + if (timeCumul < nextTime) { + return; + } else { + while (timeCumul >= nextTime) { + displaySnapshot(nextTime, newState, newStateRewards); + nextTime += snapshotTimeStep; + } + } + } else { + displayStep(timeSpent, timeCumul, action, transitionRewards, newState, newStateRewards); + } + } + + public void end() + { + endDisplay(); + } + + // Display methods to be implemented by subclasses + + /** + * Start displaying a path beginning with state {@code initialState}. + */ + public abstract void startDisplay(State initialState, double[] initialStateRewards); + + /** + * Displaying a step of a path. + */ + public abstract void displayStep(double timeSpent, double timeCumul, Object action, double[] transitionRewards, State newState, double[] newStateRewards); + + /** + * Displaying a snapshot of a path at a particular time instant. + */ + public abstract void displaySnapshot(double timeCumul, State newState, double[] newStateRewards); + + /** + * Finish displaying a path.. + */ + public abstract void endDisplay(); +} diff --git a/prism/src/simulator/PathFull.java b/prism/src/simulator/PathFull.java index 65751e88..3e4f118f 100644 --- a/prism/src/simulator/PathFull.java +++ b/prism/src/simulator/PathFull.java @@ -27,10 +27,11 @@ package simulator; import java.util.ArrayList; + import org.jfree.data.xy.XYDataItem; -import parser.*; -import parser.ast.*; +import parser.State; +import parser.ast.ModulesFile; import prism.PrismException; import prism.PrismLog; import userinterface.graph.Graph; @@ -108,7 +109,7 @@ public class PathFull extends Path implements PathFullInfo @Override public void addStep(int choice, int moduleOrActionIndex, double[] transitionRewards, State newState, double[] newStateRewards, TransitionList transitionList) { - addStep(0.0, choice, moduleOrActionIndex, transitionRewards, newState, newStateRewards, transitionList); + addStep(1.0, choice, moduleOrActionIndex, transitionRewards, newState, newStateRewards, transitionList); } @Override @@ -233,6 +234,24 @@ public class PathFull extends Path implements PathFullInfo return steps.get(steps.size() - 1).state; } + @Override + public int getPreviousModuleOrActionIndex() + { + return steps.get(steps.size() - 2).moduleOrActionIndex; + } + + @Override + public String getPreviousModuleOrAction() + { + int i = getPreviousModuleOrActionIndex(); + if (i < 0) + return modulesFile.getModuleName(-i - 1); + else if (i > 0) + return "[" + modulesFile.getSynchs().get(i - 1) + "]"; + else + return "?"; + } + @Override public double getTotalTime() { @@ -257,18 +276,36 @@ public class PathFull extends Path implements PathFullInfo return steps.get(steps.size() - 2).stateRewards[rsi]; } + @Override + public double[] getPreviousStateRewards() + { + return steps.get(steps.size() - 2).stateRewards; + } + @Override public double getPreviousTransitionReward(int rsi) { return steps.get(steps.size() - 2).transitionRewards[rsi]; } + @Override + public double[] getPreviousTransitionRewards() + { + return steps.get(steps.size() - 2).transitionRewards; + } + @Override public double getCurrentStateReward(int rsi) { return steps.get(steps.size() - 1).stateRewards[rsi]; } + @Override + public double[] getCurrentStateRewards() + { + return steps.get(steps.size() - 1).stateRewards; + } + @Override public boolean isLooping() { @@ -308,6 +345,15 @@ public class PathFull extends Path implements PathFullInfo return steps.get(step).stateRewards[rsi]; } + /** + * Get an array of state rewards for the state at a given step of the path. + * @param step Step index (0 = initial state/step of path) + */ + protected double[] getStateRewards(int step) + { + return steps.get(step).stateRewards; + } + /** * Get the total time spent up until entering a given step of the path. * @param step Step index (0 = initial state/step of path) @@ -381,6 +427,15 @@ public class PathFull extends Path implements PathFullInfo return steps.get(step).transitionRewards[rsi]; } + /** + * Get an array of transitions reward associated with a given step. + * @param step Step index (0 = initial state/step of path) + */ + protected double[] getTransitionRewards(int step) + { + return steps.get(step).transitionRewards; + } + @Override public boolean hasRewardInfo() { @@ -414,114 +469,62 @@ public class PathFull extends Path implements PathFullInfo // Other methods /** - * Export path to a file. - * @param log PrismLog to which the path should be exported to. - * @param timeCumul Show time in cumulative form? - * @param colSep String used to separate columns in display - * @param vars Restrict printing to these variables (indices) and steps which change them (ignore if null) + * Pass the path to a PathDisplayer object. + * @param displayer The PathDisplayer */ - public void exportToLog(PrismLog log, boolean timeCumul, String colSep, ArrayList vars) throws PrismException + public void display(PathDisplayer displayer) throws PrismException { - int i, j, n, nv; - double d, t; - boolean contTime = modulesFile.getModelType().continuousTime(); - boolean changed; - int varsNum = 0, varsIndices[] = null; - + // In the absence of model info, do nothing if (modulesFile == null) { - log.flush(); - log.close(); return; } - - // Get sizes - n = size(); - nv = modulesFile.getNumVars(); - - // if necessary, store info about which vars to display - if (vars != null) { - varsNum = vars.size(); - varsIndices = new int[varsNum]; - for (i = 0; i < varsNum; i++) - varsIndices[i] = vars.get(i); + // Display path + displayer.start(getState(0), getStateRewards(0)); + int n = size(); + for (int i = 1; i <= n; i++) { + displayer.step(getTime(i - 1), getCumulativeTime(i), getModuleOrAction(i - 1), getTransitionRewards(i), getState(i), getStateRewards(i)); } + displayer.end(); + } - // Write header - log.print("action"); - log.print(colSep + "step"); - if (contTime) - log.print(colSep + (timeCumul ? "time" : "time_in_state")); - if (vars == null) - for (j = 0; j < nv; j++) - log.print(colSep + modulesFile.getVarName(j)); - else - for (j = 0; j < varsNum; j++) - log.print(colSep + modulesFile.getVarName(varsIndices[j])); - if (numRewardStructs == 1) { - log.print(colSep + "state_reward" + colSep + "transition_reward"); - } else { - for (j = 0; j < numRewardStructs; j++) - log.print(colSep + "state_reward" + (j + 1) + colSep + "transition_reward" + (j + 1)); - } - log.println(); - - // Write path - t = 0.0; - for (i = 0; i <= n; i++) { - // (if required) see if relevant vars have changed - if (vars != null && i > 0) { - changed = false; - for (j = 0; j < varsNum; j++) { - if (!getState(i).varValues[varsIndices[j]].equals(getState(i - 1).varValues[varsIndices[j]])) - changed = true; - } - if (!changed) { - d = (i < n) ? getTime(i) : 0.0; - t += d; - continue; - } - } - // write action - log.print(i == 0 ? "-" : getModuleOrAction(i - 1)); - // write state index - log.print(colSep); - log.print(i); - // print time (if continuous time) - if (contTime) { - d = (i < n) ? getTime(i) : 0.0; - log.print(colSep + (timeCumul ? t : d)); - t += d; - } - // write vars - if (vars == null) { - for (j = 0; j < nv; j++) { - log.print(colSep); - log.print(getState(i).varValues[j]); - } - } else { - for (j = 0; j < varsNum; j++) { - log.print(colSep); - log.print(getState(i).varValues[varsIndices[j]]); - } - } - // write rewards - for (j = 0; j < numRewardStructs; j++) { - log.print(colSep + ((i < n - 1) ? getStateReward(i, j) : 0.0)); - log.print(colSep + ((i < n - 1) ? getTransitionReward(i, j) : 0.0)); - } - log.println(); + /** + * Pass the path to a PathDisplayer object, running in a new thread. + * @param displayer The PathDisplayer + */ + public void displayThreaded(PathDisplayer displayer) throws PrismException + { + // In the absence of model info, do nothing + if (modulesFile == null) { + return; } - - log.flush(); - log.close(); + // Display path + new DisplayThread(displayer).start(); } + /** + * Export path to a PrismLog (e.g. file, stdout). + * @param log PrismLog to which the path should be exported to. + * @param showTimeCumul Show time in cumulative form? + * @param colSep String used to separate columns in display + * @param vars Restrict printing to these variables (indices) and steps which change them (ignore if null) + */ + public void exportToLog(PrismLog log, boolean showTimeCumul, String colSep, ArrayList vars) throws PrismException + { + PathToText displayer = new PathToText(log, modulesFile); + displayer.setShowTimeCumul(showTimeCumul); + displayer.setColSep(colSep); + displayer.setVarsToShow(vars); + display(displayer); + } + /** * Plot path on a graph. + * @param graphModel Graph on which to plot path */ - public void plotOnGraph(Graph graphModel) + public void plotOnGraph(Graph graphModel) throws PrismException { - new PlotOnGraphThread(graphModel).start(); + PathToGraph displayer = new PathToGraph(graphModel, modulesFile); + displayThreaded(displayer); } @Override @@ -575,9 +578,9 @@ public class PathFull extends Path implements PathFullInfo { private Graph graphModel = null; - public PlotOnGraphThread(Graph graphmodel) + public PlotOnGraphThread(Graph graphModel) { - this.graphModel = graphmodel; + this.graphModel = graphModel; } public void run() @@ -617,4 +620,23 @@ public class PathFull extends Path implements PathFullInfo } } } + + class DisplayThread extends Thread + { + private PathDisplayer displayer = null; + + public DisplayThread(PathDisplayer displayer) + { + this.displayer = displayer; + } + + public void run() + { + try { + display(displayer); + } catch (PrismException e) { + // Just ignore problems + } + } + } } diff --git a/prism/src/simulator/PathFullPrefix.java b/prism/src/simulator/PathFullPrefix.java index a114fdba..46402e6e 100644 --- a/prism/src/simulator/PathFullPrefix.java +++ b/prism/src/simulator/PathFullPrefix.java @@ -101,6 +101,18 @@ public class PathFullPrefix extends Path return pathFull.getState(prefixLength); } + @Override + public int getPreviousModuleOrActionIndex() + { + return pathFull.getModuleOrActionIndex(prefixLength - 1); + } + + @Override + public String getPreviousModuleOrAction() + { + return pathFull.getModuleOrAction(prefixLength - 1); + } + @Override public double getTotalTime() { @@ -125,18 +137,36 @@ public class PathFullPrefix extends Path return pathFull.getStateReward(prefixLength - 1, rsi); } + @Override + public double[] getPreviousStateRewards() + { + return pathFull.getStateRewards(prefixLength - 1); + } + @Override public double getPreviousTransitionReward(int rsi) { return pathFull.getTransitionReward(prefixLength - 1, rsi); } + @Override + public double[] getPreviousTransitionRewards() + { + return pathFull.getTransitionRewards(prefixLength - 1); + } + @Override public double getCurrentStateReward(int rsi) { return pathFull.getStateReward(prefixLength, rsi); } + @Override + public double[] getCurrentStateRewards() + { + return pathFull.getStateRewards(prefixLength); + } + @Override public boolean isLooping() { diff --git a/prism/src/simulator/PathOnTheFly.java b/prism/src/simulator/PathOnTheFly.java index 43cae778..3b42ed64 100644 --- a/prism/src/simulator/PathOnTheFly.java +++ b/prism/src/simulator/PathOnTheFly.java @@ -46,6 +46,7 @@ public class PathOnTheFly extends Path protected int size; protected State previousState; protected State currentState; + protected int previousModuleOrActionIndex; protected double totalTime; double timeInPreviousState; protected double totalRewards[]; @@ -113,17 +114,18 @@ public class PathOnTheFly extends Path } @Override - public void addStep(int choice, int actionIndex, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList) + public void addStep(int choice, int moduleOrActionIndex, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList) { - addStep(0, choice, actionIndex, transRewards, newState, newStateRewards, transitionList); + addStep(1.0, choice, moduleOrActionIndex, transRewards, newState, newStateRewards, transitionList); } @Override - public void addStep(double time, int choice, int actionIndex, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList) + public void addStep(double time, int choice, int moduleOrActionIndex, double[] transRewards, State newState, double[] newStateRewards, TransitionList transitionList) { size++; previousState.copy(currentState); currentState.copy(newState); + previousModuleOrActionIndex = moduleOrActionIndex; totalTime += time; timeInPreviousState = time; for (int i = 0; i < numRewardStructs; i++) { @@ -166,6 +168,24 @@ public class PathOnTheFly extends Path return currentState; } + @Override + public int getPreviousModuleOrActionIndex() + { + return previousModuleOrActionIndex; + } + + @Override + public String getPreviousModuleOrAction() + { + int i = getPreviousModuleOrActionIndex(); + if (i < 0) + return modulesFile.getModuleName(-i - 1); + else if (i > 0) + return "[" + modulesFile.getSynchs().get(i - 1) + "]"; + else + return "?"; + } + @Override public double getTotalTime() { @@ -190,18 +210,36 @@ public class PathOnTheFly extends Path return previousStateRewards[rsi]; } + @Override + public double[] getPreviousStateRewards() + { + return previousStateRewards; + } + @Override public double getPreviousTransitionReward(int rsi) { return previousTransitionRewards[rsi]; } + @Override + public double[] getPreviousTransitionRewards() + { + return previousTransitionRewards; + } + @Override public double getCurrentStateReward(int rsi) { return currentStateRewards[rsi]; } + @Override + public double[] getCurrentStateRewards() + { + return currentStateRewards; + } + @Override public boolean isLooping() { diff --git a/prism/src/simulator/PathToGraph.java b/prism/src/simulator/PathToGraph.java new file mode 100644 index 00000000..e621dce7 --- /dev/null +++ b/prism/src/simulator/PathToGraph.java @@ -0,0 +1,121 @@ +//============================================================================== +// +// 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 simulator; + +import org.jfree.data.xy.XYDataItem; + +import parser.State; +import parser.ast.ModulesFile; +import userinterface.graph.Graph; +import userinterface.graph.Graph.SeriesKey; + +/** + * Class to display a simulation path in text form, sending to a PrismLog. + */ +public class PathToGraph extends PathDisplayer +{ + /** Graph on which to plot path */ + private Graph graphModel = null; + private SeriesKey seriesKeys[] = null; + + // Model info + private ModulesFile modulesFile; + private int numVars; + private int numRewardStructs; + + // Displayer state + /** Step counter */ + private double lastTime; + private State lastState; + + /** + * Construct a {@link PathToGraph} object + * @param graphModel Graph on which to plot path + * @param modulesFile Model associated with path + */ + public PathToGraph(Graph graphModel, ModulesFile modulesFile) + { + this.graphModel = graphModel; + this.modulesFile = modulesFile; + + // Get model info + numVars = modulesFile.getNumVars(); + numRewardStructs = modulesFile.getNumRewardStructs(); + } + + // Display methods + + @Override + public void startDisplay(State initialState, double[] stateRewards) + { + // Configure axes + graphModel.getXAxisSettings().setHeading("Time"); + graphModel.getYAxisSettings().setHeading("Value"); + + // Create series + seriesKeys = new SeriesKey[numVars]; + for (int j = 0; j < numVars; j++) { + seriesKeys[j] = graphModel.addSeries(modulesFile.getVarName(j)); + } + + // Display initial state + lastState = new State(initialState.varValues.length); + displayState(0.0, initialState, true); + } + + @Override + public void displayStep(double timeSpent, double timeCumul, Object action, double[] transitionRewards, State newState, double[] newStateRewards) + { + displayState(timeCumul, newState, false); + } + + @Override + public void displaySnapshot(double timeCumul, State newState, double[] newStateRewards) + { + displayState(timeCumul, newState, false); + } + + private void displayState(double time, State state, boolean force) + { + for (int j = 0; j < numVars; j++) { + // TODO: other var types? + if (force || !state.varValues[j].equals(lastState.varValues[j])) { + graphModel.addPointToSeries(seriesKeys[j], new XYDataItem(time, ((Integer) state.varValues[j]).intValue())); + } + } + lastTime = time; + lastState.copy(state); + } + + @Override + public void endDisplay() + { + // Always display last points to ensure complete plot lines + // (it's OK to overwrite points) + displayState(lastTime, lastState, true); + } +} diff --git a/prism/src/simulator/PathToText.java b/prism/src/simulator/PathToText.java new file mode 100644 index 00000000..9d7ca9ae --- /dev/null +++ b/prism/src/simulator/PathToText.java @@ -0,0 +1,272 @@ +//============================================================================== +// +// 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 simulator; + +import parser.State; +import parser.ast.ModulesFile; +import prism.PrismLog; + +/** + * Class to display a simulation path in text form, sending to a PrismLog. + */ +public class PathToText extends PathDisplayer +{ + /** Log to display path to */ + private PrismLog log; + + // Model info + private ModulesFile modulesFile; + private int numVars; + private int numRewardStructs; + private boolean contTime; + + // Config + private boolean showTimeCumul = true; + private boolean showTimeSpent = false; + private String colSep = " "; + + // Displayer state + /** Step counter */ + private int step; + /** Is the next column the first? */ + private boolean firstCol; + /** Last state */ + private State lastState; + /** Last state rewards */ + private double[] lastStateRewards; + + /** + * Construct a {@link PathToText} object + * @param log Log to output path to + * @param modulesFile Model associated with path + */ + public PathToText(PrismLog log, ModulesFile modulesFile) + { + this.log = log; + this.modulesFile = modulesFile; + + // Get model info + numVars = modulesFile.getNumVars(); + numRewardStructs = modulesFile.getNumRewardStructs(); + contTime = modulesFile.getModelType().continuousTime(); + } + + // Setters + + /** + * Set whether we show cumulative time (for continuous models only) + */ + public void setShowTimeCumul(boolean showTimeCumul) + { + this.showTimeCumul = showTimeCumul; + } + + /** + * Set whether we show time spent in each state (for continuous models only) + */ + public void setShowTimeSpent(boolean showTimeSpent) + { + this.showTimeSpent = showTimeSpent; + } + + /** + * Set the column separator for the table of path contents + */ + public void setColSep(String colSep) + { + this.colSep = colSep; + } + + // Display methods + + @Override + public void startDisplay(State initialState, double[] initialStateRewards) + { + int j; + + // Display header + firstCol = true; + if (!getShowSnapshots()) { + log.print(getColSep() + "action"); + log.print(getColSep() + "step"); + } + if (contTime && showTimeCumul) + log.print(getColSep() + "time"); + if (varsToShow == null) + for (j = 0; j < numVars; j++) + log.print(getColSep() + modulesFile.getVarName(j)); + else + for (int v : varsToShow) + log.print(getColSep() + modulesFile.getVarName(v)); + if (getShowRewards()) { + if (numRewardStructs == 1) { + log.print(getColSep() + "state_reward"); + if (!getShowSnapshots()) + log.print(getColSep() + "transition_reward"); + } else { + for (j = 0; j < numRewardStructs; j++) { + log.print(getColSep() + "state_reward" + (j + 1)); + if (!getShowSnapshots()) + log.print(getColSep() + "transition_reward" + (j + 1)); + } + } + } + if (!getShowSnapshots()) { + if (contTime && showTimeSpent) + log.print(getColSep() + "time_in_state"); + } + log.println(); + + // Display initial step + step = 0; + firstCol = true; + if (!getShowSnapshots()) { + log.print(getColSep() + "-" + getColSep() + "0"); + } + if (contTime && showTimeCumul) + log.print(getColSep() + "0.0"); + lastState = new State(initialState.varValues.length); + displayState(initialState); + if (getShowRewards()) { + lastStateRewards = explicit.Utils.cloneDoubleArray(initialStateRewards); + } + if (getShowSnapshots()) { + log.println(); + } + } + + @Override + public void displayStep(double timeSpent, double timeCumul, Object action, double[] transitionRewards, State newState, double[] newStateRewards) + { + step++; + + // (if required) see if relevant vars have changed + if (varsToShow != null && step > 0) { + boolean changed = false; + for (int v : varsToShow){ + if (!newState.varValues[v].equals(lastState.varValues[v])) { + changed = true; + continue; + } + } + if (!changed) { + return; + } + } + + // display rewards for last state + if (getShowRewards()) { + for (int j = 0; j < numRewardStructs; j++) { + log.print(getColSep() + lastStateRewards[j]); + log.print(getColSep() + transitionRewards[j]); + } + explicit.Utils.copyDoubleArray(newStateRewards, lastStateRewards); + } + // display time spent in state + if (contTime && showTimeSpent) + log.print(getColSep() + timeSpent); + log.println(); + + firstCol = true; + + // display action + log.print(getColSep() + action); + // display state index + log.print(getColSep() + step); + // display cumulative time + if (contTime && showTimeCumul) + log.print(getColSep() + timeCumul); + // display state + displayState(newState); + } + + @Override + public void displaySnapshot(double timeCumul, State newState, double[] newStateRewards) + { + step++; + firstCol = true; + + // display cumulative time + if (contTime && showTimeCumul) + log.print(getColSep() + timeCumul); + // display state + displayState(newState); + // display state rewards + if (getShowRewards()) { + for (int j = 0; j < numRewardStructs; j++) { + log.print(getColSep() + newStateRewards[j]); + } + } + log.println(); + } + + private void displayState(State state) + { + int j; + if (varsToShow == null) { + for (j = 0; j < numVars; j++) { + log.print(getColSep()); + log.print(state.varValues[j]); + } + } else { + for (int v : varsToShow) { + log.print(getColSep()); + log.print(state.varValues[v]); + } + } + lastState.copy(state); + } + + private String getColSep() + { + if (firstCol) { + firstCol = false; + return ""; + } else { + return colSep; + } + } + + @Override + public void endDisplay() + { + if (!getShowSnapshots()) { + // display state rewards for last state + // (transition rewards unknown because no outgoing transition) + if (getShowRewards()) { + for (int j = 0; j < numRewardStructs; j++) { + log.print(getColSep() + lastStateRewards[j]); + log.print(getColSep() + "?"); + } + } + // display (zero) time spent in state + if (contTime && showTimeSpent) + log.print(getColSep() + 0.0); + log.println(); + } + } +} diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index 613939fc..ded0b4b8 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -1007,6 +1007,15 @@ public class SimulatorEngine // Querying of current path (full or on-the-fly) // ------------------------------------------------------------------------------ + /** + * Get access to the {@code Path} object storing the current path. + * This object is only valid until the next time {@link #createNewPath} is called. + */ + public Path getPath() + { + return (Path) path; + } + /** * Get the size of the current path (number of steps; or number of states - 1). */ @@ -1024,9 +1033,16 @@ public class SimulatorEngine } /** - * For paths with continuous-time info, get the total time elapsed so far - * (where zero time has been spent in the current (final) state). - * For discrete-time models, just returns 0.0. + * Returns the previous state of the current path in the simulator. + */ + public State getPreviousState() + { + return path.getPreviousState(); + } + + /** + * Get the total time elapsed so far (where zero time has been spent in the current (final) state). + * For discrete-time models, this is just the number of steps (but returned as a double). */ public double getTotalTimeForPath() { @@ -1225,8 +1241,9 @@ public class SimulatorEngine /** * Plot the current path on a Graph. + * @param graphModel Graph on which to plot path */ - public void plotPath(Graph graphModel) + public void plotPath(Graph graphModel) throws PrismException { ((PathFull) path).plotOnGraph(graphModel); } diff --git a/prism/src/userinterface/simulator/GUIPathPlotDialog.java b/prism/src/userinterface/simulator/GUIPathPlotDialog.java new file mode 100644 index 00000000..85ed4d49 --- /dev/null +++ b/prism/src/userinterface/simulator/GUIPathPlotDialog.java @@ -0,0 +1,191 @@ +//============================================================================== +// +// 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 javax.swing.*; +import userinterface.*; + +public class GUIPathPlotDialog extends javax.swing.JDialog +{ + public static final int OK = 0; + public static final int CANCELLED = 1; + + static double time = 0.0; + static boolean first = true; + + private boolean cancelled = true; + + /** Call this static method to construct a new GUIPathPlotDialog to get a time value. */ + public static int requestTime(GUIPrism parent) + { + return new GUIPathPlotDialog(parent).requestTime(); + } + + public int requestTime() + { + setVisible(true); + return cancelled ? CANCELLED : OK; + } + + public static double getTime() + { + return time; + } + + /** Creates new form GUIPathPlotDialog */ + public GUIPathPlotDialog(java.awt.Frame parent) + { + super(parent, "Define time", true); + initComponents(); + this.getRootPane().setDefaultButton(okayButton); + setLocationRelativeTo(getParent()); // centre + if (!first) + timeField.setText("" + time); + } + + /** This method is called from within the constructor to + * initialize the form. + * WARNING: Do NOT modify this code. The content of this method is + * always regenerated by the Form Editor. + */ + private void initComponents() + {//GEN-BEGIN:initComponents + java.awt.GridBagConstraints gridBagConstraints; + + jPanel1 = new javax.swing.JPanel(); + jPanel2 = new javax.swing.JPanel(); + jPanel3 = new javax.swing.JPanel(); + jPanel4 = new javax.swing.JPanel(); + jPanel5 = new javax.swing.JPanel(); + jLabel1 = new javax.swing.JLabel(); + timeField = new javax.swing.JTextField(); + jPanel6 = new javax.swing.JPanel(); + okayButton = new javax.swing.JButton(); + cancelButton = new javax.swing.JButton(); + + setDefaultCloseOperation(javax.swing.WindowConstants.DISPOSE_ON_CLOSE); + jPanel1.setLayout(new java.awt.GridBagLayout()); + + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.gridx = 0; + gridBagConstraints.gridy = 0; + jPanel1.add(jPanel2, gridBagConstraints); + + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.gridx = 2; + gridBagConstraints.gridy = 0; + jPanel1.add(jPanel3, gridBagConstraints); + + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.gridx = 0; + gridBagConstraints.gridy = 2; + jPanel1.add(jPanel4, gridBagConstraints); + + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.gridx = 0; + gridBagConstraints.gridy = 4; + jPanel1.add(jPanel5, gridBagConstraints); + + jLabel1.setText("Please specify a time limit for simulation:"); + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.gridx = 1; + gridBagConstraints.gridy = 1; + gridBagConstraints.anchor = java.awt.GridBagConstraints.WEST; + jPanel1.add(jLabel1, gridBagConstraints); + + timeField.setColumns(10); + gridBagConstraints = new java.awt.GridBagConstraints(); + gridBagConstraints.gridx = 1; + gridBagConstraints.gridy = 3; + jPanel1.add(timeField, gridBagConstraints); + + getContentPane().add(jPanel1, java.awt.BorderLayout.CENTER); + + jPanel6.setLayout(new java.awt.FlowLayout(java.awt.FlowLayout.RIGHT)); + + okayButton.setText("Okay"); + okayButton.addActionListener(new java.awt.event.ActionListener() + { + public void actionPerformed(java.awt.event.ActionEvent evt) + { + okayButtonActionPerformed(evt); + } + }); + + jPanel6.add(okayButton); + + cancelButton.setText("Cancel"); + cancelButton.addActionListener(new java.awt.event.ActionListener() + { + public void actionPerformed(java.awt.event.ActionEvent evt) + { + cancelButtonActionPerformed(evt); + } + }); + + jPanel6.add(cancelButton); + + getContentPane().add(jPanel6, java.awt.BorderLayout.SOUTH); + + pack(); + }//GEN-END:initComponents + + private void cancelButtonActionPerformed(java.awt.event.ActionEvent evt) + {//GEN-FIRST:event_cancelButtonActionPerformed + dispose(); + }//GEN-LAST:event_cancelButtonActionPerformed + + private void okayButtonActionPerformed(java.awt.event.ActionEvent evt) + {//GEN-FIRST:event_okayButtonActionPerformed + double d = 0.0; + try { + d = Double.parseDouble(timeField.getText()); + if (d < 0) + throw new NumberFormatException(); + } catch (NumberFormatException e) { + JOptionPane.showMessageDialog(this, "Error: Invalid time value.", "Error", JOptionPane.ERROR_MESSAGE); + return; + } + time = d; + first = false; + cancelled = false; + dispose(); + }//GEN-LAST:event_okayButtonActionPerformed + + // Variables declaration - do not modify//GEN-BEGIN:variables + private javax.swing.JButton cancelButton; + private javax.swing.JLabel jLabel1; + private javax.swing.JPanel jPanel1; + private javax.swing.JPanel jPanel2; + private javax.swing.JPanel jPanel3; + private javax.swing.JPanel jPanel4; + private javax.swing.JPanel jPanel5; + private javax.swing.JPanel jPanel6; + private javax.swing.JButton okayButton; + private javax.swing.JTextField timeField; + // End of variables declaration//GEN-END:variables +} diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index f7938591..3eadbb7e 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -73,7 +73,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect private SimulationView view; //Actions - private Action randomExploration, backtrack, backtrackToHere, removeToHere, newPath, newPathFromState, resetPath, exportPath, plotPath, configureView; + private Action randomExploration, backtrack, backtrackToHere, removeToHere, newPath, newPathFromState, newPathPlot, newPathPlotFromState, resetPath, + exportPath, plotPath, configureView; /** Creates a new instance of GUISimulator */ public GUISimulator(GUIPrism gui) @@ -299,6 +300,20 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } } + public void a_clearPath() + { + // Update path/tables/lists + setPathActive(false); + pathTableModel.restartPathTable(); + updateTableModel.restartUpdatesTable(); + ((GUISimLabelList) stateLabelList).clearLabels(); + ((GUISimPathFormulaeList) pathFormulaeList).clearList(); + // Update display + repaintLists(); + updatePathInfoAll(null); + doEnables(); + } + public void a_newPath(boolean chooseInitialState) { Values initialState; @@ -339,43 +354,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect if (!chooseInitialState) { initialState = null; } - // yes: + // yes: user chooses else { - // first, pick default values for chooser dialog - - // default initial state if none specified previously - if (lastInitialState == null) { - lastInitialState = new Values(parsedModel.getDefaultInitialState(), parsedModel); - } - // otherwise, check previously used state for validity - else { - boolean match = true; - int i, n; - n = parsedModel.getNumVars(); - if (lastInitialState.getNumValues() != n) { - match = false; - } else { - for (i = 0; i < n; i++) { - if (!lastInitialState.contains(parsedModel.getVarName(i))) { - match = false; - break; - } else { - int index = lastInitialState.getIndexOf(parsedModel.getVarName(i)); - if (!lastInitialState.getType(index).equals(parsedModel.getVarType(i))) { - match = false; - break; - } - } - } - } - // if there's a problem, just use the default - if (!match) { - lastInitialState = new Values(parsedModel.getDefaultInitialState(), parsedModel); - } - } - - initialState = null; - initialState = GUIInitialStatePicker.defineInitalValuesWithDialog(getGUI(), lastInitialState, parsedModel); + initialState = a_chooseInitialState(); // if user clicked cancel from dialog, bail out if (initialState == null) { return; @@ -402,7 +383,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect updatePathInfoAll(uCon); doEnables(); - // store inital state for next time + // store initial state for next time lastInitialState = initialState; if (getPrism().getSettings().getBoolean(PrismSettings.SIMULATOR_NEW_PATH_ASK_VIEW)) { @@ -418,6 +399,46 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } } + public Values a_chooseInitialState() throws PrismLangException + { + // first, pick default values for chooser dialog + + // default initial state if none specified previously + if (lastInitialState == null) { + lastInitialState = new Values(parsedModel.getDefaultInitialState(), parsedModel); + } + // otherwise, check previously used state for validity + else { + boolean match = true; + int i, n; + n = parsedModel.getNumVars(); + if (lastInitialState.getNumValues() != n) { + match = false; + } else { + for (i = 0; i < n; i++) { + if (!lastInitialState.contains(parsedModel.getVarName(i))) { + match = false; + break; + } else { + int index = lastInitialState.getIndexOf(parsedModel.getVarName(i)); + if (!lastInitialState.getType(index).equals(parsedModel.getVarType(i))) { + match = false; + break; + } + } + } + } + // if there's a problem, just use the default + if (!match) { + lastInitialState = new Values(parsedModel.getDefaultInitialState(), parsedModel); + } + } + + Values initialState = null; + initialState = GUIInitialStatePicker.defineInitalValuesWithDialog(getGUI(), lastInitialState, parsedModel); + return initialState; + } + /** Explore a number of steps. */ public void a_autoStep(int noSteps) { @@ -447,7 +468,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect repaintLists(); updatePathInfo(); setComputing(false); - + } catch (PrismException e) { this.error(e.getMessage()); guiMultiModel.getHandler().modelParseFailed((PrismLangException) e, false); @@ -594,7 +615,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect repaintLists(); updatePathInfo(); setComputing(false); - + } catch (NumberFormatException e) { this.error("The Auto update \'no. steps\' parameter is invalid.\nIt must be a positive integer representing a step in the path table"); setComputing(false); @@ -656,12 +677,84 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect public void a_plotPath() { - setComputing(true); - guiProp.tabToFront(); - Graph graphModel = new Graph(); - guiProp.getGraphHandler().addGraph(graphModel); - engine.plotPath(graphModel); - setComputing(false); + try { + setComputing(true); + guiProp.tabToFront(); + Graph graphModel = new Graph(); + guiProp.getGraphHandler().addGraph(graphModel); + engine.plotPath(graphModel); + setComputing(false); + } catch (PrismException e) { + error(e.getMessage()); + } + } + + public void a_newPathPlot(boolean chooseInitialState) + { + Values initialState; + try { + // if necessary, get values for undefined constants from user + UndefinedConstants uCon = new UndefinedConstants(parsedModel, null); + if (uCon.getMFNumUndefined() > 0) { + int result = GUIConstantsPicker.defineConstantsWithDialog(getGUI(), uCon, lastConstants, lastPropertyConstants); + if (result != GUIConstantsPicker.VALUES_DONE) + return; + } + // remember constant values for next time + lastConstants = uCon.getMFConstantValues(); + // 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) { + initialState = null; + } + // yes: user chooses + else { + initialState = a_chooseInitialState(); + // if user clicked cancel from dialog, bail out + if (initialState == null) { + return; + } + } + + // Get a time limit from user + int result = GUIPathPlotDialog.requestTime(this.getGUI()); + if (result != GUIPathPlotDialog.OK) { + return; + } + + // Create a new path in the simulator and plot it + a_clearPath(); + setComputing(true); + 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); + //String simPathDetails = "time=" + GUIPathPlotDialog.getTime() + ",snapshot=" + GUIPathPlotDialog.getTime()/500; + String simPathDetails = "time=" + GUIPathPlotDialog.getTime(); + genPath.generateAndPlotSimulationPathInThread(parsedModel, initialStateObject, simPathDetails, maxPathLength, graphModel); + setComputing(false); + + // store initial state for next time + lastInitialState = initialState; + + } catch (PrismException e) { + this.error(e.getMessage()); + if (e instanceof PrismLangException) { + guiMultiModel.getHandler().modelParseFailed((PrismLangException) e, false); + guiMultiModel.tabToFront(); + } + } } public void a_configureView() @@ -701,18 +794,19 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // Path formulas GUISimPathFormulaeList thePathFormulaeList = (GUISimPathFormulaeList) pathFormulaeList; thePathFormulaeList.clearList(); - if (1==2) if (pathActive) { - // Go through the property list from the Properties tab of GUI - GUIPropertiesList gpl = guiProp.getPropList(); - for (int i = 0; i < gpl.getNumProperties(); i++) { - GUIProperty gp = gpl.getProperty(i); - // For properties which are simulate-able... - if (gp.isValidForSimulation()) { - // Add them to the list - thePathFormulaeList.addProperty(gp.getProperty(), propertiesFile); + if (1 == 2) + if (pathActive) { + // Go through the property list from the Properties tab of GUI + GUIPropertiesList gpl = guiProp.getPropList(); + for (int i = 0; i < gpl.getNumProperties(); i++) { + GUIProperty gp = gpl.getProperty(i); + // For properties which are simulate-able... + if (gp.isValidForSimulation()) { + // Add them to the list + thePathFormulaeList.addProperty(gp.getProperty(), propertiesFile); + } } } - } } //METHODS TO IMPLEMENT THE GUIPLUGIN INTERFACE @@ -813,6 +907,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect { newPath.setEnabled(parsedModel != null && !computing); newPathFromState.setEnabled(parsedModel != null && !computing); + newPathPlot.setEnabled(parsedModel != null && !computing); + newPathPlotFromState.setEnabled(parsedModel != null && !computing); resetPath.setEnabled(pathActive && !computing); exportPath.setEnabled(pathActive && !computing); plotPath.setEnabled(pathActive && !computing); @@ -1446,6 +1542,30 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect newPathFromState.putValue(Action.NAME, "New path from state"); newPathFromState.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallStates.png")); + newPathPlot = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_newPathPlot(false); + } + }; + newPathPlot.putValue(Action.LONG_DESCRIPTION, "Creates and plots a new path."); + //newPathPlot.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_N)); + newPathPlot.putValue(Action.NAME, "Plot new path"); + newPathPlot.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileGraph.png")); + + newPathPlotFromState = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + a_newPathPlot(true); + } + }; + newPathPlotFromState.putValue(Action.LONG_DESCRIPTION, "Creates and plots a new path from a chosen state."); + //newPathPlotFromState.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_N)); + newPathPlotFromState.putValue(Action.NAME, "Plot new path from state"); + newPathPlotFromState.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileGraph.png")); + resetPath = new AbstractAction() { public void actionPerformed(ActionEvent e) @@ -1480,7 +1600,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect a_plotPath(); } }; - plotPath.putValue(Action.LONG_DESCRIPTION, "Plots the path on a graph."); plotPath.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_P)); plotPath.putValue(Action.NAME, "Plot path"); @@ -1556,6 +1675,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect pathPopupMenu = new JPopupMenu(); pathPopupMenu.add(newPath); pathPopupMenu.add(newPathFromState); + pathPopupMenu.add(newPathPlot); + pathPopupMenu.add(newPathPlotFromState); + pathPopupMenu.addSeparator(); pathPopupMenu.add(resetPath); pathPopupMenu.add(exportPath); pathPopupMenu.add(plotPath); @@ -1570,6 +1692,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect simulatorMenu = new JMenu("Simulator"); simulatorMenu.add(newPath); simulatorMenu.add(newPathFromState); + simulatorMenu.add(newPathPlot); + simulatorMenu.add(newPathPlotFromState); + simulatorMenu.addSeparator(); simulatorMenu.add(resetPath); simulatorMenu.add(exportPath); simulatorMenu.add(plotPath);