diff --git a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java index e01636e4..cb0ca2c7 100644 --- a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java +++ b/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 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