Browse Source

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
master
Mark Kattenbelt 19 years ago
parent
commit
6ee7a77774
  1. 11
      prism/src/userinterface/simulator/GUISimulator.java
  2. 4
      prism/src/userinterface/simulator/GUISimulatorPathTable.java

11
prism/src/userinterface/simulator/GUISimulator.java

@ -2230,11 +2230,11 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
{ {
if (name != null) if (name != null)
{ {
return "\"" + name + "\"";
return "" + (index + 1) + ": \"" + name + "\"";
} }
else else
{ {
return "Reward " + (index + 1) + " (unnamed)";
return "" + (index + 1) + ": (unnamed)";
} }
} }
@ -2680,9 +2680,16 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
{ return new Integer(result); } { return new Integer(result); }
} }
else if (timeStart <= columnIndex && columnIndex < rewardStart) else if (timeStart <= columnIndex && columnIndex < rewardStart)
{
if (rowIndex < SimulatorEngine.getPathSize() - 1)
{ {
return new Double(SimulatorEngine.getTimeSpentInPathState(rowIndex)); return new Double(SimulatorEngine.getTimeSpentInPathState(rowIndex));
} }
else
{
return "...";
}
}
else if (rewardStart <= columnIndex) else if (rewardStart <= columnIndex)
{ {
RewardStructure reward = (RewardStructure)view.getVisibleRewards().get(columnIndex - rewardStart); RewardStructure reward = (RewardStructure)view.getVisibleRewards().get(columnIndex - rewardStart);

4
prism/src/userinterface/simulator/GUISimulatorPathTable.java

@ -297,10 +297,8 @@ public class GUISimulatorPathTable extends GUIGroupedTable
renderer.setText(""); renderer.setText("");
else renderer.setText(value.toString()); else renderer.setText(value.toString());
Color c = Color.white; Color c = Color.white;
if(isSelected) if(isSelected)
{ {
Color newCol = new Color(c.getRed()-20, c.getGreen()-20, c.getBlue()); Color newCol = new Color(c.getRed()-20, c.getGreen()-20, c.getBlue());
@ -397,7 +395,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable
} }
else else
{ {
field.setText("no non-empty reward");
field.setText("");
} }
field.setHorizontalAlignment(JTextField.CENTER); field.setHorizontalAlignment(JTextField.CENTER);

Loading…
Cancel
Save