Browse Source

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
master
Dave Parker 14 years ago
parent
commit
992c0864dc
  1. 293
      prism/src/simulator/GenerateSimulationPath.java
  2. 34
      prism/src/simulator/Path.java
  3. 166
      prism/src/simulator/PathDisplayer.java
  4. 220
      prism/src/simulator/PathFull.java
  5. 30
      prism/src/simulator/PathFullPrefix.java
  6. 44
      prism/src/simulator/PathOnTheFly.java
  7. 121
      prism/src/simulator/PathToGraph.java
  8. 272
      prism/src/simulator/PathToText.java
  9. 25
      prism/src/simulator/SimulatorEngine.java
  10. 191
      prism/src/userinterface/simulator/GUIPathPlotDialog.java
  11. 239
      prism/src/userinterface/simulator/GUISimulator.java

293
prism/src/simulator/GenerateSimulationPath.java

@ -32,6 +32,7 @@ import java.util.ArrayList;
import prism.*; import prism.*;
import parser.*; import parser.*;
import parser.ast.*; import parser.ast.*;
import userinterface.graph.Graph;
public class GenerateSimulationPath public class GenerateSimulationPath
{ {
@ -49,7 +50,7 @@ public class GenerateSimulationPath
private State initialState; private State initialState;
private int maxPathLength; private int maxPathLength;
private File file; private File file;
// Path configuration options // Path configuration options
private PathType simPathType = null; private PathType simPathType = null;
private int simPathLength = 0; private int simPathLength = 0;
@ -58,6 +59,9 @@ public class GenerateSimulationPath
private ArrayList<Integer> simVars = null; private ArrayList<Integer> simVars = null;
private boolean simLoopCheck = true; private boolean simLoopCheck = true;
private int simPathRepeat = 1; private int simPathRepeat = 1;
private boolean simPathShowRewards = false;
private boolean simPathSnapshots = false;
private double simPathSnapshotTime = 0.0;
public GenerateSimulationPath(SimulatorEngine engine, PrismLog mainLog) public GenerateSimulationPath(SimulatorEngine engine, PrismLog mainLog)
{ {
@ -72,15 +76,52 @@ public class GenerateSimulationPath
* @param details Information about the path to be generated * @param details Information about the path to be generated
* @param file File to output the path to (stdout if null) * @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.modulesFile = modulesFile;
this.initialState = initialState; this.initialState = initialState;
this.maxPathLength = maxPathLength; this.maxPathLength = maxPathLength;
this.file = file; this.file = file;
parseDetails(details); 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) { } catch (NumberFormatException e) {
throw new PrismException("Value for \"repeat\" option must be a positive integer"); 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 { } else {
// path of fixed number of steps // path of fixed number of steps
simPathType = PathType.SIM_PATH_NUM_STEPS; simPathType = PathType.SIM_PATH_NUM_STEPS;
@ -181,25 +235,71 @@ public class GenerateSimulationPath
if (simPathLength < 0) if (simPathLength < 0)
throw new NumberFormatException(); throw new NumberFormatException();
} catch (NumberFormatException e) { } catch (NumberFormatException e) {
throw new PrismException("Invalid path length \"" + ss[i] + "\"");
throw new PrismException("Invalid path option \"" + ss[i] + "\"");
} }
} }
} }
if (simPathType == null) if (simPathType == null)
throw new PrismException("Invalid path details \"" + details + "\""); 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; boolean done;
double t = 0.0;
boolean stochastic = (modulesFile.getModelType() == ModelType.CTMC);
// print details
// Print details
switch (simPathType) { switch (simPathType) {
case SIM_PATH_NUM_STEPS: case SIM_PATH_NUM_STEPS:
mainLog.println("\nGenerating random path of length " + simPathLength + " steps..."); mainLog.println("\nGenerating random path of length " + simPathLength + " steps...");
@ -207,83 +307,164 @@ public class GenerateSimulationPath
case SIM_PATH_TIME: case SIM_PATH_TIME:
mainLog.println("\nGenerating random path with time limit " + simPathTime + "..."); mainLog.println("\nGenerating random path with time limit " + simPathTime + "...");
break; 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); engine.createNewPath(modulesFile);
// Build path
for (j = 0; j < simPathRepeat; j++) { for (j = 0; j < simPathRepeat; j++) {
path = engine.getPath();
engine.initialisePath(initialState); engine.initialisePath(initialState);
i = 0; i = 0;
t = 0.0;
done = false; done = false;
while (!done) { 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(); 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) { 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: case SIM_PATH_DEADLOCK:
if (engine.queryIsDeadlock() || i >= maxPathLength) if (engine.queryIsDeadlock() || i >= maxPathLength)
done = true; done = true;
break; 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()) if (simLoopCheck && engine.isPathLooping())
break; 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; break;
} }
if (j < simPathRepeat) if (j < simPathRepeat)
j++; 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"); mainLog.print("\nNo deadlock state found within " + maxPathLength + " steps");
if (simPathRepeat > 1) if (simPathRepeat > 1)
mainLog.print(" (generated " + simPathRepeat + " paths)"); mainLog.print(" (generated " + simPathRepeat + " paths)");
mainLog.println("."); 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 { } 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
}
} }
} }
} }

34
prism/src/simulator/Path.java

@ -76,9 +76,20 @@ public abstract class Path
public abstract State getCurrentState(); 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(); public abstract double getTotalTime();
@ -101,12 +112,23 @@ public abstract class Path
*/ */
public abstract double getPreviousStateReward(int rsi); 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. * Get the transition reward for the transition between the previous and current states.
* @param rsi Reward structure index * @param rsi Reward structure index
*/ */
public abstract double getPreviousTransitionReward(int rsi); 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. * Get the state reward for the current state.
* (For continuous-time models, need to multiply this by time spent in the 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); 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? * Does the path contain a deterministic loop?
*/ */

166
prism/src/simulator/PathDisplayer.java

@ -0,0 +1,166 @@
//==============================================================================
//
// 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 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<Integer> 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<Integer> varsToShow)
{
// Take a copy of var index list
this.varsToShow = varsToShow == null ? null : new ArrayList<Integer>(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();
}

220
prism/src/simulator/PathFull.java

@ -27,10 +27,11 @@
package simulator; package simulator;
import java.util.ArrayList; import java.util.ArrayList;
import org.jfree.data.xy.XYDataItem; import org.jfree.data.xy.XYDataItem;
import parser.*;
import parser.ast.*;
import parser.State;
import parser.ast.ModulesFile;
import prism.PrismException; import prism.PrismException;
import prism.PrismLog; import prism.PrismLog;
import userinterface.graph.Graph; import userinterface.graph.Graph;
@ -108,7 +109,7 @@ public class PathFull extends Path implements PathFullInfo
@Override @Override
public void addStep(int choice, int moduleOrActionIndex, double[] transitionRewards, State newState, double[] newStateRewards, TransitionList transitionList) 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 @Override
@ -233,6 +234,24 @@ public class PathFull extends Path implements PathFullInfo
return steps.get(steps.size() - 1).state; 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 @Override
public double getTotalTime() public double getTotalTime()
{ {
@ -257,18 +276,36 @@ public class PathFull extends Path implements PathFullInfo
return steps.get(steps.size() - 2).stateRewards[rsi]; return steps.get(steps.size() - 2).stateRewards[rsi];
} }
@Override
public double[] getPreviousStateRewards()
{
return steps.get(steps.size() - 2).stateRewards;
}
@Override @Override
public double getPreviousTransitionReward(int rsi) public double getPreviousTransitionReward(int rsi)
{ {
return steps.get(steps.size() - 2).transitionRewards[rsi]; return steps.get(steps.size() - 2).transitionRewards[rsi];
} }
@Override
public double[] getPreviousTransitionRewards()
{
return steps.get(steps.size() - 2).transitionRewards;
}
@Override @Override
public double getCurrentStateReward(int rsi) public double getCurrentStateReward(int rsi)
{ {
return steps.get(steps.size() - 1).stateRewards[rsi]; return steps.get(steps.size() - 1).stateRewards[rsi];
} }
@Override
public double[] getCurrentStateRewards()
{
return steps.get(steps.size() - 1).stateRewards;
}
@Override @Override
public boolean isLooping() public boolean isLooping()
{ {
@ -308,6 +345,15 @@ public class PathFull extends Path implements PathFullInfo
return steps.get(step).stateRewards[rsi]; 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. * Get the total time spent up until entering a given step of the path.
* @param step Step index (0 = initial state/step of 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]; 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 @Override
public boolean hasRewardInfo() public boolean hasRewardInfo()
{ {
@ -414,114 +469,62 @@ public class PathFull extends Path implements PathFullInfo
// Other methods // 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<Integer> 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) { if (modulesFile == null) {
log.flush();
log.close();
return; 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<Integer> 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. * 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 @Override
@ -575,9 +578,9 @@ public class PathFull extends Path implements PathFullInfo
{ {
private Graph graphModel = null; private Graph graphModel = null;
public PlotOnGraphThread(Graph graphmodel)
public PlotOnGraphThread(Graph graphModel)
{ {
this.graphModel = graphmodel;
this.graphModel = graphModel;
} }
public void run() 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
}
}
}
} }

30
prism/src/simulator/PathFullPrefix.java

@ -101,6 +101,18 @@ public class PathFullPrefix extends Path
return pathFull.getState(prefixLength); return pathFull.getState(prefixLength);
} }
@Override
public int getPreviousModuleOrActionIndex()
{
return pathFull.getModuleOrActionIndex(prefixLength - 1);
}
@Override
public String getPreviousModuleOrAction()
{
return pathFull.getModuleOrAction(prefixLength - 1);
}
@Override @Override
public double getTotalTime() public double getTotalTime()
{ {
@ -125,18 +137,36 @@ public class PathFullPrefix extends Path
return pathFull.getStateReward(prefixLength - 1, rsi); return pathFull.getStateReward(prefixLength - 1, rsi);
} }
@Override
public double[] getPreviousStateRewards()
{
return pathFull.getStateRewards(prefixLength - 1);
}
@Override @Override
public double getPreviousTransitionReward(int rsi) public double getPreviousTransitionReward(int rsi)
{ {
return pathFull.getTransitionReward(prefixLength - 1, rsi); return pathFull.getTransitionReward(prefixLength - 1, rsi);
} }
@Override
public double[] getPreviousTransitionRewards()
{
return pathFull.getTransitionRewards(prefixLength - 1);
}
@Override @Override
public double getCurrentStateReward(int rsi) public double getCurrentStateReward(int rsi)
{ {
return pathFull.getStateReward(prefixLength, rsi); return pathFull.getStateReward(prefixLength, rsi);
} }
@Override
public double[] getCurrentStateRewards()
{
return pathFull.getStateRewards(prefixLength);
}
@Override @Override
public boolean isLooping() public boolean isLooping()
{ {

44
prism/src/simulator/PathOnTheFly.java

@ -46,6 +46,7 @@ public class PathOnTheFly extends Path
protected int size; protected int size;
protected State previousState; protected State previousState;
protected State currentState; protected State currentState;
protected int previousModuleOrActionIndex;
protected double totalTime; protected double totalTime;
double timeInPreviousState; double timeInPreviousState;
protected double totalRewards[]; protected double totalRewards[];
@ -113,17 +114,18 @@ public class PathOnTheFly extends Path
} }
@Override @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 @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++; size++;
previousState.copy(currentState); previousState.copy(currentState);
currentState.copy(newState); currentState.copy(newState);
previousModuleOrActionIndex = moduleOrActionIndex;
totalTime += time; totalTime += time;
timeInPreviousState = time; timeInPreviousState = time;
for (int i = 0; i < numRewardStructs; i++) { for (int i = 0; i < numRewardStructs; i++) {
@ -166,6 +168,24 @@ public class PathOnTheFly extends Path
return currentState; 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 @Override
public double getTotalTime() public double getTotalTime()
{ {
@ -190,18 +210,36 @@ public class PathOnTheFly extends Path
return previousStateRewards[rsi]; return previousStateRewards[rsi];
} }
@Override
public double[] getPreviousStateRewards()
{
return previousStateRewards;
}
@Override @Override
public double getPreviousTransitionReward(int rsi) public double getPreviousTransitionReward(int rsi)
{ {
return previousTransitionRewards[rsi]; return previousTransitionRewards[rsi];
} }
@Override
public double[] getPreviousTransitionRewards()
{
return previousTransitionRewards;
}
@Override @Override
public double getCurrentStateReward(int rsi) public double getCurrentStateReward(int rsi)
{ {
return currentStateRewards[rsi]; return currentStateRewards[rsi];
} }
@Override
public double[] getCurrentStateRewards()
{
return currentStateRewards;
}
@Override @Override
public boolean isLooping() public boolean isLooping()
{ {

121
prism/src/simulator/PathToGraph.java

@ -0,0 +1,121 @@
//==============================================================================
//
// 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 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);
}
}

272
prism/src/simulator/PathToText.java

@ -0,0 +1,272 @@
//==============================================================================
//
// 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 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();
}
}
}

25
prism/src/simulator/SimulatorEngine.java

@ -1007,6 +1007,15 @@ public class SimulatorEngine
// Querying of current path (full or on-the-fly) // 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). * 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() public double getTotalTimeForPath()
{ {
@ -1225,8 +1241,9 @@ public class SimulatorEngine
/** /**
* Plot the current path on a Graph. * 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); ((PathFull) path).plotOnGraph(graphModel);
} }

191
prism/src/userinterface/simulator/GUIPathPlotDialog.java

@ -0,0 +1,191 @@
//==============================================================================
//
// 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 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
}

239
prism/src/userinterface/simulator/GUISimulator.java

@ -73,7 +73,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
private SimulationView view; private SimulationView view;
//Actions //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 */ /** Creates a new instance of GUISimulator */
public GUISimulator(GUIPrism gui) 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) public void a_newPath(boolean chooseInitialState)
{ {
Values initialState; Values initialState;
@ -339,43 +354,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
if (!chooseInitialState) { if (!chooseInitialState) {
initialState = null; initialState = null;
} }
// yes:
// yes: user chooses
else { 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 user clicked cancel from dialog, bail out
if (initialState == null) { if (initialState == null) {
return; return;
@ -402,7 +383,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
updatePathInfoAll(uCon); updatePathInfoAll(uCon);
doEnables(); doEnables();
// store inital state for next time
// store initial state for next time
lastInitialState = initialState; lastInitialState = initialState;
if (getPrism().getSettings().getBoolean(PrismSettings.SIMULATOR_NEW_PATH_ASK_VIEW)) { 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. */ /** Explore a number of steps. */
public void a_autoStep(int noSteps) public void a_autoStep(int noSteps)
{ {
@ -447,7 +468,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
repaintLists(); repaintLists();
updatePathInfo(); updatePathInfo();
setComputing(false); setComputing(false);
} catch (PrismException e) { } catch (PrismException e) {
this.error(e.getMessage()); this.error(e.getMessage());
guiMultiModel.getHandler().modelParseFailed((PrismLangException) e, false); guiMultiModel.getHandler().modelParseFailed((PrismLangException) e, false);
@ -594,7 +615,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
repaintLists(); repaintLists();
updatePathInfo(); updatePathInfo();
setComputing(false); setComputing(false);
} catch (NumberFormatException e) { } 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"); 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); setComputing(false);
@ -656,12 +677,84 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
public void a_plotPath() 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() public void a_configureView()
@ -701,18 +794,19 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
// Path formulas // Path formulas
GUISimPathFormulaeList thePathFormulaeList = (GUISimPathFormulaeList) pathFormulaeList; GUISimPathFormulaeList thePathFormulaeList = (GUISimPathFormulaeList) pathFormulaeList;
thePathFormulaeList.clearList(); 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 //METHODS TO IMPLEMENT THE GUIPLUGIN INTERFACE
@ -813,6 +907,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
{ {
newPath.setEnabled(parsedModel != null && !computing); newPath.setEnabled(parsedModel != null && !computing);
newPathFromState.setEnabled(parsedModel != null && !computing); newPathFromState.setEnabled(parsedModel != null && !computing);
newPathPlot.setEnabled(parsedModel != null && !computing);
newPathPlotFromState.setEnabled(parsedModel != null && !computing);
resetPath.setEnabled(pathActive && !computing); resetPath.setEnabled(pathActive && !computing);
exportPath.setEnabled(pathActive && !computing); exportPath.setEnabled(pathActive && !computing);
plotPath.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.NAME, "New path from state");
newPathFromState.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallStates.png")); 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() resetPath = new AbstractAction()
{ {
public void actionPerformed(ActionEvent e) public void actionPerformed(ActionEvent e)
@ -1480,7 +1600,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
a_plotPath(); a_plotPath();
} }
}; };
plotPath.putValue(Action.LONG_DESCRIPTION, "Plots the path on a graph."); plotPath.putValue(Action.LONG_DESCRIPTION, "Plots the path on a graph.");
plotPath.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_P)); plotPath.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_P));
plotPath.putValue(Action.NAME, "Plot path"); plotPath.putValue(Action.NAME, "Plot path");
@ -1556,6 +1675,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
pathPopupMenu = new JPopupMenu(); pathPopupMenu = new JPopupMenu();
pathPopupMenu.add(newPath); pathPopupMenu.add(newPath);
pathPopupMenu.add(newPathFromState); pathPopupMenu.add(newPathFromState);
pathPopupMenu.add(newPathPlot);
pathPopupMenu.add(newPathPlotFromState);
pathPopupMenu.addSeparator();
pathPopupMenu.add(resetPath); pathPopupMenu.add(resetPath);
pathPopupMenu.add(exportPath); pathPopupMenu.add(exportPath);
pathPopupMenu.add(plotPath); pathPopupMenu.add(plotPath);
@ -1570,6 +1692,9 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
simulatorMenu = new JMenu("Simulator"); simulatorMenu = new JMenu("Simulator");
simulatorMenu.add(newPath); simulatorMenu.add(newPath);
simulatorMenu.add(newPathFromState); simulatorMenu.add(newPathFromState);
simulatorMenu.add(newPathPlot);
simulatorMenu.add(newPathPlotFromState);
simulatorMenu.addSeparator();
simulatorMenu.add(resetPath); simulatorMenu.add(resetPath);
simulatorMenu.add(exportPath); simulatorMenu.add(exportPath);
simulatorMenu.add(plotPath); simulatorMenu.add(plotPath);

Loading…
Cancel
Save