Browse Source

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.
accumulation-v4.7
Dave Parker 5 years ago
parent
commit
2c9a0cac2a
  1. 19
      prism/src/explicit/DTMC.java
  2. 49
      prism/src/explicit/DTMCExplicit.java
  3. 4
      prism/src/explicit/DTMCFromMDPMemorylessAdversary.java
  4. 17
      prism/src/explicit/modelviews/DTMCView.java

19
prism/src/explicit/DTMC.java

@ -34,6 +34,7 @@ import java.util.PrimitiveIterator.OfInt;
import common.IterableStateSet; import common.IterableStateSet;
import common.iterable.IterableInt; import common.iterable.IterableInt;
import common.iterable.MappingIterator;
import prism.ModelType; import prism.ModelType;
import prism.Pair; import prism.Pair;
import prism.PrismException; 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. * Get an iterator over the transitions from state s, with their attached actions if present.
*/ */
public Iterator<Entry<Integer, Pair<Double, Object>>> getTransitionsAndActionsIterator(int s);
public default Iterator<Entry<Integer, Pair<Double, Object>>> getTransitionsAndActionsIterator(int s)
{
// Default implementation just adds null actions
final Iterator<Entry<Integer, Double>> 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<Integer, Pair<Double, Object>> attachAction(final Entry<Integer, Double> 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, * Functional interface for a consumer,

49
prism/src/explicit/DTMCExplicit.java

@ -26,58 +26,9 @@
package explicit; 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. * Base class for explicit-state representations of a DTMC.
*/ */
public abstract class DTMCExplicit extends ModelExplicit implements DTMC public abstract class DTMCExplicit extends ModelExplicit implements DTMC
{ {
// Accessors (for DTMC)
@Override
public Iterator<Entry<Integer, Pair<Double, Object>>> getTransitionsAndActionsIterator(int s)
{
// Default implementation: extend iterator, setting all actions to null
return new AddDefaultActionToTransitionsIterator(getTransitionsIterator(s), null);
}
public class AddDefaultActionToTransitionsIterator implements Iterator<Map.Entry<Integer, Pair<Double, Object>>>
{
private Iterator<Entry<Integer, Double>> transIter;
private Object defaultAction;
private Entry<Integer, Double> next;
public AddDefaultActionToTransitionsIterator(Iterator<Entry<Integer, Double>> transIter, Object defaultAction)
{
this.transIter = transIter;
this.defaultAction = defaultAction;
}
@Override
public Entry<Integer, Pair<Double, Object>> 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
}
}
} }

4
prism/src/explicit/DTMCFromMDPMemorylessAdversary.java

@ -32,6 +32,7 @@ import java.util.Iterator;
import java.util.List; import java.util.List;
import java.util.Map.Entry; import java.util.Map.Entry;
import common.iterable.MappingIterator;
import parser.State; import parser.State;
import parser.Values; import parser.Values;
import prism.Pair; import prism.Pair;
@ -161,7 +162,8 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit
public Iterator<Entry<Integer, Pair<Double, Object>>> getTransitionsAndActionsIterator(int s) public Iterator<Entry<Integer, Pair<Double, Object>>> getTransitionsAndActionsIterator(int s)
{ {
if (adv[s] >= 0) { if (adv[s] >= 0) {
return new DTMCExplicit.AddDefaultActionToTransitionsIterator(mdp.getTransitionsIterator(s, adv[s]), mdp.getAction(s, adv[s]));
final Iterator<Entry<Integer, Double>> transitions = mdp.getTransitionsIterator(s, adv[s]);
return new MappingIterator.From<>(transitions, transition -> DTMC.attachAction(transition, mdp.getAction(s, adv[s])));
} else { } else {
// Empty iterator // Empty iterator
return Collections.<Entry<Integer,Pair<Double, Object>>>emptyIterator(); return Collections.<Entry<Integer,Pair<Double, Object>>>emptyIterator();

17
prism/src/explicit/modelviews/DTMCView.java

@ -38,7 +38,6 @@ import common.iterable.MappingIterator;
import explicit.DTMC; import explicit.DTMC;
import explicit.Distribution; import explicit.Distribution;
import explicit.SuccessorsIterator; import explicit.SuccessorsIterator;
import prism.Pair;
/** /**
* Base class for a DTMC view, i.e., a virtual DTMC that is obtained * 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();} public int nextInt() {return transitions.next().getKey();}
}, true); }, true);
} }
//--- DTMC ---
public static Entry<Integer, Pair<Double, Object>> attachAction(final Entry<Integer, Double> 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<Entry<Integer, Pair<Double, Object>>> getTransitionsAndActionsIterator(final int state)
{
final Iterator<Entry<Integer, Double>> transitions = getTransitionsIterator(state);
return new MappingIterator.From<>(transitions, transition -> attachAction(transition, null));
}
} }
Loading…
Cancel
Save