diff --git a/prism/src/explicit/DTMC.java b/prism/src/explicit/DTMC.java
index 5b17c9fd..0a56fdc1 100644
--- a/prism/src/explicit/DTMC.java
+++ b/prism/src/explicit/DTMC.java
@@ -41,14 +41,14 @@ public class DTMC extends Model
 	public static ModelType modelType = ModelType.DTMC;
 
 	// Transition matrix (distribution list) 
-	public List<Distribution> trans;
+	protected List<Distribution> trans;
 
 	// Rewards
-	private List<Double> transRewards;
-	private Double transRewardsConstant;
+	protected List<Double> transRewards;
+	protected Double transRewardsConstant;
 
 	// Other statistics
-	public int numTransitions;
+	protected int numTransitions;
 
 	/**
 	 * Constructor: empty DTMC.
@@ -171,6 +171,14 @@ public class DTMC extends Model
 		return 1;
 	}
 
+	/**
+	 * Get the transitions (a distribution) for state s.
+	 */
+	public Distribution getTransitions(int s)
+	{
+		return trans.get(s);
+	}
+	
 	/**
 	 * Get the transition reward (if any) for the transitions in state s.
 	 */
@@ -191,6 +199,14 @@ public class DTMC extends Model
 		return trans.get(s1).contains(s2);
 	}
 	
+	/**
+	 * Get the total number of transitions in the model.
+	 */
+	public int getNumTransitions()
+	{
+		return numTransitions;
+	}
+	
 	/**
 	 * Checks for deadlocks (states with no transitions) and throws an exception if any exist.
 	 * States in 'except' (If non-null) are excluded from the check.
diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java
index 08925f3d..ac3dfbe0 100644
--- a/prism/src/explicit/MDP.java
+++ b/prism/src/explicit/MDP.java
@@ -42,22 +42,20 @@ public class MDP extends Model
 	public static ModelType modelType = ModelType.MDP;
 
 	// Transition function (Steps)
-	public List<ArrayList<Distribution>> steps;
+	protected List<List<Distribution>> trans;
 
 	// Rewards
-	private List<List<Double>> transRewards;
-	private Double transRewardsConstant;
+	protected List<List<Double>> transRewards;
+	protected Double transRewardsConstant;
 
-	// Flag: allow dupes in distribution sets?
-	public boolean allowDupes = false;
+	// Flag: allow duplicates in distribution sets?
+	protected boolean allowDupes = false;
 
 	// Other statistics
-	public int numDistrs;
-	public int numTransitions;
-	public int maxNumDistrs;
-	public boolean maxNumDistrsOk;
-
-	// TODO: add accessor for maxNumDistrs that recomputes if necessary 
+	protected int numDistrs;
+	protected int numTransitions;
+	protected int maxNumDistrs;
+	protected boolean maxNumDistrsOk;
 
 	/**
 	 * Constructor: empty MDP.
@@ -83,9 +81,9 @@ public class MDP extends Model
 		super.initialise(numStates);
 		numDistrs = numTransitions = maxNumDistrs = 0;
 		maxNumDistrsOk = true;
-		steps = new ArrayList<ArrayList<Distribution>>(numStates);
+		trans = new ArrayList<List<Distribution>>(numStates);
 		for (int i = 0; i < numStates; i++) {
-			steps.add(new ArrayList<Distribution>());
+			trans.add(new ArrayList<Distribution>());
 		}
 		clearAllRewards();
 	}
@@ -99,13 +97,13 @@ public class MDP extends Model
 		if (s >= numStates || s < 0)
 			return;
 		// Clear data structures and update stats
-		List<Distribution> list = steps.get(s);
+		List<Distribution> list = trans.get(s);
 		numDistrs -= list.size();
 		for (Distribution distr : list) {
 			numTransitions -= distr.size();
 		}
-		//TODO: recompute maxNumDistrs (reset maxNumDistrsOk flag)
-		steps.get(s).clear();
+		maxNumDistrsOk = false;
+		trans.get(s).clear();
 		if (transRewards != null && transRewards.get(s) != null)
 			transRewards.get(s).clear();
 	}
@@ -125,7 +123,7 @@ public class MDP extends Model
 	public void addStates(int numToAdd)
 	{
 		for (int i = 0; i < numToAdd; i++) {
-			steps.add(new ArrayList<Distribution>());
+			trans.add(new ArrayList<Distribution>());
 			if (transRewards != null)
 				transRewards.add(null);
 			numStates++;
@@ -133,20 +131,20 @@ public class MDP extends Model
 	}
 
 	/**
-	 * Add distribution 'distr' to state s (which must exist).
+	 * Add a choice (distribution 'distr') to state s (which must exist).
 	 * Distribution is only actually added if it does not already exists for state s.
 	 * (Assuming 'allowDupes' flag is not enabled.)
 	 * Returns the index of the (existing or newly added) distribution.
 	 * Returns -1 in case of error.
 	 */
-	public int addDistribution(int s, Distribution distr) throws PrismException
+	public int addChoice(int s, Distribution distr)
 	{
-		ArrayList<Distribution> set;
+		List<Distribution> set;
 		// Check state exists
 		if (s >= numStates || s < 0)
 			return -1;
 		// Add distribution (if new)
-		set = steps.get(s);
+		set = trans.get(s);
 		if (!allowDupes) {
 			int i = set.indexOf(distr);
 			if (i != -1)
@@ -198,7 +196,7 @@ public class MDP extends Model
 		}
 		// If no rewards for state i yet, create list
 		if (transRewards.get(s) == null) {
-			int n = steps.get(s).size();
+			int n = trans.get(s).size();
 			List<Double> list = new ArrayList<Double>(n);
 			for (int j = 0; j < n; j++) {
 				list.add(0.0);
@@ -214,9 +212,25 @@ public class MDP extends Model
 	 */
 	public int getNumChoices(int s)
 	{
-		return steps.get(s).size();
+		return trans.get(s).size();
 	}
-
+	
+	/**
+	 * Get the list of choices (distributions) for state s.
+	 */
+	public List<Distribution> getChoices(int s)
+	{
+		return trans.get(s);
+	}
+	
+	/**
+	 * Get the ith choice (distribution) for state s.
+	 */
+	public Distribution getChoice(int s, int i)
+	{
+		return trans.get(s).get(i);
+	}
+	
 	/**
 	 * Get the transition reward (if any) for choice i of state s.
 	 */
@@ -235,13 +249,43 @@ public class MDP extends Model
 	 */
 	public boolean isSuccessor(int s1, int s2)
 	{
-		for (Distribution distr : steps.get(s1)) {
+		for (Distribution distr : trans.get(s1)) {
 			if (distr.contains(s2))
 				return true;
 		}
 		return false;
 	}
 	
+	/**
+	 * Get the total number of choices (distributions) over all states.
+	 */
+	public int getNumChoices()
+	{
+		return numDistrs;
+	}
+	
+	/**
+	 * Get the total number of transitions in the model.
+	 */
+	public int getNumTransitions()
+	{
+		return numTransitions;
+	}
+	
+	/**
+	 * Get the maximum number of choices (distributions) in any state.
+	 */
+	public int getMaxNumChoices()
+	{
+		// Recompute if necessary
+		if (!maxNumDistrsOk) {
+			maxNumDistrs = 0;
+			for (int s = 0; s < numStates; s++)
+				maxNumDistrs = Math.max(maxNumDistrs, getNumChoices(s));
+		}
+		return maxNumDistrs;
+	}
+	
 	/**
 	 * Checks for deadlocks (states with no choices) and throws an exception if any exist.
 	 * States in 'except' (If non-null) are excluded from the check.
@@ -249,7 +293,7 @@ public class MDP extends Model
 	public void checkForDeadlocks(BitSet except) throws PrismException
 	{
 		for (int i = 0; i < numStates; i++) {
-			if (steps.get(i).isEmpty() && (except == null || !except.get(i)))
+			if (trans.get(i).isEmpty() && (except == null || !except.get(i)))
 				throw new PrismException("MDP has a deadlock in state " + i);
 		}
 		// TODO: Check for empty distributions too?
@@ -292,7 +336,7 @@ public class MDP extends Model
 				if (i != iLast || k != kLast) {
 					// Add any previous distribution to the last state, create new one
 					if (distr != null) {
-						addDistribution(iLast, distr);
+						addChoice(iLast, distr);
 					}
 					distr = new Distribution();
 				}
@@ -304,7 +348,7 @@ public class MDP extends Model
 				s = in.readLine();
 			}
 			// Add previous distribution to the last state
-			addDistribution(iLast, distr);
+			addChoice(iLast, distr);
 			// Close file
 			in.close();
 		} catch (IOException e) {
@@ -349,11 +393,11 @@ public class MDP extends Model
 		int k;
 		double d, prob, minmax;
 		boolean first;
-		ArrayList<Distribution> step;
+		List<Distribution> step;
 
 		minmax = 0;
 		first = true;
-		step = steps.get(s);
+		step = trans.get(s);
 		for (Distribution distr : step) {
 			// Compute sum for this distribution
 			d = 0.0;
@@ -383,13 +427,13 @@ public class MDP extends Model
 		int j, k;
 		double d, prob;
 		List<Integer> res;
-		ArrayList<Distribution> step;
+		List<Distribution> step;
 
 		// Create data structures to store strategy
 		res = new ArrayList<Integer>();
 		// One row of matrix-vector operation 
 		j = -1;
-		step = steps.get(s);
+		step = trans.get(s);
 		for (Distribution distr : step) {
 			j++;
 			// Compute sum for this distribution
@@ -442,12 +486,12 @@ public class MDP extends Model
 		int j, k;
 		double d, prob, minmax;
 		boolean first;
-		ArrayList<Distribution> step;
+		List<Distribution> step;
 
 		minmax = 0;
 		first = true;
 		j = -1;
-		step = steps.get(s);
+		step = trans.get(s);
 		for (Distribution distr : step) {
 			j++;
 			// Compute sum for this distribution
@@ -478,13 +522,13 @@ public class MDP extends Model
 		int j, k;
 		double d, prob;
 		List<Integer> res;
-		ArrayList<Distribution> step;
+		List<Distribution> step;
 
 		// Create data structures to store strategy
 		res = new ArrayList<Integer>();
 		// One row of matrix-vector operation 
 		j = -1;
-		step = steps.get(s);
+		step = trans.get(s);
 		for (Distribution distr : step) {
 			j++;
 			// Compute sum for this distribution
@@ -528,7 +572,7 @@ public class MDP extends Model
 			out.write(numStates + " " + numDistrs + " " + numTransitions + "\n");
 			for (i = 0; i < numStates; i++) {
 				j = -1;
-				for (Distribution distr : steps.get(i)) {
+				for (Distribution distr : trans.get(i)) {
 					j++;
 					for (Map.Entry<Integer, Double> e : distr) {
 						out.write(i + " " + j + " " + e.getKey() + " " + e.getValue() + "\n");
@@ -543,7 +587,7 @@ public class MDP extends Model
 			out.write(numStates + " " + "?" + " " + "?" + "\n");
 			for (i = 0; i < numStates; i++) {
 				j = -1;
-				for (Distribution distr : steps.get(i)) {
+				for (Distribution distr : trans.get(i)) {
 					j++;
 					for (Map.Entry<Integer, Double> e : distr) {
 						out.write(i + " " + j + " " + e.getKey() + " " + "1.0" + "\n");
@@ -569,7 +613,7 @@ public class MDP extends Model
 				if (mark != null && mark.get(i))
 					out.write(i + " [style=filled  fillcolor=\"#cccccc\"]\n");
 				j = -1;
-				for (Distribution distr : steps.get(i)) {
+				for (Distribution distr : trans.get(i)) {
 					j++;
 					for (Map.Entry<Integer, Double> e : distr) {
 						out.write(i + " -> " + e.getKey() + " [ label=\"");
@@ -593,7 +637,7 @@ public class MDP extends Model
 		s += numStates + " states";
 		s += ", " + numDistrs + " distributions";
 		s += ", " + numTransitions + " transitions";
-		s += ", dist max/avg = " + maxNumDistrs + "/" + PrismUtils.formatDouble2dp(((double) numDistrs) / numStates);
+		s += ", dist max/avg = " + getMaxNumChoices() + "/" + PrismUtils.formatDouble2dp(((double) numDistrs) / numStates);
 		return s;
 	}
 
@@ -612,7 +656,7 @@ public class MDP extends Model
 				first = false;
 			else
 				s += ", ";
-			s += i + ": " + steps.get(i) + transRewards.get(i);
+			s += i + ": " + trans.get(i) + transRewards.get(i);
 		}
 		s += " ]";
 		return s;
@@ -630,7 +674,7 @@ public class MDP extends Model
 			return false;
 		if (!initialStates.equals(mdp.initialStates))
 			return false;
-		if (!steps.equals(mdp.steps))
+		if (!trans.equals(mdp.trans))
 			return false;
 		// TODO: compare rewards (complicated: null = 0,0,0,0)
 		return true;
diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java
index 3514d7b5..79e41c69 100644
--- a/prism/src/explicit/MDPModelChecker.java
+++ b/prism/src/explicit/MDPModelChecker.java
@@ -80,7 +80,7 @@ public class MDPModelChecker extends ModelChecker
 					b2 = target.get(i);
 					if (!b2) {
 						b2 = min; // there exists or for all choices
-						for (Distribution distr : mdp.steps.get(i)) {
+						for (Distribution distr : mdp.getChoices(i)) {
 							b3 = true; // all transitions are to u states
 							b4 = false; // some transition goes to v
 							for (Map.Entry<Integer, Double> e : distr) {
diff --git a/prism/src/explicit/PrismSTPGAbstractRefine.java b/prism/src/explicit/PrismSTPGAbstractRefine.java
index 199c194d..627aab06 100644
--- a/prism/src/explicit/PrismSTPGAbstractRefine.java
+++ b/prism/src/explicit/PrismSTPGAbstractRefine.java
@@ -154,12 +154,12 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 			switch (modelType) {
 			case DTMC:
 				distr = buildAbstractDistribution(c, (DTMC) modelConcrete);
-				j = ((MDP) abstraction).addDistribution(a, distr);
+				j = ((MDP) abstraction).addChoice(a, distr);
 				((MDP) abstraction).setTransitionReward(a, j, ((DTMC) modelConcrete).getTransitionReward(c));
 				break;
 			case CTMC:
 				distr = buildAbstractDistribution(c, (CTMC) modelConcrete);
-				j = ((CTMDP) abstraction).addDistribution(a, distr);
+				j = ((CTMDP) abstraction).addChoice(a, distr);
 				break;
 			case MDP:
 				set = buildAbstractDistributionSet(c, (MDP) modelConcrete, (STPG) abstraction);
@@ -181,7 +181,7 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 	 */
 	protected Distribution buildAbstractDistribution(int c, DTMC dtmc)
 	{
-		return dtmc.trans.get(c).map(concreteToAbstract);
+		return dtmc.getTransitions(c).map(concreteToAbstract);
 	}
 
 	/**
@@ -190,7 +190,7 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 	protected DistributionSet buildAbstractDistributionSet(int c, MDP mdp, STPG stpg)
 	{
 		DistributionSet set = ((STPG) stpg).newDistributionSet(null);
-		for (Distribution distr : mdp.steps.get(c)) {
+		for (Distribution distr : mdp.getChoices(c)) {
 			set.add(distr.map(concreteToAbstract));
 		}
 		return set;
@@ -305,12 +305,12 @@ public class PrismSTPGAbstractRefine extends STPGAbstractRefine
 				switch (modelType) {
 				case DTMC:
 					distr = buildAbstractDistribution(c, (DTMC) modelConcrete);
-					j = ((MDP) abstraction).addDistribution(a, distr);
+					j = ((MDP) abstraction).addChoice(a, distr);
 					((MDP) abstraction).setTransitionReward(a, j, ((DTMC) modelConcrete).getTransitionReward(c));
 					break;
 				case CTMC:
 					distr = buildAbstractDistribution(c, (CTMC) modelConcrete);
-					j = ((CTMDP) abstraction).addDistribution(a, distr);
+					j = ((CTMDP) abstraction).addChoice(a, distr);
 					// TODO: recompute unif?
 					break;
 				case MDP:
diff --git a/prism/src/explicit/STPG.java b/prism/src/explicit/STPG.java
index bf786b5c..70bf7813 100644
--- a/prism/src/explicit/STPG.java
+++ b/prism/src/explicit/STPG.java
@@ -41,22 +41,22 @@ public class STPG extends Model
 	// Model type
 	public static ModelType modelType = ModelType.STPG;
 
-	// Transitions function (Steps)
-	public List<ArrayList<DistributionSet>> steps;
+	// Transition function (Steps)
+	protected List<ArrayList<DistributionSet>> trans;
 
 	// Rewards
-	private List<List<Double>> transRewards;
-	private Double transRewardsConstant;
+	protected List<List<Double>> transRewards;
+	protected Double transRewardsConstant;
 
 	// Flag: allow dupes in distribution sets?
 	public boolean allowDupes = false;
 
 	// Other statistics
-	public int numDistrSets;
-	public int numDistrs;
-	public int numTransitions;
-	public int maxNumDistrSets;
-	public int maxNumDistrs;
+	protected int numDistrSets;
+	protected int numDistrs;
+	protected int numTransitions;
+	protected int maxNumDistrSets;
+	protected int maxNumDistrs;
 
 	/**
 	 * Constructor: empty STPG.
@@ -82,12 +82,10 @@ public class STPG extends Model
 		DistributionSet set;
 		int i;
 		initialise(m.numStates);
-		i = 0;
-		for (ArrayList<Distribution> distrs : m.steps) {
+		for (i = 0; i < numStates; i++) {
 			set = newDistributionSet(null);
-			set.addAll(distrs);
+			set.addAll(m.getChoices(i));
 			addDistributionSet(i, set);
-			i++;
 		}
 	}
 
@@ -99,9 +97,9 @@ public class STPG extends Model
 		super.initialise(numStates);
 		numDistrSets = numDistrs = numTransitions = 0;
 		maxNumDistrSets = maxNumDistrs = 0;
-		steps = new ArrayList<ArrayList<DistributionSet>>(numStates);
+		trans = new ArrayList<ArrayList<DistributionSet>>(numStates);
 		for (int i = 0; i < numStates; i++) {
-			steps.add(new ArrayList<DistributionSet>());
+			trans.add(new ArrayList<DistributionSet>());
 		}
 		clearAllRewards();
 	}
@@ -115,7 +113,7 @@ public class STPG extends Model
 		if (i >= numStates || i < 0)
 			return;
 		// Clear data structures and update stats
-		List<DistributionSet> list = steps.get(i);
+		List<DistributionSet> list = trans.get(i);
 		numDistrSets -= list.size();
 		for (DistributionSet set : list) {
 			numDistrs -= set.size();
@@ -125,7 +123,7 @@ public class STPG extends Model
 		//TODO: recompute maxNumDistrSets
 		//TODO: recompute maxNumDistrs
 		// Remove all distribution sets
-		steps.set(i, new ArrayList<DistributionSet>(0));
+		trans.set(i, new ArrayList<DistributionSet>(0));
 	}
 
 	/**
@@ -143,7 +141,7 @@ public class STPG extends Model
 	public void addStates(int numToAdd)
 	{
 		for (int i = 0; i < numToAdd; i++) {
-			steps.add(new ArrayList<DistributionSet>());
+			trans.add(new ArrayList<DistributionSet>());
 		}
 		numStates += numToAdd;
 	}
@@ -172,7 +170,7 @@ public class STPG extends Model
 		if (s >= numStates || s < 0)
 			return -1;
 		// Add distribution set (if new)
-		set = steps.get(s);
+		set = trans.get(s);
 		if (!allowDupes) {
 			int i = set.indexOf(newSet);
 			if (i != -1)
@@ -224,7 +222,7 @@ public class STPG extends Model
 		}
 		// If no rewards for state i yet, create list
 		if (transRewards.get(s) == null) {
-			int n = steps.get(s).size();
+			int n = trans.get(s).size();
 			List<Double> list = new ArrayList<Double>(n);
 			for (int j = 0; j < n; j++) {
 				list.add(0.0);
@@ -240,9 +238,25 @@ public class STPG extends Model
 	 */
 	public int getNumChoices(int s)
 	{
-		return steps.get(s).size();
+		return trans.get(s).size();
 	}
 
+	/**
+	 * Get the list of choices (distribution sets) for state s.
+	 */
+	public List<DistributionSet> getChoices(int s)
+	{
+		return trans.get(s);
+	}
+	
+	/**
+	 * Get the ith choice (distribution set) for state s.
+	 */
+	public DistributionSet getChoice(int s, int i)
+	{
+		return trans.get(s).get(i);
+	}
+	
 	/**
 	 * Get the transition reward (if any) for choice i of state s.
 	 */
@@ -261,7 +275,7 @@ public class STPG extends Model
 	 */
 	public boolean isSuccessor(int s1, int s2)
 	{
-		for (DistributionSet distrs : steps.get(s1)) {
+		for (DistributionSet distrs : trans.get(s1)) {
 			for (Distribution distr : distrs) {
 				if (distr.contains(s2))
 					return true;
@@ -277,7 +291,7 @@ public class STPG extends Model
 	 */
 	public boolean allSuccessorsInSet(int s, BitSet set)
 	{
-		for (DistributionSet distrs : steps.get(s)) {
+		for (DistributionSet distrs : trans.get(s)) {
 			for (Distribution distr : distrs) {
 				if (!distr.isSubsetOf(set))
 					return false;
@@ -286,6 +300,48 @@ public class STPG extends Model
 		return true;
 	}
 
+	/**
+	 * Get the total number of player 1 choices (distribution sets) over all states.
+	 */
+	public int getNumP1Choices()
+	{
+		return numDistrSets;
+	}
+	
+	/**
+	 * Get the total number of player 2 choices (distributions) over all states.
+	 */
+	public int getNumP2Choices()
+	{
+		return numDistrs;
+	}
+	
+	/**
+	 * Get the total number of transitions in the model.
+	 */
+	public int getNumTransitions()
+	{
+		return numTransitions;
+	}
+	
+	/**
+	 * Get the maximum number of player 1 choices (distribution sets) in any state.
+	 */
+	public int getMaxNumP1Choices()
+	{
+		// TODO: Recompute if necessary
+		return maxNumDistrSets;
+	}
+	
+	/**
+	 * Get the maximum number of player 2 choices (distributions) in any state.
+	 */
+	public int getMaxNumP2Choices()
+	{
+		// TODO: Recompute if necessary
+		return maxNumDistrs;
+	}
+	
 	/**
 	 * Checks for deadlocks (states with no choices) and throws an exception if any exist.
 	 * States in 'except' (If non-null) are excluded from the check.
@@ -293,7 +349,7 @@ public class STPG extends Model
 	public void checkForDeadlocks(BitSet except) throws PrismException
 	{
 		for (int i = 0; i < numStates; i++) {
-			if (steps.get(i).isEmpty() && (except == null || !except.get(i)))
+			if (trans.get(i).isEmpty() && (except == null || !except.get(i)))
 				throw new PrismException("STPG has a deadlock in state " + i);
 		}
 		// TODO: Check for empty distributions sets too?
@@ -347,7 +403,7 @@ public class STPG extends Model
 
 		minmax1 = 0;
 		first1 = true;
-		step = steps.get(s);
+		step = trans.get(s);
 		for (DistributionSet distrs : step) {
 			minmax2 = 0;
 			first2 = true;
@@ -393,7 +449,7 @@ public class STPG extends Model
 		res = new ArrayList<Integer>();
 		// One row of matrix-vector operation 
 		j = -1;
-		step = steps.get(s);
+		step = trans.get(s);
 		for (DistributionSet distrs : step) {
 			j++;
 			minmax2 = 0;
@@ -451,7 +507,7 @@ public class STPG extends Model
 				if (mark != null && mark.get(i))
 					out.write(i + " [style=filled  fillcolor=\"#cccccc\"]\n");
 				j = -1;
-				for (DistributionSet distrs : steps.get(i)) {
+				for (DistributionSet distrs : trans.get(i)) {
 					j++;
 					k = -1;
 					for (Distribution distr : distrs) {
@@ -500,7 +556,7 @@ public class STPG extends Model
 				first = false;
 			else
 				s += ", ";
-			s += i + ": " + steps.get(i);
+			s += i + ": " + trans.get(i);
 		}
 		s += " ]";
 		return s;
@@ -518,7 +574,7 @@ public class STPG extends Model
 			return false;
 		if (!initialStates.equals(stpg.initialStates))
 			return false;
-		if (!steps.equals(stpg.steps))
+		if (!trans.equals(stpg.trans))
 			return false;
 		return true;
 	}
diff --git a/prism/src/explicit/STPGAbstractRefine.java b/prism/src/explicit/STPGAbstractRefine.java
index 59e682dc..2279fe9c 100644
--- a/prism/src/explicit/STPGAbstractRefine.java
+++ b/prism/src/explicit/STPGAbstractRefine.java
@@ -473,7 +473,7 @@ public abstract class STPGAbstractRefine
 				// Compute... note lbsoln for both is ok sinec = ubsoln
 				lb = ((STPG) abstraction).mvMultMinMaxSingle(i, lbSoln, true, min);
 				ub = ((STPG) abstraction).mvMultMinMaxSingle(i, lbSoln, false, min);
-				mainLog.println(((STPG) abstraction).steps.get(i));
+				mainLog.println(((STPG) abstraction).getChoices(i));
 				mainLog.println("XX " + i + ": old=[" + lbSoln[i] + "," + ubSoln[i] + "], new=[" + lb + "," + ub + "]");
 				if (PrismUtils.doublesAreClose(ub, lb, refineTermCritParam, refineTermCrit == RefineTermCrit.ABSOLUTE)) {
 					lbSoln[i] = ubSoln[i] = lb;
@@ -1177,7 +1177,7 @@ public abstract class STPGAbstractRefine
 				//out.write(i + " [label=\"" + i + " [" + (ubSoln[i]) + "-" + (lbSoln[i]) + "=" + (ubSoln[i] - lbSoln[i]) + "]" + "\"");
 				out.write("]\n");
 				j = 0;
-				for (DistributionSet distrs : stpg.steps.get(i)) {
+				for (DistributionSet distrs : stpg.getChoices(i)) {
 					k = 0;
 					for (Distribution distr : distrs) {
 						for (Map.Entry<Integer, Double> e : distr) {
diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java
index ac9c3166..d9e55704 100644
--- a/prism/src/explicit/STPGModelChecker.java
+++ b/prism/src/explicit/STPGModelChecker.java
@@ -77,7 +77,7 @@ public class STPGModelChecker extends ModelChecker
 				b1 = target.get(i);
 				if (!b1) {
 					b1 = min1; // there exists or for all player 1 choices
-					for (DistributionSet distrs : stpg.steps.get(i)) {
+					for (DistributionSet distrs : stpg.getChoices(i)) {
 						b2 = min2; // there exists or for all player 2 choices
 						for (Distribution distr : distrs) {
 							b3 = false; // some transition goes to u
@@ -170,7 +170,7 @@ public class STPGModelChecker extends ModelChecker
 					b1 = target.get(i);
 					if (!b1) {
 						b1 = min1; // there exists or for all player 1 choices
-						for (DistributionSet distrs : stpg.steps.get(i)) {
+						for (DistributionSet distrs : stpg.getChoices(i)) {
 							b2 = min2; // there exists or for all player 2 choices
 							for (Distribution distr : distrs) {
 								b3 = true; // all transitions are to u states