diff --git a/prism/src/explicit/DTMC.java b/prism/src/explicit/DTMC.java
index 5ca11310..4ef5ff42 100644
--- a/prism/src/explicit/DTMC.java
+++ b/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.
+ *
+ * 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
diff --git a/prism/src/explicit/NondetModel.java b/prism/src/explicit/NondetModel.java
index d4cb72bd..3c91ed2c 100644
--- a/prism/src/explicit/NondetModel.java
+++ b/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.
+ *
+ * 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