Added getNodeCount for ODD and fixed a bug concerning boolean meta variables.

Former-commit-id: 79eb69226b

src/storage/dd/CuddDdMetaVariable.cpp

@@ -10,7 +10,7 @@ namespace storm {
             }
         }
         
-        DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Bool), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
+        DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Bool), low(0), high(1), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
             // Create the cube of all variables of this meta variable.
             for (auto const& ddVariable : this->ddVariables) {
                 this->cube *= ddVariable;

src/storage/dd/CuddOdd.cpp

@@ -59,6 +59,20 @@ namespace storm {
             return this->elseOffset + this->thenOffset;
         }
         
+        uint_fast64_t Odd<DdType::CUDD>::getNodeCount() const {
+            // If the ODD contains a constant (and thus has no children), the size is 1.
+            if (this->elseNode == nullptr && this->thenNode == nullptr) {
+                return 1;
+            }
+            
+            // If the two successors are actually the same, we need to count the subnodes only once.
+            if (this->elseNode == this->thenNode) {
+                return this->elseNode->getNodeCount();
+            } else {
+                return this->elseNode->getNodeCount() + this->thenNode->getNodeCount();
+            }
+        }
+        
         std::shared_ptr<Odd<DdType::CUDD>> Odd<DdType::CUDD>::buildOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& uniqueTableForLevels) {
             // Check whether the ODD for this node has already been computed (for this level) and if so, return this instead.
             auto const& iterator = uniqueTableForLevels[currentLevel].find(dd);

src/storage/dd/CuddOdd.h

@@ -80,6 +80,14 @@ namespace storm {
              */
             uint_fast64_t getTotalOffset() const;
             
+            /*!
+             * Retrieves the size of the ODD. Note: the size is computed by a traversal, so this may be costlier than
+             * expected.
+             *
+             * @return The size (in nodes) of this ODD.
+             */
+            uint_fast64_t getNodeCount() const;
+            
         private:
             /*!
              * Constructs an offset-labeled DD with the given topmost DD node, else- and then-successor.

test/functional/storage/CuddDdTest.cpp

@@ -386,6 +386,8 @@ TEST(CuddDd, OddTest) {
     storm::dd::Odd<storm::dd::DdType::CUDD> odd;
     ASSERT_NO_THROW(odd = storm::dd::Odd<storm::dd::DdType::CUDD>(dd));
     EXPECT_EQ(9, odd.getTotalOffset());
+    EXPECT_EQ(12, odd.getNodeCount());
+
     std::vector<double> ddAsVector;
     ASSERT_NO_THROW(ddAsVector = dd.toDoubleVector());
     EXPECT_EQ(9, ddAsVector.size());