diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 06c9a2ba4..4084f6cd9 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -39,7 +39,7 @@ namespace storm { // A structure holding information about the reachable state space. struct StateInformation { - StateInformation(uint64_t bitsPerState) : bitsPerState(bitsPerState), reachableStates(), stateToIndexMap(bitsPerState, 100000) { + StateInformation(uint64_t bitsPerState) : bitsPerState(bitsPerState), reachableStates(), stateToIndexMap(bitsPerState, 1000000) { // Intentionally left empty. } @@ -47,7 +47,7 @@ namespace storm { uint64_t bitsPerState; // A list of reachable states as indices in the stateToIndexMap. - std::vector reachableStates; + std::vector reachableStates; // A list of initial states in terms of their global indices. std::vector initialStateIndices; @@ -264,15 +264,15 @@ namespace storm { * @param stateInformation The information about the already explored part of the reachable state space. * @return A pair indicating whether the state was already discovered before and the state id of the state. */ - static uint32_t getOrAddStateIndex(StateType const& state, StateInformation& stateInformation, std::queue& stateQueue) { + static uint32_t getOrAddStateIndex(StateType const& state, StateInformation& stateInformation, std::queue& stateQueue) { uint32_t newIndex = stateInformation.reachableStates.size(); // Check, if the state was already registered. std::pair actualIndexBucketPair = stateInformation.stateToIndexMap.findOrAddAndGetBucket(state, newIndex); if (actualIndexBucketPair.first == newIndex) { - stateQueue.push(actualIndexBucketPair.second); - stateInformation.reachableStates.push_back(actualIndexBucketPair.second); + stateQueue.push(state); + stateInformation.reachableStates.push_back(state); } return actualIndexBucketPair.first; @@ -336,7 +336,7 @@ namespace storm { return result; } - static std::vector> getUnlabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue& stateQueue) { + static std::vector> getUnlabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue& stateQueue) { std::vector> result; // Iterate over all modules. @@ -382,7 +382,7 @@ namespace storm { return result; } - static std::vector> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue& stateQueue) { + static std::vector> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue& stateQueue) { std::vector> result; for (uint_fast64_t actionIndex : program.getActionIndices()) { @@ -495,7 +495,7 @@ namespace storm { std::vector> choiceLabels; // Initialize a queue and insert the initial state. - std::queue stateQueue; + std::queue stateQueue; StateType initialState(stateInformation.bitsPerState); // We need to initialize the values of the variables to their initial value. @@ -515,9 +515,9 @@ namespace storm { storm::expressions::ExprtkExpressionEvaluator evaluator(program.getManager()); while (!stateQueue.empty()) { // Get the current state and unpack it. - std::size_t currentStateBucket = stateQueue.front(); - std::pair stateValuePair = stateInformation.stateToIndexMap.getBucketAndValue(currentStateBucket); - storm::storage::BitVector const& currentState = stateValuePair.first; + storm::storage::BitVector currentState = stateQueue.front(); + stateQueue.pop(); + ValueType stateIndex = stateInformation.stateToIndexMap.getValue(currentState); unpackStateIntoEvaluator(currentState, variableInformation, evaluator); // Retrieve all choices for the current state. @@ -532,7 +532,7 @@ namespace storm { if (!storm::settings::generalSettings().isDontFixDeadlocksSet()) { // Insert empty choice labeling for added self-loop transitions. choiceLabels.push_back(boost::container::flat_set()); - transitionMatrixBuilder.addNextValue(currentRow, stateValuePair.second, storm::utility::one()); + transitionMatrixBuilder.addNextValue(currentRow, stateIndex, storm::utility::one()); ++currentRow; } else { LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."); @@ -649,8 +649,6 @@ namespace storm { } } } - - stateQueue.pop(); } return choiceLabels; @@ -743,7 +741,7 @@ namespace storm { result.addAtomicProposition(label.getName()); } for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) { - unpackStateIntoEvaluator(stateInformation.stateToIndexMap.getBucketAndValue(stateInformation.reachableStates[index]).first, variableInformation, evaluator); + unpackStateIntoEvaluator(stateInformation.reachableStates[index], variableInformation, evaluator); for (auto const& label : labels) { // Add label to state, if the corresponding expression is true. if (evaluator.asBool(label.getStatePredicateExpression())) { @@ -774,7 +772,7 @@ namespace storm { std::vector result(stateInformation.reachableStates.size()); for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) { result[index] = storm::utility::zero(); - unpackStateIntoEvaluator(stateInformation.stateToIndexMap.getBucketAndValue(stateInformation.reachableStates[index]).first, variableInformation, evaluator); + unpackStateIntoEvaluator(stateInformation.reachableStates[index], variableInformation, evaluator); for (auto const& reward : rewards) { // Add this reward to the state if the state is included in the state reward. diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index c7c3912a6..669678394 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -331,7 +331,7 @@ public: } for (auto it = singleLabelings.begin(); it != singleLabelings.end(); ++it) { - boost::hash_combine(result, it->hash()); + boost::hash_combine(result, std::hash()(*it)); } return result; diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index 4f7d4fff8..0cafd4c0c 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -571,10 +571,6 @@ namespace storm { return const_iterator(bucketVector.data(), bitCount, bitCount, false); } - std::size_t BitVector::hash() const { - return boost::hash_range(bucketVector.begin(), bucketVector.end()); - } - uint_fast64_t BitVector::getNextSetIndex(uint_fast64_t startingIndex) const { return getNextSetIndex(bucketVector.data(), startingIndex, bitCount); } @@ -634,6 +630,22 @@ namespace storm { return out; } + + std::size_t NonZeroBitVectorHash::operator()(storm::storage::BitVector const& bv) const { + STORM_LOG_ASSERT(bv.size() > 0, "Cannot hash bit vector of zero size."); + std::size_t result = 0; + + for (uint_fast64_t index = 0; index < bv.bucketVector.size(); ++index) { + result ^= result << 3; + result ^= result >> bv.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::iterator begin, std::vector::iterator end); diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 0312f39f9..1d2583755 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -105,7 +105,7 @@ namespace storm { * @param length The number of bits the bit vector should be able to hold. * @param init The initial value of the first |length| bits. */ - BitVector(uint_fast64_t length, bool init = false); + explicit BitVector(uint_fast64_t length, bool init = false); /*! * Creates a bit vector that has exactly the bits set that are given by the provided input iterator range @@ -425,13 +425,6 @@ namespace storm { */ const_iterator end() const; - /*! - * Calculates a hash value for this bit vector. - * - * @return The hash value of this bit vector. - */ - std::size_t hash() const; - /* * Retrieves the index of the bit that is the next bit set to true in the bit vector. If there is none, * this function returns the number of bits this vector holds in total. Put differently, if the return @@ -445,6 +438,7 @@ namespace storm { friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector); friend struct std::hash; + friend struct NonZeroBitVectorHash; private: /*! @@ -488,6 +482,11 @@ 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/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp index 115d25cd6..e8ef62cae 100644 --- a/src/storage/BitVectorHashMap.cpp +++ b/src/storage/BitVectorHashMap.cpp @@ -40,6 +40,8 @@ namespace storm { ++currentSizeIterator; STORM_LOG_ASSERT(currentSizeIterator != sizes.end(), "Hash map became to big."); + // Create new containers and swap them with the old ones. + numberOfElements = 0; storm::storage::BitVector oldBuckets(bucketSize * *currentSizeIterator); std::swap(oldBuckets, buckets); storm::storage::BitVector oldOccupied = storm::storage::BitVector(*currentSizeIterator); @@ -48,40 +50,87 @@ namespace storm { std::swap(oldValues, values); // Now iterate through the elements and reinsert them in the new storage. - numberOfElements = 0; - for (auto const& bucketIndex : oldOccupied) { - this->findOrAdd(oldBuckets.get(bucketIndex * bucketSize, bucketSize), oldValues[bucketIndex]); + bool fail = false; + for (auto bucketIndex : oldOccupied) { + fail = !this->insertWithoutIncreasingSize(oldBuckets.get(bucketIndex * bucketSize, bucketSize), oldValues[bucketIndex]); + + // If we failed to insert just one element, we have to redo the procedure with a larger container size. + if (fail) { + break; + } + } + + uint_fast64_t failCount = 0; + while (fail) { + ++failCount; + STORM_LOG_ASSERT(failCount < 10, "Increasing size failed too often."); + + ++currentSizeIterator; + STORM_LOG_ASSERT(currentSizeIterator != sizes.end(), "Hash map became to big."); + + numberOfElements = 0; + buckets = storm::storage::BitVector(bucketSize * *currentSizeIterator); + occupied = storm::storage::BitVector(*currentSizeIterator); + values = std::vector(*currentSizeIterator); + + for (auto bucketIndex : oldOccupied) { + fail = !this->insertWithoutIncreasingSize(oldBuckets.get(bucketIndex * bucketSize, bucketSize), oldValues[bucketIndex]); + + // If we failed to insert just one element, we have to redo the procedure with a larger container size. + if (fail) { + continue; + } + } } } template - ValueType BitVectorHashMap::findOrAdd(storm::storage::BitVector const& key, ValueType value) { + bool BitVectorHashMap::insertWithoutIncreasingSize(storm::storage::BitVector const& key, ValueType const& value) { + std::tuple flagBucketTuple = this->findBucketToInsert(key); + if (std::get<2>(flagBucketTuple)) { + return false; + } + + if (std::get<0>(flagBucketTuple)) { + return true; + } else { + // Insert the new bits into the bucket. + buckets.set(std::get<1>(flagBucketTuple) * bucketSize, key); + occupied.set(std::get<1>(flagBucketTuple)); + values[std::get<1>(flagBucketTuple)] = value; + ++numberOfElements; + return true; + } + } + + template + ValueType BitVectorHashMap::findOrAdd(storm::storage::BitVector const& key, ValueType const& value) { return findOrAddAndGetBucket(key, value).first; } template - std::pair BitVectorHashMap::findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType value) { + std::pair BitVectorHashMap::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(); } - std::pair flagBucketPair = this->findBucket(key); - if (flagBucketPair.first) { - return std::make_pair(values[flagBucketPair.second], flagBucketPair.second); + std::tuple flagBucketTuple = this->findBucketToInsert(key); + STORM_LOG_ASSERT(!std::get<2>(flagBucketTuple), "Failed to find bucket for insertion."); + if (std::get<0>(flagBucketTuple)) { + return std::make_pair(values[std::get<1>(flagBucketTuple)], std::get<1>(flagBucketTuple)); } else { // Insert the new bits into the bucket. - buckets.set(flagBucketPair.second * bucketSize, key); - occupied.set(flagBucketPair.second); - values[flagBucketPair.second] = value; + buckets.set(std::get<1>(flagBucketTuple) * bucketSize, key); + occupied.set(std::get<1>(flagBucketTuple)); + values[std::get<1>(flagBucketTuple)] = value; ++numberOfElements; - return std::make_pair(value, flagBucketPair.second); + return std::make_pair(value, std::get<1>(flagBucketTuple)); } } template ValueType BitVectorHashMap::getValue(storm::storage::BitVector const& key) const { - std::cout << "calling getValue with key " << key << std::endl; std::pair flagBucketPair = this->findBucket(key); STORM_LOG_ASSERT(flagBucketPair.first, "Unknown key."); return flagBucketPair.second; @@ -91,18 +140,52 @@ namespace storm { std::pair BitVectorHashMap::findBucket(storm::storage::BitVector const& key) const { uint_fast64_t initialHash = hasher1(key) % *currentSizeIterator; uint_fast64_t bucket = initialHash; - + + uint_fast64_t counter = 0; while (isBucketOccupied(bucket)) { + ++counter; if (buckets.matches(bucket * bucketSize, key)) { return std::make_pair(true, bucket); } bucket += hasher2(key); bucket %= *currentSizeIterator; + + if (bucket == initialHash) { + return std::make_pair(false, bucket); + } } return std::make_pair(false, bucket); } + template + template + std::tuple BitVectorHashMap::findBucketToInsert(storm::storage::BitVector const& key) { + uint_fast64_t initialHash = hasher1(key) % *currentSizeIterator; + uint_fast64_t bucket = initialHash; + + uint_fast64_t counter = 0; + while (isBucketOccupied(bucket)) { + ++counter; + if (buckets.matches(bucket * bucketSize, key)) { + return std::make_tuple(true, bucket, false); + } + bucket += hasher2(key); + bucket %= *currentSizeIterator; + + if (bucket == initialHash) { + if (increaseStorage) { + this->increaseSize(); + bucket = initialHash = hasher1(key) % *currentSizeIterator; + } else { + return std::make_tuple(false, bucket, true); + } + } + } + + return std::make_tuple(false, bucket, false); + } + template std::pair BitVectorHashMap::getBucketAndValue(std::size_t bucket) const { return std::make_pair(buckets.get(bucket * bucketSize, bucketSize), values[bucket]); diff --git a/src/storage/BitVectorHashMap.h b/src/storage/BitVectorHashMap.h index 9d6ea299f..c4b564fab 100644 --- a/src/storage/BitVectorHashMap.h +++ b/src/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, class Hash2 = std::hash> + template, class Hash2 = storm::storage::NonZeroBitVectorHash> class BitVectorHashMap { public: /*! @@ -35,7 +35,7 @@ namespace storm { * @param value The value that is inserted if the key is not already found in the map. * @return The found value if the key is already contained in the map and the provided new value otherwise. */ - ValueType findOrAdd(storm::storage::BitVector const& key, ValueType value); + ValueType findOrAdd(storm::storage::BitVector const& key, ValueType const& value); /*! * Searches for the given key in the map. If it is found, the mapped-to value is returned. Otherwise, the @@ -47,7 +47,7 @@ namespace storm { * the provided new value otherwise and whose second component is the index of the bucket into which the key * was inserted. */ - std::pair findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType value); + std::pair findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType const& value); /*! * Retrieves the key stored in the given bucket (if any) and the value it is mapped to. @@ -89,14 +89,38 @@ namespace storm { bool isBucketOccupied(uint_fast64_t bucket) const; /*! - * Searches for the bucket into which the given key can be inserted. + * Searches for the bucket with the given key. * * @param key The key to search for. * @return A pair whose first component indicates whether the key is already contained in the map and whose - * second component indicates in which bucket the key is stored/is supposed to be stored. + * second component indicates in which bucket the key is stored. */ std::pair findBucket(storm::storage::BitVector const& key) const; + /*! + * Searches for the bucket into which the given key can be inserted. If no empty bucket can be found, the + * size of the underlying data structure is increased. + * + * @param key The key to search for. + * @param increaseStorage A flag indicating whether the storage should be increased if no bucket can be found. + * @return A tuple whose first component indicates whether the key is already contained in the map, whose + * second component indicates in which bucket the key is supposed to be stored and whose third component is + * an error flag indicating that the bucket could not be found (e.g. due to the restriction that the storage + * must not be increased). + */ + template + std::tuple findBucketToInsert(storm::storage::BitVector const& key); + + /*! + * Inserts the given key-value pair without resizing the underlying storage. If that fails, this is + * indicated by the return value. + * + * @param key The key to insert. + * @param value The value to insert. + * @return True iff the key-value pair could be inserted without resizing the storage. + */ + bool insertWithoutIncreasingSize(storm::storage::BitVector const& key, ValueType const& value); + /*! * Increases the size of the hash map and performs the necessary rehashing of all entries. */