From 95feea13ce93899f8dc16022b429e69dcc35b9a9 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 23 Jan 2015 01:41:50 +0000 Subject: [PATCH] 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 --- prism/src/common/IterableBitSet.java | 184 +++++++++++++++++++++++++ prism/src/common/IterableStateSet.java | 183 ++++++++++++++++++++++++ 2 files changed, 367 insertions(+) create mode 100644 prism/src/common/IterableBitSet.java create mode 100644 prism/src/common/IterableStateSet.java diff --git a/prism/src/common/IterableBitSet.java b/prism/src/common/IterableBitSet.java new file mode 100644 index 00000000..9d2ec873 --- /dev/null +++ b/prism/src/common/IterableBitSet.java @@ -0,0 +1,184 @@ +//============================================================================== +// +// Copyright (c) 2014- +// 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 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:

+ * for (Integer index : getSetBits(set)) { ... }
+ */ +public class IterableBitSet implements Iterable +{ + 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 { + 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 { + 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 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!"); + } + } +} diff --git a/prism/src/common/IterableStateSet.java b/prism/src/common/IterableStateSet.java new file mode 100644 index 00000000..eb8b8d91 --- /dev/null +++ b/prism/src/common/IterableStateSet.java @@ -0,0 +1,183 @@ +//============================================================================== +// +// Copyright (c) 2014- +// 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 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 { + 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 + { + 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 + { + @Override + public boolean hasNext() + { + return false; + } + + @Override + public Integer next() + { + throw new NoSuchElementException(); + } + + @Override + public void remove() + { + throw new UnsupportedOperationException(); + } + }; + + @Override + public Iterator 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); + } + } +}