From 3c691c980acbb2fc95534eb5741b3ab6e89b1895 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 21 Jul 2017 13:23:58 +0000
Subject: [PATCH] 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        | 17 +++++++++++++++++
 prism/src/explicit/NondetModel.java | 23 ++++++++++++++++++++++-
 2 files changed, 39 insertions(+), 1 deletion(-)

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.
+	 * <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
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.
+	 * <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