Browse Source
refactor explicit.Model/NondetModel, getSuccessorsIterator: new abstract method getSuccessors, getSuccessorsIterator becomes default method
refactor explicit.Model/NondetModel, getSuccessorsIterator: new abstract method getSuccessors, getSuccessorsIterator becomes default method
The getSuccessorsIterator provides an iterator over the set of successors, i.e., deduplication is sometimes required (e.g. for MDPs). We introduce here a SuccessorsIterator class that allows to make deduplication optional, which may have benefits in performance. Additionally, SuccessorsIterator implements a primitive OfInt iterator, which can avoid auto-boxing. Subclasses of explicit.Model now have to provide an implementation for getSuccessors(int s), getSuccessorsIterator(int s) is provided via a default method that automatically requests deduplication. Subclasses of explicit.NondetModel now have to provide an implementation for getSuccessors(int s, int)., getSuccessorsIterator(int s, int i) is provided via a default method that automatically requests deduplication. Adapt the existing subclasses of explicit.Model. Provides additional default methods and removes unneeded specializations in sub-classes: boolean isSuccessor(int s1, int s2) boolean allSuccessorsInSet(int s, BitSet set) boolean someSuccessorsInSet(int s, BitSet set) boolean allSuccessorsMatch(int s, IntPredicate p) boolean someSuccessorsMatch(int s, IntPredicate p) and for NondetModel: boolean allSuccessorsInSet(int s, int i, BitSet set) boolean someSuccessorsInSet(int s, int i, BitSet set) boolean allSuccessorsMatch(int s, int i, IntPredicate p) boolean someSuccessorsMatch(int s, int i, IntPredicate p) git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12085 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Joachim Klein
9 years ago
16 changed files with 556 additions and 398 deletions
-
53prism/src/automata/LTSFromDA.java
-
23prism/src/explicit/DTMCEmbeddedSimple.java
-
19prism/src/explicit/DTMCFromMDPAndMDStrategy.java
-
23prism/src/explicit/DTMCFromMDPMemorylessAdversary.java
-
7prism/src/explicit/DTMCSimple.java
-
20prism/src/explicit/DTMCUniformisedSimple.java
-
38prism/src/explicit/LTSExplicit.java
-
49prism/src/explicit/MDPSimple.java
-
127prism/src/explicit/MDPSparse.java
-
87prism/src/explicit/Model.java
-
3prism/src/explicit/ModelExplicit.java
-
93prism/src/explicit/NondetModel.java
-
27prism/src/explicit/STPGAbstrSimple.java
-
106prism/src/explicit/SubNondetModel.java
-
264prism/src/explicit/SuccessorsIterator.java
-
15prism/src/param/ParamModel.java
@ -0,0 +1,264 @@ |
|||
//============================================================================== |
|||
// |
|||
// Copyright (c) 2016- |
|||
// Authors: |
|||
// * Joachim Klein <klein@tcs.inf.tu-dresden.de> (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. |
|||
* <br> |
|||
* 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. |
|||
* <br> |
|||
* 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<Integer> iterator */ |
|||
private static class SuccessorsIteratorFromIterator extends SuccessorsIterator { |
|||
private Iterator<Integer> it; |
|||
private boolean distinct; |
|||
|
|||
public SuccessorsIteratorFromIterator(Iterator<Integer> 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<SuccessorsIterator> iterators; |
|||
private SuccessorsIterator current; |
|||
private boolean distinct; |
|||
|
|||
public ChainedSuccessorsIterator(Iterator<SuccessorsIterator> 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<Integer> */ |
|||
public static SuccessorsIterator from(Iterator<Integer> 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<SuccessorsIterator> iterators) |
|||
{ |
|||
return new ChainedSuccessorsIterator(iterators); |
|||
} |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue