From c8d8f75a10dfbfc0618e2ebf71d2c256a9544c47 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 1 Apr 2015 16:12:19 +0200
Subject: [PATCH] Working on ODD generation for BDDs (not yet working).
Former-commit-id: 5665dd1f248573eb2ff0b8b7534cc99eb3590825
---
src/storage/dd/CuddOdd.cpp | 121 +++++++++++++++++++++++--
src/storage/dd/CuddOdd.h | 17 +++-
test/functional/storage/CuddDdTest.cpp | 24 ++++-
3 files changed, 147 insertions(+), 15 deletions(-)
diff --git a/src/storage/dd/CuddOdd.cpp b/src/storage/dd/CuddOdd.cpp
index 342f7458a..0a41ec736 100644
--- a/src/storage/dd/CuddOdd.cpp
+++ b/src/storage/dd/CuddOdd.cpp
@@ -16,9 +16,8 @@ namespace storm {
// Prepare a unique table for each level that keeps the constructed ODD nodes unique.
std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>> uniqueTableForLevels(ddVariableIndices.size() + 1);
- // Now construct the ODD structure.
- // Currently, the DD needs to be an MTBDD, because complement edges are not supported.
- std::shared_ptr<Odd<DdType::CUDD>> rootOdd = buildOddRec(add.getCuddDdNode(), manager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
+ // Now construct the ODD structure from the ADD.
+ std::shared_ptr<Odd<DdType::CUDD>> rootOdd = buildOddFromAddRec(add.getCuddDdNode(), manager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
// Finally, move the children of the root ODD into this ODD.
this->elseNode = std::move(rootOdd->elseNode);
@@ -27,7 +26,41 @@ namespace storm {
this->thenOffset = rootOdd->thenOffset;
}
+ Odd<DdType::CUDD>::Odd(Bdd<DdType::CUDD> const& bdd) {
+ std::shared_ptr<DdManager<DdType::CUDD> const> manager = bdd.getDdManager();
+
+ // First, we need to determine the involved DD variables indices.
+ std::vector<uint_fast64_t> ddVariableIndices = bdd.getSortedVariableIndices();
+
+ // Prepare a unique table for each level that keeps the constructed ODD nodes unique.
+ std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>> 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<Odd<DdType::CUDD>> rootOdd = buildOddFromBddRec(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;
+ }
+
Odd<DdType::CUDD>::Odd(std::shared_ptr<Odd<DdType::CUDD>> elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd<DdType::CUDD>> 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.
}
@@ -73,7 +106,7 @@ namespace storm {
}
}
- 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) {
+ std::shared_ptr<Odd<DdType::CUDD>> Odd<DdType::CUDD>::buildOddFromAddRec(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);
if (iterator != uniqueTableForLevels[currentLevel].end()) {
@@ -81,29 +114,97 @@ namespace storm {
} else {
// 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 a Odd without
+ // If we are already past the maximal level that is to be considered, we can simply create an Odd without
// successors
if (currentLevel == maxLevel) {
uint_fast64_t elseOffset = 0;
uint_fast64_t thenOffset = 0;
// If the DD is not the zero leaf, then the then-offset is 1.
- if (dd != Cudd_ReadZero(manager.getManager())) {
+ if ((Cudd_IsComplement(dd) && dd != Cudd_ReadOne(manager.getManager())) || (!Cudd_IsComplement(dd) && dd != Cudd_ReadZero(manager.getManager()))) {
thenOffset = 1;
}
return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(nullptr, elseOffset, nullptr, thenOffset));
} else if (ddVariableIndices[currentLevel] < static_cast<uint_fast64_t>(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<Odd<DdType::CUDD>> elseNode = buildOddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
+ std::shared_ptr<Odd<DdType::CUDD>> elseNode = buildOddFromAddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd<DdType::CUDD>> thenNode = elseNode;
return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()));
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
- std::shared_ptr<Odd<DdType::CUDD>> elseNode = buildOddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
- std::shared_ptr<Odd<DdType::CUDD>> thenNode = buildOddRec(Cudd_T(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
- return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()));
+ 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<Odd<DdType::CUDD>> elseNode = buildOddFromAddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
+ std::shared_ptr<Odd<DdType::CUDD>> thenNode = buildOddFromAddRec(Cudd_T(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
+ uint_fast64_t totalElseOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
+ uint_fast64_t totalThenOffset = thenNode->getElseOffset() + thenNode->getThenOffset();
+ return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(elseNode, elseComplemented ? (1ull << (maxLevel - currentLevel - 1)) - totalElseOffset : totalElseOffset, thenNode, thenComplemented ? (1ull << (maxLevel - currentLevel - 1)) - totalThenOffset : totalThenOffset));
+ }
+ }
+ }
+
+ std::shared_ptr<Odd<DdType::CUDD>> Odd<DdType::CUDD>::buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, 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);
+ 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;
+ 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<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(nullptr, elseOffset, nullptr, thenOffset));
+ } else if (ddVariableIndices[currentLevel] < static_cast<uint_fast64_t>(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<Odd<DdType::CUDD>> elseNode = buildOddFromBddRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, uniqueTableForLevels);
+ std::shared_ptr<Odd<DdType::CUDD>> 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<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(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<Odd<DdType::CUDD>> elseNode = buildOddFromBddRec(Cudd_E(dd), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels);
+ std::cout << "following then node..." << std::endl;
+ std::shared_ptr<Odd<DdType::CUDD>> 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<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(elseNode, elseComplemented ? (1ull << (maxLevel - currentLevel - 1)) - totalElseOffset : totalElseOffset, thenNode, thenComplemented ? (1ull << (maxLevel - currentLevel - 1)) - totalThenOffset : totalThenOffset));
}
}
}
diff --git a/src/storage/dd/CuddOdd.h b/src/storage/dd/CuddOdd.h
index 9d93d6e47..f09bfed65 100644
--- a/src/storage/dd/CuddOdd.h
+++ b/src/storage/dd/CuddOdd.h
@@ -16,12 +16,19 @@ namespace storm {
class Odd<DdType::CUDD> {
public:
/*!
- * Constructs an offset-labeled DD from the given DD.
+ * Constructs an offset-labeled DD from the given ADD.
*
- * @param add The ADD for which to build the offset-labeled DD.
+ * @param add The ADD for which to build the offset-labeled ADD.
*/
Odd(Add<DdType::CUDD> const& add);
+ /*!
+ * Constructs an offset-labeled DD from the given BDD.
+ *
+ * @param bdd The BDD for which to build the offset-labeled ADD.
+ */
+ Odd(Bdd<DdType::CUDD> const& bdd);
+
// Instantiate all copy/move constructors/assignments with the default implementation.
Odd() = default;
Odd(Odd<DdType::CUDD> const& other) = default;
@@ -101,7 +108,7 @@ namespace storm {
Odd(std::shared_ptr<Odd<DdType::CUDD>> elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd<DdType::CUDD>> thenNode, uint_fast64_t thenOffset);
/*!
- * Recursively builds the ODD.
+ * Recursively builds the ODD from an ADD (that has no complement edges).
*
* @param dd The DD for which to build the ODD.
* @param manager The manager responsible for the DD.
@@ -112,7 +119,9 @@ namespace storm {
* ODD nodes for the same DD and level unique.
* @return A pointer to the constructed ODD for the given arguments.
*/
- static std::shared_ptr<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);
+ static std::shared_ptr<Odd<DdType::CUDD>> buildOddFromAddRec(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);
+
+ static std::shared_ptr<Odd<DdType::CUDD>> buildOddFromBddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& uniqueTableForLevels);
// The then- and else-nodes.
std::shared_ptr<Odd<DdType::CUDD>> elseNode;
diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp
index 654283a90..431661d00 100644
--- a/test/functional/storage/CuddDdTest.cpp
+++ b/test/functional/storage/CuddDdTest.cpp
@@ -318,7 +318,7 @@ TEST(CuddDd, OddTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
std::pair<storm::expressions::Variable, storm::expressions::Variable> a = manager->addMetaVariable("a");
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
-
+
storm::dd::Add<storm::dd::DdType::CUDD> dd = manager->getIdentity(x.first);
storm::dd::Odd<storm::dd::DdType::CUDD> odd;
ASSERT_NO_THROW(odd = storm::dd::Odd<storm::dd::DdType::CUDD>(dd));
@@ -356,4 +356,26 @@ TEST(CuddDd, OddTest) {
EXPECT_EQ(9, matrix.getRowGroupCount());
EXPECT_EQ(9, matrix.getColumnCount());
EXPECT_EQ(106, matrix.getNonzeroEntryCount());
+
+ std::cout << "########################################################################################" << std::endl;
+
+ // Recreate the ODDs, this time starting from a BDD.
+ ASSERT_NO_THROW(rowOdd = storm::dd::Odd<storm::dd::DdType::CUDD>(manager->getRange(x.first)));
+ ASSERT_NO_THROW(columnOdd = storm::dd::Odd<storm::dd::DdType::CUDD>(manager->getRange(x.second)));
+
+ // Try to translate the 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));
+ ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, {a.first}, rowOdd, columnOdd));
+ EXPECT_EQ(18, matrix.getRowCount());
+ EXPECT_EQ(9, matrix.getRowGroupCount());
+ EXPECT_EQ(9, matrix.getColumnCount());
+ EXPECT_EQ(106, matrix.getNonzeroEntryCount());
}
\ No newline at end of file