From 086bdb1ee6ed44582900d728078e2ef59553b431 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Thu, 8 Feb 2018 10:37:38 +0100
Subject: [PATCH] DTMCUniformisedSimple: add deadlock accessor methods

As noted in #48, DTMCUniformisedSimple does not implement the full range of ModelExplicit methods. Trying to use it outside of the areas where it's currently used in PRISM can then lead to NullPointerExceptions etc.

We add here accessors for the deadlock states, passing through the method calls to the underlying CTMC.

Additionally, point to the fully-featured uniformised DTMC object / construction method.
---
 prism/src/explicit/DTMCUniformisedSimple.java | 29 +++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/prism/src/explicit/DTMCUniformisedSimple.java b/prism/src/explicit/DTMCUniformisedSimple.java
index b5bf79ac..ec766b86 100644
--- a/prism/src/explicit/DTMCUniformisedSimple.java
+++ b/prism/src/explicit/DTMCUniformisedSimple.java
@@ -42,6 +42,10 @@ import explicit.rewards.MCRewards;
 /**
 * Simple explicit-state representation of a DTMC, constructed (implicitly) as the uniformised DTMC of a CTMC.
 * This class is read-only: most of data is pointers to other model info.
+* <br>
+* Note: This implicitly constructed DTMC does not provide implementations for
+* all methods of a full DTMCExplicit model. See {@link CTMCSimple#buildUniformisedDTMC} for
+* a method to obtain an explicit uniformised DTMC.
 */
 public class DTMCUniformisedSimple extends DTMCExplicit
 {
@@ -114,6 +118,31 @@ public class DTMCUniformisedSimple extends DTMCExplicit
 		return ctmc.isInitialState(i);
 	}
 
+	@Override
+	public int getNumDeadlockStates()
+	{
+		return ctmc.getNumDeadlockStates();
+	}
+
+	@Override
+	public Iterable<Integer> getDeadlockStates()
+	{
+		return ctmc.getDeadlockStates();
+	}
+
+	@Override
+	public StateValues getDeadlockStatesList()
+	{
+		return ctmc.getDeadlockStatesList();
+	}
+
+	@Override
+	public int getFirstDeadlockState()
+	{
+		return ctmc.getFirstDeadlockState();
+	}
+
+	@Override
 	public boolean isDeadlockState(int i)
 	{
 		return ctmc.isDeadlockState(i);