explicit.DTMC/NondetModel: add default method getNumTransitions(OfInt states)

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12100 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/DTMC.java

@@ -126,6 +126,23 @@ 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/NondetModel.java

@@ -28,6 +28,7 @@ package explicit;
 
 import java.util.BitSet;
 import java.util.Iterator;
+import java.util.PrimitiveIterator;
 import java.util.function.IntPredicate;
 
 import prism.PrismLog;
@@ -69,7 +70,27 @@ public interface NondetModel extends Model
 	 * Get the number of transitions from choice {@code i} of state {@code s}.
 	 */
 	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