Browse Source

Added ModelType.probabilityOrRate() method, used in simulator.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3447 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 15 years ago
parent
commit
6b21b0543d
  1. 15
      prism/src/prism/ModelType.java
  2. 6
      prism/src/userinterface/simulator/GUISimulator.java

15
prism/src/prism/ModelType.java

@ -135,6 +135,21 @@ public enum ModelType {
return true; return true;
} }
/**
* Does this model have probabilities or rates?
* @return "Probability" or "Rate"
*/
public String probabilityOrRate()
{
switch (this) {
case CTMC:
case CTMDP:
return "Rate";
default:
return "Probability";
}
}
public static ModelType parseName(String name) public static ModelType parseName(String name)
{ {
if ("ctmc".equals(name)) if ("ctmc".equals(name))

6
prism/src/userinterface/simulator/GUISimulator.java

@ -2077,11 +2077,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
case 0: case 0:
return "Module/[action]"; return "Module/[action]";
case 1: { case 1: {
if (parsedModel != null && parsedModel.getModelType() == ModelType.CTMC)
return "Rate";
else
return "Probability";
return parsedModel == null ? "Probability" : parsedModel.getModelType().probabilityOrRate();
} }
case 2: case 2:
return "Update"; return "Update";

Loading…
Cancel
Save