diff --git a/prism/src/explicit/DTMC.java b/prism/src/explicit/DTMC.java index f5909838..c2d588e2 100644 --- a/prism/src/explicit/DTMC.java +++ b/prism/src/explicit/DTMC.java @@ -34,6 +34,7 @@ import java.util.PrimitiveIterator.OfInt; import common.IterableStateSet; import common.iterable.IterableInt; +import common.iterable.MappingIterator; import prism.ModelType; import prism.Pair; import prism.PrismException; @@ -164,7 +165,23 @@ public interface DTMC extends Model /** * Get an iterator over the transitions from state s, with their attached actions if present. */ - public Iterator>> getTransitionsAndActionsIterator(int s); + public default Iterator>> getTransitionsAndActionsIterator(int s) + { + // Default implementation just adds null actions + final Iterator> transitions = getTransitionsIterator(s); + return new MappingIterator.From<>(transitions, transition -> attachAction(transition, null)); + } + + /** + * Attach an action to a transition, assuming iterators as used in + * {@link #getTransitionsIterator(int)} and {@link #getTransitionsAndActionsIterator(int)} + */ + public static Entry> attachAction(final Entry transition, final Object action) + { + final Integer state = transition.getKey(); + final Double probability = transition.getValue(); + return new AbstractMap.SimpleImmutableEntry<>(state, new Pair<>(probability, action)); + } /** * Functional interface for a consumer, diff --git a/prism/src/explicit/DTMCExplicit.java b/prism/src/explicit/DTMCExplicit.java index 64bd1cdd..87a9ee7b 100644 --- a/prism/src/explicit/DTMCExplicit.java +++ b/prism/src/explicit/DTMCExplicit.java @@ -26,58 +26,9 @@ package explicit; -import java.util.AbstractMap; -import java.util.Iterator; -import java.util.Map; -import java.util.Map.Entry; - -import prism.Pair; - /** * Base class for explicit-state representations of a DTMC. */ public abstract class DTMCExplicit extends ModelExplicit implements DTMC { - // Accessors (for DTMC) - - @Override - public Iterator>> getTransitionsAndActionsIterator(int s) - { - // Default implementation: extend iterator, setting all actions to null - return new AddDefaultActionToTransitionsIterator(getTransitionsIterator(s), null); - } - - public class AddDefaultActionToTransitionsIterator implements Iterator>> - { - private Iterator> transIter; - private Object defaultAction; - private Entry next; - - public AddDefaultActionToTransitionsIterator(Iterator> transIter, Object defaultAction) - { - this.transIter = transIter; - this.defaultAction = defaultAction; - } - - @Override - public Entry> next() - { - next = transIter.next(); - final Integer state = next.getKey(); - final Double probability = next.getValue(); - return new AbstractMap.SimpleImmutableEntry<>(state, new Pair<>(probability, defaultAction)); - } - - @Override - public boolean hasNext() - { - return transIter.hasNext(); - } - - @Override - public void remove() - { - // Do nothing: read-only - } - } } diff --git a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java index 2f328841..5b805705 100644 --- a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java +++ b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java @@ -32,6 +32,7 @@ import java.util.Iterator; import java.util.List; import java.util.Map.Entry; +import common.iterable.MappingIterator; import parser.State; import parser.Values; import prism.Pair; @@ -161,7 +162,8 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit public Iterator>> getTransitionsAndActionsIterator(int s) { if (adv[s] >= 0) { - return new DTMCExplicit.AddDefaultActionToTransitionsIterator(mdp.getTransitionsIterator(s, adv[s]), mdp.getAction(s, adv[s])); + final Iterator> transitions = mdp.getTransitionsIterator(s, adv[s]); + return new MappingIterator.From<>(transitions, transition -> DTMC.attachAction(transition, mdp.getAction(s, adv[s]))); } else { // Empty iterator return Collections.>>emptyIterator(); diff --git a/prism/src/explicit/modelviews/DTMCView.java b/prism/src/explicit/modelviews/DTMCView.java index 2f953dac..1f9dbefb 100644 --- a/prism/src/explicit/modelviews/DTMCView.java +++ b/prism/src/explicit/modelviews/DTMCView.java @@ -38,7 +38,6 @@ import common.iterable.MappingIterator; import explicit.DTMC; import explicit.Distribution; import explicit.SuccessorsIterator; -import prism.Pair; /** * Base class for a DTMC view, i.e., a virtual DTMC that is obtained @@ -104,20 +103,4 @@ public abstract class DTMCView extends ModelView implements DTMC, Cloneable public int nextInt() {return transitions.next().getKey();} }, true); } - - //--- DTMC --- - - public static Entry> attachAction(final Entry transition, final Object action) - { - final Integer state = transition.getKey(); - final Double probability = transition.getValue(); - return new AbstractMap.SimpleImmutableEntry<>(state, new Pair<>(probability, action)); - } - - @Override - public Iterator>> getTransitionsAndActionsIterator(final int state) - { - final Iterator> transitions = getTransitionsIterator(state); - return new MappingIterator.From<>(transitions, transition -> attachAction(transition, null)); - } }