From 5e00f01dc0c29422f4b1d61e0bbd4fa4b430b830 Mon Sep 17 00:00:00 2001 From: Mark Kattenbelt Date: Fri, 1 Dec 2006 11:55:00 +0000 Subject: [PATCH] Small update to both the Java and C part of the simulator to facilitate the display of (instant) state rewards of the most current state. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@174 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/simulator/simpath.cc | 18 ++--- .../userinterface/simulator/GUISimulator.java | 68 +++++++++++++++---- .../simulator/GUISimulatorPathTable.java | 41 ++++++++--- 3 files changed, 93 insertions(+), 34 deletions(-) diff --git a/prism/src/simulator/simpath.cc b/prism/src/simulator/simpath.cc index 24d7e6c6..e0c43e20 100644 --- a/prism/src/simulator/simpath.cc +++ b/prism/src/simulator/simpath.cc @@ -552,7 +552,6 @@ int Get_Path_Data(int var_index, int state_index) */ double Get_Time_Spent_In_Path_State(int state_index) { - if(state_index == current_index) return UNDEFINED_DOUBLE; else { @@ -568,8 +567,7 @@ double Get_Time_Spent_In_Path_State(int state_index) */ double Get_State_Reward_Of_Path_State(int state_index, int i) { - - if(state_index == current_index) return UNDEFINED_DOUBLE; + if(state_index > current_index) return UNDEFINED_DOUBLE; else return stored_path[state_index]->state_instant_cost[i]; } @@ -580,8 +578,7 @@ double Get_State_Reward_Of_Path_State(int state_index, int i) */ double Get_Transition_Reward_Of_Path_State(int state_index, int i) { - - if(state_index == current_index) return UNDEFINED_DOUBLE; + if(state_index >= current_index) return UNDEFINED_DOUBLE; else return stored_path[state_index]->transition_cost[i]; } @@ -673,19 +670,22 @@ inline void Add_Current_State_To_Path() Report_Error("Out of memory when allocating new path"); throw "out of memory error: simpath.cc 003"; } - stored_path.push_back(ps); + stored_path.push_back(ps); } } CPathState* curr_state = stored_path[current_index]; curr_state->Make_This_Current_State(); + + Calculate_State_Reward(curr_state->variables); + for(int i = 0; i < no_reward_structs; i++) { + curr_state->state_instant_cost[i] = Get_State_Reward(i); + } if(current_index > 0) { CPathState * last_state = stored_path[current_index-1]; - for(int i = 0; i < no_reward_structs; i++) { - last_state->state_instant_cost[i] = Get_State_Reward(i); - } + if(model_type == STOCHASTIC) { double time_in_state = Get_Sampled_Time(); diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java index 2b045f07..57406afe 100644 --- a/prism/src/userinterface/simulator/GUISimulator.java +++ b/prism/src/userinterface/simulator/GUISimulator.java @@ -2247,15 +2247,24 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect public class RewardStructureValue { private RewardStructure rewardStructure; - + private Double stateReward; private Double transitionReward; - + + private boolean transitionRewardUnknown; + + private boolean stateRewardVisible; + private boolean transitionRewardVisible; + public RewardStructureValue(RewardStructure rewardStructure, Double stateReward, Double transitionReward) { this.rewardStructure = rewardStructure; this.stateReward = stateReward; this.transitionReward = transitionReward; + this.transitionRewardUnknown = false; + + this.stateRewardVisible = true; + this.transitionRewardVisible = true; } public RewardStructure getRewardStructure() @@ -2277,7 +2286,37 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect public void setTransitionReward(Double transitionReward) { this.transitionReward = transitionReward; - } + } + + public void setStateRewardVisible(boolean b) + { + this.stateRewardVisible = b; + } + + public boolean isStateRewardVisible() + { + return this.stateRewardVisible; + } + + public void setTransitionRewardVisible(boolean b) + { + this.transitionRewardVisible = b; + } + + public boolean isTransitionRewardVisible() + { + return this.transitionRewardVisible; + } + + public void setTransitionRewardUnknown() + { + this.transitionRewardUnknown = true; + } + + public boolean isTransitionRewardUnknown() + { + return this.transitionRewardUnknown; + } } public class SimulationView extends Observable @@ -2693,22 +2732,23 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect else if (rewardStart <= columnIndex) { RewardStructure reward = (RewardStructure)view.getVisibleRewards().get(columnIndex - rewardStart); - if (rowIndex < SimulatorEngine.getPathSize() - 1) + if (rowIndex == SimulatorEngine.getPathSize() - 1) { RewardStructureValue value = new RewardStructureValue(reward, SimulatorEngine.getStateRewardOfPathState(rowIndex, reward.getIndex()), SimulatorEngine.getTransitionRewardOfPathState(rowIndex, reward.getIndex())); - - if (reward.isStateEmpty() && view.hideEmptyRewards()) - { value.setStateReward(null); } - - if (reward.isTransitionEmpty() && view.hideEmptyRewards()) - { value.setTransitionReward(null); } + value.setTransitionRewardUnknown(); + value.setStateRewardVisible(!(reward.isStateEmpty() && view.hideEmptyRewards())); + value.setTransitionRewardVisible(!(reward.isTransitionEmpty() && view.hideEmptyRewards())); return value; } - else - { - return "..."; - } + else if (rowIndex < SimulatorEngine.getPathSize() - 1) + { + RewardStructureValue value = new RewardStructureValue(reward, SimulatorEngine.getStateRewardOfPathState(rowIndex, reward.getIndex()), SimulatorEngine.getTransitionRewardOfPathState(rowIndex, reward.getIndex())); + value.setStateRewardVisible(!(reward.isStateEmpty() && view.hideEmptyRewards())); + value.setTransitionRewardVisible(!(reward.isTransitionEmpty() && view.hideEmptyRewards())); + + return value; + } } } } diff --git a/prism/src/userinterface/simulator/GUISimulatorPathTable.java b/prism/src/userinterface/simulator/GUISimulatorPathTable.java index cad59a27..f53c801d 100644 --- a/prism/src/userinterface/simulator/GUISimulatorPathTable.java +++ b/prism/src/userinterface/simulator/GUISimulatorPathTable.java @@ -381,25 +381,44 @@ public class GUISimulatorPathTable extends GUIGroupedTable else if (value instanceof GUISimulator.RewardStructureValue) { GUISimulator.RewardStructureValue rewardValue = (GUISimulator.RewardStructureValue)value; - if (rewardValue.getStateReward() != null && rewardValue.getTransitionReward() != null) - { - field.setText(rewardValue.getStateReward().toString() + " [ " + rewardValue.getTransitionReward().toString() + " ]"); - } - else if (rewardValue.getStateReward() == null && rewardValue.getTransitionReward() != null) + + //GUISimulator.RewardStructure reward = rewardValue.getRewardStructure(); + + String text = ""; + String tooltipText = ""; + + if (rewardValue.isStateRewardVisible()) { - field.setText("[ " + rewardValue.getTransitionReward().toString() + " ]"); + text += rewardValue.getStateReward().toString(); + tooltipText += "State reward"; } - else if (rewardValue.getStateReward() != null && rewardValue.getTransitionReward() == null) + + if (rewardValue.isStateRewardVisible() && rewardValue.isTransitionRewardVisible()) { - field.setText(rewardValue.getStateReward().toString()); + text += " "; + tooltipText += " "; } - else + + if (rewardValue.isTransitionRewardVisible()) { - field.setText(""); + text += "[ "; + text += (rewardValue.isTransitionRewardUnknown()) ? "..." : rewardValue.getTransitionReward().toString(); + text += " ]"; + + if (rewardValue.isTransitionRewardUnknown()) + { + tooltipText = "The transition reward is still unknown"; + } + else + { + tooltipText += "[ Transition reward ]"; + } } + field.setText(text); + field.setHorizontalAlignment(JTextField.CENTER); - field.setToolTipText("State Reward [ Transition Reward ]"); + field.setToolTipText(tooltipText); } else {