Merge branch 'master' into lpsolverInterface

Former-commit-id: 09c7d170b8

src/storage/dd/CuddDd.cpp

@@ -473,15 +473,15 @@ namespace storm {
             return this->ddManager;
         }
         
-        DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::begin() const {
+        DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::begin(bool enumerateDontCareMetaVariables) const {
             int* cube;
             double value;
             DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value);
-            return DdForwardIterator<DdType::CUDD>(this->getDdManager(), generator, cube, value, Cudd_IsGenEmpty(generator), &this->getContainedMetaVariableNames());
+            return DdForwardIterator<DdType::CUDD>(this->getDdManager(), generator, cube, value, Cudd_IsGenEmpty(generator), &this->getContainedMetaVariableNames(), enumerateDontCareMetaVariables);
         }
         
-        DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::end() const {
-            return DdForwardIterator<DdType::CUDD>(this->getDdManager(), nullptr, nullptr, 0, true, nullptr);
+        DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::end(bool enumerateDontCareMetaVariables) const {
+            return DdForwardIterator<DdType::CUDD>(this->getDdManager(), nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables);
         }
         
         std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd) {

src/storage/dd/CuddDd.h

@@ -440,16 +440,20 @@ namespace storm {
             /*!
              * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value.
              *
+             * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
+             * if a meta variable does not at all influence the the function value.
              * @return An iterator that points to the first meta variable assignment with a non-zero function value.
              */
-            DdForwardIterator<DdType::CUDD> begin() const;
+            DdForwardIterator<DdType::CUDD> begin(bool enumerateDontCareMetaVariables = true) const;
             
             /*!
              * Retrieves an iterator that points past the end of the container.
              *
+             * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
+             * if a meta variable does not at all influence the the function value.
              * @return An iterator that points past the end of the container.
              */
-            DdForwardIterator<DdType::CUDD> end() const;
+            DdForwardIterator<DdType::CUDD> end(bool enumerateDontCareMetaVariables = true) const;
             
             friend std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd);
         private:

src/storage/dd/CuddDdForwardIterator.cpp

@@ -5,7 +5,11 @@
 
 namespace storm {
     namespace dd {
-        DdForwardIterator<DdType::CUDD>::DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<std::string> const* metaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation() {
+        DdForwardIterator<DdType::CUDD>::DdForwardIterator() : ddManager(), generator(), cube(), value(), isAtEnd(), metaVariables(), enumerateDontCareMetaVariables(), cubeCounter(), relevantDontCareDdVariables(), currentValuation() {
+            // Intentionally left empty.
+        }
+        
+        DdForwardIterator<DdType::CUDD>::DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<std::string> const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(ddManager), generator(generator), cube(cube), value(value), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation() {
             // If the given generator is not yet at its end, we need to create the current valuation from the cube from
             // scratch.
             if (!this->isAtEnd) {
@@ -49,6 +53,7 @@ namespace storm {
         }
         
         DdForwardIterator<DdType::CUDD>::~DdForwardIterator() {
+            // We free the pointers sind Cudd allocates them using malloc rather than new/delete.
             if (this->cube != nullptr) {
                 free(this->cube);
             }
@@ -108,29 +113,60 @@ namespace storm {
             // don't cares. In the latter case, we add them to a special list, so we can iterate over their concrete
             // valuations later.
             for (auto const& metaVariableName : *this->metaVariables) {
+                bool metaVariableAppearsInCube = false;
+                std::vector<std::tuple<ADD, std::string, uint_fast64_t>> localRelenvantDontCareDdVariables;
                 auto const& metaVariable = this->ddManager->getMetaVariable(metaVariableName);
                 if (metaVariable.getType() == DdMetaVariable<DdType::CUDD>::MetaVariableType::Bool) {
                     if (this->cube[metaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 0) {
-                        currentValuation.setBooleanValue(metaVariableName, false);
+                        metaVariableAppearsInCube = true;
+                        if (!currentValuation.containsBooleanIdentifier(metaVariableName)) {
+                            currentValuation.addBooleanIdentifier(metaVariableName, false);
+                        } else {
+                            currentValuation.setBooleanValue(metaVariableName, false);
+                        }
                     } else if (this->cube[metaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 1) {
-                        currentValuation.setBooleanValue(metaVariableName, true);
+                        metaVariableAppearsInCube = true;
+                        if (!currentValuation.containsBooleanIdentifier(metaVariableName)) {
+                            currentValuation.addBooleanIdentifier(metaVariableName, true);
+                        } else {
+                            currentValuation.setBooleanValue(metaVariableName, true);
+                        }
                     } else {
-                        relevantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[0].getCuddAdd(), metaVariableName, 0));
+                        localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[0].getCuddAdd(), metaVariableName, 0));
                     }
                 } else {
                     int_fast64_t intValue = 0;
                     for (uint_fast64_t bitIndex = 0; bitIndex < metaVariable.getNumberOfDdVariables(); ++bitIndex) {
                         if (cube[metaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 0) {
                             // Leave bit unset.
+                            metaVariableAppearsInCube = true;
                         } else if (cube[metaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 1) {
                             intValue |= 1ull << (metaVariable.getNumberOfDdVariables() - bitIndex - 1);
+                            metaVariableAppearsInCube = true;
                         } else {
                             // Temporarily leave bit unset so we can iterate trough the other option later.
                             // Add the bit to the relevant don't care bits.
-                            this->relevantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[bitIndex].getCuddAdd(), metaVariableName, metaVariable.getNumberOfDdVariables() - bitIndex - 1));
+                            localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable.getDdVariables()[bitIndex].getCuddAdd(), metaVariableName, metaVariable.getNumberOfDdVariables() - bitIndex - 1));
                         }
                     }
-                    currentValuation.setIntegerValue(metaVariableName, intValue + metaVariable.getLow());
+                    if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) {
+                        if (!currentValuation.containsIntegerIdentifier(metaVariableName)) {
+                            currentValuation.addIntegerIdentifier(metaVariableName);
+                        }
+                        currentValuation.setIntegerValue(metaVariableName, intValue + metaVariable.getLow());
+                    }
+                }
+                
+                // If all meta variables are to be enumerated or the meta variable appeared in the cube, we register the
+                // missing bits to later enumerate all possible valuations.
+                if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) {
+                    relevantDontCareDdVariables.insert(relevantDontCareDdVariables.end(), localRelenvantDontCareDdVariables.begin(), localRelenvantDontCareDdVariables.end());
+                }
+                
+                // If the meta variable does not appear in the cube and we're not supposed to enumerate such meta variables
+                // we remove the meta variable from the valuation.
+                if (!this->enumerateDontCareMetaVariables && !metaVariableAppearsInCube) {
+                    currentValuation.removeIdentifier(metaVariableName);
                 }
             }
             

src/storage/dd/CuddDdForwardIterator.h

@@ -25,7 +25,7 @@ namespace storm {
             friend class Dd<DdType::CUDD>;
 
             // Default-instantiate the constructor.
-            DdForwardIterator() = default;
+            DdForwardIterator();
             
             // Forbid copy-construction and copy assignment, because ownership of the internal pointer is unclear then.
             DdForwardIterator(DdForwardIterator<DdType::CUDD> const& other) = delete;
@@ -82,8 +82,10 @@ namespace storm {
              * @param isAtEnd A flag that indicates whether the iterator is at its end and may not be moved forward any
              * more.
              * @param metaVariables The meta variables that appear in the DD.
+             * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
+             * if a meta variable does not at all influence the the function value.
              */
-            DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<std::string> const* metaVariables = nullptr);
+            DdForwardIterator(std::shared_ptr<DdManager<DdType::CUDD>> ddManager, DdGen* generator, int* cube, double value, bool isAtEnd, std::set<std::string> const* metaVariables = nullptr, bool enumerateDontCareMetaVariables = true);
             
             /*!
              * Recreates the internal information when a new cube needs to be treated.
@@ -114,6 +116,10 @@ namespace storm {
             // The set of meta variables appearing in the DD.
             std::set<std::string> const* metaVariables;
             
+            // A flag that indicates whether the iterator is supposed to enumerate meta variable valuations even if
+            // they don't influence the function value.
+            bool enumerateDontCareMetaVariables;
+            
             // A number that represents how many assignments of the current cube have already been returned previously.
             // This is needed, because cubes may represent many assignments (if they have don't care variables).
             uint_fast64_t cubeCounter;

src/storage/expressions/SimpleValuation.cpp

@@ -2,102 +2,109 @@
 #include "src/storage/expressions/SimpleValuation.h"
 #include "src/exceptions/ExceptionMacros.h"
 #include "src/exceptions/InvalidArgumentException.h"
+#include "src/exceptions/InvalidAccessException.h"
 
 namespace storm {
     namespace expressions {
-        SimpleValuation::SimpleValuation() : booleanIdentifierToIndexMap(new std::unordered_map<std::string, uint_fast64_t>()), integerIdentifierToIndexMap(new std::unordered_map<std::string, uint_fast64_t>()), doubleIdentifierToIndexMap(new std::unordered_map<std::string, uint_fast64_t>()), booleanValues(), integerValues(), doubleValues() {
-            // Intentionally left empty.
-        }
-        
         bool SimpleValuation::operator==(SimpleValuation const& other) const {
-            return this->booleanIdentifierToIndexMap.get() == other.booleanIdentifierToIndexMap.get() && this->integerIdentifierToIndexMap.get() == other.integerIdentifierToIndexMap.get() && this->doubleIdentifierToIndexMap.get() == other.doubleIdentifierToIndexMap.get() && this->booleanValues == other.booleanValues && this->integerValues == other.integerValues && this->doubleValues == other.doubleValues;
+            return this->identifierToValueMap == other.identifierToValueMap;
         }
         
         void SimpleValuation::addBooleanIdentifier(std::string const& name, bool initialValue) {
-            LOG_THROW(this->booleanIdentifierToIndexMap->find(name) == this->booleanIdentifierToIndexMap->end(), storm::exceptions::InvalidArgumentException, "Boolean identifier '" << name << "' already registered.");
-            
-            this->booleanIdentifierToIndexMap->emplace(name, this->booleanValues.size());
-            this->booleanValues.push_back(initialValue);
+            LOG_THROW(this->identifierToValueMap.find(name) == this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Identifier '" << name << "' already registered.");
+            this->identifierToValueMap.emplace(name, initialValue);
         }
         
         void SimpleValuation::addIntegerIdentifier(std::string const& name, int_fast64_t initialValue) {
-            LOG_THROW(this->booleanIdentifierToIndexMap->find(name) == this->booleanIdentifierToIndexMap->end(), storm::exceptions::InvalidArgumentException, "Integer identifier '" << name << "' already registered.");
-
-            this->integerIdentifierToIndexMap->emplace(name, this->integerValues.size());
-            this->integerValues.push_back(initialValue);
+            LOG_THROW(this->identifierToValueMap.find(name) == this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Identifier '" << name << "' already registered.");
+            this->identifierToValueMap.emplace(name, initialValue);
         }
         
         void SimpleValuation::addDoubleIdentifier(std::string const& name, double initialValue) {
-            LOG_THROW(this->booleanIdentifierToIndexMap->find(name) == this->booleanIdentifierToIndexMap->end(), storm::exceptions::InvalidArgumentException, "Double identifier '" << name << "' already registered.");
-
-            this->doubleIdentifierToIndexMap->emplace(name, this->doubleValues.size());
-            this->doubleValues.push_back(initialValue);
+            LOG_THROW(this->identifierToValueMap.find(name) == this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Identifier '" << name << "' already registered.");
+            this->identifierToValueMap.emplace(name, initialValue);
         }
         
         void SimpleValuation::setBooleanValue(std::string const& name, bool value) {
-            this->booleanValues[this->booleanIdentifierToIndexMap->at(name)] = value;
+            this->identifierToValueMap[name] = value;
         }
         
         void SimpleValuation::setIntegerValue(std::string const& name, int_fast64_t value) {
-            this->integerValues[this->integerIdentifierToIndexMap->at(name)] = value;
+            this->identifierToValueMap[name] = value;
         }
         
         void SimpleValuation::setDoubleValue(std::string const& name, double value) {
-            this->doubleValues[this->doubleIdentifierToIndexMap->at(name)] = value;
+            this->identifierToValueMap[name] = value;
+        }
+        
+        void SimpleValuation::removeIdentifier(std::string const& name) {
+            auto nameValuePair = this->identifierToValueMap.find(name);
+            LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidArgumentException, "Deleting unknown identifier '" << name << "'.");
+            this->identifierToValueMap.erase(nameValuePair);
+        }
+        
+        bool SimpleValuation::containsBooleanIdentifier(std::string const& name) const {
+            auto nameValuePair = this->identifierToValueMap.find(name);
+            if (nameValuePair == this->identifierToValueMap.end()) {
+                return false;
+            }
+            return nameValuePair->second.type() == typeid(bool);
+        }
+        
+        bool SimpleValuation::containsIntegerIdentifier(std::string const& name) const {
+            auto nameValuePair = this->identifierToValueMap.find(name);
+            if (nameValuePair == this->identifierToValueMap.end()) {
+                return false;
+            }
+            return nameValuePair->second.type() == typeid(int_fast64_t);
+        }
+        
+        bool SimpleValuation::containsDoubleIdentifier(std::string const& name) const {
+            auto nameValuePair = this->identifierToValueMap.find(name);
+            if (nameValuePair == this->identifierToValueMap.end()) {
+                return false;
+            }
+            return nameValuePair->second.type() == typeid(double);
         }
         
         bool SimpleValuation::getBooleanValue(std::string const& name) const {
-            auto const& nameIndexPair = this->booleanIdentifierToIndexMap->find(name);
-            return this->booleanValues[nameIndexPair->second];
+            auto nameValuePair = this->identifierToValueMap.find(name);
+            LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'.");
+            return boost::get<bool>(nameValuePair->second);
         }
         
         int_fast64_t SimpleValuation::getIntegerValue(std::string const& name) const {
-            auto const& nameIndexPair = this->integerIdentifierToIndexMap->find(name);
-            return this->integerValues[nameIndexPair->second];
+            auto nameValuePair = this->identifierToValueMap.find(name);
+            LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'.");
+            return boost::get<int_fast64_t>(nameValuePair->second);
         }
         
         double SimpleValuation::getDoubleValue(std::string const& name) const {
-            auto const& nameIndexPair = this->doubleIdentifierToIndexMap->find(name);
-            return this->doubleValues[nameIndexPair->second];
+            auto nameValuePair = this->identifierToValueMap.find(name);
+            LOG_THROW(nameValuePair != this->identifierToValueMap.end(), storm::exceptions::InvalidAccessException, "Access to unkown identifier '" << name << "'.");
+            return boost::get<double>(nameValuePair->second);
         }
         
         std::ostream& operator<<(std::ostream& stream, SimpleValuation const& valuation) {
-            stream << "valuation { bool [";
-            if (!valuation.booleanValues.empty()) {
-                for (uint_fast64_t i = 0; i < valuation.booleanValues.size() - 1; ++i) {
-                    stream << valuation.booleanValues[i] << ", ";
-                }
-                stream << valuation.booleanValues.back();
-            }
-            stream << "] int [";
-            if (!valuation.integerValues.empty()) {
-                for (uint_fast64_t i = 0; i < valuation.integerValues.size() - 1; ++i) {
-                    stream << valuation.integerValues[i] << ", ";
-                }
-                stream << valuation.integerValues.back();
-            }
-            stream << "] double [";
-            if (!valuation.doubleValues.empty()) {
-                for (uint_fast64_t i = 0; i < valuation.doubleValues.size() - 1; ++i) {
-                    stream << valuation.doubleValues[i] << ", ";
+            stream << "{ ";
+            uint_fast64_t elementIndex = 0;
+            for (auto const& nameValuePair : valuation.identifierToValueMap) {
+                stream << nameValuePair.first << " -> " << nameValuePair.second << " ";
+                ++elementIndex;
+                if (elementIndex < valuation.identifierToValueMap.size()) {
+                    stream << ", ";
                 }
-                stream << valuation.doubleValues.back();
             }
-            stream << "] }";
+            stream << "}";
             
             return stream;
         }
         
         std::size_t SimpleValuationPointerHash::operator()(SimpleValuation* valuation) const {
             size_t seed = 0;
-            for (auto const& value : valuation->booleanValues) {
-                boost::hash_combine<bool>(seed, value);
-            }
-            for (auto const& value : valuation->integerValues) {
-                boost::hash_combine<int_fast64_t>(seed, value);
-            }
-            for (auto const& value : valuation->doubleValues) {
-                boost::hash_combine<double>(seed, value);
+            for (auto const& nameValuePair : valuation->identifierToValueMap) {
+                boost::hash_combine(seed, nameValuePair.first);
+                boost::hash_combine(seed, nameValuePair.second);
             }
             return seed;
         }
@@ -107,21 +114,7 @@ namespace storm {
         }
         
         bool SimpleValuationPointerLess::operator()(SimpleValuation* valuation1, SimpleValuation* valuation2) const {
-            // Compare boolean variables.
-            bool less = valuation1->booleanValues < valuation2->booleanValues;
-            if (less) {
-                return true;
-            }
-            less = valuation1->integerValues < valuation2->integerValues;
-            if (less) {
-                return true;
-            }
-            less = valuation1->doubleValues < valuation2->doubleValues;
-            if (less) {
-                return true;
-            } else {
-                return false;
-            }
+            return valuation1->identifierToValueMap < valuation2->identifierToValueMap;
         }
     }
 }

src/storage/expressions/SimpleValuation.h

@@ -1,9 +1,8 @@
 #ifndef STORM_STORAGE_EXPRESSIONS_SIMPLEVALUATION_H_
 #define STORM_STORAGE_EXPRESSIONS_SIMPLEVALUATION_H_
 
-#include <memory>
-#include <vector>
-#include <unordered_map>
+#include <boost/container/flat_map.hpp>
+#include <boost/variant.hpp>
 #include <iostream>
 
 #include "src/storage/expressions/Valuation.h"
@@ -16,12 +15,8 @@ namespace storm {
             friend class SimpleValuationPointerHash;
             friend class SimpleValuationPointerLess;
             
-            /*!
-             * Creates a simple valuation without any identifiers.
-            */
-            SimpleValuation();
-
             // Instantiate some constructors and assignments with their default implementations.
+            SimpleValuation() = default;
             SimpleValuation(SimpleValuation const&) = default;
             SimpleValuation& operator=(SimpleValuation const&) = default;
 #ifndef WINDOWS            
@@ -83,7 +78,17 @@ namespace storm {
              */
             void setDoubleValue(std::string const& name, double value);
             
+            /*!
+             * Removes the given identifier from this valuation.
+             *
+             * @param name The name of the identifier that is to be removed.
+             */
+            void removeIdentifier(std::string const& name);
+            
             // Override base class methods.
+            virtual bool containsBooleanIdentifier(std::string const& name) const override;
+            virtual bool containsIntegerIdentifier(std::string const& name) const override;
+            virtual bool containsDoubleIdentifier(std::string const& name) const override;
             virtual bool getBooleanValue(std::string const& name) const override;
             virtual int_fast64_t getIntegerValue(std::string const& name) const override;
             virtual double getDoubleValue(std::string const& name) const override;
@@ -92,22 +97,7 @@ namespace storm {
 
         private:
             // A mapping of boolean identifiers to their local indices in the value container.
-            std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> booleanIdentifierToIndexMap;
-            
-            // A mapping of integer identifiers to their local indices in the value container.
-            std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> integerIdentifierToIndexMap;
-            
-            // A mapping of double identifiers to their local indices in the value container.
-            std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> doubleIdentifierToIndexMap;
-            
-            // The value container for all boolean identifiers.
-            std::vector<bool> booleanValues;
-            
-            // The value container for all integer identifiers.
-            std::vector<int_fast64_t> integerValues;
-            
-            // The value container for all double identifiers.
-            std::vector<double> doubleValues;
+            boost::container::flat_map<std::string, boost::variant<bool, int_fast64_t, double>> identifierToValueMap;
         };
         
         /*!

src/storage/expressions/Valuation.h

@@ -34,6 +34,31 @@ namespace storm {
              * @return The value of the double identifier.
              */
             virtual double getDoubleValue(std::string const& name) const = 0;
+            
+            /*!
+             * Retrieves whether there exists a boolean identifier with the given name in the valuation.
+             *
+             * @param name The name of the boolean identifier to query.
+             * @return True iff the identifier exists and is of boolean type.
+             */
+            virtual bool containsBooleanIdentifier(std::string const& name) const = 0;
+            
+            /*!
+             * Retrieves whether there exists a integer identifier with the given name in the valuation.
+             *
+             * @param name The name of the integer identifier to query.
+             * @return True iff the identifier exists and is of boolean type.
+             */
+            virtual bool containsIntegerIdentifier(std::string const& name) const = 0;
+            
+            /*!
+             * Retrieves whether there exists a double identifier with the given name in the valuation.
+             *
+             * @param name The name of the double identifier to query.
+             * @return True iff the identifier exists and is of boolean type.
+             */
+            virtual bool containsDoubleIdentifier(std::string const& name) const = 0;
+
         };
     }
 }

test/functional/storage/CuddDdTest.cpp

@@ -307,4 +307,26 @@ TEST(CuddDd, ForwardIteratorTest) {
         ++numberOfValuations;
     }
     EXPECT_EQ(9, numberOfValuations);
+
+    dd = manager->getRange("x");
+    dd = dd.ite(manager->getOne(), manager->getOne());
+    ASSERT_NO_THROW(it = dd.begin());
+    ASSERT_NO_THROW(ite = dd.end());
+    numberOfValuations = 0;
+    while (it != ite) {
+        ASSERT_NO_THROW(valuationValuePair = *it);
+        ASSERT_NO_THROW(++it);
+        ++numberOfValuations;
+    }
+    EXPECT_EQ(16, numberOfValuations);
+    
+    ASSERT_NO_THROW(it = dd.begin(false));
+    ASSERT_NO_THROW(ite = dd.end());
+    numberOfValuations = 0;
+    while (it != ite) {
+        ASSERT_NO_THROW(valuationValuePair = *it);
+        ASSERT_NO_THROW(++it);
+        ++numberOfValuations;
+    }
+    EXPECT_EQ(1, numberOfValuations);
 }