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

Code tidy in GUI simulator: replace ==CTMC checks with isContinuousTime(). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3446 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
72551d7248
commit
afa2d79305
2 changed files with 8 additions and 8 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. 12
      prism/src/userinterface/simulator/GUISimulator.java
  2. 4
      prism/src/userinterface/simulator/GUISimulatorPathTable.java

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

@ -255,7 +255,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
typeExploreCombo.addItem("Steps"); typeExploreCombo.addItem("Steps");
typeExploreCombo.addItem("Up to step"); typeExploreCombo.addItem("Up to step");
if (mf != null && mf.getModelType() == ModelType.CTMC) {
if (mf != null && mf.getModelType().continuousTime()) {
typeExploreCombo.addItem("Time"); typeExploreCombo.addItem("Time");
typeExploreCombo.addItem("Up to time"); typeExploreCombo.addItem("Up to time");
} }
@ -266,7 +266,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
typeBacktrackCombo.addItem("Steps"); typeBacktrackCombo.addItem("Steps");
typeBacktrackCombo.addItem("Back to step"); typeBacktrackCombo.addItem("Back to step");
if (mf != null && mf.getModelType() == ModelType.CTMC) {
if (mf != null && mf.getModelType().continuousTime()) {
typeBacktrackCombo.addItem("Time"); typeBacktrackCombo.addItem("Time");
typeBacktrackCombo.addItem("Back to time"); typeBacktrackCombo.addItem("Back to time");
} }
@ -590,7 +590,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
} }
double time = -1; double time = -1;
if (parsedModel.getModelType() == ModelType.CTMC) {
if (parsedModel.getModelType().continuousTime()) {
if (!autoTimeCheck.isSelected()) { if (!autoTimeCheck.isSelected()) {
time = GUITimeDialog.askTime(this.getGUI(), this); time = GUITimeDialog.askTime(this.getGUI(), this);
if (time < 0.0d) // dialog cancelled if (time < 0.0d) // dialog cancelled
@ -808,7 +808,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
typeBacktrackCombo.setEnabled(pathActive); typeBacktrackCombo.setEnabled(pathActive);
currentUpdatesTable.setEnabled(pathActive && !computing); currentUpdatesTable.setEnabled(pathActive && !computing);
autoTimeCheck.setEnabled(pathActive && parsedModel != null && parsedModel.getModelType() == ModelType.CTMC);
autoTimeCheck.setEnabled(pathActive && parsedModel != null && parsedModel.getModelType().continuousTime());
//resetPathButton.setEnabled(pathActive && !computing); //resetPathButton.setEnabled(pathActive && !computing);
//exportPathButton.setEnabled(pathActive && !computing); //exportPathButton.setEnabled(pathActive && !computing);
@ -823,8 +823,8 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
modelType.setEnabled(parsedModel != null); modelType.setEnabled(parsedModel != null);
modelTypeLabel.setEnabled(parsedModel != null); modelTypeLabel.setEnabled(parsedModel != null);
totalTime.setEnabled(pathActive && parsedModel != null && parsedModel.getModelType() == ModelType.CTMC);
totalTimeLabel.setEnabled(pathActive && parsedModel != null && parsedModel.getModelType() == ModelType.CTMC);
totalTime.setEnabled(pathActive && parsedModel != null && parsedModel.getModelType().continuousTime());
totalTimeLabel.setEnabled(pathActive && parsedModel != null && parsedModel.getModelType().continuousTime());
pathLength.setEnabled(pathActive); pathLength.setEnabled(pathActive);
pathLengthLabel.setEnabled(pathActive); pathLengthLabel.setEnabled(pathActive);

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

@ -389,7 +389,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable
// Reward value // Reward value
else if (value instanceof RewardStructureValue) { else if (value instanceof RewardStructureValue) {
RewardStructureValue rewardValue = (RewardStructureValue) value; RewardStructureValue rewardValue = (RewardStructureValue) value;
// Default case (everything except cumulative for CTMCs)
// Default case (everything except cumulative time)
if (!(ptm.canShowTime() && rewardValue.getRewardStructureColumn().isCumulativeReward())) { if (!(ptm.canShowTime() && rewardValue.getRewardStructureColumn().isCumulativeReward())) {
// Position (horiz centred, vert centred) // Position (horiz centred, vert centred)
x = (getWidth() / 2) - (width / 2); x = (getWidth() / 2) - (width / 2);
@ -423,7 +423,7 @@ public class GUISimulatorPathTable extends GUIGroupedTable
g2.drawString(stringValue, x, y); g2.drawString(stringValue, x, y);
} }
} }
// For cumulative rewards on CTMCs, we left-align (like for display of time)
// For continuous-time cumulative rewards, we left-align (like for display of time)
else { else {
// Position (left aligned, vert centred) // Position (left aligned, vert centred)
x = 3; x = 3;

Write Preview
Loading…
Cancel
Save