From 6d06d3d914830dfce0a7c2b632bef99ecbc74d04 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffen=20M=C3=A4rcker?= Date: Thu, 30 Mar 2023 19:48:19 +0200 Subject: [PATCH] Use OfInt in Model and improve SuccessorsIterator --- prism/src/explicit/DTMCEmbeddedSimple.java | 3 +- .../explicit/DTMCFromMDPAndMDStrategy.java | 3 +- .../DTMCFromMDPMemorylessAdversary.java | 3 +- prism/src/explicit/DTMCSimple.java | 6 +- prism/src/explicit/DTMCSparse.java | 6 +- prism/src/explicit/DTMCUniformisedSimple.java | 5 +- prism/src/explicit/Model.java | 10 ++- prism/src/explicit/ModelExplicit.java | 10 ++- prism/src/explicit/STPGAbstrSimple.java | 19 ++--- prism/src/explicit/SubNondetModel.java | 11 ++- prism/src/explicit/SuccessorsIterator.java | 84 +++++++------------ .../modelviews/DTMCAlteredDistributions.java | 6 +- .../modelviews/MDPAdditionalChoices.java | 6 +- .../modelviews/MDPDroppedAllChoices.java | 14 ++-- .../modelviews/MDPDroppedChoicesCached.java | 3 +- prism/src/explicit/modelviews/MDPEquiv.java | 3 +- .../src/explicit/modelviews/MDPFromDTMC.java | 11 ++- 17 files changed, 92 insertions(+), 111 deletions(-) diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index 4bf0094280..c1dd4cb83a 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/prism/src/explicit/DTMCEmbeddedSimple.java @@ -29,6 +29,7 @@ import java.util.*; import java.util.Map.Entry; +import common.iterable.FunctionalPrimitiveIterable; import explicit.rewards.MCRewards; import parser.State; import parser.Values; @@ -86,7 +87,7 @@ public int getNumInitialStates() return ctmc.getNumInitialStates(); } - public Iterable getInitialStates() + public FunctionalPrimitiveIterable.OfInt getInitialStates() { return ctmc.getInitialStates(); } diff --git a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java index 09cc053d0c..6a8442c20c 100644 --- a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java +++ b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java @@ -29,6 +29,7 @@ import java.util.*; import java.util.Map.Entry; +import common.iterable.FunctionalPrimitiveIterable; import explicit.rewards.MCRewards; import parser.State; import parser.Values; @@ -76,7 +77,7 @@ public int getNumInitialStates() return mdp.getNumInitialStates(); } - public Iterable getInitialStates() + public FunctionalPrimitiveIterable.OfInt getInitialStates() { return mdp.getInitialStates(); } diff --git a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java index 34400c988c..fd3db1efef 100644 --- a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java +++ b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java @@ -32,6 +32,7 @@ import java.util.List; import java.util.Map.Entry; +import common.iterable.FunctionalPrimitiveIterable; import common.iterable.Reducible; import parser.State; import parser.Values; @@ -80,7 +81,7 @@ public int getNumInitialStates() return mdp.getNumInitialStates(); } - public Iterable getInitialStates() + public FunctionalPrimitiveIterable.OfInt getInitialStates() { return mdp.getInitialStates(); } diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index 789f80dacd..a32c1c3c21 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -30,6 +30,8 @@ import java.util.Map.Entry; import java.io.*; +import common.iterable.FunctionalPrimitiveIterator; +import common.iterable.Reducible; import prism.PrismException; /** @@ -213,9 +215,9 @@ public int getNumTransitions(int s) /** Get an iterator over the successors of state s */ @Override - public Iterator getSuccessorsIterator(final int s) + public FunctionalPrimitiveIterator.OfInt getSuccessorsIterator(final int s) { - return trans.get(s).getSupport().iterator(); + return Reducible.unboxInt(trans.get(s).getSupport()).iterator(); } @Override diff --git a/prism/src/explicit/DTMCSparse.java b/prism/src/explicit/DTMCSparse.java index b082ff39dd..4b23cd99aa 100644 --- a/prism/src/explicit/DTMCSparse.java +++ b/prism/src/explicit/DTMCSparse.java @@ -38,6 +38,8 @@ import java.util.function.Function; import common.IterableStateSet; +import common.iterable.FunctionalPrimitiveIterator; +import common.iterable.IterableArray; import common.iterable.PrimitiveIterable; import explicit.rewards.MCRewards; import prism.PrismException; @@ -151,9 +153,9 @@ public int getNumTransitions(int state) } @Override - public OfInt getSuccessorsIterator(final int state) + public FunctionalPrimitiveIterator.OfInt getSuccessorsIterator(final int state) { - return Arrays.stream(columns, rows[state], rows[state+1]).iterator(); + return new IterableArray.OfInt(columns, rows[state], rows[state+1]).iterator(); } @Override diff --git a/prism/src/explicit/DTMCUniformisedSimple.java b/prism/src/explicit/DTMCUniformisedSimple.java index 3489332676..6eb6b00bc2 100644 --- a/prism/src/explicit/DTMCUniformisedSimple.java +++ b/prism/src/explicit/DTMCUniformisedSimple.java @@ -33,6 +33,7 @@ import java.util.Map; import java.util.Map.Entry; +import common.iterable.FunctionalPrimitiveIterable; import parser.State; import parser.Values; import prism.PrismException; @@ -98,7 +99,7 @@ public int getNumInitialStates() return ctmc.getNumInitialStates(); } - public Iterable getInitialStates() + public FunctionalPrimitiveIterable.OfInt getInitialStates() { return ctmc.getInitialStates(); } @@ -120,7 +121,7 @@ public int getNumDeadlockStates() } @Override - public Iterable getDeadlockStates() + public FunctionalPrimitiveIterable.OfInt getDeadlockStates() { return ctmc.getDeadlockStates(); } diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index 1208dd3320..ffc46cc888 100644 --- a/prism/src/explicit/Model.java +++ b/prism/src/explicit/Model.java @@ -39,6 +39,8 @@ import java.util.function.IntPredicate; import common.IteratorTools; +import common.iterable.FunctionalPrimitiveIterable; +import common.iterable.FunctionalPrimitiveIterator; import explicit.graphviz.Decorator; import parser.State; import parser.Values; @@ -77,7 +79,7 @@ public interface Model /** * Get iterator over initial state list. */ - public Iterable getInitialStates(); + public FunctionalPrimitiveIterable.OfInt getInitialStates(); /** * Get the index of the first initial state @@ -101,7 +103,7 @@ public interface Model * Get iterator over states that are/were deadlocks. * (Such states may have been fixed at build-time by adding self-loops) */ - public Iterable getDeadlockStates(); + public FunctionalPrimitiveIterable.OfInt getDeadlockStates(); /** * Get list of states that are/were deadlocks. @@ -184,7 +186,7 @@ public default int getNumTransitions() */ public default int getNumTransitions(int s) { - return Math.toIntExact(IteratorTools.count(getSuccessorsIterator(s))); + return Math.toIntExact(getSuccessorsIterator(s).count()); } /** @@ -210,7 +212,7 @@ public default long getNumTransitions(PrimitiveIterator.OfInt states) * from {@code getSuccessors}, ensuring that there are no * duplicates. */ - public default Iterator getSuccessorsIterator(int s) + public default FunctionalPrimitiveIterator.OfInt getSuccessorsIterator(int s) { SuccessorsIterator successors = getSuccessors(s); return successors.distinct(); diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index f24d329477..a9a0302417 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/prism/src/explicit/ModelExplicit.java @@ -34,6 +34,8 @@ import java.util.TreeMap; import java.util.TreeSet; +import common.iterable.FunctionalPrimitiveIterable; +import common.iterable.Reducible; import parser.State; import parser.Values; import parser.VarList; @@ -279,9 +281,9 @@ public int getNumInitialStates() } @Override - public Iterable getInitialStates() + public FunctionalPrimitiveIterable.OfInt getInitialStates() { - return initialStates; + return Reducible.unboxInt(initialStates); } @Override @@ -303,9 +305,9 @@ public int getNumDeadlockStates() } @Override - public Iterable getDeadlockStates() + public FunctionalPrimitiveIterable.OfInt getDeadlockStates() { - return deadlocks; + return Reducible.unboxInt(deadlocks); } @Override diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index c8683de4bd..f234716d96 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -31,15 +31,11 @@ import java.io.File; import java.io.FileReader; import java.io.IOException; -import java.util.ArrayList; -import java.util.BitSet; -import java.util.HashSet; -import java.util.Iterator; -import java.util.List; -import java.util.Map; +import java.util.*; import java.util.Map.Entry; import common.IterableStateSet; +import common.iterable.*; import explicit.rewards.STPGRewards; import prism.PrismException; import prism.PrismLog; @@ -285,17 +281,12 @@ public int getNumTransitions() } @Override - public Iterator getSuccessorsIterator(final int s) + public FunctionalPrimitiveIterator.OfInt getSuccessorsIterator(final int s) { // Need to build set to avoid duplicates // So not necessarily the fastest method to access successors - HashSet succs = new HashSet(); - for (DistributionSet distrs : trans.get(s)) { - for (Distribution distr : distrs) { - succs.addAll(distr.getSupport()); - } - } - return succs.iterator(); + FunctionalIterable support = Reducible.concat(trans.get(s)).flatMap(Distribution::getSupport).distinct(); + return Reducible.unboxInt(support.iterator()); } @Override diff --git a/prism/src/explicit/SubNondetModel.java b/prism/src/explicit/SubNondetModel.java index b1f49b9dcc..4dc428c2f6 100644 --- a/prism/src/explicit/SubNondetModel.java +++ b/prism/src/explicit/SubNondetModel.java @@ -35,6 +35,9 @@ import java.util.Set; import common.IterableStateSet; +import common.iterable.FunctionalPrimitiveIterable; +import common.iterable.FunctionalPrimitiveIterator; +import common.iterable.Reducible; import parser.State; import parser.Values; import parser.VarList; @@ -99,14 +102,14 @@ public int getNumInitialStates() } @Override - public Iterable getInitialStates() + public FunctionalPrimitiveIterable.OfInt getInitialStates() { - List is = new ArrayList(); + List is = new ArrayList<>(); for (int i = initialStates.nextSetBit(0); i >= 0; i = initialStates.nextSetBit(i + 1)) { is.add(translateState(i)); } - return is; + return Reducible.unboxInt(is); } @Override @@ -128,7 +131,7 @@ public int getNumDeadlockStates() } @Override - public Iterable getDeadlockStates() + public FunctionalPrimitiveIterable.OfInt getDeadlockStates() { throw new UnsupportedOperationException(); } diff --git a/prism/src/explicit/SuccessorsIterator.java b/prism/src/explicit/SuccessorsIterator.java index 60e49988ab..0900a748b7 100644 --- a/prism/src/explicit/SuccessorsIterator.java +++ b/prism/src/explicit/SuccessorsIterator.java @@ -34,9 +34,7 @@ import java.util.stream.IntStream; import java.util.stream.StreamSupport; -import common.iterable.FunctionalIterator; -import common.iterable.Reducible; -import common.iterable.SingletonIterator; +import common.iterable.*; /** * Base class and static helpers for iterators over successor states. @@ -46,7 +44,7 @@ * over the set of successors or the multiset of successors. The latter * might have better performance, as no deduplication is needed. */ -public abstract class SuccessorsIterator implements PrimitiveIterator.OfInt +public abstract class SuccessorsIterator implements FunctionalPrimitiveIterator.OfInt { /** Is it guaranteed that every successor will occur only once? */ public abstract boolean successorsAreDistinct(); @@ -70,7 +68,7 @@ public SuccessorsIterator distinct() if (successorsAreDistinct()) { return this; } else { - return new SuccessorsIteratorFromOfInt(Reducible.extend(this).distinct(), true); + return new SuccessorsIteratorFromOfInt(FunctionalPrimitiveIterator.OfInt.super.distinct(), true); } } @@ -83,9 +81,10 @@ public IntStream stream() } /** Wrapper, underlying iterator is an OfInt iterator */ - private static class SuccessorsIteratorFromOfInt extends SuccessorsIterator { - private java.util.PrimitiveIterator.OfInt it; - private boolean distinct; + private static class SuccessorsIteratorFromOfInt extends SuccessorsIterator + { + protected PrimitiveIterator.OfInt it; + protected boolean distinct; public SuccessorsIteratorFromOfInt(PrimitiveIterator.OfInt it, boolean distinct) { @@ -113,9 +112,10 @@ public int nextInt() } /** Wrapper, underlying iterator is an Iterator iterator */ - private static class SuccessorsIteratorFromIterator extends SuccessorsIterator { - private Iterator it; - private boolean distinct; + private static class SuccessorsIteratorFromIterator extends SuccessorsIterator + { + protected Iterator it; + protected boolean distinct; public SuccessorsIteratorFromIterator(Iterator it, boolean distinct) { @@ -129,6 +129,7 @@ public boolean hasNext() return it.hasNext(); } + // Override to avoid boxing and unboxing of default implementation @Override public Integer next() { @@ -149,7 +150,8 @@ public boolean successorsAreDistinct() }; /** Helper, empty iterator */ - private static class SuccessorsIteratorEmpty extends SuccessorsIterator { + private static class SuccessorsIteratorEmpty extends SuccessorsIterator + { @Override public boolean hasNext() { @@ -170,20 +172,20 @@ public boolean successorsAreDistinct() }; /** Helper, chain multiple SuccessorsIterators */ - private static class ChainedSuccessorsIterator extends SuccessorsIterator { - private Iterator iterators; - private SuccessorsIterator current; - private boolean distinct; + private static class ChainedSuccessorsIterator extends SuccessorsIterator + { + protected FunctionalPrimitiveIterator.OfInt iterator; + protected boolean distinct; public ChainedSuccessorsIterator(Iterator iterators) { - this.iterators = iterators; - current = iterators.hasNext() ? iterators.next() : null; - if (current != null && !iterators.hasNext()) { - // only a single successor iterator, can inherit elementsAreDistinct - distinct = current.successorsAreDistinct(); + if (iterators.hasNext()) { + SuccessorsIterator first = iterators.next(); + // we inherit elementsAreDistinct if we've got only one Iterator + this.distinct = !iterators.hasNext() && first.successorsAreDistinct(); + iterator = new ChainedIterator.OfInt(first, iterators); } else { - // can not guarantee that successors are distinct + iterator = EmptyIterator.ofInt(); distinct = false; } } @@ -191,38 +193,13 @@ public ChainedSuccessorsIterator(Iterator iterators) @Override public boolean hasNext() { - if (current == null) { - return false; - } - - if (current.hasNext()) { - // the current iterator has another element - return true; - } - - // the current iterator has no more elements, - // search for the next iterator that as an element - while (iterators.hasNext()) { - // consider the next iterator - current = iterators.next(); - if (current.hasNext()) { - // iterator has element, keep current and return true - return true; - } - } - - // there are no more iterators / elements - current = null; - return false; + return iterator.hasNext(); } @Override public int nextInt() { - if (!hasNext()) { - throw new NoSuchElementException(); - } - return current.nextInt(); + return iterator.nextInt(); } @Override @@ -235,15 +212,12 @@ public boolean successorsAreDistinct() /** Obtain a SuccessorsIterator with the given distinctness guarantee from an Iterator */ public static SuccessorsIterator from(Iterator it, boolean distinctElements) { + if (it instanceof PrimitiveIterator.OfInt) { + return new SuccessorsIteratorFromOfInt((PrimitiveIterator.OfInt) it, distinctElements); + } return new SuccessorsIteratorFromIterator(it, distinctElements); } - /** Obtain a SuccessorsIterator with the given distinctness guarantee from an OfInt */ - public static SuccessorsIterator from(PrimitiveIterator.OfInt it, boolean distinctElements) - { - return new SuccessorsIteratorFromOfInt(it, distinctElements); - } - /** Obtain a SuccessorsIterator for a single state */ public static SuccessorsIterator fromSingleton(int i) { diff --git a/prism/src/explicit/modelviews/DTMCAlteredDistributions.java b/prism/src/explicit/modelviews/DTMCAlteredDistributions.java index 128d8a7b8c..8715a892a8 100644 --- a/prism/src/explicit/modelviews/DTMCAlteredDistributions.java +++ b/prism/src/explicit/modelviews/DTMCAlteredDistributions.java @@ -36,6 +36,7 @@ import java.util.function.IntFunction; import java.util.function.Predicate; +import common.iterable.FunctionalPrimitiveIterable; import common.iterable.Reducible; import common.iterable.SingletonIterator; import parser.State; @@ -105,7 +106,7 @@ public int getNumInitialStates() } @Override - public Iterable getInitialStates() + public FunctionalPrimitiveIterable.OfInt getInitialStates() { return model.getInitialStates(); } @@ -191,8 +192,7 @@ protected void fixDeadlocks() public static DTMCAlteredDistributions fixDeadlocks(final DTMC model) { - final BitSet deadlockStates = new BitSet(); - model.getDeadlockStates().forEach(deadlockStates::set); + final BitSet deadlockStates = model.getDeadlockStates().collect(new BitSet()); final DTMCAlteredDistributions fixed = addSelfLoops(model, deadlockStates); fixed.deadlockStates = deadlockStates; fixed.fixedDeadlocks = true; diff --git a/prism/src/explicit/modelviews/MDPAdditionalChoices.java b/prism/src/explicit/modelviews/MDPAdditionalChoices.java index cae7ebd79c..08ab01de28 100644 --- a/prism/src/explicit/modelviews/MDPAdditionalChoices.java +++ b/prism/src/explicit/modelviews/MDPAdditionalChoices.java @@ -37,6 +37,7 @@ import java.util.function.IntFunction; import java.util.function.IntPredicate; +import common.iterable.FunctionalPrimitiveIterable; import common.iterable.SingletonIterator; import explicit.MDP; import parser.State; @@ -104,7 +105,7 @@ public int getNumInitialStates() } @Override - public Iterable getInitialStates() + public FunctionalPrimitiveIterable.OfInt getInitialStates() { return model.getInitialStates(); } @@ -232,8 +233,7 @@ private int getNumAdditionalChoices(final int state) public static MDPView fixDeadlocks(final MDP model) { - final BitSet deadlockStates = new BitSet(); - model.getDeadlockStates().forEach(deadlockStates::set); + final BitSet deadlockStates = model.getDeadlockStates().collect(new BitSet()); final MDPView fixed = addSelfLoops(model, deadlockStates); fixed.deadlockStates = deadlockStates; fixed.fixedDeadlocks = true; diff --git a/prism/src/explicit/modelviews/MDPDroppedAllChoices.java b/prism/src/explicit/modelviews/MDPDroppedAllChoices.java index c8cdf9d441..b1f4af0db7 100644 --- a/prism/src/explicit/modelviews/MDPDroppedAllChoices.java +++ b/prism/src/explicit/modelviews/MDPDroppedAllChoices.java @@ -27,13 +27,13 @@ package explicit.modelviews; -import java.util.BitSet; -import java.util.Iterator; -import java.util.List; +import java.util.*; import java.util.Map.Entry; -import java.util.Set; +import common.iterable.EmptyIterable; import common.iterable.EmptyIterator; +import common.iterable.FunctionalPrimitiveIterable; +import common.iterable.FunctionalPrimitiveIterator; import explicit.MDP; import parser.State; import parser.Values; @@ -90,7 +90,7 @@ public int getNumInitialStates() } @Override - public Iterable getInitialStates() + public FunctionalPrimitiveIterable.OfInt getInitialStates() { return model.getInitialStates(); } @@ -145,9 +145,9 @@ public boolean hasLabel(String name) @Override - public Iterator getSuccessorsIterator(final int state) + public FunctionalPrimitiveIterator.OfInt getSuccessorsIterator(final int state) { - return states.get(state) ? EmptyIterator.of() : model.getSuccessorsIterator(state); + return states.get(state) ? EmptyIterator.ofInt() : model.getSuccessorsIterator(state); } diff --git a/prism/src/explicit/modelviews/MDPDroppedChoicesCached.java b/prism/src/explicit/modelviews/MDPDroppedChoicesCached.java index 9a5096e119..f8697246d7 100644 --- a/prism/src/explicit/modelviews/MDPDroppedChoicesCached.java +++ b/prism/src/explicit/modelviews/MDPDroppedChoicesCached.java @@ -35,6 +35,7 @@ import java.util.Set; import common.functions.PairPredicateInt; +import common.iterable.FunctionalPrimitiveIterable; import explicit.Distribution; import explicit.MDP; import parser.State; @@ -111,7 +112,7 @@ public int getNumInitialStates() } @Override - public Iterable getInitialStates() + public FunctionalPrimitiveIterable.OfInt getInitialStates() { return model.getInitialStates(); } diff --git a/prism/src/explicit/modelviews/MDPEquiv.java b/prism/src/explicit/modelviews/MDPEquiv.java index 992fa0603a..04586c7afc 100644 --- a/prism/src/explicit/modelviews/MDPEquiv.java +++ b/prism/src/explicit/modelviews/MDPEquiv.java @@ -39,6 +39,7 @@ import common.functions.PairPredicateInt; import common.IterableBitSet; import common.IterableStateSet; +import common.iterable.FunctionalPrimitiveIterable; import common.iterable.Reducible; import explicit.BasicModelTransformation; import explicit.MDP; @@ -142,7 +143,7 @@ public int getNumInitialStates() } @Override - public Iterable getInitialStates() + public FunctionalPrimitiveIterable.OfInt getInitialStates() { return model.getInitialStates(); } diff --git a/prism/src/explicit/modelviews/MDPFromDTMC.java b/prism/src/explicit/modelviews/MDPFromDTMC.java index dc2e980719..bc8a164143 100644 --- a/prism/src/explicit/modelviews/MDPFromDTMC.java +++ b/prism/src/explicit/modelviews/MDPFromDTMC.java @@ -27,12 +27,11 @@ package explicit.modelviews; -import java.util.BitSet; -import java.util.Iterator; -import java.util.List; +import java.util.*; import java.util.Map.Entry; -import java.util.Set; +import common.iterable.FunctionalPrimitiveIterable; +import common.iterable.FunctionalPrimitiveIterator; import explicit.DTMC; import explicit.DTMCSimple; import explicit.MDP; @@ -89,7 +88,7 @@ public int getNumInitialStates() } @Override - public Iterable getInitialStates() + public FunctionalPrimitiveIterable.OfInt getInitialStates() { return model.getInitialStates(); } @@ -144,7 +143,7 @@ public boolean hasLabel(String name) @Override - public Iterator getSuccessorsIterator(final int state) + public FunctionalPrimitiveIterator.OfInt getSuccessorsIterator(final int state) { return model.getSuccessorsIterator(state); }