s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Added tooltips to the cells of the GUISimulatorPathTable. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@200 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Mark Kattenbelt 20 years ago
parent
6684d121be
commit
b274cf97eb
2 changed files with 153 additions and 74 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 23
      prism/src/userinterface/simulator/GUISimulator.java
  2. 204
      prism/src/userinterface/simulator/GUISimulatorPathTable.java

23
prism/src/userinterface/simulator/GUISimulator.java
View File

@ -2182,11 +2182,12 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
{
private Double value;
private boolean timeValueUnknown;
private boolean isCumulative;
public TimeValue(Double value)
public TimeValue(Double value, boolean isCumulative)
{
this.value = value;
this.value = value;
this.isCumulative = isCumulative;
}
public Double getValue()
@ -2208,6 +2209,16 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
{
return this.timeValueUnknown;
}
public boolean isCumulative()
{
return isCumulative;
}
public void setCumulative(boolean isCumulative)
{
this.isCumulative = isCumulative;
}
}
/**
@ -2658,7 +2669,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
if (view.showSteps())
{
if (groupCount == groupIndex)
{ return "Step"; }
{ return "State"; }
groupCount++;
}
@ -2849,14 +2860,14 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
else if (timeStart <= columnIndex && columnIndex < cumulativeTimeStart)
{
timeValue = new TimeValue(SimulatorEngine.getTimeSpentInPathState(rowIndex));
timeValue = new TimeValue(SimulatorEngine.getTimeSpentInPathState(rowIndex), false);
timeValue.setTimeValueUnknown(rowIndex >= SimulatorEngine.getPathSize() - 1);
return timeValue;
}
else if (cumulativeTimeStart <= columnIndex && columnIndex < varStart)
{
timeValue = new TimeValue(SimulatorEngine.getCumulativeTimeSpentInPathState(rowIndex));
timeValue = new TimeValue(SimulatorEngine.getCumulativeTimeSpentInPathState(rowIndex), true);
timeValue.setTimeValueUnknown(rowIndex >= SimulatorEngine.getPathSize() - 1);
return timeValue;

204
prism/src/userinterface/simulator/GUISimulatorPathTable.java
View File

@ -286,78 +286,92 @@ public class GUISimulatorPathTable extends GUIGroupedTable
}
class PathChangeTableRenderer extends JPanel implements TableCellRenderer
{
private boolean onlyShowChange;
class PathChangeCellRenderer extends JPanel
{
private PathChangeTableRenderer pctr;
private Object value;
private String tooltip;
private String stringValue;
private boolean isLastRow;
private boolean isSelected;
private JTextField field = new JTextField();
private int row;
private int column;
private Color defaultColor;
private Color defaultVariableColor;
private Color defaultRewardColor;
private Color selectedColor;
private Color labelColor;
private Color selectedLabelColor;
public PathChangeTableRenderer(boolean onlyShowChange)
private int row;
public PathChangeCellRenderer(PathChangeTableRenderer pctr, Object value, boolean isSelected, int row)
{
super();
this.onlyShowChange = onlyShowChange;
defaultColor = Color.white;
defaultVariableColor = Color.white;
defaultRewardColor = Color.white;
selectedColor = new Color(defaultColor.getRed()-20, defaultColor.getGreen()-20, defaultColor.getBlue());
selectedLabelColor = new Color(selectedColor.getRed()-20, selectedColor.getGreen(), selectedColor.getBlue()-20);
labelColor = new Color(defaultColor.getRed()-50, defaultColor.getGreen(), defaultColor.getBlue()-50);
isSelected = false;
}
public Component getTableCellRendererComponent(JTable table, Object value,
boolean isSelected, boolean hasFocus, int row, int column)
{
GUISimulator.SimulationView view = ((GUISimulator.PathTableModel)table.getModel()).getView();
int stepStart = 0;
int timeStart = stepStart + (view.showSteps() ? 1 : 0);
int varStart = timeStart + (view.showTime() ? 1 : 0) + (view.showCumulativeTime() ? 1 : 0);
int rewardStart = varStart + view.getVisibleVariables().size();
this.row = row;
this.column = table.convertColumnIndexToModel(column);
this.pctr = pctr;
this.value = value;
this.isSelected = isSelected;
this.row = row;
if (value instanceof String)
{
stringValue = (String)value;
this.setToolTipText("State \"" + row + "\" of this path");
}
else if (value instanceof GUISimulator.TimeValue)
{
GUISimulator.TimeValue timeValue = (GUISimulator.TimeValue)value;
if (timeValue.isTimeValueUnknown())
{
stringValue = "?";
if (timeValue.isCumulative())
this.setToolTipText("The cumulative time spend in states upto and including \"" + (row) + "\" is unknown");
else
this.setToolTipText("The time spend in state \"" + (row) + "\" is unknown");
}
else
{
stringValue = (PrismUtils.formatDouble(simulator.getPrism().getSettings(), ((Double)timeValue.getValue())));
if (timeValue.isCumulative())
this.setToolTipText("The cumulative time spend in states upto and including \"" + (row) + "\" is \"" + stringValue + "\" time units");
else
this.setToolTipText("The time spend in state \"" + (row) + "\" is \"" + stringValue + "\" time units");
}
}
else if (value instanceof GUISimulator.VariableValue)
{
GUISimulator.VariableValue variableValue = (GUISimulator.VariableValue)value;
stringValue = (variableValue.getValue() instanceof Double) ? (PrismUtils.formatDouble(simulator.getPrism().getSettings(), ((Double)variableValue.getValue()))) : variableValue.getValue().toString();
this.setToolTipText("Value of variable \"" + variableValue.getVariable().getName() + "\" in state \"" + (row) + "\" is \"" + stringValue + "\"");
}
else if (value instanceof GUISimulator.RewardStructureValue)
{
GUISimulator.RewardStructureValue rewardValue = (GUISimulator.RewardStructureValue)value;
String rewardName = rewardValue.getRewardStructureColumn().getRewardStructure().getColumnName();
if (rewardValue.isRewardValueUnknown())
{
stringValue = "?";
if (rewardValue.getRewardStructureColumn().isCumulativeReward())
this.setToolTipText("The cumulative reward of reward structure " + rewardName + " upto and including state \"" + (row) + "\" is unknown");
if (rewardValue.getRewardStructureColumn().isStateReward())
this.setToolTipText("The state reward of reward structure " + rewardName + " in state \"" + (row) + "\" is unknown");
if (rewardValue.getRewardStructureColumn().isTransitionReward())
this.setToolTipText("The transition reward of reward structure " + rewardName + " for the transition from state \"" + (row) + "\" to state \"" + (row + 1) + "\" is unknown");
}
else
{
stringValue = PrismUtils.formatDouble(simulator.getPrism().getSettings(), rewardValue.getRewardValue());
this.isSelected = isSelected;
if (rewardValue.getRewardStructureColumn().isCumulativeReward())
this.setToolTipText("The cumulative reward of reward structure " + rewardName + " upto and including state \"" + (row) + "\" is \"" + (stringValue) + "\"");
if (rewardValue.getRewardStructureColumn().isStateReward())
this.setToolTipText("The state reward of reward structure " + rewardName + " in state \"" + (row) + "\" is \"" + (stringValue) + "\"");
if (rewardValue.getRewardStructureColumn().isTransitionReward())
this.setToolTipText("The transition reward of reward structure " + rewardName + " for the transition from state \"" + (row) + "\" to state \"" + (row + 1) + "\" is \"" + (stringValue) + "\"");
}
}
boolean shouldColourRow = ptm.shouldColourRow(row);
Color backGround = defaultColor;
if(isSelected && !shouldColourRow)
backGround = selectedColor;
else if (isSelected && shouldColourRow)
backGround = selectedLabelColor;
else if (!isSelected && shouldColourRow)
backGround = labelColor;
this.setBackground(backGround);
return this;
}
public void paintComponent(Graphics g)
{
super.paintComponent(g);
@ -379,8 +393,6 @@ public class GUISimulatorPathTable extends GUIGroupedTable
else if (value instanceof GUISimulator.VariableValue)
{
GUISimulator.VariableValue variableValue = (GUISimulator.VariableValue)value;
String stringValue = (variableValue.getValue() instanceof Double) ? (PrismUtils.formatDouble(simulator.getPrism().getSettings(), ((Double)variableValue.getValue()))) : variableValue.getValue().toString();
double width = getStringWidth(stringValue, g2);
@ -388,14 +400,14 @@ public class GUISimulatorPathTable extends GUIGroupedTable
Color color = (variableValue.hasChanged()) ? (Color.black) : (Color.lightGray);
if (onlyShowChange)
if (pctr.onlyShowChange())
{
g2.setColor(Color.black);
g2.drawLine(getWidth()/2, 0, getWidth()/2, getHeight());
if (isSelected || variableValue.hasChanged())
{
g2.setColor(defaultVariableColor);
g2.setColor(Color.white);
g2.fill(rec);
g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);
@ -418,8 +430,6 @@ public class GUISimulatorPathTable extends GUIGroupedTable
else if (value instanceof GUISimulator.RewardStructureValue)
{
GUISimulator.RewardStructureValue rewardValue = (GUISimulator.RewardStructureValue)value;
String stringValue = (rewardValue.isRewardValueUnknown()) ? "?" : PrismUtils.formatDouble(simulator.getPrism().getSettings(), rewardValue.getRewardValue());
double width = getStringWidth(stringValue, g2);
@ -427,14 +437,14 @@ public class GUISimulatorPathTable extends GUIGroupedTable
Color color = (rewardValue.hasChanged() || rewardValue.isRewardValueUnknown()) ? (Color.black) : (Color.lightGray);
if (onlyShowChange)
if (pctr.onlyShowChange())
{
g2.setColor(Color.black);
g2.drawLine(getWidth()/2, 0, getWidth()/2, getHeight());
if ((isSelected || rewardValue.hasChanged()))
{
g2.setColor(defaultRewardColor);
g2.setColor(Color.white);
g2.fill(rec);
g2.setRenderingHint(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON);
@ -455,9 +465,15 @@ public class GUISimulatorPathTable extends GUIGroupedTable
}
}
else if (value instanceof GUISimulator.TimeValue)
{
{
GUISimulator.TimeValue timeValue = (GUISimulator.TimeValue)value;
String stringValue = (timeValue.isTimeValueUnknown()) ? "?" : PrismUtils.formatDouble(simulator.getPrism().getSettings(), timeValue.getValue());
if (timeValue.isTimeValueUnknown())
this.setToolTipText("The time spent in state " + row + " of this path is not yet known");
else
this.setToolTipText(stringValue + " time units were spent in state " + row + " of this path");
double width = getStringWidth(stringValue, g2);
@ -469,6 +485,58 @@ public class GUISimulatorPathTable extends GUIGroupedTable
}
}
}
class PathChangeTableRenderer implements TableCellRenderer
{
private boolean onlyShowChange;
private Color defaultColor;
private Color selectedColor;
private Color labelColor;
private Color selectedLabelColor;
public PathChangeTableRenderer(boolean onlyShowChange)
{
super();
this.onlyShowChange = onlyShowChange;
defaultColor = Color.white;
selectedColor = new Color(defaultColor.getRed()-20, defaultColor.getGreen()-20, defaultColor.getBlue());
selectedLabelColor = new Color(selectedColor.getRed()-20, selectedColor.getGreen(), selectedColor.getBlue()-20);
labelColor = new Color(defaultColor.getRed()-50, defaultColor.getGreen(), defaultColor.getBlue()-50);
}
public Component getTableCellRendererComponent(JTable table, Object value,
boolean isSelected, boolean hasFocus, int row, int column)
{
PathChangeCellRenderer pctr = new PathChangeCellRenderer(this, value, isSelected, row);
boolean shouldColourRow = ptm.shouldColourRow(row);
Color backGround = defaultColor;
if(isSelected && !shouldColourRow)
backGround = selectedColor;
else if (isSelected && shouldColourRow)
backGround = selectedLabelColor;
else if (!isSelected && shouldColourRow)
backGround = labelColor;
pctr.setBackground(backGround);
return pctr;
}
public boolean onlyShowChange()
{
return onlyShowChange;
}
}
/** Method which computes width of a string for a given Graphics2D object
*/

Write Preview
Loading…
Cancel
Save