diff --git a/prism/src/automata/LTSFromDA.java b/prism/src/automata/LTSFromDA.java index 6fd466c4..58cca064 100644 --- a/prism/src/automata/LTSFromDA.java +++ b/prism/src/automata/LTSFromDA.java @@ -27,10 +27,6 @@ package automata; import java.util.BitSet; -import java.util.Collections; -import java.util.HashSet; -import java.util.Iterator; -import java.util.Set; import prism.ModelType; import prism.PrismException; @@ -39,6 +35,7 @@ import strat.MDStrategy; import explicit.LTS; import explicit.Model; import explicit.ModelExplicit; +import explicit.SuccessorsIterator; /** * Class giving access to the labelled transition system (LTS) underlying a deterministic automaton (DA). @@ -58,38 +55,30 @@ public class LTSFromDA extends ModelExplicit implements LTS // Methods to implement Model @Override - public Iterator getSuccessorsIterator(int s) + public SuccessorsIterator getSuccessors(int s) { - Set succs = new HashSet(); - int n = da.getNumEdges(s); - for (int i = 0; i < n; i++) { - succs.add(da.getEdgeDest(s, i)); - } - return succs.iterator(); - } + return new SuccessorsIterator() { + private int n = da.getNumEdges(s); + private int i = 0; - @Override - public boolean allSuccessorsInSet(int s, BitSet set) - { - int n = da.getNumEdges(s); - for (int i = 0; i < n; i++) { - if (!set.get(da.getEdgeDest(s, i))) { + @Override + public boolean successorsAreDistinct() + { return false; } - } - return true; - } - @Override - public boolean someSuccessorsInSet(int s, BitSet set) - { - int n = da.getNumEdges(s); - for (int i = 0; i < n; i++) { - if (set.get(da.getEdgeDest(s, i))) { - return true; + @Override + public boolean hasNext() + { + return i < n; } - } - return false; + + @Override + public int nextInt() + { + return da.getEdgeDest(s, i++); + } + }; } @Override @@ -213,9 +202,9 @@ public class LTSFromDA extends ModelExplicit implements LTS } @Override - public Iterator getSuccessorsIterator(int s, int i) + public SuccessorsIterator getSuccessors(int s, int i) { - return Collections.singleton(da.getEdgeDest(s, i)).iterator(); + return SuccessorsIterator.fromSingleton(da.getEdgeDest(s, i)); } @Override diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index ec16e713..4a7c62da 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/prism/src/explicit/DTMCEmbeddedSimple.java @@ -129,31 +129,14 @@ public class DTMCEmbeddedSimple extends DTMCExplicit } @Override - public Iterator getSuccessorsIterator(final int s) + public SuccessorsIterator getSuccessors(final int s) { if (exitRates[s] == 0) { - List list = new ArrayList(1); - list.add(s); - return list.iterator(); + return SuccessorsIterator.fromSingleton(s); } else { - return ctmc.getSuccessorsIterator(s); + return ctmc.getSuccessors(s); } } - - public boolean isSuccessor(int s1, int s2) - { - return exitRates[s1] == 0 ? (s1 == s2) : ctmc.isSuccessor(s1, s2); - } - - public boolean allSuccessorsInSet(int s, BitSet set) - { - return exitRates[s] == 0 ? set.get(s) : ctmc.allSuccessorsInSet(s, set); - } - - public boolean someSuccessorsInSet(int s, BitSet set) - { - return exitRates[s] == 0 ? set.get(s) : ctmc.someSuccessorsInSet(s, set); - } public int getNumChoices(int s) { diff --git a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java index cb0ca2c7..d0c48ad2 100644 --- a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java +++ b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java @@ -122,24 +122,9 @@ public class DTMCFromMDPAndMDStrategy extends DTMCExplicit return numTransitions; } - public Iterator getSuccessorsIterator(final int s) + public SuccessorsIterator getSuccessors(final int s) { - return mdp.getSuccessorsIterator(s, strat.getChoiceIndex(s)); - } - - public boolean isSuccessor(int s1, int s2) - { - throw new RuntimeException("Not implemented yet"); - } - - public boolean allSuccessorsInSet(int s, BitSet set) - { - return mdp.allSuccessorsInSet(s, strat.getChoiceIndex(s), set); - } - - public boolean someSuccessorsInSet(int s, BitSet set) - { - return mdp.someSuccessorsInSet(s, strat.getChoiceIndex(s), set); + return mdp.getSuccessors(s, strat.getChoiceIndex(s)); } public int getNumChoices(int s) diff --git a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java index d1bd2b2e..6c011199 100644 --- a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java +++ b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java @@ -124,24 +124,13 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit return numTransitions; } - public Iterator getSuccessorsIterator(final int s) + public SuccessorsIterator getSuccessors(final int s) { - throw new RuntimeException("Not implemented yet"); - } - - public boolean isSuccessor(int s1, int s2) - { - throw new RuntimeException("Not implemented yet"); - } - - public boolean allSuccessorsInSet(int s, BitSet set) - { - throw new RuntimeException("Not implemented yet"); - } - - public boolean someSuccessorsInSet(int s, BitSet set) - { - throw new RuntimeException("Not implemented yet"); + if (adv[s] >= 0) { + return mdp.getSuccessors(s, adv[s]); + } else { + return SuccessorsIterator.empty(); + } } public int getNumChoices(int s) diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index 017314b6..19d9c4c8 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -208,12 +208,19 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple return numTransitions; } + /** Get an iterator over the successors of state s */ @Override public Iterator getSuccessorsIterator(final int s) { return trans.get(s).getSupport().iterator(); } + @Override + public SuccessorsIterator getSuccessors(int s) + { + return SuccessorsIterator.from(getSuccessorsIterator(s), true); + } + @Override public boolean isSuccessor(int s1, int s2) { diff --git a/prism/src/explicit/DTMCUniformisedSimple.java b/prism/src/explicit/DTMCUniformisedSimple.java index 86bc8d3f..62be8c84 100644 --- a/prism/src/explicit/DTMCUniformisedSimple.java +++ b/prism/src/explicit/DTMCUniformisedSimple.java @@ -134,25 +134,7 @@ public class DTMCUniformisedSimple extends DTMCExplicit return ctmc.getNumTransitions() + numExtraTransitions; } - public Iterator getSuccessorsIterator(final int s) - { - // TODO - throw new Error("Not yet supported"); - } - - public boolean isSuccessor(int s1, int s2) - { - // TODO - throw new Error("Not yet supported"); - } - - public boolean allSuccessorsInSet(int s, BitSet set) - { - // TODO - throw new Error("Not yet supported"); - } - - public boolean someSuccessorsInSet(int s, BitSet set) + public SuccessorsIterator getSuccessors(final int s) { // TODO throw new Error("Not yet supported"); diff --git a/prism/src/explicit/LTSExplicit.java b/prism/src/explicit/LTSExplicit.java index aa6da40f..7e006a43 100644 --- a/prism/src/explicit/LTSExplicit.java +++ b/prism/src/explicit/LTSExplicit.java @@ -131,10 +131,10 @@ public class LTSExplicit extends ModelExplicit implements LTS } @Override - public Iterator getSuccessorsIterator(int s, int i) + public SuccessorsIterator getSuccessors(int s, int i) { // single successor for s, i - return Collections.singletonList(successors.get(s).get(i)).iterator(); + return SuccessorsIterator.fromSingleton(successors.get(s).get(i)); } @Override @@ -150,30 +150,9 @@ public class LTSExplicit extends ModelExplicit implements LTS } @Override - public Iterator getSuccessorsIterator(int s) + public SuccessorsIterator getSuccessors(int s) { - // make successors unique - LinkedHashSet succ = new LinkedHashSet(); - succ.addAll(successors.get(s)); - return succ.iterator(); - } - - @Override - public boolean allSuccessorsInSet(int s, BitSet set) - { - for (int t : successors.get(s)) { - if (!set.get(t)) return false; - } - return true; - } - - @Override - public boolean someSuccessorsInSet(int s, BitSet set) - { - for (int t : successors.get(s)) { - if (set.get(t)) return true; - } - return false; + return SuccessorsIterator.from(successors.get(s).iterator(), false); } @Override @@ -200,15 +179,6 @@ public class LTSExplicit extends ModelExplicit implements LTS return numTransitions; } - @Override - public boolean isSuccessor(int s1, int s2) - { - for (Iterator it = getSuccessorsIterator(s1); it.hasNext(); ) { - if (it.next() == s2) return true; - } - return false; - } - @Override public void checkForDeadlocks(BitSet except) throws PrismException { diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index a80e48c3..5669ff0d 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -33,7 +33,6 @@ 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; @@ -476,48 +475,6 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple return numTransitions; } - @Override - public Iterator 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 (Distribution distr : trans.get(s)) { - succs.addAll(distr.getSupport()); - } - return succs.iterator(); - } - - @Override - public boolean isSuccessor(int s1, int s2) - { - for (Distribution distr : trans.get(s1)) { - if (distr.contains(s2)) - return true; - } - return false; - } - - @Override - public boolean allSuccessorsInSet(int s, BitSet set) - { - for (Distribution distr : trans.get(s)) { - if (!distr.isSubsetOf(set)) - return false; - } - return true; - } - - @Override - public boolean someSuccessorsInSet(int s, BitSet set) - { - for (Distribution distr : trans.get(s)) { - if (distr.containsOneOf(set)) - return true; - } - return false; - } - @Override public void findDeadlocks(boolean fix) throws PrismException { @@ -596,6 +553,12 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple return trans.get(s).get(i).getSupport().iterator(); } + @Override + public SuccessorsIterator getSuccessors(final int s, final int i) + { + return SuccessorsIterator.from(getSuccessorsIterator(s, i), true); + } + // Accessors (for MDP) @Override diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index e2d12556..1b0fc6f1 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -33,7 +33,6 @@ 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; @@ -384,75 +383,40 @@ public class MDPSparse extends MDPExplicit return numTransitions; } - @Override - public Iterator getSuccessorsIterator(final int s) + private SuccessorsIterator colsIterator(int start, int end, boolean distinct) { - // Need to build set to avoid duplicates - // So not necessarily the fastest method to access successors - int start = choiceStarts[rowStarts[s]]; - int end = choiceStarts[rowStarts[s + 1]]; - HashSet succs = new HashSet(); - for (int i = start; i < end; i++) { - succs.add(cols[i]); - } - return succs.iterator(); - } + return new SuccessorsIterator() { + int cur = start; - @Override - public boolean isSuccessor(int s1, int s2) - { - int j, k, l1, h1, l2, h2; - l1 = rowStarts[s1]; - h1 = rowStarts[s1 + 1]; - for (j = l1; j < h1; j++) { - l2 = choiceStarts[j]; - h2 = choiceStarts[j + 1]; - for (k = l2; k < h2; k++) { - // Assume that only non-zero entries are stored - if (cols[k] == s2) { - return true; - } + @Override + public boolean successorsAreDistinct() + { + return distinct; } - } - return false; - } - @Override - public boolean allSuccessorsInSet(int s, BitSet set) - { - int j, k, l1, h1, l2, h2; - l1 = rowStarts[s]; - h1 = rowStarts[s + 1]; - for (j = l1; j < h1; j++) { - l2 = choiceStarts[j]; - h2 = choiceStarts[j + 1]; - for (k = l2; k < h2; k++) { - // Assume that only non-zero entries are stored - if (!set.get(cols[k])) { - return false; - } + @Override + public boolean hasNext() + { + return cur < end; } - } - return true; + + @Override + public int nextInt() + { + return cols[cur++]; + } + }; } @Override - public boolean someSuccessorsInSet(int s, BitSet set) + public SuccessorsIterator getSuccessors(final int s) { - int j, k, l1, h1, l2, h2; - l1 = rowStarts[s]; - h1 = rowStarts[s + 1]; - for (j = l1; j < h1; j++) { - l2 = choiceStarts[j]; - h2 = choiceStarts[j + 1]; - for (k = l2; k < h2; k++) { - // Assume that only non-zero entries are stored - if (set.get(cols[k])) { - return true; - } - } - } - return false; + // Assumes that only non-zero entries are stored + int start = choiceStarts[rowStarts[s]]; + int end = choiceStarts[rowStarts[s + 1]]; + // we can guarantee that the successors are distinct if there is at most one successor... + boolean distinct = (start == end || start + 1 == end); + return colsIterator(start, end, distinct); } @Override @@ -505,47 +469,12 @@ public class MDPSparse extends MDPExplicit } @Override - public boolean allSuccessorsInSet(int s, int i, BitSet set) - { - int j, k, l2, h2; - j = rowStarts[s] + i; - l2 = choiceStarts[j]; - h2 = choiceStarts[j + 1]; - for (k = l2; k < h2; k++) { - // Assume that only non-zero entries are stored - if (!set.get(cols[k])) { - return false; - } - } - return true; - } - - @Override - public boolean someSuccessorsInSet(int s, int i, BitSet set) - { - int j, k, l2, h2; - j = rowStarts[s] + i; - l2 = choiceStarts[j]; - h2 = choiceStarts[j + 1]; - for (k = l2; k < h2; k++) { - // Assume that only non-zero entries are stored - if (set.get(cols[k])) { - return true; - } - } - return false; - } - - @Override - public Iterator getSuccessorsIterator(final int s, final int i) + public SuccessorsIterator getSuccessors(final int s, final int i) { int start = choiceStarts[rowStarts[s] + i]; int end = choiceStarts[rowStarts[s] + i + 1]; - List succs = new ArrayList(); - for (int j = start; j < end; j++) { - succs.add(cols[j]); - } - return succs.iterator(); + // we assume here that the successors for a single choice are distinct + return colsIterator(start, end, true); } // Accessors (for MDP) diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index fc93f99a..3450d59c 100644 --- a/prism/src/explicit/Model.java +++ b/prism/src/explicit/Model.java @@ -31,6 +31,7 @@ import java.util.BitSet; import java.util.Iterator; import java.util.List; import java.util.Set; +import java.util.function.IntPredicate; import parser.State; import parser.Values; @@ -144,27 +145,103 @@ public interface Model /** * Get an iterator over the successors of state s. + * Default implementation via the SuccessorsIterator returned + * from {@code getSuccessors}, ensuring that there are no + * duplicates. */ - public Iterator getSuccessorsIterator(int s); - + public default Iterator getSuccessorsIterator(int s) + { + SuccessorsIterator successors = getSuccessors(s); + return successors.distinct(); + } + + /** + * Get a SuccessorsIterator for state s. + */ + public SuccessorsIterator getSuccessors(int s); + /** * Returns true if state s2 is a successor of state s1. */ - public boolean isSuccessor(int s1, int s2); + public default boolean isSuccessor(int s1, int s2) + { + // the code for this method is equivalent to the following stream expression, + // but kept explicit for performance + // + // return getSuccessors(s1).stream().anyMatch( + // (t) -> {return t == s2;} + // ); + + SuccessorsIterator it = getSuccessors(s1); + while (it.hasNext()) { + int t = it.nextInt(); + if (t == s2) + return true; + } + return false; + } /** * Check if all the successor states of a state are in a set. * @param s The state to check * @param set The set to test for inclusion */ - public boolean allSuccessorsInSet(int s, BitSet set); + public default boolean allSuccessorsInSet(int s, BitSet set) + { + return allSuccessorsMatch(s, set::get); + } /** * Check if any successor states of a state are in a set. * @param s The state to check * @param set The set to test for inclusion */ - public boolean someSuccessorsInSet(int s, BitSet set); + public default boolean someSuccessorsInSet(int s, BitSet set) + { + return someSuccessorsMatch(s, set::get); + } + + /** + * Check if all the successor states of a state match the predicate. + * @param s The state to check + * @param p the predicate + */ + public default boolean allSuccessorsMatch(int s, IntPredicate p) + { + // the code for this method is equivalent to the following stream expression, + // but kept explicit for performance + // + // return getSuccessors(s).stream().allMatch(p); + + SuccessorsIterator it = getSuccessors(s); + while (it.hasNext()) { + int t = it.nextInt(); + if (!p.test(t)) + return false; + } + return true; + } + + /** + * Check if any successor states of a state match the predicate. + * @param s The state to check + * @param p the predicate + */ + public default boolean someSuccessorsMatch(int s, IntPredicate p) + { + // the code for this method is equivalent to the following stream expression, + // but kept explicit for performance + // + // return getSuccessors(s).stream().anyMatch(p); + + SuccessorsIterator it = getSuccessors(s); + while (it.hasNext()) { + int t = it.nextInt(); + if (p.test(t)) + return true; + } + return false; + } /** * Find all deadlock states and store this information in the model. diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java index f62db21e..5f354aa6 100644 --- a/prism/src/explicit/ModelExplicit.java +++ b/prism/src/explicit/ModelExplicit.java @@ -355,9 +355,6 @@ public abstract class ModelExplicit implements Model @Override public abstract int getNumTransitions(); - @Override - public abstract boolean isSuccessor(int s1, int s2); - @Override public void checkForDeadlocks() throws PrismException { diff --git a/prism/src/explicit/NondetModel.java b/prism/src/explicit/NondetModel.java index 44758269..a9abb9fc 100644 --- a/prism/src/explicit/NondetModel.java +++ b/prism/src/explicit/NondetModel.java @@ -28,6 +28,7 @@ package explicit; import java.util.BitSet; import java.util.Iterator; +import java.util.function.IntPredicate; import prism.PrismLog; import strat.MDStrategy; @@ -75,7 +76,10 @@ public interface NondetModel extends Model * @param i Choice index * @param set The set to test for inclusion */ - public boolean allSuccessorsInSet(int s, int i, BitSet set); + public default boolean allSuccessorsInSet(int s, int i, BitSet set) + { + return allSuccessorsMatch(s, i, set::get); + } /** * Check if some successor state from choice {@code i} of state {@code s} is in the set {@code set}. @@ -83,15 +87,94 @@ public interface NondetModel extends Model * @param i Choice index * @param set The set to test for inclusion */ - public boolean someSuccessorsInSet(int s, int i, BitSet set); - + public default boolean someSuccessorsInSet(int s, int i, BitSet set) + { + return someSuccessorsMatch(s, i, set::get); + } + + /** + * Check if all the successor states from choice {@code i} of state {@code s} match the predicate. + * @param s The state to check + * @param i Choice index + * @param p The predicate + */ + public default boolean allSuccessorsMatch(int s, int i, IntPredicate p) + { + // the code for this method is equivalent to the following stream expression, + // but kept explicit for performance + // + // return getSuccessors(s,i).stream().allMatch(p); + + SuccessorsIterator it = getSuccessors(s,i); + while (it.hasNext()) { + int t = it.nextInt(); + if (!p.test(t)) + return false; + } + return true; + } + + /** + * Check if some successor state from choice {@code i} of state {@code s} match the predicate. + * @param s The state to check + * @param i Choice index + * @param p The predicate + */ + public default boolean someSuccessorsMatch(int s, int i, IntPredicate p) + { + // the code for this method is equivalent to the following stream expression, + // but kept explicit for performance + // + // return getSuccessors(s,i).stream().anyMatch(p); + + SuccessorsIterator it = getSuccessors(s, i); + while (it.hasNext()) { + int t = it.nextInt(); + if (p.test(t)) + return true; + } + return false; + } + /** * Get an iterator over the successor states from choice {@code i} of state {@code s}. * @param s The state * @param i Choice index */ - public Iterator getSuccessorsIterator(int s, int i); - + public default Iterator getSuccessorsIterator(int s, int i) + { + SuccessorsIterator successors = getSuccessors(s, i); + return successors.distinct(); + } + + /** + * Get a SuccessorsIterator for state s and choice i. + * @param s The state + * @param i Choice index + */ + public SuccessorsIterator getSuccessors(int s, int i); + + @Override + public default SuccessorsIterator getSuccessors(final int s) + { + return SuccessorsIterator.chain(new Iterator() { + private int choice = 0; + private int choices = getNumChoices(s); + + @Override + public boolean hasNext() + { + return choice < choices; + } + + @Override + public SuccessorsIterator next() + { + return getSuccessors(s, choice++); + } + }); + } + /** * Construct a model that is induced by applying strategy {@code strat} to this model. * Note that the "new" model may be just an implicit (read-only) representation. diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index 1d9ce338..b8d9c0eb 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -499,17 +499,26 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS { return trans.get(s).get(i).containsOneOf(set); } - + @Override - public Iterator getSuccessorsIterator(final int s, final int i) + public SuccessorsIterator getSuccessors(final int s, final int i) { - // Need to build set to avoid duplicates - // So not necessarily the fastest method to access successors - HashSet succs = new HashSet(); - for (Distribution distr : trans.get(s).get(i)) { - succs.addAll(distr.getSupport()); - } - return succs.iterator(); + return SuccessorsIterator.chain(new Iterator() { + private Iterator iterator = trans.get(s).get(i).iterator(); + + @Override + public boolean hasNext() + { + return iterator.hasNext(); + } + + @Override + public SuccessorsIterator next() + { + Distribution dist = iterator.next(); + return SuccessorsIterator.from(dist.getSupport().iterator(), true); + } + }); } // Accessors (for STPG) diff --git a/prism/src/explicit/SubNondetModel.java b/prism/src/explicit/SubNondetModel.java index 7cfd2ce2..929248b4 100644 --- a/prism/src/explicit/SubNondetModel.java +++ b/prism/src/explicit/SubNondetModel.java @@ -36,6 +36,7 @@ import java.util.Iterator; import java.util.List; import java.util.Map; import java.util.Set; +import java.util.function.IntConsumer; import common.IterableStateSet; import parser.State; @@ -210,55 +211,6 @@ public class SubNondetModel implements NondetModel return numTransitions; } - @Override - public Iterator getSuccessorsIterator(int s) - { - s = translateState(s); - HashSet succs = new HashSet(); - for (int i : new IterableStateSet(actions.get(s), model.getNumChoices(s))){ - Iterator it = model.getSuccessorsIterator(s, i); - while (it.hasNext()) { - int j = it.next(); - succs.add(inverseTranslateState(j)); - } - } - return succs.iterator(); - } - - @Override - public boolean isSuccessor(int s1, int s2) - { - s1 = translateState(s1); - s2 = translateState(s2); - return model.isSuccessor(s1, s2); - } - - @Override - public boolean allSuccessorsInSet(int s, BitSet set) - { - Iterator successors = getSuccessorsIterator(s); - while (successors.hasNext()) { - Integer successor = successors.next(); - if (!set.get(successor)) { - return false; - } - } - return true; - } - - @Override - public boolean someSuccessorsInSet(int s, BitSet set) - { - Iterator successors = getSuccessorsIterator(s); - while (successors.hasNext()) { - Integer successor = successors.next(); - if (set.get(successor)) { - return true; - } - } - return false; - } - @Override public void findDeadlocks(boolean fix) throws PrismException { @@ -402,45 +354,35 @@ public class SubNondetModel implements NondetModel int iOriginal = translateAction(s, i); return model.getNumTransitions(sOriginal, iOriginal); } - + @Override - public boolean allSuccessorsInSet(int s, int i, BitSet set) + public SuccessorsIterator getSuccessors(int s, int i) { - Iterator successors = getSuccessorsIterator(s, i); - while (successors.hasNext()) { - Integer successor = successors.next(); - if (!set.get(successor)) { - return false; + int sOriginal = translateState(s); + int iOriginal = translateAction(s, i); + + SuccessorsIterator it = model.getSuccessors(sOriginal, iOriginal); + return new SuccessorsIterator() { + + @Override + public boolean successorsAreDistinct() + { + return it.successorsAreDistinct(); } - } - return true; - } - @Override - public boolean someSuccessorsInSet(int s, int i, BitSet set) - { - Iterator successors = getSuccessorsIterator(s, i); - while (successors.hasNext()) { - Integer successor = successors.next(); - if (set.get(successor)) { - return true; + @Override + public boolean hasNext() + { + return it.hasNext(); } - } - return false; - } - @Override - public Iterator getSuccessorsIterator(int s, int i) - { - int sOriginal = translateState(s); - int iOriginal = translateAction(s, i); - List succ = new ArrayList(); - Iterator it = model.getSuccessorsIterator(sOriginal, iOriginal); - while (it.hasNext()) { - int j = it.next(); - succ.add(inverseTranslateState(j)); - } - return succ.iterator(); + @Override + public int nextInt() + { + return inverseTranslateState(it.next()); + } + + }; } private BitSet translateSet(BitSet set) diff --git a/prism/src/explicit/SuccessorsIterator.java b/prism/src/explicit/SuccessorsIterator.java new file mode 100644 index 00000000..1751e981 --- /dev/null +++ b/prism/src/explicit/SuccessorsIterator.java @@ -0,0 +1,264 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * 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; + +import java.util.Iterator; +import java.util.NoSuchElementException; +import java.util.PrimitiveIterator; +import java.util.Spliterator; +import java.util.Spliterators; +import java.util.stream.IntStream; +import java.util.stream.StreamSupport; + +import common.iterable.FilteringIterator; +import common.iterable.SingletonIterator; + +/** + * Base class and static helpers for iterators over successor states. + *
+ * Carries information whether the successors are known to be distinct + * and helpers to ensure that this is the case, i.e., allowing iteration + * 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 +{ + /** Is it guaranteed that every successor will occur only once? */ + public abstract boolean successorsAreDistinct(); + + @Override + public abstract boolean hasNext(); + + @Override + public abstract int nextInt(); + + /** + * Return a SuccessorsIterator that guarantees that there + * are no duplicates in the successor states, i.e., iterating + * over the set of successors instead of a multiset. + *
+ * The iterator this method is called on can not be used afterwards, + * only the returned iterator. + */ + public SuccessorsIterator distinct() + { + if (successorsAreDistinct()) { + return this; + } else { + return new SuccessorsIteratorFromOfInt(FilteringIterator.dedupe(this), true); + } + } + + /** Provide an IntStream */ + public IntStream stream() + { + return StreamSupport.intStream( + Spliterators.spliteratorUnknownSize(this, successorsAreDistinct() ? Spliterator.DISTINCT : 0), + false); + } + + /** Wrapper, underlying iterator is an OfInt iterator */ + private static class SuccessorsIteratorFromOfInt extends SuccessorsIterator { + private java.util.PrimitiveIterator.OfInt it; + private boolean distinct; + + public SuccessorsIteratorFromOfInt(PrimitiveIterator.OfInt it, boolean distinct) + { + this.it = it; + this.distinct = distinct; + } + + @Override + public boolean successorsAreDistinct() + { + return distinct; + } + + @Override + public boolean hasNext() + { + return it.hasNext(); + } + + @Override + public int nextInt() + { + return it.nextInt(); + } + } + + /** Wrapper, underlying iterator is an Iterator iterator */ + private static class SuccessorsIteratorFromIterator extends SuccessorsIterator { + private Iterator it; + private boolean distinct; + + public SuccessorsIteratorFromIterator(Iterator it, boolean distinct) + { + this.it = it; + this.distinct = distinct; + } + + @Override + public boolean hasNext() + { + return it.hasNext(); + } + + @Override + public Integer next() + { + return it.next(); + } + + @Override + public int nextInt() + { + return it.next(); + } + + @Override + public boolean successorsAreDistinct() + { + return distinct; + } + }; + + /** Helper, empty iterator */ + private static class SuccessorsIteratorEmpty extends SuccessorsIterator { + @Override + public boolean hasNext() + { + return false; + } + + @Override + public int nextInt() + { + throw new NoSuchElementException(); + } + + @Override + public boolean successorsAreDistinct() + { + return true; + } + }; + + /** Helper, chain multiple SuccessorsIterators */ + private static class ChainedSuccessorsIterator extends SuccessorsIterator { + private Iterator iterators; + private SuccessorsIterator current; + private 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(); + } else { + // can not guarantee that successors are distinct + distinct = false; + } + } + + @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; + } + + @Override + public int nextInt() + { + if (!hasNext()) { + throw new NoSuchElementException(); + } + return current.nextInt(); + } + + @Override + public boolean successorsAreDistinct() + { + return distinct; + } + }; + + /** Obtain a SuccessorsIterator with the given distinctness guarantee from an Iterator */ + public static SuccessorsIterator from(Iterator it, boolean 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) + { + return new SuccessorsIteratorFromOfInt(new SingletonIterator.OfInt(i), true); + } + + /** Obtain an empty SuccessorsIterator */ + public static SuccessorsIterator empty() + { + return new SuccessorsIteratorEmpty(); + } + + /** Obtain a SuccessorsIterator, chaining multiple SuccessorsIterators one after the other */ + public static SuccessorsIterator chain(Iterator iterators) + { + return new ChainedSuccessorsIterator(iterators); + } +} diff --git a/prism/src/param/ParamModel.java b/prism/src/param/ParamModel.java index 0a5b8d84..56df56ac 100644 --- a/prism/src/param/ParamModel.java +++ b/prism/src/param/ParamModel.java @@ -38,6 +38,7 @@ import prism.ModelType; import prism.PrismException; import prism.PrismLog; import explicit.ModelExplicit; +import explicit.SuccessorsIterator; /** * Represents a parametric Markov model. @@ -112,7 +113,7 @@ public final class ParamModel extends ModelExplicit } @Override - public Iterator getSuccessorsIterator(int s) + public SuccessorsIterator getSuccessors(int s) { throw new UnsupportedOperationException(); } @@ -130,18 +131,6 @@ public final class ParamModel extends ModelExplicit return false; } - @Override - public boolean allSuccessorsInSet(int s, BitSet set) - { - throw new UnsupportedOperationException(); - } - - @Override - public boolean someSuccessorsInSet(int s, BitSet set) - { - throw new UnsupportedOperationException(); - } - /** * Get an iterator over the transitions from choice {@code i} of state {@code s}. *