From 2c9a0cac2a620f36ce59dbd38df64f78e1b39159 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 10 Sep 2020 09:21:56 +0100 Subject: [PATCH] Add default implementation of getTransitionsAndActionsIterator to DTMC. This just sets a null action for all existing transitions. Previously, this was in DTMCExplicit, but has been removed from there. This means it can also be removed from DTMCView. In fact the implementation is taken from DTMCView, which was cleaner. Furthermore, the same mechanism is now also used for implementing getTransitionsAndActionsIterator in DTMCFromMDPMemorylessAdversary. --- prism/src/explicit/DTMC.java | 19 ++++++- prism/src/explicit/DTMCExplicit.java | 49 ------------------- .../DTMCFromMDPMemorylessAdversary.java | 4 +- prism/src/explicit/modelviews/DTMCView.java | 17 ------- 4 files changed, 21 insertions(+), 68 deletions(-) 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)); - } }