A couple of small bugfixes to the simulator table. Added tooltip, changed default unnamed reward column name, fixed initial grouped header update issue.

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

prism/src/userinterface/simulator/GUISimulator.java

@@ -2391,6 +2391,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 				{
 					stepsVisible = true;
 					hideEmptyRewards = true;
+					showTime = mf.getType() == ModulesFile.STOCHASTIC;
 					
 					for (int i = 0; i < engine.getNumVariables(); i++)
 					{
@@ -2403,7 +2404,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 						String rewardName = rewardStruct.getName();
 						
 						if (rewardName.trim().length() == 0)
-						{	rewardName = "Reward model " + r + " (unnamed)"; }
+						{	rewardName = " (unnamed reward model " + (r + 1) + ")"; }
 						visibleRewards.add(new RewardStructure(r, rewardName, mf.getRewardStruct(r).getNumStateItems() == 0,  mf.getRewardStruct(r).getNumTransItems() == 0));
 					}				
 				}

prism/src/userinterface/simulator/GUISimulatorPathTable.java

@@ -369,6 +369,8 @@ public class GUISimulatorPathTable extends GUIGroupedTable
 			bg = Color.white;
 			if(column == 0 || column > ptm.getView().getVisibleVariables().size())
 			{
+				field.setToolTipText(null);
+				
 				if(value instanceof Double)
 				{
 					Double dv = (Double)value;
@@ -398,7 +400,8 @@ public class GUISimulatorPathTable extends GUIGroupedTable
 						field.setText("no non-empty reward");
 					}
 					
-					field.setHorizontalAlignment(JTextField.CENTER);					
+					field.setHorizontalAlignment(JTextField.CENTER);	
+					field.setToolTipText("State Reward [ Transition Reward ]");
 				}
 				else 
 				{

prism/src/userinterface/util/GUIGroupedTableColumnModel.java

@@ -80,6 +80,7 @@ public class GUIGroupedTableColumnModel extends DefaultTableColumnModel implemen
 		}
 		
 		lastColumn.add(new Integer(this.getColumnCount()-1));
+		updateGroups();
 	}
 		
 	/**