diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java index fb8c98f6..0b5e2ee2 100644 --- a/prism/src/explicit/MDP.java +++ b/prism/src/explicit/MDP.java @@ -39,11 +39,6 @@ import explicit.rewards.MDPRewards; */ public interface MDP extends NondetModel { - /** - * Get the number of transitions from choice {@code i} of state {@code s}. - */ - public int getNumTransitions(int s, int i); - /** * Get an iterator over the transitions from choice {@code i} of state {@code s}. */ diff --git a/prism/src/explicit/NondetModel.java b/prism/src/explicit/NondetModel.java index 02b1fbeb..3cc9a9cd 100644 --- a/prism/src/explicit/NondetModel.java +++ b/prism/src/explicit/NondetModel.java @@ -27,12 +27,8 @@ package explicit; import java.util.BitSet; -import java.util.Iterator; -import java.util.Map.Entry; -import prism.PrismException; import prism.PrismLog; - import strat.MDStrategy; /** @@ -67,6 +63,11 @@ public interface NondetModel extends Model */ public boolean areAllChoiceActionsUnique(); + /** + * Get the number of transitions from choice {@code i} of state {@code s}. + */ + public int getNumTransitions(int s, int i); + /** * Check if all the successor states from choice {@code i} of state {@code s} are in the set {@code set}. * @param s The state to check @@ -86,7 +87,7 @@ public interface NondetModel extends Model /** * Get an iterator over the transitions of state s and action i. */ - public Iterator> getTransitionsIterator(int s, int i); + //public Iterator> getTransitionsIterator(int s, int i); /** * Construct a model that is induced by applying strategy {@code strat} to this model. diff --git a/prism/src/explicit/SubNondetModel.java b/prism/src/explicit/SubNondetModel.java index ade6b67b..d8773e39 100644 --- a/prism/src/explicit/SubNondetModel.java +++ b/prism/src/explicit/SubNondetModel.java @@ -34,7 +34,6 @@ import java.util.HashMap; import java.util.Iterator; import java.util.List; import java.util.Map; -import java.util.Map.Entry; import parser.State; import parser.Values; @@ -150,8 +149,7 @@ public class SubNondetModel implements NondetModel @Override public List getStatesList() { - //We use lazy generation because in many cases the state list is not - //needed + // We use lazy generation because in many cases the state list is not needed if (statesList == null) { statesList = generateSubStateList(states); } @@ -191,14 +189,13 @@ public class SubNondetModel implements NondetModel public Iterator getSuccessorsIterator(int s) { s = translateState(s); - List succ = new ArrayList(); for (int i = 0; i < model.getNumChoices(s); i++) { if (actions.get(s).get(i)) { - Iterator> it = model.getTransitionsIterator(s, i); + Iterator it = model.getSuccessorsIterator(s); while (it.hasNext()) { - int succc = it.next().getKey(); - succ.add(inverseTranslateState(succc)); + int j = it.next(); + succ.add(inverseTranslateState(j)); } } } @@ -361,6 +358,14 @@ public class SubNondetModel implements NondetModel throw new RuntimeException("Not implemented"); } + @Override + public int getNumTransitions(int s, int i) + { + s = translateState(s); + i = translateAction(s, i); + return model.getNumTransitions(s, i); + } + @Override public boolean allSuccessorsInSet(int s, int i, BitSet set) { @@ -405,31 +410,13 @@ public class SubNondetModel implements NondetModel { int transitions = 0; for (int i = 0; i < model.getNumChoices(state); i++) { - Iterator> it = model.getTransitionsIterator(state, i); - while (it.hasNext()) { - it.next(); - transitions += 1; + if (actions.get(state).get(i)) { + transitions += model.getNumTransitions(state, i); } } return transitions; } - @Override - public Iterator> getTransitionsIterator(int s, int i) - { - s = translateState(s); - i = translateAction(s, i); - - Map distrs = new HashMap(); - Iterator> it = model.getTransitionsIterator(s, i); - while (it.hasNext()) { - Entry e = it.next(); - int succ = inverseTranslateState(e.getKey()); - distrs.put(succ, e.getValue()); - } - return distrs.entrySet().iterator(); - } - @Override public Model constructInducedModel(MDStrategy strat) {