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

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
master
Mark Kattenbelt 19 years ago
parent
a7874d4790
commit
5e00f01dc0
3 changed files with 93 additions and 34 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. 18
      prism/src/simulator/simpath.cc
  2. 68
      prism/src/userinterface/simulator/GUISimulator.java
  3. 41
      prism/src/userinterface/simulator/GUISimulatorPathTable.java

18
prism/src/simulator/simpath.cc
View File

@ -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();

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

@ -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;
}
}
}
}

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

@ -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
{

Write Preview
Loading…
Cancel
Save