Fixed some bugs.

Former-commit-id: dce463081d

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<std::size_t> reachableStates;
+                std::vector<storm::storage::BitVector> reachableStates;
                 
                 // A list of initial states in terms of their global indices.
                 std::vector<uint32_t> 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<std::size_t>& stateQueue) {
+            static uint32_t getOrAddStateIndex(StateType const& state, StateInformation& stateInformation, std::queue<storm::storage::BitVector>& stateQueue) {
                 uint32_t newIndex = stateInformation.reachableStates.size();
                 
                 // Check, if the state was already registered.
                 std::pair<uint32_t, std::size_t> 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<Choice<ValueType>> getUnlabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue<std::size_t>& stateQueue) {
+            static std::vector<Choice<ValueType>> getUnlabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue<storm::storage::BitVector>& stateQueue) {
                 std::vector<Choice<ValueType>> result;
 
                 // Iterate over all modules.
@@ -382,7 +382,7 @@ namespace storm {
                 return result;
             }
             
-            static std::vector<Choice<ValueType>> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue<std::size_t>& stateQueue) {
+            static std::vector<Choice<ValueType>> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue<storm::storage::BitVector>& stateQueue) {
                 std::vector<Choice<ValueType>> result;
                 
                 for (uint_fast64_t actionIndex : program.getActionIndices()) {
@@ -495,7 +495,7 @@ namespace storm {
                 std::vector<boost::container::flat_set<uint_fast64_t>> choiceLabels;
                 
                 // Initialize a queue and insert the initial state.
-                std::queue<std::size_t> stateQueue;
+                std::queue<storm::storage::BitVector> 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<storm::storage::BitVector, uint32_t> 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<uint_fast64_t>());
-                            transitionMatrixBuilder.addNextValue(currentRow, stateValuePair.second, storm::utility::one<ValueType>());
+                            transitionMatrixBuilder.addNextValue(currentRow, stateIndex, storm::utility::one<ValueType>());
                             ++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<ValueType> result(stateInformation.reachableStates.size());
                 for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) {
                     result[index] = storm::utility::zero<ValueType>();
-                    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.

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<storm::storage::BitVector>()(*it));
 		}
 
 		return result;

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<uint_fast64_t>::iterator begin, std::vector<uint_fast64_t>::iterator end);

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<storm::storage::BitVector>;
+            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
 

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<ValueType>(*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<class ValueType, class Hash1, class Hash2>
-        ValueType BitVectorHashMap<ValueType, Hash1, Hash2>::findOrAdd(storm::storage::BitVector const& key, ValueType value) {
+        bool BitVectorHashMap<ValueType, Hash1, Hash2>::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;
+            }
+            
+            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<class ValueType, class Hash1, class Hash2>
+        ValueType BitVectorHashMap<ValueType, Hash1, Hash2>::findOrAdd(storm::storage::BitVector const& key, ValueType const& value) {
             return findOrAddAndGetBucket(key, value).first;
         }
         
         template<class ValueType, class Hash1, class Hash2>
-        std::pair<ValueType, std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType value) {
+        std::pair<ValueType, std::size_t> BitVectorHashMap<ValueType, Hash1, Hash2>::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<bool, std::size_t> flagBucketPair = this->findBucket(key);
-            if (flagBucketPair.first) {
-                return std::make_pair(values[flagBucketPair.second], flagBucketPair.second);
+            std::tuple<bool, std::size_t, bool> flagBucketTuple = this->findBucketToInsert<true>(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<class ValueType, class Hash1, class Hash2>
         ValueType BitVectorHashMap<ValueType, Hash1, Hash2>::getValue(storm::storage::BitVector const& key) const {
-            std::cout << "calling getValue with key " << key << std::endl;
             std::pair<bool, std::size_t> flagBucketPair = this->findBucket(key);
             STORM_LOG_ASSERT(flagBucketPair.first, "Unknown key.");
             return flagBucketPair.second;
@@ -91,18 +140,52 @@ namespace storm {
         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 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<class ValueType, class Hash1, class Hash2>
+        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 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<class ValueType, class Hash1, class Hash2>
         std::pair<storm::storage::BitVector, ValueType> BitVectorHashMap<ValueType, Hash1, Hash2>::getBucketAndValue(std::size_t bucket) const {
             return std::make_pair(buckets.get(bucket * bucketSize, bucketSize), values[bucket]);

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 ValueType, class Hash1 = std::hash<storm::storage::BitVector>, class Hash2 = std::hash<storm::storage::BitVector>>
+        template<class ValueType, class Hash1 = std::hash<storm::storage::BitVector>, 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<ValueType, std::size_t> findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType value);
+            std::pair<ValueType, std::size_t> 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<bool, std::size_t> 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<bool increaseStorage>
+            std::tuple<bool, std::size_t, bool> 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.
              */