diff --git a/prism/src/automata/LTL2WDBA.java b/prism/src/automata/LTL2WDBA.java
index 371805c8..16b4ed47 100644
--- a/prism/src/automata/LTL2WDBA.java
+++ b/prism/src/automata/LTL2WDBA.java
@@ -50,7 +50,7 @@ import acceptance.AcceptanceReach;
 import common.IterableBitSet;
 
 import explicit.LTS;
-import explicit.LTSExplicit;
+import explicit.LTSSimple;
 import explicit.NonProbModelChecker;
 import explicit.SCCComputer;
 import explicit.SCCConsumerStore;
@@ -510,7 +510,7 @@ public class LTL2WDBA extends PrismComponent
 		BitSet expanded = new BitSet();
 		BitSet F = new BitSet();
 
-		LTSExplicit lts = new LTSExplicit();
+		LTSSimple lts = new LTSSimple();
 
 		for (int startNBA : IterableBitSet.getSetBits(p.idToState.get(lasso.cycleStart))) {
 			int i = lts.addState();
@@ -552,7 +552,7 @@ public class LTL2WDBA extends PrismComponent
 					//System.out.println("new: " + prodTo + " = " +toProd);
 				}
 
-				lts.addEdge(curProd, prodTo);
+				lts.addTransition(curProd, prodTo);
 				//System.out.println(" " + curProd +" -> " +prodTo);
 			}
 		}
diff --git a/prism/src/automata/LTSFromDA.java b/prism/src/automata/LTSFromDA.java
index 53e2aa88..0dac7613 100644
--- a/prism/src/automata/LTSFromDA.java
+++ b/prism/src/automata/LTSFromDA.java
@@ -193,4 +193,12 @@ public class LTSFromDA extends ModelExplicit implements LTS
 	{
 		throw new RuntimeException("Not implemented yet");
 	}
+	
+	// Methods to implement LTS
+	
+	@Override
+	public int getSuccessor(int s, int i)
+	{
+		return da.getEdgeDest(s, i); 
+	}
 }
diff --git a/prism/src/explicit/LTS.java b/prism/src/explicit/LTS.java
index 294f9ab3..d82fffd7 100644
--- a/prism/src/explicit/LTS.java
+++ b/prism/src/explicit/LTS.java
@@ -93,4 +93,11 @@ public interface LTS extends NondetModel
 	{
 		throw new UnsupportedOperationException();
 	}
+	
+	// Accessors
+	
+	/**
+	 * Get the successor state for the {@code i}th choice/transition from state {@code s}.
+	 */
+	public int getSuccessor(int s, int i);
 }
diff --git a/prism/src/explicit/LTSNBAProduct.java b/prism/src/explicit/LTSNBAProduct.java
index 3957e90d..ba6588e8 100644
--- a/prism/src/explicit/LTSNBAProduct.java
+++ b/prism/src/explicit/LTSNBAProduct.java
@@ -163,7 +163,7 @@ public class LTSNBAProduct extends Product<Model>
 		HashMap<ProductState, Integer> productStateToProductId = new HashMap<ProductState, Integer>();
 
 		// storage for the product model
-		LTSExplicit productModel = new LTSExplicit();
+		LTSSimple productModel = new LTSSimple();
 		// the accepting states in the product model
 		BitSet acceptingStates = new BitSet();
 
@@ -257,7 +257,7 @@ public class LTSNBAProduct extends Product<Model>
 					}
 
 					// add the edge
-					productModel.addEdge(fromId, successorID);
+					productModel.addTransition(fromId, successorID);
 				}
 
 				// fromId is fully expanded in the product
diff --git a/prism/src/explicit/LTSSimple.java b/prism/src/explicit/LTSSimple.java
new file mode 100644
index 00000000..d0267c3a
--- /dev/null
+++ b/prism/src/explicit/LTSSimple.java
@@ -0,0 +1,268 @@
+//==============================================================================
+//	
+//	Copyright (c) 2016-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+
+package explicit;
+
+import java.util.ArrayList;
+import java.util.BitSet;
+import java.util.List;
+
+import prism.PrismException;
+import strat.MDStrategy;
+
+/**
+ * Simple explicit-state representation of an LTS (labelled transition system).
+ * 
+ * Each transition from a state is considered to be a separate (singleton) "choice",
+ * following the terminology in other nondeterministic explicit-state models.
+ */
+public class LTSSimple extends ModelExplicit implements LTS, NondetModelSimple
+{
+	// Transition relation
+	protected List<List<Integer>> trans;
+	
+	// Statistics: total number of transitions
+	protected int numTransitions;
+
+	// Constructors
+
+	/**
+	 * Constructor: empty LTS.
+	 */
+	public LTSSimple()
+	{
+		initialise(0);
+	}
+
+	/**
+	 * Constructor: new LTS with fixed number of states.
+	 */
+	public LTSSimple(int numStates)
+	{
+		initialise(numStates);
+	}
+
+	/**
+	 * Construct an LTS from an existing one.
+	 */
+	public LTSSimple(LTSSimple lts)
+	{
+		this(lts.getNumStates());
+		copyFrom(lts);
+		// Copy storage directly
+		for (int s = 0; s < numStates; s++) {
+			List<Integer> succs = trans.get(s);
+			for (int succ : lts.trans.get(s)) {
+				succs.add(succ);
+			}
+		}
+		// Copy stats too
+		numTransitions = lts.numTransitions;
+	}
+
+	/**
+	 * Construct an LTS from an existing one and a state index permutation,
+	 * i.e. in which state index i becomes index permut[i].
+	 */
+	public LTSSimple(LTSSimple lts, int permut[])
+	{
+		this(lts.getNumStates());
+		copyFrom(lts, permut);
+		// Copy storage directly
+		for (int s = 0; s < numStates; s++) {
+			List<Integer> succs = trans.get(permut[s]);
+			for (int succ : lts.trans.get(s)) {
+				succs.add(permut[succ]);
+			}
+		}
+		// Copy stats too
+		numTransitions = lts.numTransitions;
+	}
+
+	// Mutators (for ModelSimple)
+
+	@Override
+	public void initialise(int numStates)
+	{
+		super.initialise(numStates);
+		trans = new ArrayList<List<Integer>>();
+		for (int i = 0; i < numStates; i++) {
+			trans.add(new ArrayList<Integer>());
+		}
+		numTransitions = 0;
+	}
+
+	@Override
+	public void clearState(int s)
+	{
+		// Clear data structures and update stats
+		List<Integer> list = trans.get(s);
+		numTransitions -= list.size();
+		list.clear();
+	}
+
+	@Override
+	public int addState()
+	{
+		addStates(1);
+		return numStates - 1;
+	}
+
+	@Override
+	public void addStates(int numToAdd)
+	{
+		for (int i = 0; i < numToAdd; i++) {
+			trans.add(new ArrayList<Integer>());
+			numStates++;
+		}
+	}
+
+	@Override
+	public void buildFromPrismExplicit(String filename) throws PrismException
+	{
+		throw new UnsupportedOperationException();
+	}
+
+	// Mutators (other)
+	
+	public void addTransition(int s, int t)
+	{
+		// We don't care if a transition from s to t already exists
+		trans.get(s).add(t);
+		numTransitions++;
+	}
+
+	// Accessors (for Model)
+	
+	@Override
+	public int getNumTransitions()
+	{
+		return numTransitions;
+	}
+
+	@Override
+	public int getNumTransitions(int s)
+	{
+		return getNumChoices(s);
+	}
+
+	@Override
+	public void findDeadlocks(boolean fix) throws PrismException
+	{
+		for (int i = 0; i < numStates; i++) {
+			if (trans.get(i).isEmpty()) {
+				addDeadlockState(i);
+				if (fix) {
+					addTransition(i, i);
+				}
+			}
+		}
+	}
+
+	@Override
+	public void checkForDeadlocks(BitSet except) throws PrismException
+	{
+		for (int i = 0; i < numStates; i++) {
+			if (trans.get(i).isEmpty() && (except == null || !except.get(i)))
+				throw new PrismException("Model has a deadlock in state " + i);
+		}
+	}
+	
+	// Accessors (for NondetModel)
+
+	@Override
+	public int getNumChoices(int s)
+	{
+		// one choice per successor for s
+		return trans.get(s).size();
+	}
+
+	@Override
+	public int getNumChoices()
+	{
+		return numTransitions;
+	}
+
+	@Override
+	public Object getAction(int s, int i)
+	{
+		// we don't have action labels
+		return null;
+	}
+
+	@Override
+	public int getNumTransitions(int s, int i)
+	{
+		if (i < getNumChoices(s)) {
+			// one transition per choice
+			return 1;
+		}
+		throw new IllegalArgumentException();
+	}
+
+	@Override
+	public boolean allSuccessorsInSet(int s, int i, BitSet set)
+	{
+		// single successor for s, i
+		return set.get(trans.get(s).get(i));
+	}
+
+	@Override
+	public boolean someSuccessorsInSet(int s, int i, BitSet set)
+	{
+		// single successor for s, i
+		return set.get(trans.get(s).get(i));
+	}
+
+	@Override
+	public SuccessorsIterator getSuccessors(int s, int i)
+	{
+		// single successor for s, i
+		return SuccessorsIterator.fromSingleton(trans.get(s).get(i));
+	}
+
+	@Override
+	public SuccessorsIterator getSuccessors(int s)
+	{
+		return SuccessorsIterator.from(trans.get(s).iterator(), false);
+	}
+
+	@Override
+	public Model constructInducedModel(MDStrategy strat)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	// Accessors (for LTS)
+	
+	@Override
+	public int getSuccessor(int s, int i)
+	{
+		return trans.get(s).get(i); 
+	}
+}
diff --git a/prism/src/explicit/LTSExplicit.java b/prism/src/explicit/LTSSimple.java~Convert LTSExplicit to LTSSimple.
similarity index 50%
rename from prism/src/explicit/LTSExplicit.java
rename to prism/src/explicit/LTSSimple.java~Convert LTSExplicit to LTSSimple.
index 65a54292..0706a4df 100644
--- a/prism/src/explicit/LTSExplicit.java
+++ b/prism/src/explicit/LTSSimple.java~Convert LTSExplicit to LTSSimple.	
@@ -3,6 +3,7 @@
 //	Copyright (c) 2016-
 //	Authors:
 //	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham)
 //	
 //------------------------------------------------------------------------------
 //	
@@ -29,135 +30,212 @@ package explicit;
 
 import java.util.ArrayList;
 import java.util.BitSet;
+import java.util.List;
 
 import prism.PrismException;
 import strat.MDStrategy;
 
 /**
- * This is a minimal implementation of an explicitly stored labeled transition system.
- * Each target state of an edge is modeled as a choice, with a single transition for
- * this choice.
+ * Simple explicit-state representation of an LTS (labelled transition system).
+ * 
+ * Each transition from a state is considered to be a separate (singleton) "choice",
+ * following the terminology in other nondeterministic explicit-state models.
  */
-public class LTSExplicit extends ModelExplicit implements LTS
+public class LTSSimple extends ModelExplicit implements LTS, NondetModelSimple
 {
-	protected ArrayList<ArrayList<Integer>> successors = new ArrayList<ArrayList<Integer>>();
-	protected int numTransitions = 0;
-	protected int maxNumChoices = 0;
+	// Transition relation
+	protected List<List<Integer>> trans;
+	
+	// Statistics: total number of transitions
+	protected int numTransitions;
 
-	public LTSExplicit()
+	// Constructors
+
+	/**
+	 * Constructor: empty LTS.
+	 */
+	public LTSSimple()
 	{
 		initialise(0);
 	}
 
-	public int addState()
+	/**
+	 * Constructor: new LTS with fixed number of states.
+	 */
+	public LTSSimple(int numStates)
 	{
-		successors.add(new ArrayList<Integer>());
-		return numStates++;
+		initialise(numStates);
 	}
 
-	public void addEdge(int s, int t)
+	/**
+	 * Construct an LTS from an existing one and a state index permutation,
+	 * i.e. in which state index i becomes index permut[i].
+	 */
+	public LTSSimple(LTSSimple lts, int permut[])
 	{
-		// we don't care if an edge from s to t already exists
-		successors.get(s).add(t);
-		numTransitions++;
-		maxNumChoices = Math.max(getNumChoices(s), maxNumChoices);
+		this(lts.getNumStates());
+		copyFrom(lts, permut);
+		// Copy storage directly
+		for (int s = 0; s < numStates; s++) {
+			List<Integer> succs = trans.get(permut[s]);
+			for (int succ : lts.trans.get(s)) {
+				succs.add(permut[succ]);
+			}
+		}
+		// Copy stats too
+		numTransitions = lts.numTransitions;
 	}
 
+	// Mutators (for ModelSimple)
+
 	@Override
-	public int getNumChoices(int s)
+	public void initialise(int numStates)
 	{
-		// one choice per successor for s
-		return successors.get(s).size();
+		super.initialise(numStates);
+		trans = new ArrayList<List<Integer>>();
+		for (int i = 0; i < numStates; i++) {
+			trans.add(new ArrayList<Integer>());
+		}
+		numTransitions = 0;
 	}
 
 	@Override
-	public int getMaxNumChoices()
+	public void clearState(int s)
 	{
-		return maxNumChoices;
+		// Clear data structures and update stats
+		List<Integer> list = trans.get(s);
+		numTransitions -= list.size();
+		list.clear();
 	}
 
 	@Override
-	public int getNumChoices()
+	public int addState()
+	{
+		addStates(1);
+		return numStates - 1;
+	}
+
+	@Override
+	public void addStates(int numToAdd)
+	{
+		for (int i = 0; i < numToAdd; i++) {
+			trans.add(new ArrayList<Integer>());
+			numStates++;
+		}
+	}
+
+	@Override
+	public void buildFromPrismExplicit(String filename) throws PrismException
+	{
+		throw new UnsupportedOperationException();
+	}
+
+	// Mutators (other)
+	
+	public void addTransition(int s, int t)
+	{
+		// We don't care if a transition from s to t already exists
+		trans.get(s).add(t);
+		numTransitions++;
+	}
+
+	// Accessors (for Model)
+	
+	@Override
+	public int getNumTransitions()
 	{
 		return numTransitions;
 	}
 
 	@Override
-	public Object getAction(int s, int i)
+	public int getNumTransitions(int s)
 	{
-		// we don't have action labels
-		return null;
+		return getNumChoices(s);
 	}
 
 	@Override
-	public int getNumTransitions(int s, int i)
+	public void findDeadlocks(boolean fix) throws PrismException
 	{
-		if (i < getNumChoices(s)) {
-			// one transition per choice
-			return 1;
+		for (int i = 0; i < numStates; i++) {
+			if (trans.get(i).isEmpty()) {
+				addDeadlockState(i);
+				if (fix) {
+					addTransition(i, i);
+				}
+			}
 		}
-		throw new IllegalArgumentException();
 	}
 
 	@Override
-	public boolean allSuccessorsInSet(int s, int i, BitSet set)
+	public void checkForDeadlocks(BitSet except) throws PrismException
 	{
-		// single successor for s, i
-		return set.get(successors.get(s).get(i));
+		for (int i = 0; i < numStates; i++) {
+			if (trans.get(i).isEmpty() && (except == null || !except.get(i)))
+				throw new PrismException("Model has a deadlock in state " + i);
+		}
 	}
+	
+	// Accessors (for NondetModel)
 
 	@Override
-	public boolean someSuccessorsInSet(int s, int i, BitSet set)
+	public int getNumChoices(int s)
 	{
-		// single successor for s, i
-		return set.get(successors.get(s).get(i));
+		// one choice per successor for s
+		return trans.get(s).size();
 	}
 
 	@Override
-	public SuccessorsIterator getSuccessors(int s, int i)
+	public int getNumChoices()
 	{
-		// single successor for s, i
-		return SuccessorsIterator.fromSingleton(successors.get(s).get(i));
+		return numTransitions;
 	}
 
 	@Override
-	public Model constructInducedModel(MDStrategy strat)
+	public Object getAction(int s, int i)
 	{
-		throw new UnsupportedOperationException();
+		// we don't have action labels
+		return null;
 	}
 
 	@Override
-	public SuccessorsIterator getSuccessors(int s)
+	public int getNumTransitions(int s, int i)
 	{
-		return SuccessorsIterator.from(successors.get(s).iterator(), false);
+		if (i < getNumChoices(s)) {
+			// one transition per choice
+			return 1;
+		}
+		throw new IllegalArgumentException();
 	}
 
 	@Override
-	public void findDeadlocks(boolean fix) throws PrismException
+	public boolean allSuccessorsInSet(int s, int i, BitSet set)
 	{
-		throw new UnsupportedOperationException();
+		// single successor for s, i
+		return set.get(trans.get(s).get(i));
 	}
 
 	@Override
-	public void buildFromPrismExplicit(String filename) throws PrismException
+	public boolean someSuccessorsInSet(int s, int i, BitSet set)
 	{
-		throw new UnsupportedOperationException();
+		// single successor for s, i
+		return set.get(trans.get(s).get(i));
 	}
 
 	@Override
-	public int getNumTransitions()
+	public SuccessorsIterator getSuccessors(int s, int i)
 	{
-		return numTransitions;
+		// single successor for s, i
+		return SuccessorsIterator.fromSingleton(trans.get(s).get(i));
 	}
 
 	@Override
-	public int getNumTransitions(int s)
+	public SuccessorsIterator getSuccessors(int s)
 	{
-		return getNumChoices(s);
+		return SuccessorsIterator.from(trans.get(s).iterator(), false);
 	}
 
 	@Override
-	public void checkForDeadlocks(BitSet except) throws PrismException
+	public Model constructInducedModel(MDStrategy strat)
 	{
 		throw new UnsupportedOperationException();
 	}
diff --git a/prism/src/explicit/LTSSimple.java~HEAD b/prism/src/explicit/LTSSimple.java~HEAD
new file mode 100644
index 00000000..a5694d59
--- /dev/null
+++ b/prism/src/explicit/LTSSimple.java~HEAD
@@ -0,0 +1,305 @@
+//==============================================================================
+//	
+//	Copyright (c) 2016-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+
+package explicit;
+
+import java.util.ArrayList;
+import java.util.BitSet;
+import java.util.List;
+
+import prism.PrismException;
+import strat.MDStrategy;
+
+/**
+ * Simple explicit-state representation of an LTS (labelled transition system).
+ * 
+ * Each transition from a state is considered to be a separate (singleton) "choice",
+ * following the terminology in other nondeterministic explicit-state models.
+ */
+public class LTSSimple extends ModelExplicit implements LTS, NondetModelSimple
+{
+	// Transition relation
+	protected List<List<Integer>> trans;
+	
+	// Action labels
+	protected ChoiceActionsSimple actions;
+
+	// Statistics: total number of transitions
+	protected int numTransitions;
+
+	// Constructors
+
+	/**
+	 * Constructor: empty LTS.
+	 */
+	public LTSSimple()
+	{
+		initialise(0);
+	}
+
+	/**
+	 * Constructor: new LTS with fixed number of states.
+	 */
+	public LTSSimple(int numStates)
+	{
+		initialise(numStates);
+	}
+
+	/**
+	 * Construct an LTS from an existing one.
+	 */
+	public LTSSimple(LTSSimple lts)
+	{
+		this(lts.getNumStates());
+		copyFrom(lts);
+		// Copy storage directly
+		for (int s = 0; s < numStates; s++) {
+			List<Integer> succs = trans.get(s);
+			for (int succ : lts.trans.get(s)) {
+				succs.add(succ);
+			}
+		}
+		actions = new ChoiceActionsSimple(lts.actions);
+		// Copy stats too
+		numTransitions = lts.numTransitions;
+	}
+
+	/**
+	 * Construct an LTS from an existing one and a state index permutation,
+	 * i.e. in which state index i becomes index permut[i].
+	 */
+	public LTSSimple(LTSSimple lts, int permut[])
+	{
+		this(lts.getNumStates());
+		copyFrom(lts, permut);
+		// Copy storage directly
+		for (int s = 0; s < numStates; s++) {
+			List<Integer> succs = trans.get(permut[s]);
+			for (int succ : lts.trans.get(s)) {
+				succs.add(permut[succ]);
+			}
+		}
+		actions = new ChoiceActionsSimple(lts.actions, permut);
+		// Copy stats too
+		numTransitions = lts.numTransitions;
+	}
+
+	// Mutators (for ModelSimple)
+
+	@Override
+	public void initialise(int numStates)
+	{
+		super.initialise(numStates);
+		trans = new ArrayList<List<Integer>>();
+		for (int i = 0; i < numStates; i++) {
+			trans.add(new ArrayList<Integer>());
+		}
+		actions = new ChoiceActionsSimple();
+		numTransitions = 0;
+	}
+
+	@Override
+	public void clearState(int s)
+	{
+		// Clear data structures and update stats
+		List<Integer> list = trans.get(s);
+		numTransitions -= list.size();
+		list.clear();
+		actions.clearState(s);
+	}
+
+	@Override
+	public int addState()
+	{
+		addStates(1);
+		return numStates - 1;
+	}
+
+	@Override
+	public void addStates(int numToAdd)
+	{
+		for (int i = 0; i < numToAdd; i++) {
+			trans.add(new ArrayList<Integer>());
+			numStates++;
+		}
+	}
+
+	@Override
+	public void buildFromPrismExplicit(String filename) throws PrismException
+	{
+		throw new UnsupportedOperationException();
+	}
+
+	// Mutators (other)
+	
+	/**
+	 * Add a transition from state {@code s} (which must exist) to state {code t}.
+	 */
+	public void addTransition(int s, int t)
+	{
+		// We don't care if a transition from s to t already exists
+		trans.get(s).add(t);
+		numTransitions++;
+	}
+
+	/**
+	 * Add a transition from state {@code s} (which must exist)
+	 * to state {code t}, labelled with {@code action}.
+	 */
+	public void addActionLabelledTransition(int s, int t, Object action)
+	{
+		// We don't care if a transition from s to t already exists
+		trans.get(s).add(t);
+		actions.setAction(s, trans.get(s).size() - 1, action);
+		numTransitions++;
+	}
+
+	/**
+	 * Set the action label for choice/transition i in some state s.
+	 * Note that i is the index of the choice/transition, not the destination.
+	 */
+	public void setAction(int s, int i, Object action)
+	{
+		actions.setAction(s, i, action);
+	}
+
+	// Accessors (for Model)
+	
+	@Override
+	public int getNumTransitions()
+	{
+		return numTransitions;
+	}
+
+	@Override
+	public int getNumTransitions(int s)
+	{
+		return getNumChoices(s);
+	}
+
+	@Override
+	public void findDeadlocks(boolean fix) throws PrismException
+	{
+		for (int i = 0; i < numStates; i++) {
+			if (trans.get(i).isEmpty()) {
+				addDeadlockState(i);
+				if (fix) {
+					addTransition(i, i);
+				}
+			}
+		}
+	}
+
+	@Override
+	public void checkForDeadlocks(BitSet except) throws PrismException
+	{
+		for (int i = 0; i < numStates; i++) {
+			if (trans.get(i).isEmpty() && (except == null || !except.get(i)))
+				throw new PrismException("Model has a deadlock in state " + i);
+		}
+	}
+	
+	// Accessors (for NondetModel)
+
+	@Override
+	public int getNumChoices(int s)
+	{
+		// one choice per successor for s
+		return trans.get(s).size();
+	}
+
+	@Override
+	public int getNumChoices()
+	{
+		return numTransitions;
+	}
+
+	@Override
+	public Object getAction(int s, int i)
+	{
+		return actions.getAction(s, i);
+	}
+
+	@Override
+	public boolean areAllChoiceActionsUnique()
+	{
+		// as we don't assign action labels, they are not unique
+		return false;
+	}
+
+	@Override
+	public int getNumTransitions(int s, int i)
+	{
+		if (i < getNumChoices(s)) {
+			// one transition per choice
+			return 1;
+		}
+		throw new IllegalArgumentException();
+	}
+
+	@Override
+	public boolean allSuccessorsInSet(int s, int i, BitSet set)
+	{
+		// single successor for s, i
+		return set.get(trans.get(s).get(i));
+	}
+
+	@Override
+	public boolean someSuccessorsInSet(int s, int i, BitSet set)
+	{
+		// single successor for s, i
+		return set.get(trans.get(s).get(i));
+	}
+
+	@Override
+	public SuccessorsIterator getSuccessors(int s, int i)
+	{
+		// single successor for s, i
+		return SuccessorsIterator.fromSingleton(trans.get(s).get(i));
+	}
+
+	@Override
+	public SuccessorsIterator getSuccessors(int s)
+	{
+		return SuccessorsIterator.from(trans.get(s).iterator(), false);
+	}
+
+	@Override
+	public Model constructInducedModel(MDStrategy strat)
+	{
+		throw new UnsupportedOperationException();
+	}
+	
+	// Accessors (for LTS)
+	
+	@Override
+	public int getSuccessor(int s, int i)
+	{
+		return trans.get(s).get(i); 
+	}
+}