From e83d191be3aab22306e0149b66c46d4aa4eee5d1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 1 Apr 2015 19:44:48 +0200 Subject: [PATCH] ODDs can now also be constructed from BDDs directly (without a transformation step to ADDs). Former-commit-id: d19bbc3ff5c21d92173b4797850e8ec499d443c5 --- src/storage/dd/CuddAdd.cpp | 2 +- src/storage/dd/CuddOdd.cpp | 64 +++++++------------------- src/storage/dd/CuddOdd.h | 13 ++++++ test/functional/storage/CuddDdTest.cpp | 34 +++++++++++--- 4 files changed, 59 insertions(+), 54 deletions(-) diff --git a/src/storage/dd/CuddAdd.cpp b/src/storage/dd/CuddAdd.cpp index 3d3695d15..9fb267d7e 100644 --- a/src/storage/dd/CuddAdd.cpp +++ b/src/storage/dd/CuddAdd.cpp @@ -466,7 +466,7 @@ namespace storm { // Prepare the vectors that represent the matrix. std::vector rowIndications(rowOdd.getTotalOffset() + 1); std::vector> columnsAndValues(this->getNonZeroCount()); - + // Create a trivial row grouping. std::vector trivialRowGroupIndices(rowIndications.size()); uint_fast64_t i = 0; diff --git a/src/storage/dd/CuddOdd.cpp b/src/storage/dd/CuddOdd.cpp index 0a41ec736..e459406aa 100644 --- a/src/storage/dd/CuddOdd.cpp +++ b/src/storage/dd/CuddOdd.cpp @@ -35,32 +35,17 @@ namespace storm { // Prepare a unique table for each level that keeps the constructed ODD nodes unique. std::vector>>> uniqueTableForLevels(ddVariableIndices.size() + 1); - // Now construct the ODD structure from the ADD. - bdd.exportToDot("bdd.dot"); - bdd.toAdd().exportToDot("add.dot"); - std::cout << "count: " << bdd.getNonZeroCount() << std::endl; - std::cout << "root cmpl? " << Cudd_IsComplement(bdd.getCuddDdNode()) << std::endl; - std::shared_ptr> rootOdd = buildOddFromBddRec(bdd.getCuddDdNode(), manager->getCuddManager(), 0, Cudd_IsComplement(bdd.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); + // Now construct the ODD structure from the BDD. + std::shared_ptr> rootOdd = buildOddFromBddRec(Cudd_Regular(bdd.getCuddDdNode()), manager->getCuddManager(), 0, Cudd_IsComplement(bdd.getCuddDdNode()), ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels); // Finally, move the children of the root ODD into this ODD. this->elseNode = std::move(rootOdd->elseNode); this->thenNode = std::move(rootOdd->thenNode); - - // If the node is a complement node, - if (Cudd_IsComplement(bdd.getCuddDdNode())) { - this->elseOffset = (1ull << (ddVariableIndices.size() - 1)) - rootOdd->elseOffset; - this->thenOffset = (1ull << (ddVariableIndices.size() - 1)) - rootOdd->thenOffset; - } else { - this->elseOffset = rootOdd->elseOffset; - this->thenOffset = rootOdd->thenOffset; - } - - std::cout << "then offset is: " << this->thenOffset << std::endl; - std::cout << "else offset is: " << this->elseOffset << std::endl; + this->elseOffset = rootOdd->elseOffset; + this->thenOffset = rootOdd->thenOffset; } Odd::Odd(std::shared_ptr> elseNode, uint_fast64_t elseOffset, std::shared_ptr> thenNode, uint_fast64_t thenOffset) : elseNode(elseNode), thenNode(thenNode), elseOffset(elseOffset), thenOffset(thenOffset) { - std::cout << "creating ODD with offsets (" << elseOffset << ", " << thenOffset << ")" << std::endl; // Intentionally left empty. } @@ -121,13 +106,12 @@ namespace storm { uint_fast64_t thenOffset = 0; // If the DD is not the zero leaf, then the then-offset is 1. - if ((Cudd_IsComplement(dd) && dd != Cudd_ReadOne(manager.getManager())) || (!Cudd_IsComplement(dd) && dd != Cudd_ReadZero(manager.getManager()))) { + if (dd != Cudd_ReadZero(manager.getManager())) { thenOffset = 1; } return std::shared_ptr>(new Odd(nullptr, elseOffset, nullptr, thenOffset)); } else if (ddVariableIndices[currentLevel] < static_cast(dd->index)) { - // If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same // node for the then-successor as well. std::shared_ptr> elseNode = buildOddFromAddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); @@ -137,7 +121,6 @@ namespace storm { // Otherwise, we compute the ODDs for both the then- and else successors. bool elseComplemented = Cudd_IsComplement(Cudd_E(dd)); bool thenComplemented = Cudd_IsComplement(Cudd_T(dd)); - std::cout << "something complemented? " << elseComplemented << " // " << thenComplemented << std::endl; std::shared_ptr> elseNode = buildOddFromAddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr> thenNode = buildOddFromAddRec(Cudd_T(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); uint_fast64_t totalElseOffset = elseNode->getElseOffset() + elseNode->getThenOffset(); @@ -153,58 +136,45 @@ namespace storm { if (iterator != uniqueTableForLevels[currentLevel].end()) { return iterator->second; } else { - std::cout << "treating level " << currentLevel << std::endl; // Otherwise, we need to recursively compute the ODD. // If we are already past the maximal level that is to be considered, we can simply create an Odd without // successors if (currentLevel == maxLevel) { - std::cout << "curLev " << currentLevel << " and max " << maxLevel << std::endl; uint_fast64_t elseOffset = 0; uint_fast64_t thenOffset = 0; // If the DD is not the zero leaf, then the then-offset is 1. - std::cout << "complement flag set? " << complement << std::endl; - DdNode* node = Cudd_Regular(dd); - if (node != Cudd_ReadZero(manager.getManager())) { - std::cout << "offset is one" << std::endl; + if (dd != Cudd_ReadZero(manager.getManager())) { thenOffset = 1; } // If we need to complement the 'terminal' node, we need to negate its offset. if (complement) { - std::cout << "negating offset" << std::endl; thenOffset = 1 - thenOffset; } - std::cout << "(1) new ODD at level " << currentLevel << std::endl; return std::shared_ptr>(new Odd(nullptr, elseOffset, nullptr, thenOffset)); } else if (ddVariableIndices[currentLevel] < static_cast(dd->index)) { // If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same // node for the then-successor as well. - std::cout << "following then/else node..." << std::endl; std::shared_ptr> elseNode = buildOddFromBddRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr> thenNode = elseNode; uint_fast64_t totalOffset = elseNode->getElseOffset() + elseNode->getThenOffset(); - if (complement) { - totalOffset = (1ull << (maxLevel - currentLevel - 1)) - totalOffset; - } - - std::cout << "(2) new ODD at level " << currentLevel << std::endl; return std::shared_ptr>(new Odd(elseNode, totalOffset, thenNode, totalOffset)); } else { // Otherwise, we compute the ODDs for both the then- and else successors. - bool elseComplemented = Cudd_IsComplement(Cudd_E(dd)) ^ complement; - bool thenComplemented = Cudd_IsComplement(Cudd_T(dd)) ^ complement; - std::cout << "something complemented? " << elseComplemented << " // " << thenComplemented << std::endl; - std::cout << "following else node..." << std::endl; - std::shared_ptr> elseNode = buildOddFromBddRec(Cudd_E(dd), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels); - std::cout << "following then node..." << std::endl; - std::shared_ptr> thenNode = buildOddFromBddRec(Cudd_T(dd), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels); - uint_fast64_t totalElseOffset = elseNode->getElseOffset() + elseNode->getThenOffset(); - uint_fast64_t totalThenOffset = thenNode->getElseOffset() + thenNode->getThenOffset(); - std::cout << "(3) new ODD at level " << currentLevel << std::endl; - return std::shared_ptr>(new Odd(elseNode, elseComplemented ? (1ull << (maxLevel - currentLevel - 1)) - totalElseOffset : totalElseOffset, thenNode, thenComplemented ? (1ull << (maxLevel - currentLevel - 1)) - totalThenOffset : totalThenOffset)); + DdNode* thenDdNode = Cudd_T(dd); + DdNode* elseDdNode = Cudd_E(dd); + + // Determine whether we have to evaluate the successors as if they were complemented. + bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement; + bool thenComplemented = Cudd_IsComplement(thenDdNode) ^ complement; + + std::shared_ptr> elseNode = buildOddFromBddRec(Cudd_Regular(elseDdNode), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels); + std::shared_ptr> thenNode = buildOddFromBddRec(Cudd_Regular(thenDdNode), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels); + + return std::shared_ptr>(new Odd(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset())); } } } diff --git a/src/storage/dd/CuddOdd.h b/src/storage/dd/CuddOdd.h index f09bfed65..0c4c1793f 100644 --- a/src/storage/dd/CuddOdd.h +++ b/src/storage/dd/CuddOdd.h @@ -121,6 +121,19 @@ namespace storm { */ static std::shared_ptr> buildOddFromAddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>>& uniqueTableForLevels); + /*! + * Recursively builds the ODD from a BDD (that potentially has complement edges). + * + * @param dd The DD for which to build the ODD. + * @param manager The manager responsible for the DD. + * @param currentLevel The currently considered level in the DD. + * @param complement A flag indicating whether or not the given node is to be considered as complemented. + * @param maxLevel The number of levels that need to be considered. + * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. + * @param uniqueTableForLevels A vector of unique tables, one for each level to be considered, that keeps + * ODD nodes for the same DD and level unique. + * @return A pointer to the constructed ODD for the given arguments. + */ static std::shared_ptr> buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector const& ddVariableIndices, std::vector>>>& uniqueTableForLevels); // The then- and else-nodes. diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 431661d00..71efcadaf 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -314,7 +314,7 @@ TEST(CuddDd, ForwardIteratorTest) { EXPECT_EQ(1, numberOfValuations); } -TEST(CuddDd, OddTest) { +TEST(CuddDd, AddOddTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair a = manager->addMetaVariable("a"); std::pair x = manager->addMetaVariable("x", 1, 9); @@ -345,7 +345,7 @@ TEST(CuddDd, OddTest) { // Try to translate the matrix. storm::storage::SparseMatrix matrix; ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, rowOdd, columnOdd)); - + EXPECT_EQ(9, matrix.getRowCount()); EXPECT_EQ(9, matrix.getColumnCount()); EXPECT_EQ(25, matrix.getNonzeroEntryCount()); @@ -356,20 +356,42 @@ TEST(CuddDd, OddTest) { EXPECT_EQ(9, matrix.getRowGroupCount()); EXPECT_EQ(9, matrix.getColumnCount()); EXPECT_EQ(106, matrix.getNonzeroEntryCount()); +} + +TEST(CuddDd, BddOddTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair a = manager->addMetaVariable("a"); + std::pair x = manager->addMetaVariable("x", 1, 9); + + storm::dd::Add dd = manager->getIdentity(x.first); + 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.toVector()); + EXPECT_EQ(9, ddAsVector.size()); + for (uint_fast64_t i = 0; i < ddAsVector.size(); ++i) { + EXPECT_TRUE(i+1 == ddAsVector[i]); + } - std::cout << "########################################################################################" << std::endl; + // Create a non-trivial matrix. + dd = manager->getIdentity(x.first).equals(manager->getIdentity(x.second)) * manager->getRange(x.first).toAdd(); + dd += manager->getEncoding(x.first, 1).toAdd() * manager->getRange(x.second).toAdd() + manager->getEncoding(x.second, 1).toAdd() * manager->getRange(x.first).toAdd(); - // Recreate the ODDs, this time starting from a BDD. + // Create the ODDs. + storm::dd::Odd rowOdd; ASSERT_NO_THROW(rowOdd = storm::dd::Odd(manager->getRange(x.first))); + storm::dd::Odd columnOdd; ASSERT_NO_THROW(columnOdd = storm::dd::Odd(manager->getRange(x.second))); // Try to translate the matrix. + storm::storage::SparseMatrix matrix; ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, rowOdd, columnOdd)); EXPECT_EQ(9, matrix.getRowCount()); EXPECT_EQ(9, matrix.getColumnCount()); - - std::cout << matrix << std::endl; EXPECT_EQ(25, matrix.getNonzeroEntryCount()); dd = manager->getRange(x.first).toAdd() * manager->getRange(x.second).toAdd() * manager->getEncoding(a.first, 0).toAdd().ite(dd, dd + manager->getConstant(1));