diff --git a/src/storage/dd/CuddDdMetaVariable.cpp b/src/storage/dd/CuddDdMetaVariable.cpp index 303cb192c..13667bd99 100644 --- a/src/storage/dd/CuddDdMetaVariable.cpp +++ b/src/storage/dd/CuddDdMetaVariable.cpp @@ -10,7 +10,7 @@ namespace storm { } } - DdMetaVariable::DdMetaVariable(std::string const& name, std::vector> const& ddVariables, std::shared_ptr> manager) : name(name), type(MetaVariableType::Bool), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) { + DdMetaVariable::DdMetaVariable(std::string const& name, std::vector> const& ddVariables, std::shared_ptr> 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; diff --git a/src/storage/dd/CuddOdd.cpp b/src/storage/dd/CuddOdd.cpp index 3f97dc861..dc84d9fd7 100644 --- a/src/storage/dd/CuddOdd.cpp +++ b/src/storage/dd/CuddOdd.cpp @@ -59,6 +59,20 @@ namespace storm { return this->elseOffset + this->thenOffset; } + uint_fast64_t Odd::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::buildOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>>& 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); diff --git a/src/storage/dd/CuddOdd.h b/src/storage/dd/CuddOdd.h index 2927bfde6..1d36613f0 100644 --- a/src/storage/dd/CuddOdd.h +++ b/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. diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 7f8a3f299..5a6376e9f 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -386,6 +386,8 @@ TEST(CuddDd, OddTest) { storm::dd::Odd odd; ASSERT_NO_THROW(odd = storm::dd::Odd(dd)); EXPECT_EQ(9, odd.getTotalOffset()); + EXPECT_EQ(12, odd.getNodeCount()); + std::vector ddAsVector; ASSERT_NO_THROW(ddAsVector = dd.toDoubleVector()); EXPECT_EQ(9, ddAsVector.size());