diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h index c4811cf1a..bc4c43710 100644 --- a/src/counterexamples/PathBasedSubsystemGenerator.h +++ b/src/counterexamples/PathBasedSubsystemGenerator.h @@ -617,7 +617,7 @@ public: // If so the init state represents a subsystem with probability mass 1. // -> return it if((initStates & targetStates).getNumberOfSetBits() != 0) { - subSys.set((initStates & targetStates).getSetIndicesList().front(), true); + subSys.set(*(initStates & targetStates).begin()); LOG4CPLUS_INFO(logger, "Critical subsystem found."); LOG4CPLUS_INFO(logger, "Paths needed: " << pathCount); diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index 1c60b8b34..6b4542fed 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -34,6 +34,10 @@ namespace storm { bool BitVector::const_iterator::operator!=(const_iterator const& otherIterator) const { return currentIndex != otherIterator.currentIndex; } + + bool BitVector::const_iterator::operator==(const_iterator const& otherIterator) const { + return currentIndex == otherIterator.currentIndex; + } BitVector::BitVector() : bitCount(0), bucketVector() { // Intentionally left empty. @@ -350,22 +354,7 @@ namespace storm { element = 0; } } - - std::vector BitVector::getSetIndicesList() const { - std::vector result; - result.reserve(this->getNumberOfSetBits()); - for (auto index : *this) { - result.push_back(index); - } - return result; - } - - void BitVector::addSetIndicesToVector(std::vector& vector) const { - for (auto index : *this) { - vector.push_back(index); - } - } - + uint_fast64_t BitVector::getNumberOfSetBits() const { return getNumberOfSetBitsBeforeIndex(bucketVector.size() << 6); } diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 62733d12f..7e0d26c9b 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -5,6 +5,7 @@ #include #include #include +#include namespace storm { namespace storage { @@ -18,7 +19,7 @@ namespace storm { * A class that enables iterating over the indices of the bit vector whose corresponding bits are set to true. * Note that this is a const iterator, which cannot alter the bit vector. */ - class const_iterator { + class const_iterator : public std::iterator { // Declare the BitVector class as a friend class to access its internal storage. friend class BitVector; @@ -56,7 +57,15 @@ namespace storm { * @param otherIterator The iterator with respect to which inequality is checked. * @return True if the two iterators are unequal. */ - bool operator!=(const const_iterator& otherIterator) const; + bool operator!=(const_iterator const& otherIterator) const; + + /*! + * Compares the iterator with another iterator for equality. + * + * @param otherIterator The iterator with respect to which equality is checked. + * @return True if the two iterators are equal. + */ + bool operator==(const_iterator const& otherIterator) const; private: // The underlying bit vector of this iterator. @@ -286,22 +295,7 @@ namespace storm { * Removes all set bits from the bit vector. */ void clear(); - - /*! - * Returns a list containing all indices such that the bits at these indices are set to true - * in the bit vector. - * - * @return A vector of indices of set bits in the bit vector. - */ - std::vector getSetIndicesList() const; - - /*! - * Adds all indices of bits set to one to the given list. - * - * @param list The list to which to append the indices. - */ - void addSetIndicesToVector(std::vector& vector) const; - + /*! * Returns the number of bits that are set (to one) in this bit vector. * diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index 773d1372f..2f9b8eba2 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -103,8 +103,7 @@ namespace storm { // Now erase the states that have no option to stay inside the MEC with all successors. mecChanged |= !statesToRemove.empty(); - std::vector statesToRemoveList = statesToRemove.getSetIndicesList(); - scc.erase(storm::storage::VectorSet(statesToRemoveList)); + scc.erase(storm::storage::VectorSet(statesToRemove.begin(), statesToRemove.end())); // Now check which states should be reconsidered, because successors of them were removed. statesToCheck.clear(); diff --git a/src/storage/VectorSet.cpp b/src/storage/VectorSet.cpp index b10f2673d..bd5cc0a2e 100644 --- a/src/storage/VectorSet.cpp +++ b/src/storage/VectorSet.cpp @@ -13,6 +13,12 @@ namespace storm { data.reserve(size); } + template + template + VectorSet::VectorSet(InputIterator first, InputIterator last) : dirty(true) { + this->data.insert(this->data.end(), first, last); + } + template VectorSet::VectorSet(std::vector const& data) : data(data), dirty(true) { ensureSet(); @@ -286,6 +292,7 @@ namespace storm { template class VectorSet; template class VectorSet>; + template VectorSet::VectorSet(storm::storage::BitVector::const_iterator, storm::storage::BitVector::const_iterator); template std::ostream& operator<<(std::ostream& stream, VectorSet const& set); template std::ostream& operator<<(std::ostream& stream, VectorSet> const& set); } diff --git a/src/storage/VectorSet.h b/src/storage/VectorSet.h index bb5de042e..aaa2cf40a 100644 --- a/src/storage/VectorSet.h +++ b/src/storage/VectorSet.h @@ -36,6 +36,9 @@ namespace storm { VectorSet(uint_fast64_t size); + template + VectorSet(InputIterator first, InputIterator last); + VectorSet(std::vector const& data); VectorSet(std::set const& data); diff --git a/src/utility/graph.h b/src/utility/graph.h index 4a7a6f067..5c08d94e7 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -56,7 +56,7 @@ namespace storm { statesWithProbabilityGreater0 |= psiStates; // Initialize the stack used for the DFS with the states. - std::vector stack = psiStates.getSetIndicesList(); + std::vector stack(psiStates.begin(), psiStates.end()); // Initialize the stack for the step bound, if the number of steps is bounded. std::vector stepStack; @@ -187,7 +187,7 @@ namespace storm { statesWithProbabilityGreater0 |= psiStates; // Initialize the stack used for the DFS with the states - std::vector stack = psiStates.getSetIndicesList(); + std::vector stack(psiStates.begin(), psiStates.end()); // Initialize the stack for the step bound, if the number of steps is bounded. std::vector stepStack; @@ -285,7 +285,7 @@ namespace storm { while (!done) { stack.clear(); storm::storage::BitVector nextStates(psiStates); - psiStates.addSetIndicesToVector(stack); + stack.insert(stack.end(), psiStates.begin(), psiStates.end()); while (!stack.empty()) { currentState = stack.back(); @@ -377,7 +377,7 @@ namespace storm { statesWithProbabilityGreater0 |= psiStates; // Initialize the stack used for the DFS with the states - std::vector stack = psiStates.getSetIndicesList(); + std::vector stack(psiStates.begin(), psiStates.end()); // Initialize the stack for the step bound, if the number of steps is bounded. std::vector stepStack; @@ -496,7 +496,7 @@ namespace storm { while (!done) { stack.clear(); storm::storage::BitVector nextStates(psiStates); - psiStates.addSetIndicesToVector(stack); + stack.insert(stack.end(), psiStates.begin(), psiStates.end()); while (!stack.empty()) { currentState = stack.back();