diff --git a/prism/src/simulator/PathFull.java b/prism/src/simulator/PathFull.java index ca5f2cf0..65751e88 100644 --- a/prism/src/simulator/PathFull.java +++ b/prism/src/simulator/PathFull.java @@ -27,11 +27,14 @@ package simulator; import java.util.ArrayList; +import org.jfree.data.xy.XYDataItem; import parser.*; import parser.ast.*; import prism.PrismException; import prism.PrismLog; +import userinterface.graph.Graph; +import userinterface.graph.Graph.SeriesKey; /** * Stores and manipulates a path though a model. @@ -513,6 +516,14 @@ public class PathFull extends Path implements PathFullInfo log.close(); } + /** + * Plot path on a graph. + */ + public void plotOnGraph(Graph graphModel) + { + new PlotOnGraphThread(graphModel).start(); + } + @Override public String toString() { @@ -559,4 +570,51 @@ public class PathFull extends Path implements PathFullInfo // Transition rewards associated with step public double transitionRewards[]; } + + class PlotOnGraphThread extends Thread + { + private Graph graphModel = null; + + public PlotOnGraphThread(Graph graphmodel) + { + this.graphModel = graphmodel; + } + + public void run() + { + int i, j, n, nv; + double d, t; + boolean contTime = modulesFile.getModelType().continuousTime(); + SeriesKey seriesKeys[] = null; + + // Configure axes + graphModel.getXAxisSettings().setHeading("Time"); + graphModel.getYAxisSettings().setHeading("Value"); + + // Get sizes + n = size(); + nv = modulesFile.getNumVars(); + + // Create series + seriesKeys = new SeriesKey[nv]; + for (j = 0; j < nv; j++) { + seriesKeys[j] = graphModel.addSeries(modulesFile.getVarName(j)); + } + + // Plot path + t = 0.0; + for (i = 0; i <= n; i++) { + if (contTime) { + d = (i < n) ? getTime(i) : 0.0; + t += d; + } + for (j = 0; j < nv; j++) { + // Always plot first/last points to ensure complete line. + // Otherwise only add a point if the variable value changed. + if (i == 0 || i == n-1 || !PathFull.this.getState(i).varValues[j].equals(PathFull.this.getState(i - 1).varValues[j])) + graphModel.addPointToSeries(seriesKeys[j], new XYDataItem(contTime ? t : i, ((Integer) PathFull.this.getState(i).varValues[j]).intValue())); + } + } + } + } } diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index b4fb0242..613939fc 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ b/prism/src/simulator/SimulatorEngine.java @@ -31,6 +31,7 @@ import java.io.*; import simulator.method.*; import simulator.sampler.*; +import userinterface.graph.Graph; import parser.*; import parser.ast.*; import parser.type.*; @@ -1221,6 +1222,14 @@ public class SimulatorEngine } ((PathFull) path).exportToLog(log, timeCumul, colSep, vars); } + + /** + * Plot the current path on a Graph. + */ + public void plotPath(Graph graphModel) + { + ((PathFull) path).plotOnGraph(graphModel); + } // ------------------------------------------------------------------------------ // Model checking (approximate) diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index 7bb1b412..ce048316 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -231,6 +231,11 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List return getPrism().getSettings().getInteger(PrismSettings.PROPERTIES_ADDITION_STRATEGY) + 1; //note the correction } + public GUIGraphHandler getGraphHandler() + { + return graphHandler; + } + /* UPDATE METHODS */ public void repaintList() diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index 3e9536cc..f7938591 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -41,6 +41,7 @@ import parser.ast.*; import prism.*; import userinterface.*; import userinterface.util.*; +import userinterface.graph.Graph; import userinterface.model.*; import userinterface.properties.*; import userinterface.simulator.networking.*; @@ -72,7 +73,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect private SimulationView view; //Actions - private Action randomExploration, backtrack, backtrackToHere, removeToHere, newPath, newPathFromState, resetPath, exportPath, configureView; + private Action randomExploration, backtrack, backtrackToHere, removeToHere, newPath, newPathFromState, resetPath, exportPath, plotPath, configureView; /** Creates a new instance of GUISimulator */ public GUISimulator(GUIPrism gui) @@ -653,6 +654,16 @@ 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); + } + public void a_configureView() { new GUIViewDialog(getGUI(), pathTableModel.getView(), pathTableModel); @@ -804,6 +815,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect newPathFromState.setEnabled(parsedModel != null && !computing); resetPath.setEnabled(pathActive && !computing); exportPath.setEnabled(pathActive && !computing); + plotPath.setEnabled(pathActive && !computing); randomExploration.setEnabled(pathActive && !computing); backtrack.setEnabled(pathActive && !computing); configureView.setEnabled(pathActive && !computing); @@ -1461,6 +1473,19 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect exportPath.putValue(Action.NAME, "Export path"); exportPath.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallExport.png")); + plotPath = new AbstractAction() + { + public void actionPerformed(ActionEvent e) + { + 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"); + plotPath.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFileGraph.png")); + randomExploration = new AbstractAction() { public void actionPerformed(ActionEvent e) @@ -1533,6 +1558,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect pathPopupMenu.add(newPathFromState); pathPopupMenu.add(resetPath); pathPopupMenu.add(exportPath); + pathPopupMenu.add(plotPath); pathPopupMenu.addSeparator(); pathPopupMenu.add(randomExploration); pathPopupMenu.add(backtrack); @@ -1546,6 +1572,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect simulatorMenu.add(newPathFromState); simulatorMenu.add(resetPath); simulatorMenu.add(exportPath); + simulatorMenu.add(plotPath); simulatorMenu.addSeparator(); simulatorMenu.add(randomExploration); simulatorMenu.add(backtrack);