diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index 4fa490d0..e13b054b 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -138,7 +138,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect } 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 (groupCount == groupIndex) - { return "Columns in this group represent global variables"; } + { return "Global variables"; } groupCount++; break; @@ -3002,7 +3002,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect if (varNames.contains(module.getDeclaration(v).getName())) { if (groupCount == groupIndex) - { return "Columns in this group represent variables of module \"" + parsedModel.getModuleName(m) + "\""; } + { return "Variables of module \"" + parsedModel.getModuleName(m) + "\""; } groupCount++; break; @@ -3014,7 +3014,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect if (view.getVisibleRewardColumns().size() > 0) { 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++; } @@ -3231,20 +3231,20 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect // The step column if (stepStart <= columnIndex && columnIndex < timeStart) { - return "The states of this path"; + return "State indices"; } 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) { - return "The cumulative time spent in states"; + return "Cumulative time"; } // A variable column 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) @@ -3253,11 +3253,11 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect String rewardName = column.getRewardStructure().getColumnName(); if (column.isStateReward()) - return "The state reward of reward structure " + rewardName; + return "State reward of reward structure " + rewardName; if (column.isTransitionReward()) - return "The transition reward of reward structure " + rewardName; + return "Transition reward of reward structure " + rewardName; if (column.isCumulativeReward()) - return "The cumulative reward of reward structure " + rewardName; + return "Cumulative reward of reward structure " + rewardName; } } return "Undefined Column"; @@ -3278,7 +3278,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect { return "" + rowIndex; } - + // Time column else if (timeStart <= columnIndex && columnIndex < cumulativeTimeStart) { timeValue = new TimeValue(SimulatorEngine.getTimeSpentInPathState(rowIndex), false); @@ -3286,14 +3286,15 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect return timeValue; } + // Cumulative time column 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; } -// A variable column + // A variable column else if (varStart <= columnIndex && columnIndex < rewardStart) { Variable var = ((Variable)view.getVisibleVariables().get(columnIndex - varStart)); @@ -3307,6 +3308,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect return variableValue; } + // A reward column else if (rewardStart <= columnIndex) { RewardStructureColumn rewardColumn = (RewardStructureColumn)view.getVisibleRewardColumns().get(columnIndex - rewardStart); @@ -3314,6 +3316,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect rewardStructureValue.setRewardStructureColumn(rewardColumn); rewardStructureValue.setRewardValueUnknown(false); + // A state reward column if (rewardColumn.isStateReward()) { 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); } + // A transition reward column else if (rewardColumn.isTransitionReward()) { 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); } + // A cumulative reward column 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; diff --git a/prism/src/userinterface/simulator/GUISimulatorPathTable.java b/prism/src/userinterface/simulator/GUISimulatorPathTable.java index 95677df6..985be471 100644 --- a/prism/src/userinterface/simulator/GUISimulatorPathTable.java +++ b/prism/src/userinterface/simulator/GUISimulatorPathTable.java @@ -318,7 +318,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable if (value instanceof String) { stringValue = (String)value; - this.setToolTipText("State \"" + row + "\" of this path"); + this.setToolTipText("State " + row); } else if (value instanceof GUISimulator.TimeValue) { @@ -327,17 +327,17 @@ public class GUISimulatorPathTable extends GUIGroupedTable { stringValue = "?"; 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 - this.setToolTipText("The time spent in state \"" + (row) + "\" is not yet known"); + this.setToolTipText("Time spent in state " + (row) + " (not yet known)"); } else { stringValue = (PrismUtils.formatDouble(simulator.getPrism().getSettings(), ((Double)timeValue.getValue()))); 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 - 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) @@ -345,7 +345,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable 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 + "\""); + this.setToolTipText("Value of variable \"" + variableValue.getVariable().getName() + "\" in state " + (row)); } else if (value instanceof GUISimulator.RewardStructureValue) { @@ -357,29 +357,25 @@ public class GUISimulatorPathTable extends GUIGroupedTable stringValue = "?"; 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()) - 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()) - 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 { stringValue = PrismUtils.formatDouble(simulator.getPrism().getSettings(), rewardValue.getRewardValue()); 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()) - 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()) - 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) @@ -390,8 +386,6 @@ public class GUISimulatorPathTable extends GUIGroupedTable if (value instanceof String) { - String stringValue = (String)value; - double width = getStringWidth(stringValue, g2); double height = g2.getFont().getSize(); @@ -478,13 +472,6 @@ public class GUISimulatorPathTable extends GUIGroupedTable { 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); Color color = (Color.black);