imported patch succ-it-from-trans-it.patch

prism/src/explicit/SuccessorsIterator.java

@@ -28,10 +28,12 @@
 package explicit;
 
 import java.util.Iterator;
+import java.util.Map;
 import java.util.NoSuchElementException;
 import java.util.PrimitiveIterator;
 import java.util.Spliterator;
 import java.util.Spliterators;
+import java.util.Map.Entry;
 import java.util.stream.IntStream;
 import java.util.stream.StreamSupport;
 
@@ -148,6 +150,42 @@ public abstract class SuccessorsIterator implements PrimitiveIterator.OfInt
 		}
 	};
 
+	/** Wrapper, underlying iterator is an Iterator<Map.Entry<Integer,?> iterator */
+	private static class SuccessorsIteratorFromTransitionsIterator extends SuccessorsIterator {
+		private Iterator<? extends Entry<Integer, ?>> it;
+		private boolean distinct;
+
+		public SuccessorsIteratorFromTransitionsIterator(Iterator<? extends Map.Entry<Integer,?>> it, boolean distinct)
+		{
+			this.it = it;
+			this.distinct = distinct;
+		}
+
+		@Override
+		public boolean hasNext()
+		{
+			return it.hasNext();
+		}
+
+		@Override
+		public Integer next()
+		{
+			return it.next().getKey();
+		}
+
+		@Override
+		public int nextInt()
+		{
+			return it.next().getKey();
+		}
+
+		@Override
+		public boolean successorsAreDistinct()
+		{
+			return distinct;
+		}
+	};
+
 	/** Helper, empty iterator */
 	private static class SuccessorsIteratorEmpty extends SuccessorsIterator {
 		@Override
@@ -244,6 +282,16 @@ public abstract class SuccessorsIterator implements PrimitiveIterator.OfInt
 		return new SuccessorsIteratorFromOfInt(it, distinctElements);
 	}
 
+	/**
+	 * Obtain a SuccessorsIterator with the given distinctness guarantee from a
+	 * transitions iterator, i.e., an iterator over Map.Entry<Integer, ?> objects
+	 * (or derived classes).
+	 */
+	public static SuccessorsIterator fromTransitionsIterator(Iterator<? extends Map.Entry<Integer,?>> it, boolean distinctElements)
+	{
+		return new SuccessorsIteratorFromTransitionsIterator(it, distinctElements);
+	}
+
 	/** Obtain a SuccessorsIterator for a single state */
 	public static SuccessorsIterator fromSingleton(int i)
 	{