From ccdb02c5f2f9fb6834545563813abd07fd1df7f0 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 19 Aug 2016 09:35:38 +0000
Subject: [PATCH] ParamModel: provide getTransitionsIterator

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11648 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/param/ParamModel.java | 53 +++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)

diff --git a/prism/src/param/ParamModel.java b/prism/src/param/ParamModel.java
index 2e9363ce..72ad5b83 100644
--- a/prism/src/param/ParamModel.java
+++ b/prism/src/param/ParamModel.java
@@ -30,6 +30,7 @@ import java.io.File;
 import java.util.BitSet;
 import java.util.Iterator;
 import java.util.LinkedList;
+import java.util.Map.Entry;
 import java.util.TreeSet;
 
 import parser.Values;
@@ -141,6 +142,58 @@ final class ParamModel extends ModelExplicit
 		throw new UnsupportedOperationException();
 	}
 
+	/**
+	 * Get an iterator over the transitions from choice {@code i} of state {@code s}.
+	 * <br>
+	 * For DTMC/CTMCs, there is only a single choice.
+	 */
+	public Iterator<Entry<Integer, Function>> getTransitionsIterator(final int s, final int i)
+	{
+		return new Iterator<Entry<Integer, Function>>()
+		{
+			final int start = choiceBegin(stateBegin(s) + i);
+			int col = start;
+			final int end = choiceBegin(stateBegin(s) + i + 1);
+
+			@Override
+			public boolean hasNext()
+			{
+				return col < end;
+			}
+
+			@Override
+			public Entry<Integer, Function> next()
+			{
+				assert (col < end);
+				final int i = col;
+				col++;
+				return new Entry<Integer, Function>()
+				{
+					int key = cols[i];
+					Function value = nonZeros[i];
+
+					@Override
+					public Integer getKey()
+					{
+						return key;
+					}
+
+					@Override
+					public Function getValue()
+					{
+						return value;
+					}
+
+					@Override
+					public Function setValue(Function arg0)
+					{
+						throw new UnsupportedOperationException();
+					}
+				};
+			}
+		};
+	}
+
 	@Override
 	public void findDeadlocks(boolean fix) throws PrismException
 	{