s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

New common.IterableBitSet and common.IterableStateSet classes [Joachim Klein]. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9542 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
280bb04868
commit
95feea13ce
2 changed files with 367 additions and 0 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 184
      prism/src/common/IterableBitSet.java
  2. 183
      prism/src/common/IterableStateSet.java

184
prism/src/common/IterableBitSet.java
View File

@ -0,0 +1,184 @@
//==============================================================================
//
// Copyright (c) 2014-
// Authors:
// * Steffen Maercker <maercker@tcs.inf.tu-dresden.de> (TU Dresden)
// * 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 common;
import java.util.BitSet;
import java.util.Iterator;
import java.util.NoSuchElementException;
/**
* Convenience class to loop easily over the set/clear bits of a BitSet.
*
* For example:<br/><br/>
* <code>for (Integer index : getSetBits(set)) { ... }</code><br/>
*/
public class IterableBitSet implements Iterable<Integer>
{
private BitSet set;
private boolean clearBits = false;
private Integer maxIndex = null;
/**
* Constructor for an Iterable that iterates over the set bits of {@code set}
*/
public IterableBitSet(BitSet set)
{
this.set = set;
this.clearBits = false;
}
/**
* Constructor for an Iterable that iterates over bits of the given set {@code set},
* up to the maximal index given by {@code maxIndex}. If {@code clearBits} is {@code true},
* iterate over the cleared bits instead of the set bits.
* @param set the underlying BitSet
* @param maxIndex the maximal index for iteration (negative = iterate over the empty set)
* @param clearBits if true, iterate over the cleared bits in the BitSet
*/
public IterableBitSet(BitSet set, int maxIndex, boolean clearBits)
{
this.set = set;
this.maxIndex = maxIndex;
this.clearBits = clearBits;
}
/** Implementation of the iterator over the set bits */
private class SetBitsIterator implements Iterator<Integer> {
private int index = set.nextSetBit(0);
@Override
public boolean hasNext() {
if (maxIndex != null && index > maxIndex) {
// limit to 0 ... maxIndex
return false;
}
return index >= 0;
}
@Override
public Integer next() {
if (hasNext()) {
Integer next = index;
index = set.nextSetBit(index + 1);
return next;
}
throw new NoSuchElementException();
}
@Override
public void remove() {
throw new UnsupportedOperationException();
}
}
/** Implementation of the iterator over the cleared bits, requires that {@code maxIndex != null} */
private class ClearBitsIterator implements Iterator<Integer> {
private int index = set.nextClearBit(0);
@Override
public boolean hasNext() {
if (index > maxIndex) {
// limit to 0 ... maxIndex
return false;
}
return true;
}
@Override
public Integer next() {
if (hasNext()) {
Integer next = index;
index = set.nextClearBit(index + 1);
return next;
}
throw new NoSuchElementException();
}
@Override
public void remove() {
throw new UnsupportedOperationException();
}
}
@Override
public Iterator<Integer> iterator() {
if (clearBits == false) {
return new SetBitsIterator();
} else {
return new ClearBitsIterator();
}
}
/**
* Get an IterableBitSet that iterates over the bits of {@code set} that are set.
* @param set a BitSet
* @return an IterableBitSet over the set bits
*/
public static IterableBitSet getSetBits(BitSet set)
{
return new IterableBitSet(set);
}
/**
* Get an IterableBitSet that iterates over the cleared bits of {@code set}, up to {@code maxIndex}
* @param set a BitSet
* @param maxIndex the maximal index
* @return an IterableBitSet over the cleared bits
*/
public static IterableBitSet getClearBits(BitSet set, int maxIndex)
{
return new IterableBitSet(set, maxIndex, true);
}
/**
* Simple test method.
*
* @param args ignored
*/
public static void main(String[] args)
{
BitSet test = new BitSet();
test.set(1);
test.set(2);
test.set(3);
test.set(5);
test.set(8);
test.set(13);
test.set(21);
System.out.println("\n" + test + " - set bits:");
for (Integer index : getSetBits(test)) {
System.out.println(index);
}
test.clear();
for (@SuppressWarnings("unused") Integer index : getSetBits(test)) {
throw new RuntimeException("BitSet should be empty!");
}
}
}

183
prism/src/common/IterableStateSet.java
View File

@ -0,0 +1,183 @@
//==============================================================================
//
// Copyright (c) 2014-
// 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 common;
import java.util.BitSet;
import java.util.Iterator;
import java.util.NoSuchElementException;
/**
* A convenience wrapper around IterableBitSet that handles the three cases of
* iterating over the set or cleared bits of a BitSet representing a set of states
* as well as iterating over all states if the BitSet is {@code null}.
*/
public class IterableStateSet implements Iterable<Integer> {
private BitSet setOfStates;
private Integer numStates = null;
private boolean complement = false;
/**
* Constructor (iterate over all states 0..numStates-1)
*
* @param numStates the number of states in the model, i.e., with indizes 0..numStates-1
*/
public IterableStateSet(int numStates)
{
this(null, numStates, false);
}
/**
* Constructor (iterate over the sets given by setOfStates or over all states)
*
* @param setOfStates the BitSet representing state indizes in the model.
* {@code null} signifies "all states in the model"
* @param numStates the number of states in the model, i.e., with indizes 0..numStates-1
*/
public IterableStateSet(BitSet setOfStates, int numStates)
{
this(setOfStates, numStates, false);
}
/**
* Constructor (most general form)
*
* @param setOfStates the BitSet representing state indizes in the model.
* {@code null} signifies "all states in the model"
* @param numStates the number of states in the model, i.e., with indizes 0..numStates-1
* @param complement if {@code true}, iterate over all the states not included in setOfStates
*/
public IterableStateSet(BitSet setOfStates, int numStates, boolean complement)
{
this.setOfStates = setOfStates;
this.numStates = numStates;
this.complement = complement;
}
/** Implementation of an Iterator that iterates over all state indizes 0..numStates-1 */
private class AllStatesIterator implements Iterator<Integer>
{
private int current = 0;
@Override
public boolean hasNext()
{
if (current < numStates) {
return true;
} else {
return false;
}
}
@Override
public Integer next()
{
if (hasNext()) {
return current++;
}
throw new NoSuchElementException();
}
@Override
public void remove()
{
throw new UnsupportedOperationException();
}
};
/** Implementation of an Iterator that iterates over the empty state set */
private class NoStatesIterator implements Iterator<Integer>
{
@Override
public boolean hasNext()
{
return false;
}
@Override
public Integer next()
{
throw new NoSuchElementException();
}
@Override
public void remove()
{
throw new UnsupportedOperationException();
}
};
@Override
public Iterator<Integer> iterator()
{
if (setOfStates == null) {
if (!complement) {
// return iterator over all states
return new AllStatesIterator();
} else {
return new NoStatesIterator();
}
} else {
// return appropriate IterableBitSet with maxIndex = numStates-1
return new IterableBitSet(setOfStates, numStates-1, complement).iterator();
}
}
/**
* Simple test method.
*
* @param args ignored
*/
public static void main(String[] args)
{
BitSet test = new BitSet();
test.set(1);
test.set(3);
int numStates = 5;
System.out.println("\n" + test + " - included states:");
for (Integer index : new IterableStateSet(test, numStates)) {
System.out.println(index);
}
System.out.println("\n" + test + " - excluded states:");
for (Integer index : new IterableStateSet(test, numStates, true)) {
System.out.println(index);
}
System.out.println("\nAll " + numStates + " states:");
for (Integer index : new IterableStateSet(null, numStates)) {
System.out.println(index);
}
System.out.println("\nNo " + numStates + " states:");
for (Integer index : new IterableStateSet(null, numStates, true)) {
System.out.println(index);
}
}
}
Write Preview
Loading…
Cancel
Save