Further bugfixes and tests for DD layer.

Former-commit-id: 32ef63f9b1

src/storage/dd/CuddDd.cpp

@@ -12,7 +12,7 @@ namespace storm {
         }
         
         bool Dd<CUDD>::operator==(Dd<CUDD> const& other) const {
-            return this->getCuddAdd() == other.getCuddAdd();
+            return this->cuddAdd == other.getCuddAdd();
         }
         
         Dd<CUDD> Dd<CUDD>::operator+(Dd<CUDD> const& other) const {
@@ -22,7 +22,7 @@ namespace storm {
         }
         
         Dd<CUDD>& Dd<CUDD>::operator+=(Dd<CUDD> const& other) {
-            this->getCuddAdd() += other.getCuddAdd();
+            this->cuddAdd += other.getCuddAdd();
             
             // Join the variable sets of the two participating DDs.
             this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
@@ -37,7 +37,7 @@ namespace storm {
         }
         
         Dd<CUDD>& Dd<CUDD>::operator*=(Dd<CUDD> const& other) {
-            this->getCuddAdd() *= other.getCuddAdd();
+            this->cuddAdd *= other.getCuddAdd();
             
             // Join the variable sets of the two participating DDs.
             this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
@@ -52,7 +52,7 @@ namespace storm {
         }
         
         Dd<CUDD>& Dd<CUDD>::operator-=(Dd<CUDD> const& other) {
-            this->getCuddAdd() -= other.getCuddAdd();
+            this->cuddAdd -= other.getCuddAdd();
             
             // Join the variable sets of the two participating DDs.
             this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
@@ -67,7 +67,7 @@ namespace storm {
         }
         
         Dd<CUDD>& Dd<CUDD>::operator/=(Dd<CUDD> const& other) {
-            this->getCuddAdd().Divide(other.getCuddAdd());
+            this->cuddAdd.Divide(other.getCuddAdd());
             
             // Join the variable sets of the two participating DDs.
             this->getContainedMetaVariableNames().insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
@@ -82,7 +82,7 @@ namespace storm {
         }
         
         Dd<CUDD>& Dd<CUDD>::complement() {
-            this->getCuddAdd() = ~this->getCuddAdd();
+            this->cuddAdd = ~this->cuddAdd;
             return *this;
         }
         
@@ -136,7 +136,7 @@ namespace storm {
                 cubeDd *= metaVariable.getCube();
             }
             
-            this->getCuddAdd().OrAbstract(cubeDd.getCuddAdd());
+            this->cuddAdd.OrAbstract(cubeDd.getCuddAdd());
         }
         
         void Dd<CUDD>::sumAbstract(std::set<std::string> const& metaVariableNames) {
@@ -153,7 +153,7 @@ namespace storm {
                 cubeDd *= metaVariable.getCube();
             }
             
-            this->getCuddAdd().ExistAbstract(cubeDd.getCuddAdd());
+            this->cuddAdd.ExistAbstract(cubeDd.getCuddAdd());
         }
         
         void Dd<CUDD>::minAbstract(std::set<std::string> const& metaVariableNames) {
@@ -170,7 +170,7 @@ namespace storm {
                 cubeDd *= metaVariable.getCube();
             }
             
-            this->getCuddAdd().Minimum(cubeDd.getCuddAdd());
+            this->cuddAdd.Minimum(cubeDd.getCuddAdd());
         }
         
         void Dd<CUDD>::maxAbstract(std::set<std::string> const& metaVariableNames) {
@@ -187,7 +187,7 @@ namespace storm {
                 cubeDd *= metaVariable.getCube();
             }
             
-            this->getCuddAdd().Maximum(cubeDd.getCuddAdd());
+            this->cuddAdd.Maximum(cubeDd.getCuddAdd());
         }
         
         void Dd<CUDD>::swapVariables(std::vector<std::pair<std::string, std::string>> const& metaVariablePairs) {
@@ -223,7 +223,7 @@ namespace storm {
             }
             
             // Finally, call CUDD to swap the variables.
-            this->getCuddAdd().SwapVariables(from, to);
+            this->cuddAdd.SwapVariables(from, to);
         }
         
         Dd<CUDD> Dd<CUDD>::multiplyMatrix(Dd<CUDD> const& otherMatrix, std::set<std::string> const& summationMetaVariableNames) {
@@ -241,7 +241,7 @@ namespace storm {
             std::set<std::string> containedMetaVariableNames;
             std::set_difference(unionOfMetaVariableNames.begin(), unionOfMetaVariableNames.end(), summationMetaVariableNames.begin(), summationMetaVariableNames.end(), std::inserter(containedMetaVariableNames, containedMetaVariableNames.begin()));
             
-            return Dd<CUDD>(this->getDdManager(), this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariableNames);
+            return Dd<CUDD>(this->getDdManager(), this->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariableNames);
         }
 
         
@@ -262,35 +262,55 @@ namespace storm {
         }
         
         double Dd<CUDD>::getMin() const {
-            ADD constantMinAdd = this->getCuddAdd().FindMin();
+            ADD constantMinAdd = this->cuddAdd.FindMin();
             return static_cast<double>(Cudd_V(constantMinAdd.getNode()));
         }
         
         double Dd<CUDD>::getMax() const {
-            ADD constantMaxAdd = this->getCuddAdd().FindMax();
+            ADD constantMaxAdd = this->cuddAdd.FindMax();
             return static_cast<double>(Cudd_V(constantMaxAdd.getNode()));
         }
         
         void Dd<CUDD>::setValue(std::string const& metaVariableName, int_fast64_t variableValue, double targetValue) {
-            std::unordered_map<std::string, int_fast64_t> metaVariableNameToValueMap;
+            std::map<std::string, int_fast64_t> metaVariableNameToValueMap;
             metaVariableNameToValueMap.emplace(metaVariableName, variableValue);
             this->setValue(metaVariableNameToValueMap, targetValue);
         }
         
         void Dd<CUDD>::setValue(std::string const& metaVariableName1, int_fast64_t variableValue1, std::string const& metaVariableName2, int_fast64_t variableValue2, double targetValue) {
-            std::unordered_map<std::string, int_fast64_t> metaVariableNameToValueMap;
+            std::map<std::string, int_fast64_t> metaVariableNameToValueMap;
             metaVariableNameToValueMap.emplace(metaVariableName1, variableValue1);
             metaVariableNameToValueMap.emplace(metaVariableName2, variableValue2);
             this->setValue(metaVariableNameToValueMap, targetValue);
         }
         
-        void Dd<CUDD>::setValue(std::unordered_map<std::string, int_fast64_t> const& metaVariableNameToValueMap, double targetValue) {
+        void Dd<CUDD>::setValue(std::map<std::string, int_fast64_t> const& metaVariableNameToValueMap, double targetValue) {
             Dd<CUDD> valueEncoding(this->getDdManager()->getOne());
             for (auto const& nameValuePair : metaVariableNameToValueMap) {
                 valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second);
+                // Also record that the DD now contains the meta variable.
+                this->addContainedMetaVariable(nameValuePair.first);
             }
             
-            this->getCuddAdd() = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd);
+            this->cuddAdd = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd);
+        }
+        
+        double Dd<CUDD>::getValue(std::map<std::string, int_fast64_t> const& metaVariableNameToValueMap) const {
+            std::set<std::string> remainingMetaVariables(this->getContainedMetaVariableNames());
+            Dd<CUDD> valueEncoding(this->getDdManager()->getOne());
+            for (auto const& nameValuePair : metaVariableNameToValueMap) {
+                valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second);
+                if (this->containsMetaVariable(nameValuePair.first)) {
+                    remainingMetaVariables.erase(nameValuePair.first);
+                }
+            }
+            
+            if (!remainingMetaVariables.empty()) {
+                throw storm::exceptions::InvalidArgumentException() << "Cannot evaluate function for which not all inputs were given.";
+            }
+            
+            Dd<CUDD> value = *this * valueEncoding;
+            return static_cast<double>(Cudd_V(value.getCuddAdd().getNode()));
         }
         
         bool Dd<CUDD>::isOne() const {
@@ -327,15 +347,15 @@ namespace storm {
         
         void Dd<CUDD>::exportToDot(std::string const& filename) const {
             if (filename.empty()) {
-                this->getDdManager()->getCuddManager().DumpDot({this->getCuddAdd()});
+                this->getDdManager()->getCuddManager().DumpDot({this->cuddAdd});
             } else {
                 FILE* filePointer = fopen(filename.c_str() , "w");
-                this->getDdManager()->getCuddManager().DumpDot({this->getCuddAdd()}, nullptr, nullptr, filePointer);
+                this->getDdManager()->getCuddManager().DumpDot({this->cuddAdd}, nullptr, nullptr, filePointer);
                 fclose(filePointer);
             }
         }
         
-        ADD& Dd<CUDD>::getCuddAdd() {
+        ADD Dd<CUDD>::getCuddAdd() {
             return this->cuddAdd;
         }
         

src/storage/dd/CuddDd.h

@@ -1,7 +1,7 @@
 #ifndef STORM_STORAGE_DD_CUDDDD_H_
 #define STORM_STORAGE_DD_CUDDDD_H_
 
-#include <unordered_map>
+#include <map>
 #include <set>
 #include <memory>
 #include <iostream>
@@ -295,7 +295,16 @@ namespace storm {
              * have. All values must be within the range of the respective meta variable.
              * @param targetValue The new function value of the modified encodings.
              */
-            void setValue(std::unordered_map<std::string, int_fast64_t> const& metaVariableNameToValueMap, double targetValue);
+            void setValue(std::map<std::string, int_fast64_t> const& metaVariableNameToValueMap, double targetValue);
+            
+            /*!
+             * Retrieves the value of the function when all meta variables are assigned the values of the given mapping.
+             * Note that the mapping must specify values for all meta variables contained in the DD.
+             *
+             * @param metaVariableNameToValueMap A mapping of meta variable names to their values.
+             * @return The value of the function evaluated with the given input.
+             */
+            double getValue(std::map<std::string, int_fast64_t> const& metaVariableNameToValueMap) const;
             
             /*!
              * Retrieves whether this DD represents the constant one function.
@@ -362,7 +371,7 @@ namespace storm {
              *
              * @return The CUDD ADD object associated with this DD.
              */
-            ADD& getCuddAdd();
+            ADD getCuddAdd();
             
             /*!
              * Retrieves the CUDD ADD object associated with this DD.

src/storage/dd/CuddDdManager.cpp

@@ -28,18 +28,23 @@ namespace storm {
                 throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'.";
             }
             
+            DdMetaVariable<CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
+            
             // Check whether the value is legal for this meta variable.
-            if (value < this->getMetaVariable(metaVariableName).getLow() || value > this->getMetaVariable(metaVariableName).getHigh()) {
+            if (value < metaVariable.getLow() || value > metaVariable.getHigh()) {
                 throw storm::exceptions::InvalidArgumentException() << "Illegal value " << value << " for meta variable '" << metaVariableName << "'.";
             }
             
-            std::vector<Dd<CUDD>> const& ddVariables = this->getMetaVariable(metaVariableName).getDdVariables();
+            // Now compute the encoding relative to the low value of the meta variable.
+            value -= metaVariable.getLow();
+            
+            std::vector<Dd<CUDD>> const& ddVariables = metaVariable.getDdVariables();
 
             Dd<CUDD> result;
             if (value & (1ull << (ddVariables.size() - 1))) {
                 result = ddVariables[0];
             } else {
-                result = ddVariables[0];
+                result = ~ddVariables[0];
             }
             
             for (std::size_t i = 1; i < ddVariables.size(); ++i) {
@@ -53,12 +58,33 @@ namespace storm {
             return result;
         }
         
-        Dd<CUDD> DdManager<CUDD>::getRange(std::string const metaVariableName) {
+        Dd<CUDD> DdManager<CUDD>::getRange(std::string const& metaVariableName) {
+            // Check whether the meta variable exists.
+            if (!this->hasMetaVariable(metaVariableName)) {
+                throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'.";
+            }
+
+            storm::dd::DdMetaVariable<CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
+            
+            Dd<CUDD> result = this->getZero();
+            
+            for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
+                result.setValue(metaVariableName, value, static_cast<double>(1));
+            }
+            return result;
+        }
+        
+        Dd<CUDD> DdManager<CUDD>::getIdentity(std::string const& metaVariableName) {
+            // Check whether the meta variable exists.
+            if (!this->hasMetaVariable(metaVariableName)) {
+                throw storm::exceptions::InvalidArgumentException() << "Unknown meta variable name '" << metaVariableName << "'.";
+            }
+            
             storm::dd::DdMetaVariable<CUDD> const& metaVariable = this->getMetaVariable(metaVariableName);
             
             Dd<CUDD> result = this->getZero();
             for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
-                result.setValue(metaVariableName, value - metaVariable.getLow(), static_cast<double>(value));
+                result.setValue(metaVariableName, value, static_cast<double>(value));
             }
             return result;
         }

src/storage/dd/CuddDdManager.h

@@ -69,9 +69,18 @@ namespace storm {
              * of the range of the meta variable to one.
              *
              * @param metaVariableName The name of the meta variable whose range to retrieve.
-             * @return The range of the meta variable
+             * @return The range of the meta variable.
              */
-            Dd<CUDD> getRange(std::string const metaVariableName);
+            Dd<CUDD> getRange(std::string const& metaVariableName);
+
+            /*!
+             * Retrieves the DD representing the identity of the meta variable, i.e., a function that maps all legal
+             * values of the range of the meta variable to themselves.
+             *
+             * @param metaVariableName The name of the meta variable whose identity to retrieve.
+             * @return The identity of the meta variable.
+             */
+            Dd<CUDD> getIdentity(std::string const& metaVariableName);
             
             /*!
              * Adds a meta variable with the given name and range.

test/functional/storage/CuddDdTest.cpp

@@ -36,7 +36,7 @@ TEST(CuddDdManager, Constants) {
     EXPECT_EQ(2, two.getMax());
 }
 
-TEST(CuddDdManager, AddMetaVariableTest) {
+TEST(CuddDdManager, AddGetMetaVariableTest) {
     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));
@@ -71,12 +71,39 @@ TEST(CuddDdManager, EncodingTest) {
     ASSERT_THROW(encoding = manager->getEncoding("x", 0), storm::exceptions::InvalidArgumentException);
     ASSERT_THROW(encoding = manager->getEncoding("x", 10), storm::exceptions::InvalidArgumentException);
     ASSERT_NO_THROW(encoding = manager->getEncoding("x", 4));
-    encoding.exportToDot("out.dot");
     EXPECT_EQ(1, encoding.getNonZeroCount());
     EXPECT_EQ(6, encoding.getNodeCount());
     EXPECT_EQ(2, encoding.getLeafCount());
 }
 
+TEST(CuddDdManager, RangeTest) {
+    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));
+    
+    storm::dd::Dd<storm::dd::CUDD> range;
+    ASSERT_THROW(range = manager->getRange("y"), storm::exceptions::InvalidArgumentException);
+    ASSERT_NO_THROW(range = manager->getRange("x"));
+    
+    EXPECT_EQ(9, range.getNonZeroCount());
+    EXPECT_EQ(2, range.getLeafCount());
+    EXPECT_EQ(6, range.getNodeCount());
+}
+
+TEST(CuddDdManager, IdentityTest) {
+    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));
+    
+    storm::dd::Dd<storm::dd::CUDD> range;
+    ASSERT_THROW(range = manager->getIdentity("y"), storm::exceptions::InvalidArgumentException);
+    ASSERT_NO_THROW(range = manager->getIdentity("x"));
+    
+    EXPECT_EQ(9, range.getNonZeroCount());
+    EXPECT_EQ(10, range.getLeafCount());
+    EXPECT_EQ(21, range.getNodeCount());
+}
+
 TEST(CuddDdMetaVariable, AccessorTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::CUDD>> manager(new storm::dd::DdManager<storm::dd::CUDD>());