Improved "Path Plot Details" dialog.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5391 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/userinterface/simulator/GUIPathPlotDialog.java

@@ -26,166 +26,318 @@
 
 package userinterface.simulator;
 
-import javax.swing.*;
-import userinterface.*;
+import java.awt.BorderLayout;
+import java.awt.FlowLayout;
+import java.awt.GridBagConstraints;
+import java.awt.GridBagLayout;
+import java.awt.Insets;
+import java.awt.event.ActionEvent;
+import java.awt.event.ActionListener;
 
-public class GUIPathPlotDialog extends javax.swing.JDialog
-{
-	public static final int OK = 0;
-	public static final int CANCELLED = 1;
+import javax.swing.DefaultComboBoxModel;
+import javax.swing.JButton;
+import javax.swing.JComboBox;
+import javax.swing.JDialog;
+import javax.swing.JLabel;
+import javax.swing.JPanel;
+import javax.swing.JTextField;
+import javax.swing.border.EmptyBorder;
 
-	static double time = 0.0;
-	static boolean first = true;
+import parser.ast.ModulesFile;
+import userinterface.GUIPrism;
 
-	private boolean cancelled = true;
+@SuppressWarnings("serial")
+public class GUIPathPlotDialog extends JDialog
+{
+	// ComboBox enums
 
-	/** Call this static method to construct a new GUIPathPlotDialog to get a time value. */
-	public static int requestTime(GUIPrism parent)
+	public enum SimulateChoice {
+		STEP, TIME;
+		public String toString()
 		{
-		return new GUIPathPlotDialog(parent).requestTime();
+			switch (this) {
+			case STEP:
+				return "Up to step";
+			case TIME:
+				return "Up to time";
+			default:
+				return this.toString();
+			}
 		}
+	};
 
-	public int requestTime()
+	public enum ShowChoice {
+		ALL_STEPS, CHANGES, SNAPSHOTS;
+		public String toString()
 		{
-		setVisible(true);
-		return cancelled ? CANCELLED : OK;
+			switch (this) {
+			case ALL_STEPS:
+				return "All steps";
+			case CHANGES:
+				return "Changes";
+			case SNAPSHOTS:
+				return "Snapshots";
+			default:
+				return this.toString();
 			}
+		}
+	};
+
+	// Static instance
+	private static GUIPathPlotDialog instance = null;
 
-	public static double getTime()
+	// State
+	private GUIPrism gui;
+	private ModulesFile modulesFile;
+	private boolean cancelled;
+	private String simPathString;
+
+	// GUI objects
+	private final JPanel contentPanel = new JPanel();
+	private JTextField textFieldTime;
+	private JTextField textFieldInterval;
+	private JLabel lblInterval;
+	private JComboBox comboBoxShow;
+	private JComboBox comboBoxSimulate;
+	private JButton okButton;
+	private JButton cancelButton;
+
+	/**
+	 * Show "Path Plot Details" dialog, return settings as a simpath string.
+	 * Returns null if the dialog was cancelled.
+	 */
+	public static String getPathPlotSettings(GUIPrism parent, ModulesFile modulesFile)
 	{
-		return time;
+		GUIPathPlotDialog dialog = getInstance(parent, modulesFile);
+		dialog.setDefaultCloseOperation(JDialog.DISPOSE_ON_CLOSE);
+		dialog.setVisible(true);
+		return dialog.wasCancelled() ? null : dialog.getSimPathString();
 	}
 
-	/** Creates new form GUIPathPlotDialog */
-	public GUIPathPlotDialog(java.awt.Frame parent)
+	/**
+	 * Get static instance, creating if necessary.
+	 */
+	private static GUIPathPlotDialog getInstance(GUIPrism parent, ModulesFile modulesFile)
 	{
-		super(parent, "Define time", true);
-		initComponents();
-		this.getRootPane().setDefaultButton(okayButton);
-		setLocationRelativeTo(getParent()); // centre
-		if (!first)
-			timeField.setText("" + time);
+		if (instance != null && instance.gui == parent && instance.modulesFile == modulesFile)
+			return instance;
+		else {
+			instance = new GUIPathPlotDialog(parent, modulesFile);
+			return instance;
+		}
 	}
 
-	/** 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.
+	/**
+	 * Create the dialog.
 	 */
-	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);
+	public GUIPathPlotDialog(GUIPrism parent, ModulesFile modulesFile)
+	{
+		super(parent, "Path Plot Details", true);
+		this.gui = parent;
+		this.modulesFile = modulesFile;
+		setBounds(100, 100, 450, 154);
+		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.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 };
+		contentPanel.setLayout(gbl_contentPanel);
+		{
+			JLabel lblSimulate = new JLabel("Simulate:");
+			GridBagConstraints gbc_lblSimulate = new GridBagConstraints();
+			gbc_lblSimulate.insets = new Insets(0, 0, 5, 5);
+			gbc_lblSimulate.anchor = GridBagConstraints.EAST;
+			gbc_lblSimulate.gridx = 1;
+			gbc_lblSimulate.gridy = 1;
+			contentPanel.add(lblSimulate, gbc_lblSimulate);
+		}
+		{
+			comboBoxSimulate = new JComboBox();
+			comboBoxSimulate.setModel(new DefaultComboBoxModel(SimulateChoice.values()));
+			GridBagConstraints gbc_comboBoxSimulate = new GridBagConstraints();
+			gbc_comboBoxSimulate.fill = GridBagConstraints.HORIZONTAL;
+			gbc_comboBoxSimulate.insets = new Insets(0, 0, 5, 5);
+			gbc_comboBoxSimulate.gridx = 2;
+			gbc_comboBoxSimulate.gridy = 1;
+			contentPanel.add(comboBoxSimulate, gbc_comboBoxSimulate);
+		}
+		{
+			textFieldTime = new JTextField();
+			GridBagConstraints gbc_textFieldTime = new GridBagConstraints();
+			gbc_textFieldTime.fill = GridBagConstraints.HORIZONTAL;
+			gbc_textFieldTime.insets = new Insets(0, 0, 5, 5);
+			gbc_textFieldTime.gridx = 3;
+			gbc_textFieldTime.gridy = 1;
+			contentPanel.add(textFieldTime, gbc_textFieldTime);
+			textFieldTime.setColumns(5);
+		}
+		{
+			JLabel lblShow = new JLabel("Show:");
+			GridBagConstraints gbc_lblShow = new GridBagConstraints();
+			gbc_lblShow.anchor = GridBagConstraints.EAST;
+			gbc_lblShow.insets = new Insets(0, 0, 5, 5);
+			gbc_lblShow.gridx = 1;
+			gbc_lblShow.gridy = 2;
+			contentPanel.add(lblShow, gbc_lblShow);
+		}
+		{
+			comboBoxShow = new JComboBox();
+			comboBoxShow.addActionListener(new ActionListener()
+			{
+				public void actionPerformed(ActionEvent e)
+				{
+					comboBoxShowActionPerformed(e);
 				}
 			});
-
-		jPanel6.add(okayButton);
-
-		cancelButton.setText("Cancel");
-		cancelButton.addActionListener(new java.awt.event.ActionListener()
+			comboBoxShow.setModel(new DefaultComboBoxModel(ShowChoice.values()));
+			GridBagConstraints gbc_comboBoxShow = new GridBagConstraints();
+			gbc_comboBoxShow.fill = GridBagConstraints.HORIZONTAL;
+			gbc_comboBoxShow.insets = new Insets(0, 0, 5, 5);
+			gbc_comboBoxShow.gridx = 2;
+			gbc_comboBoxShow.gridy = 2;
+			contentPanel.add(comboBoxShow, gbc_comboBoxShow);
+		}
+		{
+			lblInterval = new JLabel("of interval");
+			GridBagConstraints gbc_lblInterval = new GridBagConstraints();
+			gbc_lblInterval.insets = new Insets(0, 0, 5, 5);
+			gbc_lblInterval.gridx = 3;
+			gbc_lblInterval.gridy = 2;
+			contentPanel.add(lblInterval, gbc_lblInterval);
+		}
+		{
+			textFieldInterval = new JTextField();
+			GridBagConstraints gbc_textFieldInterval = new GridBagConstraints();
+			gbc_textFieldInterval.insets = new Insets(0, 0, 5, 0);
+			gbc_textFieldInterval.fill = GridBagConstraints.HORIZONTAL;
+			gbc_textFieldInterval.gridx = 4;
+			gbc_textFieldInterval.gridy = 2;
+			contentPanel.add(textFieldInterval, gbc_textFieldInterval);
+			textFieldInterval.setColumns(5);
+		}
+		{
+			JPanel buttonPane = new JPanel();
+			buttonPane.setLayout(new FlowLayout(FlowLayout.RIGHT));
+			getContentPane().add(buttonPane, BorderLayout.SOUTH);
+			{
+				okButton = new JButton("OK");
+				okButton.setActionCommand("OK");
+				okButton.addActionListener(new ActionListener()
+				{
+					public void actionPerformed(ActionEvent e)
+					{
+						okButtonActionPerformed(e);
+					}
+				});
+				buttonPane.add(okButton);
+				getRootPane().setDefaultButton(okButton);
+			}
+			{
+				cancelButton = new JButton("Cancel");
+				cancelButton.addActionListener(new ActionListener()
 				{
-			public void actionPerformed(java.awt.event.ActionEvent evt)
+					public void actionPerformed(ActionEvent e)
 					{
-				cancelButtonActionPerformed(evt);
+						cancelButtonActionPerformed(e);
 					}
 				});
+				cancelButton.setActionCommand("Cancel");
+				buttonPane.add(cancelButton);
+			}
+		}
 
-		jPanel6.add(cancelButton);
+		// defaults for new creation
+		if (modulesFile.getModelType().continuousTime()) {
+			comboBoxSimulate.setSelectedItem(SimulateChoice.TIME);
+			textFieldTime.setText("100.0");
+			textFieldInterval.setText("1.0");
+		} else {
+			textFieldTime.setText("100");
+			textFieldInterval.setText("");
+		}
 
-		getContentPane().add(jPanel6, java.awt.BorderLayout.SOUTH);
+		this.getRootPane().setDefaultButton(okButton);
+		setLocationRelativeTo(getParent()); // centre
+		doEnables();
+		cancelled = true;
+	}
 
-		pack();
-	}//GEN-END:initComponents
+	public boolean wasCancelled()
+	{
+		return cancelled;
+	}
 
-	private void cancelButtonActionPerformed(java.awt.event.ActionEvent evt)
-	{//GEN-FIRST:event_cancelButtonActionPerformed
-		dispose();
-	}//GEN-LAST:event_cancelButtonActionPerformed
+	public String getSimPathString()
+	{
+		return simPathString;
+	}
 
-	private void okayButtonActionPerformed(java.awt.event.ActionEvent evt)
-	{//GEN-FIRST:event_okayButtonActionPerformed
-		double d = 0.0;
+	private void doEnables()
+	{
+		if ((ShowChoice) comboBoxShow.getSelectedItem() == ShowChoice.SNAPSHOTS) {
+			lblInterval.setEnabled(true);
+			textFieldInterval.setEnabled(true);
+		} else {
+			lblInterval.setEnabled(false);
+			textFieldInterval.setEnabled(false);
+		}
+	}
+
+	public void comboBoxShowActionPerformed(ActionEvent e)
+	{
+		doEnables();
+	}
+
+	public void okButtonActionPerformed(ActionEvent event)
+	{
+		// Validate inputs and build simpath string 
+		simPathString = "";
+		switch ((SimulateChoice) comboBoxSimulate.getSelectedItem()) {
+		case STEP:
 			try {
-			d = Double.parseDouble(timeField.getText());
+				int i = Integer.parseInt(textFieldTime.getText());
+				if (i < 0)
+					throw new NumberFormatException();
+				simPathString += i;
+			} catch (NumberFormatException e) {
+				gui.errorDialog("Invalid number of steps \"" + textFieldTime.getText() + "\"");
+				return;
+			}
+			break;
+		case TIME:
+			try {
+				double d = Double.parseDouble(textFieldTime.getText());
+				if (d < 0)
+					throw new NumberFormatException();
+				simPathString += "time=" + d;
+			} catch (NumberFormatException e) {
+				gui.errorDialog("Invalid time \"" + textFieldTime.getText() + "\"");
+				return;
+			}
+			break;
+		}
+		if ((ShowChoice) comboBoxShow.getSelectedItem() == ShowChoice.SNAPSHOTS) {
+			try {
+				double d = Double.parseDouble(textFieldInterval.getText());
 				if (d < 0)
 					throw new NumberFormatException();
+				simPathString += ",snapshot=" + d;
 			} catch (NumberFormatException e) {
-			JOptionPane.showMessageDialog(this, "Error: Invalid time value.", "Error", JOptionPane.ERROR_MESSAGE);
+				gui.errorDialog("Invalid time interval \"" + textFieldInterval.getText() + "\"");
 				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
+	}
+
+	public void cancelButtonActionPerformed(ActionEvent e)
+	{
+		cancelled = true;
+		dispose();
+	}
 }

prism/src/userinterface/simulator/GUISimulator.java

@@ -727,11 +727,10 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 				}
 			}
 
-			// Get a time limit from user
-			int result = GUIPathPlotDialog.requestTime(this.getGUI());
-			if (result != GUIPathPlotDialog.OK) {
+			// Get path details from dialog
+			String simPathDetails = GUIPathPlotDialog.getPathPlotSettings(getGUI(), parsedModel);
+			if (simPathDetails == null)
 				return;
-			}
 						
 			// Create a new path in the simulator and plot it 
 			a_clearPath();
@@ -742,8 +741,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 			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);
 
@@ -1863,10 +1860,6 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 	public void mousePressed(MouseEvent e)
 	{
 		doPopupDetection(e);
-
-		if (e.getSource() == pathTable) {
-			int row = pathTable.getSelectedRow();
-		}
 	}
 
 	public void mouseReleased(MouseEvent e)