sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

commit to switch workplace

tempestpy_adaptions
dehnert 7 years ago
parent
f772af6241
commit
3a11914da0
5 changed files with 109 additions and 95 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/storm/builder/ExplicitModelBuilder.cpp
  2. 17
      src/storm/storage/BitVector.cpp
  3. 6
      src/storm/storage/BitVector.h
  4. 159
      src/storm/storage/BitVectorHashMap.cpp
  5. 18
      src/storm/storage/BitVectorHashMap.h

4
src/storm/builder/ExplicitModelBuilder.cpp
View File

@ -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);

17
src/storm/storage/BitVector.cpp
View File

@ -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());
}

6
src/storm/storage/BitVector.h
View File

@ -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

159
src/storm/storage/BitVectorHashMap.cpp
View File

@ -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]);
}

18
src/storm/storage/BitVectorHashMap.h
View File

@ -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
};
}

Write Preview
Loading…
Cancel
Save