Add some missing methods to DTMCFromMDPAndMDStrategy.

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

prism/src/explicit/DTMCFromMDPAndMDStrategy.java

@@ -29,6 +29,7 @@ package explicit;
 import java.util.*;
 import java.util.Map.Entry;
 
+import common.IterableStateSet;
 import explicit.rewards.MCRewards;
 import parser.State;
 import parser.Values;
@@ -123,7 +124,7 @@ public class DTMCFromMDPAndMDStrategy extends DTMCExplicit
 
 	public Iterator<Integer> getSuccessorsIterator(final int s)
 	{
-		throw new RuntimeException("Not implemented yet");
+		return mdp.getSuccessorsIterator(s, strat.getChoiceIndex(s));
 	}
 
 	public boolean isSuccessor(int s1, int s2)
@@ -133,12 +134,12 @@ public class DTMCFromMDPAndMDStrategy extends DTMCExplicit
 
 	public boolean allSuccessorsInSet(int s, BitSet set)
 	{
-		throw new RuntimeException("Not implemented yet");
+		return mdp.allSuccessorsInSet(s, strat.getChoiceIndex(s), set);
 	}
 
 	public boolean someSuccessorsInSet(int s, BitSet set)
 	{
-		throw new RuntimeException("Not implemented yet");
+		return mdp.someSuccessorsInSet(s, strat.getChoiceIndex(s), set);
 	}
 
 	public int getNumChoices(int s)
@@ -212,14 +213,17 @@ public class DTMCFromMDPAndMDStrategy extends DTMCExplicit
 
 	public void prob0step(BitSet subset, BitSet u, BitSet result)
 	{
-		// TODO
-		throw new Error("Not yet supported");
+		for (int i : new IterableStateSet(subset, numStates)) {
+			result.set(i, mdp.someSuccessorsInSet(i, strat.getChoiceIndex(i), u));
+		}
 	}
 
 	public void prob1step(BitSet subset, BitSet u, BitSet v, BitSet result)
 	{
-		// TODO
-		throw new Error("Not yet supported");
+		for (int i : new IterableStateSet(subset, numStates)) {
+			int j = strat.getChoiceIndex(i);
+			result.set(i, mdp.someSuccessorsInSet(i, j, v) && mdp.allSuccessorsInSet(i, j, u));
+		}
 	}
 
 	@Override