//============================================================================== // // Copyright (c) 2016- // Authors: // * Steffen Maercker (TU Dresden) // * Joachim Klein (TU Dresden) // //------------------------------------------------------------------------------ // // This file is part of PRISM. // // PRISM is free software; you can redistribute it and/or modify // it under the terms of the GNU General Public License as published by // the Free Software Foundation; either version 2 of the License, or // (at your option) any later version. // // PRISM is distributed in the hope that it will be useful, // but WITHOUT ANY WARRANTY; without even the implied warranty of // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the // GNU General Public License for more details. // // You should have received a copy of the GNU General Public License // along with PRISM; if not, write to the Free Software Foundation, // Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA // //============================================================================== package explicit.modelviews; import java.util.AbstractMap; import java.util.Iterator; import java.util.Map.Entry; import java.util.PrimitiveIterator; import java.util.function.IntFunction; import common.IterableStateSet; 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 * by mapping from some other model on-the-fly. *
* The main job of sub-classes is to provide an appropriate * getTransitionsIterator() method. Several other methods, providing * meta-data on the model have to be provided as well. For examples, * see the sub-classes contained in this package. */ public abstract class DTMCView extends ModelView implements DTMC, Cloneable { public DTMCView() { super(); } public DTMCView(final ModelView model) { super(model); } //--- Object --- @Override public String toString() { final IntFunction> getDistribution = new IntFunction>() { @Override public final Entry apply(final int state) { final Distribution distribution = new Distribution(getTransitionsIterator(state)); return new AbstractMap.SimpleImmutableEntry<>(state, distribution); } }; String s = "trans: [ "; final IterableStateSet states = new IterableStateSet(getNumStates()); final Iterator> distributions = new MappingIterator.FromInt<>(states, getDistribution); while (distributions.hasNext()) { final Entry dist = distributions.next(); s += dist.getKey() + ": " + dist.getValue(); if (distributions.hasNext()) { s += ", "; } } return s + " ]"; } //--- Model --- @Override public SuccessorsIterator getSuccessors(final int state) { final Iterator> transitions = getTransitionsIterator(state); return SuccessorsIterator.from(new PrimitiveIterator.OfInt() { public boolean hasNext() {return transitions.hasNext();} public int nextInt() {return transitions.next().getKey();} }, true); } @Override public String infoString() { String s = ""; s += getNumStates() + " states (" + getNumInitialStates() + " initial)"; s += ", " + getNumTransitions() + " transitions"; return s; } @Override public String infoStringTable() { String s = ""; s += "States: " + getNumStates() + " (" + getNumInitialStates() + " initial)\n"; s += "Transitions: " + getNumTransitions() + "\n"; return s; } //--- 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)); } }