diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp
index 7a552e9bd..48d5b2a75 100644
--- a/src/storm/builder/ExplicitModelBuilder.cpp
+++ b/src/storm/builder/ExplicitModelBuilder.cpp
@@ -149,7 +149,9 @@ namespace storm {
stateRemapping.get()[currentIndex] = currentRowGroup;
}
- STORM_LOG_TRACE("Exploring state with id " << currentIndex << ".");
+ if (currentIndex % 100000 == 0) {
+ STORM_LOG_TRACE("Exploring state with id " << currentIndex << ".");
+ }
generator->load(currentState);
storm::generator::StateBehavior<ValueType, StateType> behavior = generator->expand(stateToIdCallback);
diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp
index 469fb8441..e5498b82c 100644
--- a/src/storm/storage/BitVector.cpp
+++ b/src/storm/storage/BitVector.cpp
@@ -999,22 +999,6 @@ namespace storm {
out << std::endl;
}
- std::size_t NonZeroBitVectorHash::operator()(storm::storage::BitVector const& bitvector) const {
- STORM_LOG_ASSERT(bitvector.size() > 0, "Cannot hash bit vector of zero size.");
- std::size_t result = 0;
-
- for (uint_fast64_t index = 0; index < bitvector.bucketCount(); ++index) {
- result ^= result << 3;
- result ^= result >> bitvector.getAsInt(index << 6, 5);
- }
-
- // Erase the last bit and add one to definitely make this hash value non-zero.
- result &= ~1ull;
- result += 1;
-
- return result;
- }
-
// 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);
@@ -1028,7 +1012,6 @@ namespace storm {
}
namespace std {
-
std::size_t hash<storm::storage::BitVector>::operator()(storm::storage::BitVector const& bitvector) const {
return boost::hash_range(bitvector.buckets, bitvector.buckets + bitvector.bucketCount());
}
diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h
index bcb56ae0d..0b5a7670b 100644
--- a/src/storm/storage/BitVector.h
+++ b/src/storm/storage/BitVector.h
@@ -501,7 +501,6 @@ namespace storm {
friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector);
friend struct std::hash<storm::storage::BitVector>;
- friend struct NonZeroBitVectorHash;
private:
/*!
@@ -571,11 +570,6 @@ namespace storm {
static const uint_fast64_t mod64mask = (1 << 6) - 1;
};
- // A hashing functor that guarantees that the result of the hash is never going to be -1.
- struct NonZeroBitVectorHash {
- std::size_t operator()(storm::storage::BitVector const& bv) const;
- };
-
} // namespace storage
} // namespace storm
diff --git a/src/storm/storage/BitVectorHashMap.cpp b/src/storm/storage/BitVectorHashMap.cpp
index a522a5863..c1d9d46d1 100644
--- a/src/storm/storage/BitVectorHashMap.cpp
+++ b/src/storm/storage/BitVectorHashMap.cpp
@@ -9,47 +9,43 @@
namespace storm {
namespace storage {
- template<class ValueType, class Hash1, class Hash2>
- const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191, 64285127, 128572517, 257148523, 514299959, 1028599919, 2057199839, 4114399697, 8228799419, 16457598791, 32915197603, 65830395223};
+ template<class ValueType, class Hash>
+ const std::vector<std::size_t> BitVectorHashMap<ValueType, Hash>::sizes = {5, 13, 31, 79, 163, 277, 499, 1021, 2029, 3989, 8059, 16001, 32099, 64301, 127921, 256499, 511111, 1024901, 2048003, 4096891, 8192411, 15485863, 32142191, 64285127, 128572517, 257148523, 514299959, 1028599919, 2057199839, 4114399697, 8228799419, 16457598791, 32915197603, 65830395223};
- template<class ValueType, class Hash1, class Hash2>
- BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::BitVectorHashMapIterator(BitVectorHashMap const& map, BitVector::const_iterator indexIt) : map(map), indexIt(indexIt) {
-#ifndef NDEBUG
- for (uint64_t i = 0; i < sizes.size() - 1; ++i) {
- STORM_LOG_ASSERT(sizes[i] < sizes[i + 1], "Expected stricly increasing sizes.");
- }
-#endif
+ template<class ValueType, class Hash>
+ BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::BitVectorHashMapIterator(BitVectorHashMap const& map, BitVector::const_iterator indexIt) : map(map), indexIt(indexIt) {
+ // Intentionally left empty.
}
- template<class ValueType, class Hash1, class Hash2>
- bool BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator==(BitVectorHashMapIterator const& other) {
+ template<class ValueType, class Hash>
+ bool BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::operator==(BitVectorHashMapIterator const& other) {
return &map == &other.map && *indexIt == *other.indexIt;
}
- template<class ValueType, class Hash1, class Hash2>
- bool BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator!=(BitVectorHashMapIterator const& other) {
+ template<class ValueType, class Hash>
+ bool BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::operator!=(BitVectorHashMapIterator const& other) {
return !(*this == other);
}
- template<class ValueType, class Hash1, class Hash2>
- typename BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator& BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator++(int) {
+ template<class ValueType, class Hash>
+ typename BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator& BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::operator++(int) {
++indexIt;
return *this;
}
- template<class ValueType, class Hash1, class Hash2>
- typename BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator& BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator++() {
+ template<class ValueType, class Hash>
+ typename BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator& BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::operator++() {
++indexIt;
return *this;
}
- template<class ValueType, class Hash1, class Hash2>
- std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMapIterator::operator*() const {
+ template<class ValueType, class Hash>
+ std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash>::BitVectorHashMapIterator::operator*() const {
return map.getBucketAndValue(*indexIt);
}
- template<class ValueType, class Hash1, class Hash2>
- BitVectorHashMap<ValueType, Hash1, Hash2>::BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor) : loadFactor(loadFactor), bucketSize(bucketSize), numberOfElements(0) {
+ template<class ValueType, class Hash>
+ BitVectorHashMap<ValueType, Hash>::BitVectorHashMap(uint64_t bucketSize, uint64_t initialSize, double loadFactor) : loadFactor(loadFactor), bucketSize(bucketSize), numberOfElements(0) {
STORM_LOG_ASSERT(bucketSize % 64 == 0, "Bucket size must be a multiple of 64.");
currentSizeIterator = std::find_if(sizes.begin(), sizes.end(), [=] (uint64_t value) { return value > initialSize; } );
@@ -57,28 +53,42 @@ namespace storm {
buckets = storm::storage::BitVector(bucketSize * *currentSizeIterator);
occupied = storm::storage::BitVector(*currentSizeIterator);
values = std::vector<ValueType>(*currentSizeIterator);
+
+#ifndef NDEBUG
+ for (uint64_t i = 0; i < sizes.size() - 1; ++i) {
+ STORM_LOG_ASSERT(sizes[i] < sizes[i + 1], "Expected stricly increasing sizes.");
+ }
+ numberOfInsertions = 0;
+ numberOfInsertionProbingSteps = 0;
+ numberOfFinds = 0;
+ numberOfFindProbingSteps = 0;
+#endif
}
- template<class ValueType, class Hash1, class Hash2>
- bool BitVectorHashMap<ValueType, Hash1, Hash2>::isBucketOccupied(uint_fast64_t bucket) const {
+ template<class ValueType, class Hash>
+ bool BitVectorHashMap<ValueType, Hash>::isBucketOccupied(uint_fast64_t bucket) const {
return occupied.get(bucket);
}
- template<class ValueType, class Hash1, class Hash2>
- std::size_t BitVectorHashMap<ValueType, Hash1, Hash2>::size() const {
+ template<class ValueType, class Hash>
+ std::size_t BitVectorHashMap<ValueType, Hash>::size() const {
return numberOfElements;
}
- template<class ValueType, class Hash1, class Hash2>
- std::size_t BitVectorHashMap<ValueType, Hash1, Hash2>::capacity() const {
+ template<class ValueType, class Hash>
+ std::size_t BitVectorHashMap<ValueType, Hash>::capacity() const {
return *currentSizeIterator;
}
- template<class ValueType, class Hash1, class Hash2>
- void BitVectorHashMap<ValueType, Hash1, Hash2>::increaseSize() {
+ template<class ValueType, class Hash>
+ void BitVectorHashMap<ValueType, Hash>::increaseSize() {
++currentSizeIterator;
STORM_LOG_ASSERT(currentSizeIterator != sizes.end(), "Hash map became to big.");
+#ifndef NDEBUG
+ STORM_LOG_TRACE("Increasing size of hash map from " << *(currentSizeIterator - 1) << " to " << *currentSizeIterator << ". Stats: " << numberOfFinds << " finds (avg. " << (numberOfFindProbingSteps / static_cast<double>(numberOfFinds)) << " probing steps), " << numberOfInsertions << " insertions (avg. " << (numberOfInsertionProbingSteps / static_cast<double>(numberOfInsertions)) << " probing steps).");
+#else
STORM_LOG_TRACE("Increasing size of hash map from " << *(currentSizeIterator - 1) << " to " << *currentSizeIterator << ".");
+#endif
// Create new containers and swap them with the old ones.
numberOfElements = 0;
@@ -124,8 +134,8 @@ namespace storm {
}
}
- template<class ValueType, class Hash1, class Hash2>
- bool BitVectorHashMap<ValueType, Hash1, Hash2>::insertWithoutIncreasingSize(storm::storage::BitVector const& key, ValueType const& value) {
+ template<class ValueType, class Hash>
+ bool BitVectorHashMap<ValueType, Hash>::insertWithoutIncreasingSize(storm::storage::BitVector const& key, ValueType const& value) {
std::tuple<bool, std::size_t, bool> flagBucketTuple = this->findBucketToInsert<false>(key);
if (std::get<2>(flagBucketTuple)) {
return false;
@@ -143,18 +153,18 @@ namespace storm {
}
}
- template<class ValueType, class Hash1, class Hash2>
- ValueType BitVectorHashMap<ValueType, Hash1, Hash2>::findOrAdd(storm::storage::BitVector const& key, ValueType const& value) {
+ template<class ValueType, class Hash>
+ ValueType BitVectorHashMap<ValueType, Hash>::findOrAdd(storm::storage::BitVector const& key, ValueType const& value) {
return findOrAddAndGetBucket(key, value).first;
}
- template<class ValueType, class Hash1, class Hash2>
- void BitVectorHashMap<ValueType, Hash1, Hash2>::setOrAdd(storm::storage::BitVector const& key, ValueType const& value) {
+ template<class ValueType, class Hash>
+ void BitVectorHashMap<ValueType, Hash>::setOrAdd(storm::storage::BitVector const& key, ValueType const& value) {
setOrAddAndGetBucket(key, value);
}
- template<class ValueType, class Hash1, class Hash2>
- std::pair<ValueType, std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) {
+ template<class ValueType, class Hash>
+ std::pair<ValueType, std::size_t> BitVectorHashMap<ValueType, Hash>::findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) {
// If the load of the map is too high, we increase the size.
if (numberOfElements >= loadFactor * *currentSizeIterator) {
this->increaseSize();
@@ -174,8 +184,8 @@ namespace storm {
}
}
- template<class ValueType, class Hash1, class Hash2>
- std::size_t BitVectorHashMap<ValueType, Hash1, Hash2>::setOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) {
+ template<class ValueType, class Hash>
+ std::size_t BitVectorHashMap<ValueType, Hash>::setOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value) {
// If the load of the map is too high, we increase the size.
if (numberOfElements >= loadFactor * *currentSizeIterator) {
this->increaseSize();
@@ -193,42 +203,51 @@ namespace storm {
return std::get<1>(flagBucketTuple);
}
- template<class ValueType, class Hash1, class Hash2>
- ValueType BitVectorHashMap<ValueType, Hash1, Hash2>::getValue(storm::storage::BitVector const& key) const {
+ template<class ValueType, class Hash>
+ ValueType BitVectorHashMap<ValueType, Hash>::getValue(storm::storage::BitVector const& key) const {
std::pair<bool, std::size_t> flagBucketPair = this->findBucket(key);
STORM_LOG_ASSERT(flagBucketPair.first, "Unknown key.");
return values[flagBucketPair.second];
}
- template<class ValueType, class Hash1, class Hash2>
- bool BitVectorHashMap<ValueType, Hash1, Hash2>::contains(storm::storage::BitVector const& key) const {
+ template<class ValueType, class Hash>
+ bool BitVectorHashMap<ValueType, Hash>::contains(storm::storage::BitVector const& key) const {
return findBucket(key).first;
}
- template<class ValueType, class Hash1, class Hash2>
- typename BitVectorHashMap<ValueType, Hash1, Hash2>::const_iterator BitVectorHashMap<ValueType, Hash1, Hash2>::begin() const {
+ template<class ValueType, class Hash>
+ typename BitVectorHashMap<ValueType, Hash>::const_iterator BitVectorHashMap<ValueType, Hash>::begin() const {
return const_iterator(*this, occupied.begin());
}
- template<class ValueType, class Hash1, class Hash2>
- typename BitVectorHashMap<ValueType, Hash1, Hash2>::const_iterator BitVectorHashMap<ValueType, Hash1, Hash2>::end() const {
+ template<class ValueType, class Hash>
+ typename BitVectorHashMap<ValueType, Hash>::const_iterator BitVectorHashMap<ValueType, Hash>::end() const {
return const_iterator(*this, occupied.end());
}
- template<class ValueType, class Hash1, class Hash2>
- std::pair<bool, std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::findBucket(storm::storage::BitVector const& key) const {
- uint_fast64_t initialHash = hasher1(key) % *currentSizeIterator;
- uint_fast64_t stride = hasher2(key);
+ template<class ValueType, class Hash>
+ uint_fast64_t BitVectorHashMap<ValueType, Hash>::getNextBucketInProbingSequence(uint_fast64_t currentValue, uint_fast64_t step) const {
+ return (currentValue + step + step*step) % *currentSizeIterator;
+ }
+
+ template<class ValueType, class Hash>
+ std::pair<bool, std::size_t> BitVectorHashMap<ValueType, Hash>::findBucket(storm::storage::BitVector const& key) const {
+#ifndef NDEBUG
+ ++numberOfFinds;
+#endif
+ uint_fast64_t initialHash = hasher(key) % *currentSizeIterator;
uint_fast64_t bucket = initialHash;
- uint_fast64_t counter = 0;
+ uint_fast64_t i = 0;
while (isBucketOccupied(bucket)) {
- ++counter;
+ ++i;
+#ifndef NDEBUG
+ ++numberOfFindProbingSteps;
+#endif
if (buckets.matches(bucket * bucketSize, key)) {
return std::make_pair(true, bucket);
}
- bucket += stride;
- bucket %= *currentSizeIterator;
+ bucket = getNextBucketInProbingSequence(bucket, i);
if (bucket == initialHash) {
return std::make_pair(false, bucket);
@@ -238,26 +257,30 @@ namespace storm {
return std::make_pair(false, bucket);
}
- template<class ValueType, class Hash1, class Hash2>
+ template<class ValueType, class Hash>
template<bool increaseStorage>
- std::tuple<bool, std::size_t, bool> BitVectorHashMap<ValueType, Hash1, Hash2>::findBucketToInsert(storm::storage::BitVector const& key) {
- uint_fast64_t initialHash = hasher1(key) % *currentSizeIterator;
- uint_fast64_t stride = hasher2(key);
+ std::tuple<bool, std::size_t, bool> BitVectorHashMap<ValueType, Hash>::findBucketToInsert(storm::storage::BitVector const& key) {
+#ifndef NDEBUG
+ ++numberOfInsertions;
+#endif
+ uint_fast64_t initialHash = hasher(key) % *currentSizeIterator;
uint_fast64_t bucket = initialHash;
- uint_fast64_t counter = 0;
+ uint64_t i = 0;
while (isBucketOccupied(bucket)) {
- ++counter;
+ ++i;
+#ifndef NDEBUG
+ ++numberOfInsertionProbingSteps;
+#endif
if (buckets.matches(bucket * bucketSize, key)) {
return std::make_tuple(true, bucket, false);
}
- bucket += stride;
- bucket %= *currentSizeIterator;
+ bucket = getNextBucketInProbingSequence(bucket, i);
if (bucket == initialHash) {
if (increaseStorage) {
this->increaseSize();
- bucket = initialHash = hasher1(key) % *currentSizeIterator;
+ bucket = initialHash = hasher(key) % *currentSizeIterator;
} else {
return std::make_tuple(false, bucket, true);
}
@@ -267,13 +290,13 @@ namespace storm {
return std::make_tuple(false, bucket, false);
}
- template<class ValueType, class Hash1, class Hash2>
- std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash1, Hash2>::getBucketAndValue(std::size_t bucket) const {
+ template<class ValueType, class Hash>
+ std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash>::getBucketAndValue(std::size_t bucket) const {
return std::make_pair(buckets.get(bucket * bucketSize, bucketSize), values[bucket]);
}
- template<class ValueType, class Hash1, class Hash2>
- void BitVectorHashMap<ValueType, Hash1, Hash2>::remap(std::function<ValueType(ValueType const&)> const& remapping) {
+ template<class ValueType, class Hash>
+ void BitVectorHashMap<ValueType, Hash>::remap(std::function<ValueType(ValueType const&)> const& remapping) {
for (auto pos : occupied) {
values[pos] = remapping(values[pos]);
}
diff --git a/src/storm/storage/BitVectorHashMap.h b/src/storm/storage/BitVectorHashMap.h
index a5941e2f8..ab9e6c4be 100644
--- a/src/storm/storage/BitVectorHashMap.h
+++ b/src/storm/storage/BitVectorHashMap.h
@@ -14,7 +14,7 @@ namespace storm {
* queries and insertions are supported. Also, the keys must be bit vectors with a length that is a multiple of
* 64.
*/
- template<typename ValueType, typename Hash1 = std::hash<storm::storage::BitVector>, class Hash2 = storm::storage::NonZeroBitVectorHash>
+ template<typename ValueType, typename Hash = std::hash<storm::storage::BitVector>>
class BitVectorHashMap {
public:
class BitVectorHashMapIterator {
@@ -204,6 +204,11 @@ namespace storm {
*/
void increaseSize();
+ /*!
+ * Computes the next bucket in the probing sequence.
+ */
+ uint_fast64_t getNextBucketInProbingSequence(uint_fast64_t currentValue, uint_fast64_t step) const;
+
// The load factor determining when the size of the map is increased.
double loadFactor;
@@ -229,11 +234,18 @@ namespace storm {
std::vector<std::size_t>::const_iterator currentSizeIterator;
// Functor object that are used to perform the actual hashing.
- Hash1 hasher1;
- Hash2 hasher2;
+ Hash hasher;
// A static table that produces the next possible size of the hash table.
static const std::vector<std::size_t> sizes;
+
+#ifndef NDEBUG
+ // Some performance metrics.
+ mutable uint64_t numberOfInsertions;
+ mutable uint64_t numberOfInsertionProbingSteps;
+ mutable uint64_t numberOfFinds;
+ mutable uint64_t numberOfFindProbingSteps;
+#endif
};
}