Add getSuccessorsIterator to explicit Model interface.

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

prism/src/explicit/DTMCEmbeddedSimple.java

@@ -125,6 +125,18 @@ public class DTMCEmbeddedSimple extends DTMCExplicit
 		return ctmc.getNumTransitions() + numExtraTransitions;
 	}
 
+	@Override
+	public Iterator<Integer> getSuccessorsIterator(final int s)
+	{
+		if (exitRates[s] == 0) {
+			List<Integer> list = new ArrayList<Integer>(1);
+			list.add(s);
+			return list.iterator();
+		} else {
+			return ctmc.getSuccessorsIterator(s);
+		}
+	}
+	
 	public boolean isSuccessor(int s1, int s2)
 	{
 		return exitRates[s1] == 0 ? (s1 == s2) : ctmc.isSuccessor(s1, s2);

prism/src/explicit/DTMCFromMDPMemorylessAdversary.java

@@ -117,6 +117,11 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit
 		throw new RuntimeException("Not implemented");
 	}
 
+	public Iterator<Integer> getSuccessorsIterator(final int s)
+	{
+		throw new RuntimeException("Not implemented yet");
+	}
+	
 	public boolean isSuccessor(int s1, int s2)
 	{
 		throw new RuntimeException("Not implemented yet");

prism/src/explicit/DTMCSimple.java

@@ -212,6 +212,12 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple
 		return numTransitions;
 	}
 
+	@Override
+	public Iterator<Integer> getSuccessorsIterator(final int s)
+	{
+		return trans.get(s).getSupport().iterator();
+	}
+	
 	@Override
 	public boolean isSuccessor(int s1, int s2)
 	{

prism/src/explicit/DTMCUniformisedSimple.java

@@ -134,6 +134,12 @@ public class DTMCUniformisedSimple extends DTMCExplicit
 		return ctmc.getNumTransitions() + numExtraTransitions;
 	}
 
+	public Iterator<Integer> getSuccessorsIterator(final int s)
+	{
+		// TODO
+		throw new Error("Not yet supported");
+	}
+	
 	public boolean isSuccessor(int s1, int s2)
 	{
 		// TODO

prism/src/explicit/Distribution.java

@@ -158,6 +158,14 @@ public class Distribution implements Iterable<Entry<Integer,Double>>
 		return false;
 	}
 	
+	/**
+	 * Get the support of the distribution.
+	 */
+	public Set<Integer> getSupport()
+	{
+		return map.keySet();
+	}
+	
 	/**
 	 * Get an iterator over the entries of the map defining the distribution.
 	 */

prism/src/explicit/MDPSimple.java

@@ -389,6 +389,18 @@ public class MDPSimple extends MDPExplicit implements ModelSimple
 		return numTransitions;
 	}
 
+	@Override
+	public Iterator<Integer> getSuccessorsIterator(final int s)
+	{
+		// Need to build set to avoid duplicates
+		// So not necessarily the fastest method to access successors
+		HashSet<Integer> succs = new HashSet<Integer>();
+		for (Distribution distr : trans.get(s)) {
+			succs.addAll(distr.getSupport());
+		}
+		return succs.iterator();
+	}
+	
 	@Override
 	public boolean isSuccessor(int s1, int s2)
 	{

prism/src/explicit/MDPSparse.java

@@ -371,6 +371,20 @@ public class MDPSparse extends MDPExplicit
 		return numTransitions;
 	}
 
+	@Override
+	public Iterator<Integer> getSuccessorsIterator(final int s)
+	{
+		// Need to build set to avoid duplicates
+		// So not necessarily the fastest method to access successors
+		int start = choiceStarts[rowStarts[s]];
+		int end = choiceStarts[rowStarts[s + 1]];
+		HashSet<Integer> succs = new HashSet<Integer>();
+		for (int i = start; i < end; i++) {
+			succs.add(cols[i]);
+		}
+		return succs.iterator();
+	}
+	
 	@Override
 	public boolean isSuccessor(int s1, int s2)
 	{

prism/src/explicit/Model.java

@@ -28,6 +28,7 @@ package explicit;
 
 import java.io.File;
 import java.util.*;
+import java.util.Map.Entry;
 
 import parser.State;
 import parser.Values;
@@ -121,6 +122,11 @@ public interface Model
 	 */
 	public int getNumTransitions();
 
+	/**
+	 * Get an iterator over the successors of state s.
+	 */
+	public Iterator<Integer> getSuccessorsIterator(int s);
+	
 	/**
 	 * Returns true if state s2 is a successor of state s1.
 	 */

prism/src/explicit/STPGAbstrSimple.java

@@ -280,6 +280,20 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, ModelSimple
 		return numTransitions;
 	}
 
+	@Override
+	public Iterator<Integer> getSuccessorsIterator(final int s)
+	{
+		// Need to build set to avoid duplicates
+		// So not necessarily the fastest method to access successors
+		HashSet<Integer> succs = new HashSet<Integer>();
+		for (DistributionSet distrs : trans.get(s)) {
+			for (Distribution distr : distrs) {
+				succs.addAll(distr.getSupport());
+			}
+		}
+		return succs.iterator();
+	}
+	
 	@Override
 	public boolean isSuccessor(int s1, int s2)
 	{