Redesign of GUISimulator interface.

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

prism/src/userinterface/simulator/GUISimulatorPathTable.java

@@ -317,15 +317,15 @@ public class GUISimulatorPathTable extends GUIGroupedTable
 				{	
 					stringValue = "?";
 					if (timeValue.isCumulative())
-						this.setToolTipText("The cumulative time spent in states upto and including \"" + (row) + "\" is unknown");
+						this.setToolTipText("The cumulative time spent in states up to and including state \"" + (row) + "\" is not yet known");
 					else
-						this.setToolTipText("The time spent in state \"" + (row) + "\" is unknown");
+						this.setToolTipText("The time spent in state \"" + (row) + "\" is not yet known");
 				}
 				else
 				{
 					stringValue = (PrismUtils.formatDouble(simulator.getPrism().getSettings(), ((Double)timeValue.getValue())));
 					if (timeValue.isCumulative())
-						this.setToolTipText("The cumulative time spent in states upto and including \"" + (row) + "\" is \"" + stringValue + "\" time units");
+						this.setToolTipText("The cumulative time spent in states up to and including state \"" + (row) + "\" is \"" + stringValue + "\" time units");
 					else
 						this.setToolTipText("The time spent in state \"" + (row) + "\" is \"" + stringValue + "\" time units");
 				}
@@ -347,22 +347,22 @@ public class GUISimulatorPathTable extends GUIGroupedTable
 					stringValue = "?";				
 										
 					if (rewardValue.getRewardStructureColumn().isCumulativeReward())
-						this.setToolTipText("The cumulative reward of reward structure " + rewardName + " upto and including state \"" + (row) + "\" is unknown");
+						this.setToolTipText("The cumulative reward of reward structure " + rewardName + " up to and including step \"" + (row) + "\" is not yet known");
 					if (rewardValue.getRewardStructureColumn().isStateReward())
-						this.setToolTipText("The state reward of reward structure " + rewardName + " in state \"" + (row) + "\" is unknown");
+						this.setToolTipText("The state reward of reward structure " + rewardName + " in state \"" + (row) + "\" is not yet known");
 					if (rewardValue.getRewardStructureColumn().isTransitionReward())
-						this.setToolTipText("The transition reward of reward structure " + rewardName + " for the transition from state \"" + (row) + "\" to state \"" + (row + 1) + "\" is unknown");
+						this.setToolTipText("The transition reward of reward structure " + rewardName + " for step \""+(row)+"\" (from state \"" + (row) + "\" to \"" + (row + 1) + "\") is not yet known");
 				}
 				else
 				{
 					stringValue = PrismUtils.formatDouble(simulator.getPrism().getSettings(), rewardValue.getRewardValue());				
 					
 					if (rewardValue.getRewardStructureColumn().isCumulativeReward())
-						this.setToolTipText("The cumulative reward of reward structure " + rewardName + " upto and including state \"" + (row) + "\" is \"" + (stringValue) + "\"");
+						this.setToolTipText("The cumulative reward of reward structure " + rewardName + " up to and including step \"" + (row) + "\" is \"" + (stringValue) + "\"");
 					if (rewardValue.getRewardStructureColumn().isStateReward())
 						this.setToolTipText("The state reward of reward structure " + rewardName + " in state \"" + (row) + "\" is \"" + (stringValue) + "\"");
 					if (rewardValue.getRewardStructureColumn().isTransitionReward())
-						this.setToolTipText("The transition reward of reward structure " + rewardName + " for the transition from state \"" + (row) + "\" to state \"" + (row + 1) + "\" is \"" + (stringValue) + "\"");
+						this.setToolTipText("The transition reward of reward structure " + rewardName + " for step \""+(row)+"\" (from state \"" + (row) + "\" to \"" + (row + 1) + "\") is \"" + (stringValue) + "\"");
 				}
 				
 			}

prism/src/userinterface/simulator/GUITimeDialog.form

@@ -0,0 +1,145 @@
+<?xml version="1.0" encoding="UTF-8" ?>
+
+<Form version="1.0" type="org.netbeans.modules.form.forminfo.JDialogFormInfo">
+  <SyntheticProperties>
+    <SyntheticProperty name="formSizePolicy" type="int" value="2"/>
+  </SyntheticProperties>
+  <Events>
+    <EventHandler event="windowClosing" listener="java.awt.event.WindowListener" parameters="java.awt.event.WindowEvent" handler="closeDialog"/>
+  </Events>
+  <AuxValues>
+    <AuxValue name="FormSettings_generateMnemonicsCode" type="java.lang.Boolean" value="false"/>
+    <AuxValue name="FormSettings_listenerGenerationStyle" type="java.lang.Integer" value="0"/>
+    <AuxValue name="FormSettings_variablesLocal" type="java.lang.Boolean" value="false"/>
+    <AuxValue name="FormSettings_variablesModifier" type="java.lang.Integer" value="2"/>
+    <AuxValue name="designerSize" type="java.awt.Dimension" value="-84,-19,0,5,115,114,0,18,106,97,118,97,46,97,119,116,46,68,105,109,101,110,115,105,111,110,65,-114,-39,-41,-84,95,68,20,2,0,2,73,0,6,104,101,105,103,104,116,73,0,5,119,105,100,116,104,120,112,0,0,0,-81,0,0,1,-95"/>
+  </AuxValues>
+
+  <Layout class="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout"/>
+  <SubComponents>
+    <Container class="javax.swing.JPanel" name="allPanel">
+      <Properties>
+        <Property name="border" type="javax.swing.border.Border" editor="org.netbeans.modules.form.editors2.BorderEditor">
+          <Border info="org.netbeans.modules.form.compat2.border.EmptyBorderInfo">
+            <EmptyBorder bottom="5" left="5" right="5" top="5"/>
+          </Border>
+        </Property>
+      </Properties>
+      <Constraints>
+        <Constraint layoutClass="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout" value="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout$BorderConstraintsDescription">
+          <BorderConstraints direction="Center"/>
+        </Constraint>
+      </Constraints>
+
+      <Layout class="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout"/>
+      <SubComponents>
+        <Container class="javax.swing.JPanel" name="bottomPanel">
+          <Constraints>
+            <Constraint layoutClass="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout" value="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout$BorderConstraintsDescription">
+              <BorderConstraints direction="South"/>
+            </Constraint>
+          </Constraints>
+
+          <Layout class="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout"/>
+          <SubComponents>
+            <Component class="javax.swing.JLabel" name="warningLabel">
+              <Properties>
+                <Property name="text" type="java.lang.String" value="Please enter a valid positive double"/>
+                <Property name="border" type="javax.swing.border.Border" editor="org.netbeans.modules.form.editors2.BorderEditor">
+                  <Border info="org.netbeans.modules.form.compat2.border.EmptyBorderInfo">
+                    <EmptyBorder bottom="0" left="5" right="0" top="0"/>
+                  </Border>
+                </Property>
+              </Properties>
+              <Constraints>
+                <Constraint layoutClass="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout" value="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout$BorderConstraintsDescription">
+                  <BorderConstraints direction="Center"/>
+                </Constraint>
+              </Constraints>
+            </Component>
+            <Container class="javax.swing.JPanel" name="buttonPanel">
+              <Constraints>
+                <Constraint layoutClass="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout" value="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout$BorderConstraintsDescription">
+                  <BorderConstraints direction="East"/>
+                </Constraint>
+              </Constraints>
+
+              <Layout class="org.netbeans.modules.form.compat2.layouts.DesignFlowLayout">
+                <Property name="alignment" type="int" value="2"/>
+              </Layout>
+              <SubComponents>
+                <Component class="javax.swing.JButton" name="okayButton">
+                  <Properties>
+                    <Property name="text" type="java.lang.String" value="Okay"/>
+                  </Properties>
+                  <Events>
+                    <EventHandler event="actionPerformed" listener="java.awt.event.ActionListener" parameters="java.awt.event.ActionEvent" handler="okayButtonActionPerformed"/>
+                  </Events>
+                </Component>
+                <Component class="javax.swing.JButton" name="cancelButton">
+                  <Properties>
+                    <Property name="text" type="java.lang.String" value="Cancel"/>
+                  </Properties>
+                  <Events>
+                    <EventHandler event="actionPerformed" listener="java.awt.event.ActionListener" parameters="java.awt.event.ActionEvent" handler="cancelButtonActionPerformed"/>
+                  </Events>
+                </Component>
+              </SubComponents>
+            </Container>
+          </SubComponents>
+        </Container>
+        <Container class="javax.swing.JPanel" name="topPanel">
+          <Properties>
+            <Property name="border" type="javax.swing.border.Border" editor="org.netbeans.modules.form.editors2.BorderEditor">
+              <Border info="org.netbeans.modules.form.compat2.border.TitledBorderInfo">
+                <TitledBorder title="Time spent in state"/>
+              </Border>
+            </Property>
+          </Properties>
+          <Constraints>
+            <Constraint layoutClass="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout" value="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout$BorderConstraintsDescription">
+              <BorderConstraints direction="Center"/>
+            </Constraint>
+          </Constraints>
+
+          <Layout class="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout"/>
+          <SubComponents>
+            <Container class="javax.swing.JPanel" name="timeInputPanel">
+              <Properties>
+                <Property name="border" type="javax.swing.border.Border" editor="org.netbeans.modules.form.editors2.BorderEditor">
+                  <Border info="org.netbeans.modules.form.compat2.border.EmptyBorderInfo">
+                    <EmptyBorder bottom="5" left="5" right="5" top="5"/>
+                  </Border>
+                </Property>
+              </Properties>
+              <Constraints>
+                <Constraint layoutClass="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout" value="org.netbeans.modules.form.compat2.layouts.DesignBorderLayout$BorderConstraintsDescription">
+                  <BorderConstraints direction="North"/>
+                </Constraint>
+              </Constraints>
+
+              <Layout class="org.netbeans.modules.form.compat2.layouts.DesignGridLayout">
+                <Property name="columns" type="int" value="2"/>
+                <Property name="horizontalGap" type="int" value="5"/>
+                <Property name="rows" type="int" value="1"/>
+                <Property name="verticalGap" type="int" value="5"/>
+              </Layout>
+              <SubComponents>
+                <Component class="javax.swing.JLabel" name="inputLabel">
+                  <Properties>
+                    <Property name="text" type="java.lang.String" value="Provide a time:"/>
+                  </Properties>
+                </Component>
+                <Component class="javax.swing.JTextField" name="timeInputField">
+                  <Properties>
+                    <Property name="text" type="java.lang.String" value="1.0"/>
+                  </Properties>
+                </Component>
+              </SubComponents>
+            </Container>
+          </SubComponents>
+        </Container>
+      </SubComponents>
+    </Container>
+  </SubComponents>
+</Form>

prism/src/userinterface/simulator/GUITimeDialog.java

@@ -0,0 +1,247 @@
+//==============================================================================
+//
+//	Copyright (c) 2006, Mark Kattenbelt
+//
+//	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 parser.*;
+import prism.*;
+
+import javax.swing.*;
+
+import java.awt.*;
+import javax.swing.border.*;
+import javax.swing.event.DocumentEvent;
+import javax.swing.event.DocumentListener;
+import javax.swing.table.*;
+
+import com.sun.org.apache.xerces.internal.dom3.as.DocumentAS;
+
+import java.util.*;
+import java.awt.event.*;
+
+import userinterface.*;
+import userinterface.simulator.GUISimulator.RewardStructure;
+import simulator.*;
+
+public class GUITimeDialog extends JDialog
+{         
+	//ATTRIBUTES    
+	private Action okAction;
+	private Action cancelAction;
+		
+	private GUIPrism gui;
+	private GUISimulator.PathTableModel pathTableModel;
+    
+	private GUISimulator.SimulationView view;
+	private double time;
+	private boolean cancelled;
+	
+	private static double lastTime = 1.0d;
+	
+    // Variables declaration - do not modify//GEN-BEGIN:variables
+    private javax.swing.JPanel allPanel;
+    private javax.swing.JPanel bottomPanel;
+    private javax.swing.JPanel buttonPanel;
+    private javax.swing.JButton cancelButton;
+    private javax.swing.JLabel inputLabel;
+    private javax.swing.JButton okayButton;
+    private javax.swing.JTextField timeInputField;
+    private javax.swing.JPanel timeInputPanel;
+    private javax.swing.JPanel topPanel;
+    private javax.swing.JLabel warningLabel;
+    // End of variables declaration//GEN-END:variables
+    
+	/** Creates new form GUIConstantsPicker */
+	private GUITimeDialog(GUIPrism parent, GUISimulator simulator)
+	{
+		super(parent, "Provide a time", true);
+        		
+		//initialise
+		initComponents();
+		
+		this.getRootPane().setDefaultButton(okayButton);
+		
+		this.time = lastTime;
+		this.cancelled = false;
+		
+		this.timeInputField.setText("" + time);
+		
+		this.warningLabel.setIcon(new ImageIcon(this.getClass().getResource("/images/smallError.gif")));				
+		this.warningLabel.setVisible(false);
+		
+		this.timeInputField.getDocument().addDocumentListener(new DocumentListener()
+		{	
+			public void changedUpdate(DocumentEvent e) 
+			{
+				try
+				{
+					Double d = Double.parseDouble(timeInputField.getText());
+					GUITimeDialog.this.warningLabel.setVisible(false);
+					GUITimeDialog.this.okayButton.setEnabled(true);
+				}
+				catch (NumberFormatException nfe)
+				{
+					GUITimeDialog.this.warningLabel.setVisible(true);
+					GUITimeDialog.this.okayButton.setEnabled(false);
+				}				
+			}
+			
+			public void removeUpdate(DocumentEvent e) {changedUpdate(e);}			
+			public void insertUpdate(DocumentEvent e) {changedUpdate(e);}
+		});
+		
+		super.setBounds(new Rectangle(550, 300));
+		setResizable(true);
+		setLocationRelativeTo(getParent()); // centre
+				
+		this.setVisible(true);
+	}
+    
+	/** 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.
+	 */
+    // <editor-fold defaultstate="collapsed" desc=" Generated Code ">//GEN-BEGIN:initComponents
+    private void initComponents() {
+        allPanel = new javax.swing.JPanel();
+        bottomPanel = new javax.swing.JPanel();
+        warningLabel = new javax.swing.JLabel();
+        buttonPanel = new javax.swing.JPanel();
+        okayButton = new javax.swing.JButton();
+        cancelButton = new javax.swing.JButton();
+        topPanel = new javax.swing.JPanel();
+        timeInputPanel = new javax.swing.JPanel();
+        inputLabel = new javax.swing.JLabel();
+        timeInputField = new javax.swing.JTextField();
+
+        addWindowListener(new java.awt.event.WindowAdapter() {
+            public void windowClosing(java.awt.event.WindowEvent evt) {
+                closeDialog(evt);
+            }
+        });
+
+        allPanel.setLayout(new java.awt.BorderLayout());
+
+        allPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5));
+        bottomPanel.setLayout(new java.awt.BorderLayout());
+
+        warningLabel.setText("Please enter a valid positive double");
+        warningLabel.setBorder(javax.swing.BorderFactory.createEmptyBorder(0, 5, 0, 0));
+        bottomPanel.add(warningLabel, java.awt.BorderLayout.CENTER);
+
+        buttonPanel.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);
+            }
+        });
+
+        buttonPanel.add(okayButton);
+
+        cancelButton.setText("Cancel");
+        cancelButton.addActionListener(new java.awt.event.ActionListener() {
+            public void actionPerformed(java.awt.event.ActionEvent evt) {
+                cancelButtonActionPerformed(evt);
+            }
+        });
+
+        buttonPanel.add(cancelButton);
+
+        bottomPanel.add(buttonPanel, java.awt.BorderLayout.EAST);
+
+        allPanel.add(bottomPanel, java.awt.BorderLayout.SOUTH);
+
+        topPanel.setLayout(new java.awt.BorderLayout());
+
+        topPanel.setBorder(javax.swing.BorderFactory.createTitledBorder("Time spent in state"));
+        timeInputPanel.setLayout(new java.awt.GridLayout(1, 2, 5, 5));
+
+        timeInputPanel.setBorder(javax.swing.BorderFactory.createEmptyBorder(5, 5, 5, 5));
+        inputLabel.setText("Provide a time:");
+        timeInputPanel.add(inputLabel);
+
+        timeInputField.setText("1.0");
+        timeInputPanel.add(timeInputField);
+
+        topPanel.add(timeInputPanel, java.awt.BorderLayout.NORTH);
+
+        allPanel.add(topPanel, java.awt.BorderLayout.CENTER);
+
+        getContentPane().add(allPanel, java.awt.BorderLayout.CENTER);
+
+    }// </editor-fold>//GEN-END:initComponents
+
+	private void okayButtonActionPerformed(java.awt.event.ActionEvent evt)//GEN-FIRST:event_okayButtonActionPerformed
+	{//GEN-HEADEREND:event_okayButtonActionPerformed
+		try
+		{	time = Double.parseDouble(timeInputField.getText());	}
+		catch (NumberFormatException nfe)
+		{	// Shouldn't happen.
+			cancelled = true;
+		}
+		dispose();
+	}//GEN-LAST:event_okayButtonActionPerformed
+        
+	private void cancelButtonActionPerformed(java.awt.event.ActionEvent evt)//GEN-FIRST:event_cancelButtonActionPerformed
+	{//GEN-HEADEREND:event_cancelButtonActionPerformed
+		cancelled = true;
+		dispose();
+	}//GEN-LAST:event_cancelButtonActionPerformed
+        
+	/** Closes the dialog */
+	private void closeDialog(java.awt.event.WindowEvent evt)//GEN-FIRST:event_closeDialog
+	{
+		setVisible(false);
+		dispose();
+	}//GEN-LAST:event_closeDialog
+		
+	public boolean isCancelled() 
+	{
+		return cancelled;
+	}
+
+	public double getTime() 
+	{
+		return time;
+	}
+
+	/** Returns a time, or -1 for cancel. */
+	public static double askTime(GUIPrism prism, GUISimulator simulator)
+	{
+		GUITimeDialog dialog = new GUITimeDialog(prism, simulator);
+		
+		if (dialog.isCancelled())
+		{
+			return -1;
+		}
+		else
+		{
+			GUITimeDialog.lastTime = dialog.time;			
+			return dialog.time;		
+		}
+	}
+}
+
+