Browse Source

Started refactoring bit vector class.

Former-commit-id: a2fecfce2b
tempestpy_adaptions
dehnert 11 years ago
parent
commit
07fbff7a07
  1. 50
      src/counterexamples/PathBasedSubsystemGenerator.h
  2. 2
      src/counterexamples/SMTMinimalCommandSetGenerator.h
  3. 3
      src/models/AtomicPropositionsLabeling.h
  4. 508
      src/storage/BitVector.cpp
  5. 1198
      src/storage/BitVector.h
  6. 2
      src/storage/StronglyConnectedComponentDecomposition.cpp
  7. 2
      test/functional/storage/BitVectorTest.cpp

50
src/counterexamples/PathBasedSubsystemGenerator.h

@ -55,25 +55,25 @@ public:
// First store all transitions from initial states // First store all transitions from initial states
// Also save all found initial states in array of discovered states. // Also save all found initial states in array of discovered states.
for(storm::storage::BitVector::constIndexIterator init = subSysStates.begin(); init != subSysStates.end(); ++init) {
for(auto init : subSysStates) {
//use init state only if it is allowed //use init state only if it is allowed
if(allowedStates.get(*init)) {
if(allowedStates.get(init)) {
if(terminalStates.get(*init)) {
if(terminalStates.get(init)) {
// it's an init -> target search // it's an init -> target search
// save target state as discovered and get it's outgoing transitions // save target state as discovered and get it's outgoing transitions
distances[*init].first = *init;
distances[*init].second = (T) 1;
distances[init].first = init;
distances[init].second = (T) 1;
} }
typename storm::storage::SparseMatrix<T>::ConstRowIterator rowIt = transMat.begin(*init);
typename storm::storage::SparseMatrix<T>::ConstRowIterator rowIt = transMat.begin(init);
for(auto trans = rowIt.begin() ; trans != rowIt.end(); ++trans) { for(auto trans = rowIt.begin() ; trans != rowIt.end(); ++trans) {
//save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state. //save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state.
if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) {
//new state? //new state?
if(distances[trans.column()].second == (T) -1) { if(distances[trans.column()].second == (T) -1) {
distances[trans.column()].first = *init;
distances[trans.column()].first = init;
distances[trans.column()].second = trans.value(); distances[trans.column()].second = trans.value();
activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), distances[trans.column()].second)); activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), distances[trans.column()].second));
@ -91,7 +91,7 @@ public:
} }
} }
distances[trans.column()].first = *init;
distances[trans.column()].first = init;
distances[trans.column()].second = trans.value(); distances[trans.column()].second = trans.value();
activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), trans.value())); activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), trans.value()));
@ -171,30 +171,30 @@ public:
// First store all transitions from initial states // First store all transitions from initial states
// Also save all found initial states in array of discovered states. // Also save all found initial states in array of discovered states.
for(storm::storage::BitVector::constIndexIterator init = subSysStates.begin(); init != subSysStates.end(); ++init) {
for(auto init : subSysStates) {
//use init state only if it is allowed //use init state only if it is allowed
if(allowedStates.get(*init)) {
if(allowedStates.get(init)) {
if(terminalStates.get(*init)) {
if(terminalStates.get(init)) {
// it's a subsys -> subsys search // it's a subsys -> subsys search
// ignore terminal state completely // ignore terminal state completely
// (since any target state that is only reached by a path going through this state should not be reached) // (since any target state that is only reached by a path going through this state should not be reached)
continue; continue;
} }
typename storm::storage::SparseMatrix<T>::ConstRowIterator rowIt = transMat.begin(*init);
typename storm::storage::SparseMatrix<T>::ConstRowIterator rowIt = transMat.begin(init);
for(typename storm::storage::SparseMatrix<T>::ConstIterator trans = rowIt.begin(); trans != rowIt.end(); ++trans) { for(typename storm::storage::SparseMatrix<T>::ConstIterator trans = rowIt.begin(); trans != rowIt.end(); ++trans) {
//save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state. //save transition only if it's no 'virtual transition of prob 0 and it doesn't go from init state to init state.
if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) { if(trans.value() != (T) 0 && !subSysStates.get(trans.column())) {
//new state? //new state?
if(distances[trans.column()].second == (T) -1) { if(distances[trans.column()].second == (T) -1) {
//for initialization of subsys -> subsys search use prob (init -> subsys state -> found state) instead of prob(subsys state -> found state) //for initialization of subsys -> subsys search use prob (init -> subsys state -> found state) instead of prob(subsys state -> found state)
distances[trans.column()].first = *init;
distances[trans.column()].second = trans.value() * (itDistances[*init].second == -1 ? 1 : itDistances[*init].second);
distances[trans.column()].first = init;
distances[trans.column()].second = trans.value() * (itDistances[init].second == -1 ? 1 : itDistances[init].second);
activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), distances[trans.column()].second)); activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), distances[trans.column()].second));
} }
else if(distances[trans.column()].second < trans.value() * itDistances[*init].second){
else if(distances[trans.column()].second < trans.value() * itDistances[init].second){
//This state has already been discovered //This state has already been discovered
//And the distance can be improved by using this transition. //And the distance can be improved by using this transition.
@ -208,8 +208,8 @@ public:
} }
//for initialization of subsys -> subsys search use prob (init -> subsys state -> found state) instead of prob(subsys state -> found state) //for initialization of subsys -> subsys search use prob (init -> subsys state -> found state) instead of prob(subsys state -> found state)
distances[trans.column()].first = *init;
distances[trans.column()].second = trans.value() * (itDistances[*init].second == -1 ? 1 : itDistances[*init].second);
distances[trans.column()].first = init;
distances[trans.column()].second = trans.value() * (itDistances[init].second == -1 ? 1 : itDistances[init].second);
activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), trans.value())); activeSet.insert(std::pair<uint_fast64_t, T>(trans.column(), trans.value()));
} }
@ -429,12 +429,12 @@ public:
uint_fast64_t bestIndex = 0; uint_fast64_t bestIndex = 0;
T bestValue = (T) 0; T bestValue = (T) 0;
for(storm::storage::BitVector::constIndexIterator term = terminalStates.begin(); term != terminalStates.end(); ++term) {
for(auto term : terminalStates) {
//the terminal state might not have been found if it is in a system of forbidden states //the terminal state might not have been found if it is in a system of forbidden states
if(distances[*term].second != -1 && distances[*term].second > bestValue){
bestIndex = *term;
bestValue = distances[*term].second;
if(distances[term].second != -1 && distances[term].second > bestValue){
bestIndex = term;
bestValue = distances[term].second;
//if set, stop since the first target that is not null was the only one found //if set, stop since the first target that is not null was the only one found
if(stopAtFirstTarget) break; if(stopAtFirstTarget) break;
@ -443,12 +443,12 @@ public:
if(!itSearch) { if(!itSearch) {
// it's a subSys->subSys search. So target states are terminals and subsys states // it's a subSys->subSys search. So target states are terminals and subsys states
for(auto term = subSysStates.begin(); term != subSysStates.end(); ++term) {
for(auto term : subSysStates) {
//the terminal state might not have been found if it is in a system of forbidden states //the terminal state might not have been found if it is in a system of forbidden states
if(distances[*term].second != -1 && distances[*term].second > bestValue){
bestIndex = *term;
bestValue = distances[*term].second;
if(distances[term].second != -1 && distances[term].second > bestValue){
bestIndex = term;
bestValue = distances[term].second;
//if set, stop since the first target that is not null was the only one found //if set, stop since the first target that is not null was the only one found
if(stopAtFirstTarget) break; if(stopAtFirstTarget) break;

2
src/counterexamples/SMTMinimalCommandSetGenerator.h

@ -107,7 +107,7 @@ namespace storm {
relevancyInformation.relevantStates &= ~psiStates; relevancyInformation.relevantStates &= ~psiStates;
LOG4CPLUS_DEBUG(logger, "Found " << relevancyInformation.relevantStates.getNumberOfSetBits() << " relevant states."); LOG4CPLUS_DEBUG(logger, "Found " << relevancyInformation.relevantStates.getNumberOfSetBits() << " relevant states.");
LOG4CPLUS_DEBUG(logger, relevancyInformation.relevantStates.toString());
LOG4CPLUS_DEBUG(logger, relevancyInformation.relevantStates);
// Retrieve some references for convenient access. // Retrieve some references for convenient access.
storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix(); storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();

3
src/models/AtomicPropositionsLabeling.h

@ -10,6 +10,7 @@
#include "src/storage/BitVector.h" #include "src/storage/BitVector.h"
#include "src/exceptions/OutOfRangeException.h" #include "src/exceptions/OutOfRangeException.h"
#include "src/exceptions/InvalidArgumentException.h"
#include <ostream> #include <ostream>
#include <stdexcept> #include <stdexcept>
#include <set> #include <set>
@ -311,7 +312,7 @@ public:
} }
for (auto it = singleLabelings.begin(); it != singleLabelings.end(); ++it) { for (auto it = singleLabelings.begin(); it != singleLabelings.end(); ++it) {
boost::hash_combine(result, it->getHash());
boost::hash_combine(result, it->hash());
} }
return result; return result;

508
src/storage/BitVector.cpp

@ -0,0 +1,508 @@
#include "src/storage/BitVector.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/OutOfRangeException.h"
#include "src/utility/OsDetection.h"
#include "src/utility/Hash.h"
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
namespace storm {
namespace storage {
BitVector::const_iterator::const_iterator(const BitVector& bitVector, uint_fast64_t startIndex, uint_fast64_t endIndex, bool setOnFirstBit) : bitVector(bitVector), endIndex(endIndex) {
if (setOnFirstBit) {
// Set the index of the first set bit in the vector.
currentIndex = bitVector.getNextSetIndex(startIndex, endIndex);
} else {
currentIndex = startIndex;
}
}
BitVector::const_iterator& BitVector::const_iterator::operator++() {
currentIndex = bitVector.getNextSetIndex(++currentIndex, endIndex);
return *this;
}
uint_fast64_t BitVector::const_iterator::operator*() const {
return currentIndex;
}
bool BitVector::const_iterator::operator!=(const_iterator const& otherIterator) const {
return currentIndex != otherIterator.currentIndex;
}
BitVector::BitVector() : bitCount(0), bucketVector() {
// Intentionally left empty.
}
BitVector::BitVector(uint_fast64_t length, bool initTrue) : bitCount(length) {
// Compute the correct number of buckets needed to store the given number of bits.
uint_fast64_t bucketCount = length >> 6;
if ((length & mod64mask) != 0) {
++bucketCount;
}
// Initialize the storage with the required values.
if (initTrue) {
bucketVector = std::vector<uint64_t>(bucketCount, -1ll);
truncateLastBucket();
} else {
bucketVector = std::vector<uint64_t>(bucketCount, 0);
}
}
template<typename InputIterator>
BitVector::BitVector(uint_fast64_t length, InputIterator begin, InputIterator end) : BitVector(length) {
set(begin, end);
}
BitVector::BitVector(BitVector const& other) : bitCount(other.bitCount), bucketVector(other.bucketVector) {
// Intentionally left empty.
}
BitVector::BitVector(BitVector const& other, BitVector const& filter) : bitCount(filter.getNumberOfSetBits()) {
uint_fast64_t bucketCount = bitCount >> 6;
if ((bitCount & mod64mask) != 0) {
++bucketCount;
}
bucketVector = std::vector<uint64_t>(bucketCount);
// Now copy over all bits given by the filter.
uint_fast64_t nextPosition = 0;
for (auto position : filter) {
set(nextPosition, other.get(position));
nextPosition++;
}
}
BitVector::BitVector(BitVector&& other) : bitCount(other.bitCount), bucketVector(std::move(other.bucketVector)) {
// Intentionally left empty.
}
BitVector& BitVector::operator=(BitVector const& other) {
// Only perform the assignment if the source and target are not identical.
if (this != &other) {
bitCount = other.bitCount;
bucketVector = std::vector<uint64_t>(other.bucketVector);
updateSizeChange();
}
return *this;
}
BitVector& BitVector::operator=(BitVector&& other) {
// Only perform the assignment if the source and target are not identical.
if (this != &other) {
bitCount = other.bitCount;
bucketVector = std::move(other.bucketVector);
updateSizeChange();
}
return *this;
}
bool BitVector::operator==(BitVector const& other) {
// If the lengths of the vectors do not match, they are considered unequal.
if (this->bitCount != other.bitCount) return false;
// If the lengths match, we compare the buckets one by one.
for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it1 != bucketVector.end(); ++it1, ++it2) {
if (*it1 != *it2) {
return false;
}
}
// All buckets were equal, so the bit vectors are equal.
return true;
}
void BitVector::set(uint_fast64_t index, bool value) {
uint_fast64_t bucket = index >> 6;
if (index >= bitCount) throw storm::exceptions::OutOfRangeException() << "Invalid call to BitVector::set: written index " << index << " out of bounds.";
uint_fast64_t mask = static_cast<uint_fast64_t>(1) << (index & mod64mask);
if (value) {
bucketVector[bucket] |= mask;
} else {
bucketVector[bucket] &= ~mask;
}
}
template<typename InputIterator>
void BitVector::set(InputIterator begin, InputIterator end) {
for (InputIterator it = begin; it != end; ++it) {
this->set(*it);
}
}
bool BitVector::operator[](uint_fast64_t index) const {
uint_fast64_t bucket = index >> 6;
uint_fast64_t mask = static_cast<uint_fast64_t>(1) << (index & mod64mask);
return (this->bucketVector[bucket] & mask) == mask;
}
bool BitVector::get(uint_fast64_t index) const {
if (index >= bitCount) throw storm::exceptions::OutOfRangeException() << "Invalid call to BitVector::get: read index " << index << " out of bounds.";
return (*this)[index];
}
void BitVector::resize(uint_fast64_t newLength, bool initTrue) {
if (newLength > bitCount) {
uint_fast64_t newBucketCount = newLength >> 6;
if ((newLength & mod64mask) != 0) {
++newBucketCount;
}
if (newBucketCount > bucketVector.size()) {
if (initTrue) {
bucketVector.back() |= (1ll << (bitCount * 64 - bitCount * 63 - bitCount & mod64mask)) - 1ll;
bucketVector.resize(newBucketCount, -1ll);
} else {
bucketVector.resize(newBucketCount, 0);
}
bitCount = newLength;
} else {
// If the underlying storage does not need to grow, we have to insert the missing bits.
if (initTrue) {
bucketVector.back() |= (1ll << (bitCount * 64 - bitCount * 63 - bitCount & mod64mask)) - 1ll;
bitCount = newLength;
} else {
bitCount = newLength;
}
}
updateSizeChange();
} else {
bitCount = newLength;
bitCount = newLength;
uint_fast64_t newBucketCount = newLength >> 6;
if ((newLength & mod64mask) != 0) {
++newBucketCount;
}
bucketVector.resize(newBucketCount);
updateSizeChange();
}
}
BitVector BitVector::operator&(BitVector const& other) const {
uint_fast64_t minSize = std::min(other.bitCount, bitCount);
BitVector result(minSize);
std::vector<uint64_t>::iterator it = result.bucketVector.begin();
for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it != result.bucketVector.end(); ++it1, ++it2, ++it) {
*it = *it1 & *it2;
}
return result;
}
BitVector& BitVector::operator&=(BitVector const& other) {
uint_fast64_t minSize = std::min(other.bucketVector.size(), bucketVector.size());
std::vector<uint64_t>::iterator it = bucketVector.begin();
for (std::vector<uint64_t>::const_iterator otherIt = other.bucketVector.begin(); it != bucketVector.end() && otherIt != other.bucketVector.end(); ++it, ++otherIt) {
*it &= *otherIt;
}
return *this;
}
BitVector BitVector::operator|(BitVector const& other) const {
uint_fast64_t minSize = std::min(other.bitCount, bitCount);
BitVector result(minSize);
std::vector<uint64_t>::iterator it = result.bucketVector.begin();
for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it != result.bucketVector.end(); ++it1, ++it2, ++it) {
*it = *it1 | *it2;
}
result.truncateLastBucket();
return result;
}
BitVector& BitVector::operator|=(BitVector const& other) {
uint_fast64_t minSize = std::min(other.bucketVector.size(), bucketVector.size());
std::vector<uint64_t>::iterator it = bucketVector.begin();
for (std::vector<uint64_t>::const_iterator otherIt = other.bucketVector.begin(); it != bucketVector.end() && otherIt != other.bucketVector.end(); ++it, ++otherIt) {
*it |= *otherIt;
}
truncateLastBucket();
return *this;
}
BitVector BitVector::operator^(BitVector const& other) const {
uint_fast64_t minSize = std::min(other.bitCount, bitCount);
BitVector result(minSize);
std::vector<uint64_t>::iterator it = result.bucketVector.begin();
for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it != result.bucketVector.end(); ++it1, ++it2, ++it) {
*it = *it1 ^ *it2 ;
}
result.truncateLastBucket();
return result;
}
BitVector BitVector::operator~() const {
BitVector result(this->bitCount);
std::vector<uint64_t>::iterator it = result.bucketVector.begin();
for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(); it != result.bucketVector.end(); ++it1, ++it) {
*it = ~(*it1);
}
result.truncateLastBucket();
return result;
}
void BitVector::complement() {
for (auto& element : bucketVector) {
element = ~element;
}
truncateLastBucket();
}
BitVector BitVector::implies(BitVector const& other) const {
uint_fast64_t minSize = std::min(other.bitCount, bitCount);
BitVector result(minSize);
std::vector<uint64_t>::iterator it = result.bucketVector.begin();
for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it != result.bucketVector.end(); ++it1, ++it2, ++it) {
*it = ~(*it1) | *it2;
}
result.truncateLastBucket();
return result;
}
bool BitVector::isSubsetOf(BitVector const& other) const {
if (bitCount != other.bitCount) {
throw storm::exceptions::InvalidArgumentException() << "Invalid call to BitVector::isSubsetOf: length mismatch of operands.";
}
for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it1 != bucketVector.end(); ++it1, ++it2) {
if ((*it1 & *it2) != *it1) {
return false;
}
}
return true;
}
bool BitVector::isDisjointFrom(BitVector const& other) const {
if (bitCount != other.bitCount) {
throw storm::exceptions::InvalidArgumentException() << "Invalid call to BitVector::isDisjointFrom: length mismatch of operands.";
}
for (std::vector<uint64_t>::const_iterator it1 = bucketVector.begin(), it2 = other.bucketVector.begin(); it1 != bucketVector.end(); ++it1, ++it2) {
if ((*it1 & *it2) != 0) {
return false;
}
}
return true;
}
BitVector BitVector::operator%(BitVector const& other) const {
if (bitCount != other.bitCount) {
throw storm::exceptions::InvalidArgumentException() << "Invalid call to BitVector::operator%: length mismatch of operands.";
}
// Create resulting bit vector.
BitVector result(this->getNumberOfSetBits());
// If the current bit vector has not too many elements compared to the given bit vector we prefer iterating
// over its elements.
if (this->getNumberOfSetBits() / 10 < other.getNumberOfSetBits()) {
uint_fast64_t position = 0;
for (auto bit : *this) {
if (other[bit]) {
result.set(position);
}
++position;
}
} else {
// If the given bit vector had much less elements, we iterate over its elements and accept calling the more
// costly operation getNumberOfSetBitsBeforeIndex on the current bit vector.
for (auto bit : other) {
if ((*this)[bit]) {
result.set(this->getNumberOfSetBitsBeforeIndex(bit));
}
}
}
return result;
}
bool BitVector::empty() const {
for (auto& element : bucketVector) {
if (element != 0) {
return false;
}
}
return true;
}
void BitVector::clear() {
for (auto& element : bucketVector) {
element = 0;
}
}
std::vector<uint_fast64_t> BitVector::getSetIndicesList() const {
std::vector<uint_fast64_t> result;
result.reserve(this->getNumberOfSetBits());
for (auto index : *this) {
result.push_back(index);
}
return result;
}
void BitVector::addSetIndicesToVector(std::vector<uint_fast64_t>& vector) const {
for (auto index : *this) {
vector.push_back(index);
}
}
uint_fast64_t BitVector::getNumberOfSetBits() const {
return getNumberOfSetBitsBeforeIndex(bucketVector.size() << 6);
}
uint_fast64_t BitVector::getNumberOfSetBitsBeforeIndex(uint_fast64_t index) const {
uint_fast64_t result = 0;
// First, count all full buckets.
uint_fast64_t bucket = index >> 6;
for (uint_fast64_t i = 0; i < bucket; ++i) {
// Check if we are using g++ or clang++ and, if so, use the built-in function
#if (defined (__GNUG__) || defined(__clang__))
result += __builtin_popcountll(bucketVector[i]);
#elif defined WINDOWS
#include <nmmintrin.h>
// if the target machine does not support SSE4, this will fail.
result += _mm_popcnt_u64(bucketVector[i]);
#else
uint_fast32_t cnt;
uint_fast64_t bitset = bucketVector[i];
for (cnt = 0; bitset; cnt++) {
bitset &= bitset - 1;
}
result += cnt;
#endif
}
// Now check if we have to count part of a bucket.
uint64_t tmp = index & mod64mask;
if (tmp != 0) {
tmp = ((1ll << (tmp & mod64mask)) - 1ll);
tmp &= bucketVector[bucket];
// Check if we are using g++ or clang++ and, if so, use the built-in function
#if (defined (__GNUG__) || defined(__clang__))
result += __builtin_popcountll(tmp);
#else
uint_fast32_t cnt;
uint64_t bitset = tmp;
for (cnt = 0; bitset; cnt++) {
bitset &= bitset - 1;
}
result += cnt;
#endif
}
return result;
}
size_t BitVector::size() const {
return static_cast<size_t>(bitCount);
}
uint_fast64_t BitVector::getSizeInMemory() const {
return sizeof(*this) + sizeof(uint64_t) * bucketVector.size();
}
BitVector::const_iterator BitVector::begin() const {
return const_iterator(*this, 0, bitCount);
}
BitVector::const_iterator BitVector::end() const {
return const_iterator(*this, bitCount, bitCount, false);
}
std::size_t BitVector::hash() const {
std::size_t result = 0;
boost::hash_combine(result, bucketVector.size());
boost::hash_combine(result, bitCount);
for (auto& element : bucketVector) {
boost::hash_combine(result, element);
}
return result;
}
uint_fast64_t BitVector::getNextSetIndex(uint_fast64_t startingIndex) const {
return getNextSetIndex(startingIndex, bitCount);
}
uint_fast64_t BitVector::getNextSetIndex(uint_fast64_t startingIndex, uint_fast64_t endIndex) const {
uint_fast8_t currentBitInByte = startingIndex & mod64mask;
startingIndex >>= 6;
std::vector<uint64_t>::const_iterator bucketIt = bucketVector.begin() + startingIndex;
while ((startingIndex << 6) < endIndex) {
// Compute the remaining bucket content by a right shift
// to the current bit.
uint_fast64_t remainingInBucket = *bucketIt >> currentBitInByte;
// Check if there is at least one bit in the remainder of the bucket
// that is set to true.
if (remainingInBucket != 0) {
// Find that bit.
while ((remainingInBucket & 1) == 0) {
remainingInBucket >>= 1;
++currentBitInByte;
}
// Only return the index of the set bit if we are still in the
// valid range.
if ((startingIndex << 6) + currentBitInByte < endIndex) {
return (startingIndex << 6) + currentBitInByte;
} else {
return endIndex;
}
}
// Advance to the next bucket.
++startingIndex; ++bucketIt; currentBitInByte = 0;
}
return endIndex;
}
void BitVector::truncateLastBucket() {
if ((bitCount & mod64mask) != 0) {
bucketVector.back() &= (1ll << (bitCount & mod64mask)) - 1ll;
}
}
void BitVector::updateSizeChange() {
truncateLastBucket();
}
std::ostream& operator<<(std::ostream& out, BitVector const& bitVector) {
out << "bit vector(" << bitVector.getNumberOfSetBits() << "/" << bitVector.bitCount << ") [";
for (auto index : bitVector) {
out << index << " ";
}
out << "]";
return out;
}
// All necessary explicit template instantiations.
template BitVector::BitVector(uint_fast64_t length, std::vector<uint_fast64_t>::iterator begin, std::vector<uint_fast64_t>::iterator end);
template BitVector::BitVector(uint_fast64_t length, std::vector<uint_fast64_t>::const_iterator begin, std::vector<uint_fast64_t>::const_iterator end);
template void BitVector::set(std::vector<uint_fast64_t>::iterator begin, std::vector<uint_fast64_t>::iterator end);
template void BitVector::set(std::vector<uint_fast64_t>::const_iterator begin, std::vector<uint_fast64_t>::const_iterator end);
}
}

1198
src/storage/BitVector.h
File diff suppressed because it is too large
View File

2
src/storage/StronglyConnectedComponentDecomposition.cpp

@ -15,7 +15,7 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) { StronglyConnectedComponentDecomposition<ValueType>::StronglyConnectedComponentDecomposition(storm::models::AbstractModel<ValueType> const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) {
storm::storage::BitVector subsystem(model.getNumberOfStates(), block);
storm::storage::BitVector subsystem(model.getNumberOfStates(), block.begin(), block.end());
performSccDecomposition(model, subsystem, dropNaiveSccs, onlyBottomSccs); performSccDecomposition(model, subsystem, dropNaiveSccs, onlyBottomSccs);
} }

2
test/functional/storage/BitVectorTest.cpp

@ -36,7 +36,7 @@ TEST(BitVectorTest, ResizeTest) {
for (int i = 0; i < 32; ++i) { for (int i = 0; i < 32; ++i) {
ASSERT_TRUE(bvA.get(i)); ASSERT_TRUE(bvA.get(i));
} }
bool result; bool result;
for (int i = 32; i < 70; ++i) { for (int i = 32; i < 70; ++i) {
result = true; result = true;

Loading…
Cancel
Save