Added tooltips to the GUIGroupedTableHeader.

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

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)

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)

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());
     }
 }
 

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()));
     }
 
 	/** 

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)	;
 }