Another few bugfixes to the new reward display in the simulator. Different name for unnamed reward structures and normal names of both rewards and variables are in quotes.

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

prism/src/userinterface/simulator/GUISimulator.java

@@ -2177,7 +2177,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 		
 		public String toString()
 		{
-			return name;
+			return "\"" + name + "\"";
 		}
 		
 		public boolean equals(Object o)
@@ -2228,7 +2228,14 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 
 		public String toString()
 		{
-			return name;
+			if (name != null)
+			{
+				return "\"" + name + "\"";
+			}
+			else 
+			{
+				return "Reward " + (index + 1) + " (unnamed)"; 
+			}
 		}
 		
 		public boolean equals(Object o)
@@ -2404,7 +2411,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 						String rewardName = rewardStruct.getName();
 						
 						if (rewardName.trim().length() == 0)
-						{	rewardName = " (unnamed reward model " + (r + 1) + ")"; }
+						{	rewardName = null; }
 						visibleRewards.add(new RewardStructure(r, rewardName, mf.getRewardStruct(r).getNumStateItems() == 0,  mf.getRewardStruct(r).getNumTransItems() == 0));
 					}				
 				}
@@ -2624,7 +2631,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 				// A variable column
 				else if (varStart <= columnIndex && columnIndex < timeStart)
 				{						
-					return ((Variable)view.getVisibleVariables().get(columnIndex - varStart)).getName();						
+					return ((Variable)view.getVisibleVariables().get(columnIndex - varStart)).toString();						
 				}
 				else if (timeStart <= columnIndex && columnIndex < rewardStart)
 				{
@@ -2633,7 +2640,11 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 				else if (rewardStart <= columnIndex)
 				{	
 					String rewardStructName = ((RewardStructure)view.getVisibleRewards().get(columnIndex - rewardStart)).getName();
-					return  rewardStructName; 
+					if (rewardStructName != null)
+					{	
+						return  "\"" + rewardStructName + "\"";
+					}
+					else return "" + (((RewardStructure)view.getVisibleRewards().get(columnIndex - rewardStart)).getIndex() + 1);
 				}
 			}				
 			return "Undefined Column";			

prism/src/userinterface/simulator/GUISimulatorPathTable.java

@@ -393,7 +393,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable
 					}
 					else if (rewardValue.getStateReward() != null && rewardValue.getTransitionReward() == null)
 					{
-						field.setText("[  " + rewardValue.getStateReward().toString() + "  ]");						
+						field.setText(rewardValue.getStateReward().toString());						
 					}
 					else
 					{