Further tests for DD layer and bugfixing.

Former-commit-id: 752a8c55ac

src/storage/dd/CuddDdManager.cpp

@@ -57,7 +57,7 @@ namespace storm {
 
         void DdManager<CUDD>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) {
             // Check whether a meta variable already exists.
-            if (this->containsMetaVariable(name)) {
+            if (this->hasMetaVariable(name)) {
                 throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << name << "' already exists.";
             }
 
@@ -66,7 +66,7 @@ namespace storm {
                 throw storm::exceptions::InvalidArgumentException() << "Range of meta variable must be at least 2 elements.";
             }
             
-            std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low)));
+            std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
             
             std::vector<Dd<CUDD>> variables;
             for (std::size_t i = 0; i < numberOfBits; ++i) {
@@ -96,13 +96,13 @@ namespace storm {
 
             // Check whether a meta variable already exists.
             for (auto const& metaVariableName : names) {
-                if (this->containsMetaVariable(metaVariableName)) {
+                if (this->hasMetaVariable(metaVariableName)) {
                     throw storm::exceptions::InvalidArgumentException() << "A meta variable '" << metaVariableName << "' already exists.";
                 }
             }
             
             // Add the variables in interleaved order.
-            std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low)));
+            std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
             std::vector<std::vector<Dd<CUDD>>> variables(names.size());
             for (uint_fast64_t bit = 0; bit < numberOfBits; ++bit) {
                 for (uint_fast64_t i = 0; i < names.size(); ++i) {
@@ -119,7 +119,7 @@ namespace storm {
         DdMetaVariable<CUDD> const& DdManager<CUDD>::getMetaVariable(std::string const& metaVariableName) const {
             auto const& nameVariablePair = metaVariableMap.find(metaVariableName);
             
-            if (!this->containsMetaVariable(metaVariableName)) {
+            if (!this->hasMetaVariable(metaVariableName)) {
                 throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name.";
             }
             
@@ -138,7 +138,7 @@ namespace storm {
             return this->metaVariableMap.size();
         }
         
-        bool DdManager<CUDD>::containsMetaVariable(std::string const& metaVariableName) const {
+        bool DdManager<CUDD>::hasMetaVariable(std::string const& metaVariableName) const {
             return this->metaVariableMap.find(metaVariableName) != this->metaVariableMap.end();
         }
         

src/storage/dd/CuddDdManager.h

@@ -119,7 +119,7 @@ namespace storm {
              * @param metaVariableName The meta variable name whose membership to query.
              * @return True if the given meta variable name is managed by this manager.
              */
-            bool containsMetaVariable(std::string const& metaVariableName) const;
+            bool hasMetaVariable(std::string const& metaVariableName) const;
             
         private:
             /*!

src/storage/dd/DdMetaVariable.h

@@ -68,13 +68,13 @@ namespace storm {
              */
             std::shared_ptr<DdManager<Type>> getDdManager() const;
             
-            
             /*!
              * Retrieves the number of DD variables for this meta variable.
              *
              * @return The number of DD variables for this meta variable.
              */
             std::size_t getNumberOfDdVariables() const;
+            
         private:
             /*!
              * Retrieves the variables used to encode the meta variable.

test/functional/storage/CuddDdTest.cpp

@@ -36,7 +36,7 @@ TEST(CuddDdManager, Constants) {
     EXPECT_EQ(2, two.getMax());
 }
 
-TEST(CuddDdManager, AddMetaVariableTest) {
+TEST(CuddDdManager, MetaVariableTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());
     
     ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9));
@@ -51,4 +51,21 @@ TEST(CuddDdManager, AddMetaVariableTest) {
     names = {"y", "y'"};
     ASSERT_NO_THROW(manager->addMetaVariablesInterleaved(names, 0, 3));
     EXPECT_EQ(3, manager->getNumberOfMetaVariables());
-}
+    
+    EXPECT_FALSE(manager->hasMetaVariable("x'"));
+    EXPECT_TRUE(manager->hasMetaVariable("y'"));
+    
+    std::set<std::string> metaVariableSet = {"x", "y", "y'"};
+    EXPECT_EQ(metaVariableSet, manager->getAllMetaVariableNames());
+    
+    ASSERT_THROW(storm::dd::DdMetaVariable<storm::dd::CUDD> const& metaVariableX = manager->getMetaVariable("x'"), storm::exceptions::InvalidArgumentException);
+    ASSERT_NO_THROW(storm::dd::DdMetaVariable<storm::dd::CUDD> const& metaVariableX = manager->getMetaVariable("x"));
+    storm::dd::DdMetaVariable<storm::dd::CUDD> const& metaVariableX = manager->getMetaVariable("x");
+    
+    EXPECT_EQ(1, metaVariableX.getLow());
+    EXPECT_EQ(9, metaVariableX.getHigh());
+    EXPECT_EQ("x", metaVariableX.getName());
+    EXPECT_EQ(manager, metaVariableX.getDdManager());
+    EXPECT_EQ(4, metaVariableX.getNumberOfDdVariables());
+}
+