Explicit model refactoring (transition counting).

Move getNumTransitions(int) to Model from DTMC.
There is a default implementation using getSuccessorsIterator(int).
This allows us to provide a default implementation of getNumTransitions() too.

Also move getNumTransitions(PrimitiveIterator.OfInt) to Model from DTMC/NondetModel.

prism/src/automata/LTSFromDA.java

@@ -110,6 +110,12 @@ public class LTSFromDA extends ModelExplicit implements LTS
 		return num;
 	}
 
+	@Override
+	public int getNumTransitions(int s)
+	{
+		return da.getNumEdges(s);
+	}
+
 	@Override
 	public boolean isSuccessor(int s1, int s2)
 	{

prism/src/explicit/DTMC.java

@@ -41,11 +41,6 @@ import explicit.rewards.MCRewards;
  */
 public interface DTMC extends Model
 {
-	/**
-	 * Get the number of transitions from state s.
-	 */
-	public int getNumTransitions(int s);
-
 	/**
 	 * Get an iterator over the transitions from state s.
 	 */
@@ -128,23 +123,6 @@ public interface DTMC extends Model
 		return sum.sum;
 	}
 
-	/**
-	 * Get the number of transitions leaving a set of states.
-	 * <br>
-	 * Default implementation: Iterator over the states and sum the result of getNumTransitions(s).
-	 * @param states The set of states, specified by a OfInt iterator
-	 * @return the number of transitions
-	 */
-	public default long getNumTransitions(PrimitiveIterator.OfInt states)
-	{
-		long count = 0;
-		while (states.hasNext()) {
-			int s = states.nextInt();
-			count += getNumTransitions(s);
-		}
-		return count;
-	}
-
 	/**
 	 * Perform a single step of precomputation algorithm Prob0 for a single state,
 	 * i.e., for the state {@code s} returns true iff there is a transition from

prism/src/explicit/DTMCEmbeddedSimple.java

@@ -126,6 +126,15 @@ public class DTMCEmbeddedSimple extends DTMCExplicit
 		return ctmc.getNumTransitions() + numExtraTransitions;
 	}
 
+	public int getNumTransitions(int s)
+	{
+		if (exitRates[s] == 0) {
+			return 1;
+		} else {
+			return ctmc.getNumTransitions(s);
+		}
+	}
+
 	@Override
 	public SuccessorsIterator getSuccessors(final int s)
 	{
@@ -201,15 +210,6 @@ public class DTMCEmbeddedSimple extends DTMCExplicit
 
 	// Accessors (for DTMC)
 
-	public int getNumTransitions(int s)
-	{
-		if (exitRates[s] == 0) {
-			return 1;
-		} else {
-			return ctmc.getNumTransitions(s);
-		}
-	}
-
 	public Iterator<Entry<Integer,Double>> getTransitionsIterator(int s)
 	{
 		if (exitRates[s] == 0) {

prism/src/explicit/DTMCFromMDPAndMDStrategy.java

@@ -112,13 +112,9 @@ public class DTMCFromMDPAndMDStrategy extends DTMCExplicit
 		return mdp.getConstantValues();
 	}
 
-	public int getNumTransitions()
+	public int getNumTransitions(int s)
 	{
-		int numTransitions = 0;
-		for (int s = 0; s < numStates; s++)
-			if (strat.isChoiceDefined(s))
-				numTransitions += mdp.getNumTransitions(s, strat.getChoiceIndex(s));
-		return numTransitions;
+		return strat.isChoiceDefined(s) ? mdp.getNumTransitions(s, strat.getChoiceIndex(s)) : 0;
 	}
 
 	public SuccessorsIterator getSuccessors(final int s)
@@ -165,11 +161,6 @@ public class DTMCFromMDPAndMDStrategy extends DTMCExplicit
 
 	// Accessors (for DTMC)
 
-	public int getNumTransitions(int s)
-	{
-		return strat.isChoiceDefined(s) ? mdp.getNumTransitions(s, strat.getChoiceIndex(s)) : 0;
-	}
-
 	public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s)
 	{
 		if (strat.isChoiceDefined(s)) {

prism/src/explicit/DTMCFromMDPMemorylessAdversary.java

@@ -115,13 +115,9 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit
 		return mdp.getConstantValues();
 	}
 
-	public int getNumTransitions()
+	public int getNumTransitions(int s)
 	{
-		int numTransitions = 0;
-		for (int s = 0; s < numStates; s++)
-			if (adv[s] >= 0)
-				numTransitions += mdp.getNumTransitions(s, adv[s]);
-		return numTransitions;
+		return adv[s] >= 0 ? mdp.getNumTransitions(s, adv[s]) : 0;
 	}
 
 	public SuccessorsIterator getSuccessors(final int s)
@@ -168,12 +164,6 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit
 
 	// Accessors (for DTMC)
 
-	@Override
-	public int getNumTransitions(int s)
-	{
-		return adv[s] >= 0 ? mdp.getNumTransitions(s, adv[s]) : 0;
-	}
-
 	@Override
 	public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s)
 	{

prism/src/explicit/DTMCSimple.java

@@ -205,6 +205,12 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple
 		return numTransitions;
 	}
 
+	@Override
+	public int getNumTransitions(int s)
+	{
+		return trans.get(s).size();
+	}
+
 	/** Get an iterator over the successors of state s */
 	@Override
 	public Iterator<Integer> getSuccessorsIterator(final int s)
@@ -259,12 +265,6 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple
 
 	// Accessors (for DTMC)
 
-	@Override
-	public int getNumTransitions(int s)
-	{
-		return trans.get(s).size();
-	}
-
 	@Override
 	public Iterator<Entry<Integer, Double>> getTransitionsIterator(int s)
 	{

prism/src/explicit/DTMCSparse.java

@@ -145,6 +145,12 @@ public class DTMCSparse extends DTMCExplicit
 		return rows[numStates];
 	}
 
+	@Override
+	public int getNumTransitions(int state)
+	{
+		return rows[state + 1] - rows[state];
+	}
+
 	@Override
 	public OfInt getSuccessorsIterator(final int state)
 	{
@@ -235,12 +241,6 @@ public class DTMCSparse extends DTMCExplicit
 		}
 	}
 
-	@Override
-	public int getNumTransitions(int state)
-	{
-		return rows[state + 1] - rows[state];
-	}
-
 	@Override
 	public Iterator<Entry<Integer, Double>> getTransitionsIterator(final int state)
 	{

prism/src/explicit/DTMCUniformisedSimple.java

@@ -164,6 +164,12 @@ public class DTMCUniformisedSimple extends DTMCExplicit
 		return ctmc.getNumTransitions() + numExtraTransitions;
 	}
 
+	public int getNumTransitions(int s)
+	{
+		// TODO
+		throw new RuntimeException("Not implemented yet");
+	}
+
 	public SuccessorsIterator getSuccessors(final int s)
 	{
 		// TODO
@@ -211,12 +217,6 @@ public class DTMCUniformisedSimple extends DTMCExplicit
 
 	// Accessors (for DTMC)
 
-	public int getNumTransitions(int s)
-	{
-		// TODO
-		throw new RuntimeException("Not implemented yet");
-	}
-
 	public Iterator<Entry<Integer,Double>> getTransitionsIterator(int s)
 	{
 		// TODO

prism/src/explicit/LTSExplicit.java

@@ -109,11 +109,6 @@ public class LTSExplicit extends ModelExplicit implements LTS
 		throw new IllegalArgumentException();
 	}
 
-	public int getNumTransitions(int s)
-	{
-		return getNumChoices(s);
-	}
-
 	@Override
 	public boolean allSuccessorsInSet(int s, int i, BitSet set)
 	{
@@ -177,6 +172,12 @@ public class LTSExplicit extends ModelExplicit implements LTS
 		return numTransitions;
 	}
 
+	@Override
+	public int getNumTransitions(int s)
+	{
+		return getNumChoices(s);
+	}
+
 	@Override
 	public void checkForDeadlocks(BitSet except) throws PrismException
 	{

prism/src/explicit/MDPSimple.java

@@ -470,6 +470,17 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
 		return numTransitions;
 	}
 
+	@Override
+	public int getNumTransitions(int s)
+	{
+		int numTransitions = 0;
+		int numChoices = getNumChoices(s);
+		for (int j = 0; j < numChoices; j++) {
+			numTransitions += trans.get(s).get(j).size();
+		}
+		return numTransitions; 
+	}
+
 	@Override
 	public void findDeadlocks(boolean fix) throws PrismException
 	{

prism/src/explicit/MDPSparse.java

@@ -478,6 +478,12 @@ public class MDPSparse extends MDPExplicit
 		return numTransitions;
 	}
 
+	@Override
+	public int getNumTransitions(int s)
+	{
+		return choiceStarts[rowStarts[s + 1]] - choiceStarts[rowStarts[s]];
+	}
+
 	private SuccessorsIterator colsIterator(int start, int end, boolean distinct)
 	{
 		return new SuccessorsIterator() {

prism/src/explicit/Model.java

@@ -32,9 +32,11 @@ import java.util.BitSet;
 import java.util.Collections;
 import java.util.Iterator;
 import java.util.List;
+import java.util.PrimitiveIterator;
 import java.util.Set;
 import java.util.function.IntPredicate;
 
+import common.IteratorTools;
 import explicit.graphviz.Decorator;
 import parser.State;
 import parser.Values;
@@ -145,7 +147,40 @@ public interface Model
 	/**
 	 * Get the total number of transitions in the model.
 	 */
-	public int getNumTransitions();
+	public default int getNumTransitions()
+	{
+		int numStates = getNumStates();
+		int numTransitions = 0;
+		for (int s = 0; s < numStates; s++) {
+			numTransitions += getNumTransitions(s);
+		}
+		return numTransitions;
+	}
+
+	/**
+	 * Get the number of transitions from state s.
+	 */
+	public default int getNumTransitions(int s)
+	{
+		return IteratorTools.count(getSuccessorsIterator(s));
+	}
+
+	/**
+	 * Get the number of transitions leaving a set of states.
+	 * <br>
+	 * Default implementation: Iterator over the states and sum the result of getNumTransitions(s).
+	 * @param states The set of states, specified by an OfInt iterator
+	 * @return the number of transitions
+	 */
+	public default long getNumTransitions(PrimitiveIterator.OfInt states)
+	{
+		long count = 0;
+		while (states.hasNext()) {
+			int s = states.nextInt();
+			count += getNumTransitions(s);
+		}
+		return count;
+	}
 
 	/**
 	 * Get an iterator over the successors of state s.

prism/src/explicit/ModelExplicit.java

@@ -352,9 +352,6 @@ public abstract class ModelExplicit implements Model
 		return labels.keySet();
 	}
 	
-	@Override
-	public abstract int getNumTransitions();
-
 	@Override
 	public void checkForDeadlocks() throws PrismException
 	{

prism/src/explicit/NondetModel.java

@@ -71,26 +71,6 @@ public interface NondetModel extends Model
 	 */
 	public int getNumTransitions(int s, int i);
 
-	/**
-	 * Get the number of transitions leaving a set of states.
-	 * <br>
-	 * Default implementation: Iterate over the states s and choices i
-	 * and sum the result of getNumTransitions(s,i).
-	 * @param states The set of states, specified by a OfInt iterator
-	 * @return the number of transitions
-	 */
-	public default long getNumTransitions(PrimitiveIterator.OfInt states)
-	{
-		long count = 0;
-		while (states.hasNext()) {
-			int s = states.nextInt();
-			for (int choice = 0, numChoices = getNumChoices(s); choice < numChoices; choice++) {
-				count += getNumTransitions(s, choice);
-			}
-		}
-		return count;
-	}
-
 	/**
 	 * Check if all the successor states from choice {@code i} of state {@code s} are in the set {@code set}.
 	 * @param s The state to check

prism/src/explicit/modelviews/DTMCView.java

@@ -111,13 +111,9 @@ public abstract class DTMCView extends ModelView implements DTMC, Cloneable
 	}
 
 	@Override
-	public int getNumTransitions()
+	public int getNumTransitions(final int s)
 	{
-		int numTransitions = 0;
-		for (int state = 0, numStates = getNumStates(); state < numStates; state++) {
-			numTransitions += getNumTransitions(state);
-		}
-		return numTransitions;
+		return IteratorTools.count(getTransitionsIterator(s));
 	}
 
 	@Override
@@ -207,12 +203,6 @@ public abstract class DTMCView extends ModelView implements DTMC, Cloneable
 
 	//--- DTMC ---
 
-	@Override
-	public int getNumTransitions(final int state)
-	{
-		return IteratorTools.count(getTransitionsIterator(state));
-	}
-
 	public static Entry<Integer, Pair<Double, Object>> attachAction(final Entry<Integer, Double> transition, final Object action)
 	{
 		final Integer state = transition.getKey();

prism/src/explicit/modelviews/MDPView.java

@@ -109,12 +109,11 @@ public abstract class MDPView extends ModelView implements MDP, Cloneable
 	}
 
 	@Override
-	public int getNumTransitions()
+	public int getNumTransitions(int s)
 	{
 		int numTransitions = 0;
-		for (int state = 0, numStates = getNumStates(); state < numStates; state++) {
-			for (int choice = 0, numChoices = getNumChoices(state); choice < numChoices; choice++)
-				numTransitions += getNumTransitions(state, choice);
+		for (int j = 0, numChoices = getNumChoices(s); j < numChoices; j++) {
+			numTransitions += getNumTransitions(s, j);
 		}
 		return numTransitions;
 	}