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

Shifted cumulative time/rewards in the path table; and changed some tooltips. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@477 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
08a8ad01cd
commit
2fcf7d48fc
2 changed files with 45 additions and 46 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 54
      prism/src/userinterface/simulator/GUISimulator.java
  2. 37
      prism/src/userinterface/simulator/GUISimulatorPathTable.java

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

@ -138,7 +138,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
} }
else if (e.getClickCount() == 2 && !currentUpdatesTable.isEnabled()) else if (e.getClickCount() == 2 && !currentUpdatesTable.isEnabled())
{ {
GUISimulator.this.warning("Simulation", "You cannot continue exploration from the state that is current selected, please select \nthe most recently explored state in the path table first.");
GUISimulator.this.warning("Simulation", "You cannot continue exploration from the state that is current selected.\nSelect the last state in the path table to continue");
} }
} }
}); });
@ -2987,7 +2987,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
if (varNames.contains(parsedModel.getGlobal(g).getName())) if (varNames.contains(parsedModel.getGlobal(g).getName()))
{ {
if (groupCount == groupIndex) if (groupCount == groupIndex)
{ return "Columns in this group represent global variables"; }
{ return "Global variables"; }
groupCount++; groupCount++;
break; break;
@ -3002,7 +3002,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
if (varNames.contains(module.getDeclaration(v).getName())) if (varNames.contains(module.getDeclaration(v).getName()))
{ {
if (groupCount == groupIndex) if (groupCount == groupIndex)
{ return "Columns in this group represent variables of module \"" + parsedModel.getModuleName(m) + "\""; }
{ return "Variables of module \"" + parsedModel.getModuleName(m) + "\""; }
groupCount++; groupCount++;
break; break;
@ -3014,7 +3014,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
if (view.getVisibleRewardColumns().size() > 0) if (view.getVisibleRewardColumns().size() > 0)
{ {
if (groupCount == groupIndex) if (groupCount == groupIndex)
{ return "Columns in this group represent the state, transition and cumulative rewards of this model"; }
{ return "State, transition and cumulative rewards"; }
groupCount++; groupCount++;
} }
@ -3231,20 +3231,20 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
// The step column // The step column
if (stepStart <= columnIndex && columnIndex < timeStart) if (stepStart <= columnIndex && columnIndex < timeStart)
{ {
return "The states of this path";
return "State indices";
} }
else if (timeStart <= columnIndex && columnIndex < cumulativeTimeStart) else if (timeStart <= columnIndex && columnIndex < cumulativeTimeStart)
{ {
return "The time spent in a state";
return "Time spent in a state";
} }
else if (cumulativeTimeStart <= columnIndex && columnIndex < varStart) else if (cumulativeTimeStart <= columnIndex && columnIndex < varStart)
{ {
return "The cumulative time spent in states";
return "Cumulative time";
} }
// A variable column // A variable column
else if (varStart <= columnIndex && columnIndex < rewardStart) else if (varStart <= columnIndex && columnIndex < rewardStart)
{ {
return "The values of variable \"" + ((Variable)view.getVisibleVariables().get(columnIndex - varStart)).toString() + "\"";
return "Values of variable \"" + ((Variable)view.getVisibleVariables().get(columnIndex - varStart)).toString() + "\"";
} }
else if (rewardStart <= columnIndex) else if (rewardStart <= columnIndex)
@ -3253,11 +3253,11 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
String rewardName = column.getRewardStructure().getColumnName(); String rewardName = column.getRewardStructure().getColumnName();
if (column.isStateReward()) if (column.isStateReward())
return "The state reward of reward structure " + rewardName;
return "State reward of reward structure " + rewardName;
if (column.isTransitionReward()) if (column.isTransitionReward())
return "The transition reward of reward structure " + rewardName;
return "Transition reward of reward structure " + rewardName;
if (column.isCumulativeReward()) if (column.isCumulativeReward())
return "The cumulative reward of reward structure " + rewardName;
return "Cumulative reward of reward structure " + rewardName;
} }
} }
return "Undefined Column"; return "Undefined Column";
@ -3278,7 +3278,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
{ {
return "" + rowIndex; return "" + rowIndex;
} }
// Time column
else if (timeStart <= columnIndex && columnIndex < cumulativeTimeStart) else if (timeStart <= columnIndex && columnIndex < cumulativeTimeStart)
{ {
timeValue = new TimeValue(SimulatorEngine.getTimeSpentInPathState(rowIndex), false); timeValue = new TimeValue(SimulatorEngine.getTimeSpentInPathState(rowIndex), false);
@ -3286,14 +3286,15 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
return timeValue; return timeValue;
} }
// Cumulative time column
else if (cumulativeTimeStart <= columnIndex && columnIndex < varStart) else if (cumulativeTimeStart <= columnIndex && columnIndex < varStart)
{ {
timeValue = new TimeValue(SimulatorEngine.getCumulativeTimeSpentInPathState(rowIndex), true);
timeValue.setTimeValueUnknown(rowIndex >= SimulatorEngine.getPathSize() - 1);
timeValue = new TimeValue((rowIndex == 0) ? 0.0 : SimulatorEngine.getCumulativeTimeSpentInPathState(rowIndex - 1), true);
timeValue.setTimeValueUnknown(rowIndex >= SimulatorEngine.getPathSize());
return timeValue; return timeValue;
} }
// A variable column
// A variable column
else if (varStart <= columnIndex && columnIndex < rewardStart) else if (varStart <= columnIndex && columnIndex < rewardStart)
{ {
Variable var = ((Variable)view.getVisibleVariables().get(columnIndex - varStart)); Variable var = ((Variable)view.getVisibleVariables().get(columnIndex - varStart));
@ -3307,6 +3308,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
return variableValue; return variableValue;
} }
// A reward column
else if (rewardStart <= columnIndex) else if (rewardStart <= columnIndex)
{ {
RewardStructureColumn rewardColumn = (RewardStructureColumn)view.getVisibleRewardColumns().get(columnIndex - rewardStart); RewardStructureColumn rewardColumn = (RewardStructureColumn)view.getVisibleRewardColumns().get(columnIndex - rewardStart);
@ -3314,6 +3316,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
rewardStructureValue.setRewardStructureColumn(rewardColumn); rewardStructureValue.setRewardStructureColumn(rewardColumn);
rewardStructureValue.setRewardValueUnknown(false); rewardStructureValue.setRewardValueUnknown(false);
// A state reward column
if (rewardColumn.isStateReward()) if (rewardColumn.isStateReward())
{ {
double value = SimulatorEngine.getStateRewardOfPathState(rowIndex, rewardColumn.getRewardStructure().getIndex()); double value = SimulatorEngine.getStateRewardOfPathState(rowIndex, rewardColumn.getRewardStructure().getIndex());
@ -3322,6 +3325,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
rewardStructureValue.setRewardValueUnknown(rowIndex > SimulatorEngine.getPathSize() - 1); rewardStructureValue.setRewardValueUnknown(rowIndex > SimulatorEngine.getPathSize() - 1);
} }
// A transition reward column
else if (rewardColumn.isTransitionReward()) else if (rewardColumn.isTransitionReward())
{ {
double value = SimulatorEngine.getTransitionRewardOfPathState(rowIndex, rewardColumn.getRewardStructure().getIndex()); double value = SimulatorEngine.getTransitionRewardOfPathState(rowIndex, rewardColumn.getRewardStructure().getIndex());
@ -3330,13 +3334,21 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
rewardStructureValue.setRewardValueUnknown(rowIndex >= SimulatorEngine.getPathSize() - 1); rewardStructureValue.setRewardValueUnknown(rowIndex >= SimulatorEngine.getPathSize() - 1);
} }
// A cumulative reward column
else else
{
double value = SimulatorEngine.getTotalStateRewardOfPathState(rowIndex, rewardColumn.getRewardStructure().getIndex()) + SimulatorEngine.getTotalTransitionRewardOfPathState(rowIndex, rewardColumn.getRewardStructure().getIndex());
rewardStructureValue.setChanged(rowIndex == 0 || value != (SimulatorEngine.getTotalStateRewardOfPathState(rowIndex-1, rewardColumn.getRewardStructure().getIndex()) + SimulatorEngine.getTotalTransitionRewardOfPathState(rowIndex -1, rewardColumn.getRewardStructure().getIndex())));
rewardStructureValue.setRewardValue(new Double(value));
rewardStructureValue.setRewardValueUnknown(rowIndex >= SimulatorEngine.getPathSize() - 1);
{
if (rowIndex == 0) {
rewardStructureValue.setChanged(true);
rewardStructureValue.setRewardValue(new Double(0.0));
rewardStructureValue.setRewardValueUnknown(false);
}
else {
double value = SimulatorEngine.getTotalStateRewardOfPathState(rowIndex-1, rewardColumn.getRewardStructure().getIndex()) + SimulatorEngine.getTotalTransitionRewardOfPathState(rowIndex-1, rewardColumn.getRewardStructure().getIndex());
if (rowIndex == 1) rewardStructureValue.setChanged(value != 0.0);
else rewardStructureValue.setChanged(value != (SimulatorEngine.getTotalStateRewardOfPathState(rowIndex-2, rewardColumn.getRewardStructure().getIndex()) + SimulatorEngine.getTotalTransitionRewardOfPathState(rowIndex-2, rewardColumn.getRewardStructure().getIndex())));
rewardStructureValue.setRewardValue(new Double(value));
rewardStructureValue.setRewardValueUnknown(rowIndex >= SimulatorEngine.getPathSize());
}
} }
return rewardStructureValue; return rewardStructureValue;

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

@ -318,7 +318,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable
if (value instanceof String) if (value instanceof String)
{ {
stringValue = (String)value; stringValue = (String)value;
this.setToolTipText("State \"" + row + "\" of this path");
this.setToolTipText("State " + row);
} }
else if (value instanceof GUISimulator.TimeValue) else if (value instanceof GUISimulator.TimeValue)
{ {
@ -327,17 +327,17 @@ public class GUISimulatorPathTable extends GUIGroupedTable
{ {
stringValue = "?"; stringValue = "?";
if (timeValue.isCumulative()) if (timeValue.isCumulative())
this.setToolTipText("The cumulative time spent in states up to and including state \"" + (row) + "\" is not yet known");
this.setToolTipText("Cumulative time up until state " + (row) + " (not yet known)");
else else
this.setToolTipText("The time spent in state \"" + (row) + "\" is not yet known");
this.setToolTipText("Time spent in state " + (row) + " (not yet known)");
} }
else else
{ {
stringValue = (PrismUtils.formatDouble(simulator.getPrism().getSettings(), ((Double)timeValue.getValue()))); stringValue = (PrismUtils.formatDouble(simulator.getPrism().getSettings(), ((Double)timeValue.getValue())));
if (timeValue.isCumulative()) if (timeValue.isCumulative())
this.setToolTipText("The cumulative time spent in states up to and including state \"" + (row) + "\" is \"" + stringValue + "\" time units");
this.setToolTipText("Cumulative time up until state " + (row));
else else
this.setToolTipText("The time spent in state \"" + (row) + "\" is \"" + stringValue + "\" time units");
this.setToolTipText("Time spent in state " + (row));
} }
} }
else if (value instanceof GUISimulator.VariableValue) else if (value instanceof GUISimulator.VariableValue)
@ -345,7 +345,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable
GUISimulator.VariableValue variableValue = (GUISimulator.VariableValue)value; GUISimulator.VariableValue variableValue = (GUISimulator.VariableValue)value;
stringValue = (variableValue.getValue() instanceof Double) ? (PrismUtils.formatDouble(simulator.getPrism().getSettings(), ((Double)variableValue.getValue()))) : variableValue.getValue().toString(); 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 + "\"");
this.setToolTipText("Value of variable \"" + variableValue.getVariable().getName() + "\" in state " + (row));
} }
else if (value instanceof GUISimulator.RewardStructureValue) else if (value instanceof GUISimulator.RewardStructureValue)
{ {
@ -357,29 +357,25 @@ public class GUISimulatorPathTable extends GUIGroupedTable
stringValue = "?"; stringValue = "?";
if (rewardValue.getRewardStructureColumn().isCumulativeReward()) if (rewardValue.getRewardStructureColumn().isCumulativeReward())
this.setToolTipText("The cumulative reward of reward structure " + rewardName + " up to and including step \"" + (row) + "\" is not yet known");
this.setToolTipText("Cumulative reward of reward structure " + rewardName + " up until state " + (row) + " (not yet known)");
if (rewardValue.getRewardStructureColumn().isStateReward()) if (rewardValue.getRewardStructureColumn().isStateReward())
this.setToolTipText("The state reward of reward structure " + rewardName + " in state \"" + (row) + "\" is not yet known");
this.setToolTipText("State reward of reward structure " + rewardName + " in state " + (row) + " (not yet known)");
if (rewardValue.getRewardStructureColumn().isTransitionReward()) if (rewardValue.getRewardStructureColumn().isTransitionReward())
this.setToolTipText("The transition reward of reward structure " + rewardName + " for step \""+(row)+"\" (from state \"" + (row) + "\" to \"" + (row + 1) + "\") is not yet known");
this.setToolTipText("Transition reward of reward structure " + rewardName + " from state " + (row) + " to " + (row + 1) + " (not yet known)");
} }
else else
{ {
stringValue = PrismUtils.formatDouble(simulator.getPrism().getSettings(), rewardValue.getRewardValue()); stringValue = PrismUtils.formatDouble(simulator.getPrism().getSettings(), rewardValue.getRewardValue());
if (rewardValue.getRewardStructureColumn().isCumulativeReward()) if (rewardValue.getRewardStructureColumn().isCumulativeReward())
this.setToolTipText("The cumulative reward of reward structure " + rewardName + " up to and including step \"" + (row) + "\" is \"" + (stringValue) + "\"");
this.setToolTipText("Cumulative reward of reward structure " + rewardName + " up until state " + (row));
if (rewardValue.getRewardStructureColumn().isStateReward()) if (rewardValue.getRewardStructureColumn().isStateReward())
this.setToolTipText("The state reward of reward structure " + rewardName + " in state \"" + (row) + "\" is \"" + (stringValue) + "\"");
this.setToolTipText("State reward of reward structure " + rewardName + " in state " + (row));
if (rewardValue.getRewardStructureColumn().isTransitionReward()) if (rewardValue.getRewardStructureColumn().isTransitionReward())
this.setToolTipText("The transition reward of reward structure " + rewardName + " for step \""+(row)+"\" (from state \"" + (row) + "\" to \"" + (row + 1) + "\") is \"" + (stringValue) + "\"");
this.setToolTipText("Transition reward of reward structure " + rewardName + " from state " + (row) + " to " + (row + 1));
} }
} }
} }
public void paintComponent(Graphics g) public void paintComponent(Graphics g)
@ -390,8 +386,6 @@ public class GUISimulatorPathTable extends GUIGroupedTable
if (value instanceof String) if (value instanceof String)
{ {
String stringValue = (String)value;
double width = getStringWidth(stringValue, g2); double width = getStringWidth(stringValue, g2);
double height = g2.getFont().getSize(); double height = g2.getFont().getSize();
@ -478,13 +472,6 @@ public class GUISimulatorPathTable extends GUIGroupedTable
{ {
GUISimulator.TimeValue timeValue = (GUISimulator.TimeValue)value; 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); double width = getStringWidth(stringValue, g2);
Color color = (Color.black); Color color = (Color.black);

Write Preview
Loading…
Cancel
Save