diff --git a/prism/src/prism/ModelType.java b/prism/src/prism/ModelType.java index e112f2e6..680fdd52 100644 --- a/prism/src/prism/ModelType.java +++ b/prism/src/prism/ModelType.java @@ -72,6 +72,12 @@ public enum ModelType { return RATE; } + + @Override + ModelType removeNondeterminism() + { + return CTMC; + } }, DTMC("discrete-time Markov chain") { @Override @@ -92,9 +98,19 @@ public enum ModelType { return NEITHER; } + + @Override + ModelType removeNondeterminism() + { + return DTMC; + } }, MDP("Markov decision process") { - + @Override + ModelType removeNondeterminism() + { + return DTMC; + } }, PTA("probabilistic timed automaton") { @Override @@ -109,6 +125,12 @@ public enum ModelType { return true; } + + @Override + ModelType removeNondeterminism() + { + return DTMC; + } }, SMG("stochastic multi-player game") { @Override @@ -116,6 +138,12 @@ public enum ModelType { return true; } + + @Override + ModelType removeNondeterminism() + { + return DTMC; + } }; private static final String PROBABILITY = "Probability"; @@ -194,6 +222,19 @@ public enum ModelType return PROBABILITY; } + /** + * Return the model type that results from removing the nondeterminism + * in this model type. + *
+ * If there is no nondeterminism (or the removal of nondeterminism is not supported), + * returns the same model type. + */ + ModelType removeNondeterminism() + { + // default: same model type + return this; + } + public static ModelType parseName(String name) { try {