From b4041d946c712ba416011e61dd9778aa0be44538 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Sat, 16 Jun 2018 10:47:01 +0200
Subject: [PATCH] ModelType: add removeNondeterminism()

If we remove the nondeterminism in a model (e.g., using uniform choice
of actions in the simulator/statisticial model checking), we'd like to
know the resulting model type.
---
 prism/src/prism/ModelType.java | 43 +++++++++++++++++++++++++++++++++-
 1 file changed, 42 insertions(+), 1 deletion(-)

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.
+	 * <br>
+	 * 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 {