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