s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

GUI simulation path plot and can show vars and/or rewards. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5400 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 14 years ago
parent
a28c14715c
commit
6d502769be
3 changed files with 113 additions and 24 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 1
      prism/src/simulator/GenerateSimulationPath.java
  2. 93
      prism/src/simulator/PathToGraph.java
  3. 43
      prism/src/userinterface/simulator/GUIPathPlotDialog.java

1
prism/src/simulator/GenerateSimulationPath.java
View File

@ -302,6 +302,7 @@ public class GenerateSimulationPath
PathToGraph displayer;
displayer = new PathToGraph(graphModel, modulesFile);
displayer.setVarsToShow(simVars);
displayer.setShowRewards(simPathShowRewards);
displayer.setShowChangesOnly(simPathShowChangesOnly);
if (simPathSnapshots)

93
prism/src/simulator/PathToGraph.java
View File

@ -26,6 +26,9 @@
package simulator;
import java.util.ArrayList;
import java.util.List;
import org.jfree.data.xy.XYDataItem;
import parser.State;
@ -42,7 +45,8 @@ public class PathToGraph extends PathDisplayer
{
/** Graph on which to plot path */
private Graph graphModel = null;
private SeriesKey seriesKeys[] = null;
private List<SeriesKey> varSeriesKeys = null;
private List<SeriesKey> rewardSeriesKeys = null;
// Model info
private ModulesFile modulesFile;
@ -53,6 +57,7 @@ public class PathToGraph extends PathDisplayer
/** Step counter */
private double lastTime;
private State lastState;
private double[] lastStateRewards;
/**
* Construct a {@link PathToGraph} object
@ -72,54 +77,100 @@ public class PathToGraph extends PathDisplayer
// Display methods
@Override
public void startDisplay(State initialState, double[] stateRewards)
public void startDisplay(State initialState, double[] initialStateRewards)
{
// 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));
varSeriesKeys = new ArrayList<Graph.SeriesKey>();
if (varsToShow == null) {
for (int j = 0; j < numVars; j++) {
varSeriesKeys.add(graphModel.addSeries(modulesFile.getVarName(j)));
}
} else {
for (int j = 0; j < numVars; j++) {
if (varsToShow != null && varsToShow.contains(j))
varSeriesKeys.add(graphModel.addSeries(modulesFile.getVarName(j)));
else
varSeriesKeys.add(null);
}
}
if (showRewards) {
rewardSeriesKeys = new ArrayList<Graph.SeriesKey>();
for (int j = 0; j < numRewardStructs; j++) {
rewardSeriesKeys.add(graphModel.addSeries(modulesFile.getRewardStruct(j).getName()));
}
}
// Display initial state
lastState = new State(initialState.varValues.length);
displayState(0.0, initialState, true);
if (showRewards)
lastStateRewards = explicit.Utils.cloneDoubleArray(initialStateRewards);
displayState(0.0, initialState, initialStateRewards, true);
}
@Override
public void displayStep(double timeSpent, double timeCumul, Object action, double[] transitionRewards, State newState, double[] newStateRewards)
{
displayState(timeCumul, newState, !showChangesOnly);
displayState(timeCumul, newState, newStateRewards, !showChangesOnly);
}
@Override
public void displaySnapshot(double timeCumul, State newState, double[] newStateRewards)
{
displayState(timeCumul, newState, true);
displayState(timeCumul, newState, newStateRewards, true);
}
private void displayState(double time, State state, boolean force)
private void displayState(double time, State state, double[] stateRewards, boolean force)
{
for (int j = 0; j < numVars; j++) {
Object val = state.varValues[j];
double d = 0.0;
if (force || !val.equals(lastState.varValues[j])) {
try {
d = TypeDouble.getInstance().castValueTo(val).doubleValue();
graphModel.addPointToSeries(seriesKeys[j], new XYDataItem(time, d));
} catch (PrismException e) {
if (val instanceof Boolean) {
d = ((Boolean) val).booleanValue() ? 1.0 : 0.0;
graphModel.addPointToSeries(seriesKeys[j], new XYDataItem(time, d));
if (varsToShow == null) {
for (int j = 0; j < numVars; j++) {
Object val = state.varValues[j];
double d = 0.0;
if (force || !val.equals(lastState.varValues[j])) {
try {
d = TypeDouble.getInstance().castValueTo(val).doubleValue();
graphModel.addPointToSeries(varSeriesKeys.get(j), new XYDataItem(time, d));
} catch (PrismException e) {
if (val instanceof Boolean) {
d = ((Boolean) val).booleanValue() ? 1.0 : 0.0;
graphModel.addPointToSeries(varSeriesKeys.get(j), new XYDataItem(time, d));
}
}
}
}
} else {
for (int j : varsToShow) {
Object val = state.varValues[j];
double d = 0.0;
if (force || !val.equals(lastState.varValues[j])) {
try {
d = TypeDouble.getInstance().castValueTo(val).doubleValue();
graphModel.addPointToSeries(varSeriesKeys.get(j), new XYDataItem(time, d));
} catch (PrismException e) {
if (val instanceof Boolean) {
d = ((Boolean) val).booleanValue() ? 1.0 : 0.0;
graphModel.addPointToSeries(varSeriesKeys.get(j), new XYDataItem(time, d));
}
}
}
}
}
if (showRewards) {
for (int j = 0; j < numRewardStructs; j++) {
double d = stateRewards[j];
if (force || lastStateRewards[j] != stateRewards[j]) {
graphModel.addPointToSeries(rewardSeriesKeys.get(j), new XYDataItem(time, d));
}
}
}
lastTime = time;
lastState.copy(state);
if (showRewards) {
explicit.Utils.copyDoubleArray(stateRewards, lastStateRewards);
}
}
@Override
@ -127,6 +178,6 @@ public class PathToGraph extends PathDisplayer
{
// Always display last points to ensure complete plot lines
// (it's OK to overwrite points)
displayState(lastTime, lastState, true);
displayState(lastTime, lastState, lastStateRewards, true);
}
}

43
prism/src/userinterface/simulator/GUIPathPlotDialog.java
View File

@ -45,6 +45,7 @@ import javax.swing.border.EmptyBorder;
import parser.ast.ModulesFile;
import userinterface.GUIPrism;
import javax.swing.JCheckBox;
@SuppressWarnings("serial")
public class GUIPathPlotDialog extends JDialog
@ -101,6 +102,9 @@ public class GUIPathPlotDialog extends JDialog
private JComboBox comboBoxSimulate;
private JButton okButton;
private JButton cancelButton;
private JLabel lblPlot;
private JCheckBox chckbxVariables;
private JCheckBox chckbxRewards;
/**
* Show "Path Plot Details" dialog, return settings as a simpath string.
@ -135,15 +139,15 @@ public class GUIPathPlotDialog extends JDialog
super(parent, "Path Plot Details", true);
this.gui = parent;
this.modulesFile = modulesFile;
setBounds(100, 100, 450, 154);
setBounds(100, 100, 450, 200);
getContentPane().setLayout(new BorderLayout());
contentPanel.setBorder(new EmptyBorder(5, 5, 5, 5));
getContentPane().add(contentPanel, BorderLayout.CENTER);
GridBagLayout gbl_contentPanel = new GridBagLayout();
gbl_contentPanel.columnWidths = new int[] { 20, 0, 0, 0, 60, 0 };
gbl_contentPanel.rowHeights = new int[] { 20, 0, 0, 0, 0 };
gbl_contentPanel.rowHeights = new int[] { 20, 0, 0, 0, 0, 0, 0 };
gbl_contentPanel.columnWeights = new double[] { 0.0, 0.0, 0.0, 0.0, 0.0, Double.MIN_VALUE };
gbl_contentPanel.rowWeights = new double[] { 0.0, 0.0, 0.0, 0.0, Double.MIN_VALUE };
gbl_contentPanel.rowWeights = new double[] { 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, Double.MIN_VALUE };
contentPanel.setLayout(gbl_contentPanel);
{
JLabel lblSimulate = new JLabel("Simulate:");
@ -248,6 +252,33 @@ public class GUIPathPlotDialog extends JDialog
buttonPane.add(cancelButton);
}
}
{
lblPlot = new JLabel("Plot:");
GridBagConstraints gbc_lblPlot = new GridBagConstraints();
gbc_lblPlot.anchor = GridBagConstraints.EAST;
gbc_lblPlot.insets = new Insets(0, 0, 5, 5);
gbc_lblPlot.gridx = 1;
gbc_lblPlot.gridy = 3;
contentPanel.add(lblPlot, gbc_lblPlot);
}
{
chckbxVariables = new JCheckBox("Variables");
GridBagConstraints gbc_chckbxVariables = new GridBagConstraints();
gbc_chckbxVariables.anchor = GridBagConstraints.WEST;
gbc_chckbxVariables.insets = new Insets(0, 0, 5, 5);
gbc_chckbxVariables.gridx = 2;
gbc_chckbxVariables.gridy = 3;
contentPanel.add(chckbxVariables, gbc_chckbxVariables);
}
{
chckbxRewards = new JCheckBox("Rewards");
GridBagConstraints gbc_chckbxRewards = new GridBagConstraints();
gbc_chckbxRewards.anchor = GridBagConstraints.WEST;
gbc_chckbxRewards.insets = new Insets(0, 0, 5, 5);
gbc_chckbxRewards.gridx = 2;
gbc_chckbxRewards.gridy = 4;
contentPanel.add(chckbxRewards, gbc_chckbxRewards);
}
// defaults for new creation
if (modulesFile.getModelType().continuousTime()) {
@ -259,6 +290,8 @@ public class GUIPathPlotDialog extends JDialog
textFieldInterval.setText("");
}
comboBoxShow.setSelectedItem(ShowChoice.CHANGES);
chckbxVariables.setSelected(true);
chckbxRewards.setSelected(false);
this.getRootPane().setDefaultButton(okButton);
setLocationRelativeTo(getParent()); // centre
@ -334,6 +367,10 @@ public class GUIPathPlotDialog extends JDialog
if ((ShowChoice) comboBoxShow.getSelectedItem() == ShowChoice.CHANGES) {
simPathString += ",changes=true";
}
if (!chckbxVariables.isSelected()) {
simPathString += ",vars=()";
}
simPathString += ",rewards=" + chckbxRewards.isSelected();
cancelled = false;
dispose();

Write Preview
Loading…
Cancel
Save