From 6ee7a777748e5dcfd7ed5e875c51062bbcae5d23 Mon Sep 17 00:00:00 2001
From: Mark Kattenbelt <mark.kattenbelt@comlab.ox.ac.uk>
Date: Mon, 27 Nov 2006 16:38:28 +0000
Subject: [PATCH] Some cosmetic changes to the reward display in the simulator.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@172 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/userinterface/simulator/GUISimulator.java | 13 ++++++++++---
 .../simulator/GUISimulatorPathTable.java            |  8 +++-----
 2 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java
index 9cdb7f5f..2b045f07 100644
--- a/prism/src/userinterface/simulator/GUISimulator.java
+++ b/prism/src/userinterface/simulator/GUISimulator.java
@@ -2230,11 +2230,11 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 		{
 			if (name != null)
 			{
-				return "\"" + name + "\"";
+				return "" + (index + 1) + ": \"" + name + "\"";
 			}
 			else 
 			{
-				return "Reward " + (index + 1) + " (unnamed)"; 
+				return "" + (index + 1) + ": (unnamed)"; 
 			}
 		}
 		
@@ -2681,7 +2681,14 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 					}
 					else if (timeStart <= columnIndex && columnIndex < rewardStart)
 					{
-						return new Double(SimulatorEngine.getTimeSpentInPathState(rowIndex));
+						if (rowIndex < SimulatorEngine.getPathSize() - 1)
+						{
+							return new Double(SimulatorEngine.getTimeSpentInPathState(rowIndex));
+						}
+						else
+						{
+							return "...";
+						}
 					}
 					else if (rewardStart <= columnIndex)
 					{
diff --git a/prism/src/userinterface/simulator/GUISimulatorPathTable.java b/prism/src/userinterface/simulator/GUISimulatorPathTable.java
index 0c0c7e79..cad59a27 100644
--- a/prism/src/userinterface/simulator/GUISimulatorPathTable.java
+++ b/prism/src/userinterface/simulator/GUISimulatorPathTable.java
@@ -295,11 +295,9 @@ public class GUISimulatorPathTable extends GUIGroupedTable
 	    
 			if(value instanceof Double && ((Double)value).doubleValue() == SimulatorEngine.UNDEFINED_DOUBLE)
 				renderer.setText("");
-			else renderer.setText(value.toString());
-	    
-	    
-			Color c = Color.white;
+			else renderer.setText(value.toString());   
 	    
+			Color c = Color.white;    
 	    
 			if(isSelected)
 			{
@@ -397,7 +395,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable
 					}
 					else
 					{
-						field.setText("no non-empty reward");
+						field.setText("");
 					}
 					
 					field.setHorizontalAlignment(JTextField.CENTER);