diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index 7f3b1af9..3a73e215 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -2701,7 +2701,47 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect return "Undefined Group"; } - } + } + + public String getGroupToolTip(int groupIndex) + { + int groupCount = 0; + + if (view.showSteps()) + { + if (groupCount == groupIndex) + { return null; } + + groupCount++; + } + + if (view.showTime() || view.showCumulativeTime()) + { + if (groupCount == groupIndex) + { return null; } + + groupCount++; + } + + if (view.getVisibleVariables().size() > 0) + { + if (groupCount == groupIndex) + { return "Columns in this group represent variables of this model"; } + + groupCount++; + } + + // Add state and transitions rewards for each reward structure. + if (view.getVisibleRewardColumns().size() > 0) + { + if (groupCount == groupIndex) + { return "Columns in this group represent the state, transition and cumulative rewards of this model"; } + + groupCount++; + } + + return null; + } public int getLastColumnOfGroup(int groupIndex) { @@ -2842,6 +2882,53 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect return "Undefined Column"; } + + + public String getColumnToolTip(int columnIndex) + { + if(pathActive) + { + int stepStart = 0; + int timeStart = stepStart + (view.showSteps() ? 1 : 0); + int cumulativeTimeStart = timeStart + (view.showTime() ? 1 : 0); + int varStart = cumulativeTimeStart + (view.showCumulativeTime() ? 1 : 0); + int rewardStart = varStart + view.getVisibleVariables().size(); + + // The step column + if (stepStart <= columnIndex && columnIndex < timeStart) + { + return "The states of this path"; + } + else if (timeStart <= columnIndex && columnIndex < cumulativeTimeStart) + { + return "The time spent in a state"; + } + else if (cumulativeTimeStart <= columnIndex && columnIndex < varStart) + { + return "The cumulative time spent in states"; + } + // A variable column + else if (varStart <= columnIndex && columnIndex < rewardStart) + { + return "The values of variable \"" + ((Variable)view.getVisibleVariables().get(columnIndex - varStart)).toString() + "\""; + } + + else if (rewardStart <= columnIndex) + { + RewardStructureColumn column = ((RewardStructureColumn)view.getVisibleRewardColumns().get(columnIndex - rewardStart)); + String rewardName = column.getRewardStructure().getColumnName(); + + if (column.isStateReward()) + return "The state reward of reward structure " + rewardName; + if (column.isTransitionReward()) + return "The transition reward of reward structure " + rewardName; + if (column.isCumulativeReward()) + return "The cumulative reward of reward structure " + rewardName; + } + } + return "Undefined Column"; + } + public Object getValueAt(int rowIndex, int columnIndex) { if(pathActive) diff --git a/prism/src/userinterface/simulator/GUISimulatorPathTable.java b/prism/src/userinterface/simulator/GUISimulatorPathTable.java index 1da39304..08dd605c 100644 --- a/prism/src/userinterface/simulator/GUISimulatorPathTable.java +++ b/prism/src/userinterface/simulator/GUISimulatorPathTable.java @@ -317,17 +317,17 @@ public class GUISimulatorPathTable extends GUIGroupedTable { stringValue = "?"; if (timeValue.isCumulative()) - this.setToolTipText("The cumulative time spend in states upto and including \"" + (row) + "\" is unknown"); + this.setToolTipText("The cumulative time spent in states upto and including \"" + (row) + "\" is unknown"); else - this.setToolTipText("The time spend in state \"" + (row) + "\" is unknown"); + this.setToolTipText("The time spent in state \"" + (row) + "\" is unknown"); } else { stringValue = (PrismUtils.formatDouble(simulator.getPrism().getSettings(), ((Double)timeValue.getValue()))); if (timeValue.isCumulative()) - this.setToolTipText("The cumulative time spend in states upto and including \"" + (row) + "\" is \"" + stringValue + "\" time units"); + this.setToolTipText("The cumulative time spent in states upto and including \"" + (row) + "\" is \"" + stringValue + "\" time units"); else - this.setToolTipText("The time spend in state \"" + (row) + "\" is \"" + stringValue + "\" time units"); + this.setToolTipText("The time spent in state \"" + (row) + "\" is \"" + stringValue + "\" time units"); } } else if (value instanceof GUISimulator.VariableValue) diff --git a/prism/src/userinterface/util/GUIGroupedTable.java b/prism/src/userinterface/util/GUIGroupedTable.java index ae0d218d..15432c9f 100644 --- a/prism/src/userinterface/util/GUIGroupedTable.java +++ b/prism/src/userinterface/util/GUIGroupedTable.java @@ -110,9 +110,9 @@ public class GUIGroupedTable extends JTable if (columnModel != null && columnModel instanceof GUIGroupedTableColumnModel) { - return new GUIGroupedTableHeader((GUIGroupedTableColumnModel)columnModel); + return new GUIGroupedTableHeader((GUIGroupedTableColumnModel)columnModel, (GUIGroupedTableModel)this.getModel()); } - return new GUIGroupedTableHeader(new GUIGroupedTableColumnModel()); + return new GUIGroupedTableHeader(new GUIGroupedTableColumnModel(), (GUIGroupedTableModel)this.getModel()); } } diff --git a/prism/src/userinterface/util/GUIGroupedTableHeader.java b/prism/src/userinterface/util/GUIGroupedTableHeader.java index 818f2c13..7f31a51d 100644 --- a/prism/src/userinterface/util/GUIGroupedTableHeader.java +++ b/prism/src/userinterface/util/GUIGroupedTableHeader.java @@ -39,20 +39,26 @@ public class GUIGroupedTableHeader extends JTableHeader implements TableColumnMo { private JTableHeader bottomHeader; private JTableHeader topHeader; + private GUIGroupedTableColumnModel model; + private GUIGroupedTableModel tableModel; /** * Creates a new GUIGroupedTableHeader. * @param model The column model that is the basis of this table header (must be grouped). */ - public GUIGroupedTableHeader(GUIGroupedTableColumnModel model) + public GUIGroupedTableHeader(GUIGroupedTableColumnModel model, GUIGroupedTableModel tableModel) { super(); removeAll(); + this.model = model; + this.tableModel = tableModel; + topHeader = new JTableHeader(model.getGroupTableColumnModel()); topHeader.setResizingAllowed(false); topHeader.setReorderingAllowed(false); + final TableCellRenderer renderer = topHeader.getDefaultRenderer(); topHeader.setDefaultRenderer(new TableCellRenderer() { public Component getTableCellRendererComponent(JTable table, Object value, boolean isSelected, boolean hasFocus, int row, int column) @@ -82,6 +88,58 @@ public class GUIGroupedTableHeader extends JTableHeader implements TableColumnMo { cs[i].addMouseListener(this); } + + topHeader.addMouseMotionListener(new MouseMotionAdapter() + { + private TableColumn lastColumn; + + public void mouseMoved(MouseEvent e) + { + bottomHeader.setToolTipText(null); + + TableColumn currentColumn; + + int column = topHeader.getColumnModel().getColumnIndexAtX(e.getX()); + + if (column >= 0) + { + currentColumn = topHeader.getColumnModel().getColumn(column); + + if (currentColumn != lastColumn) + { + topHeader.setToolTipText((GUIGroupedTableHeader.this).tableModel.getGroupToolTip(column)); + lastColumn = currentColumn; + } + } + } + }); + bottomHeader.addMouseMotionListener(new MouseMotionAdapter() + { +private TableColumn lastColumn; + + public void mouseMoved(MouseEvent e) + { + topHeader.setToolTipText(null); + + TableColumn currentColumn; + + int column = bottomHeader.getColumnModel().getColumnIndexAtX(e.getX()); + + if (column >= 0) + { + currentColumn = bottomHeader.getColumnModel().getColumn(column); + + if (currentColumn != lastColumn) + { + bottomHeader.setToolTipText((GUIGroupedTableHeader.this).tableModel.getColumnToolTip(column)); + lastColumn = currentColumn; + } + } + } + }); + + //topHeader.setToolTipText(null); + //bottomHeader.setToolTipText(null); } @@ -155,7 +213,7 @@ public class GUIGroupedTableHeader extends JTableHeader implements TableColumnMo * Overwritten to catch events of child components. */ public void mouseClicked(MouseEvent e) { - this.dispatchEvent(new MouseEvent(this, e.getID(), e.getWhen(), e.getModifiers(), e.getX(), e.getY() + ((Component)e.getSource()).getBounds().y, e.getClickCount(), e.isPopupTrigger())); + this.dispatchEvent(new MouseEvent(this, e.getID(), e.getWhen(), e.getModifiers(), e.getX(), e.getY() + ((Component)e.getSource()).getBounds().y, e.getClickCount(), e.isPopupTrigger())); } /** diff --git a/prism/src/userinterface/util/GUIGroupedTableModel.java b/prism/src/userinterface/util/GUIGroupedTableModel.java index 6718b87d..c59aebf4 100644 --- a/prism/src/userinterface/util/GUIGroupedTableModel.java +++ b/prism/src/userinterface/util/GUIGroupedTableModel.java @@ -22,6 +22,7 @@ package userinterface.util; +import javax.swing.event.TableModelListener; import javax.swing.table.TableModel; /** @@ -29,7 +30,7 @@ import javax.swing.table.TableModel; * An interface which extends {@link TableModel} such that also group information can * be extracted automatically. Note that groups are always non-empty. */ -public interface GUIGroupedTableModel extends TableModel +public interface GUIGroupedTableModel extends TableModel { /** * @return The number of groups in this model. @@ -50,4 +51,18 @@ public interface GUIGroupedTableModel extends TableModel * @return The index of the last column in this group. */ public int getLastColumnOfGroup(int groupIndex); + + /** + * Retrieves the tooltip to be set for a group. + * @param groupIndex The index of a group. + * @return The tooltip text for a group, or null. + */ + public String getGroupToolTip(int groupIndex); + + /** + * Retrieves the tooltip to be set for a column. + * @param columnIndex The index of a column. + * @return The tooltip text for a column, or null. + */ + public String getColumnToolTip(int columnIndex) ; }