sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Working on ODD generation for BDDs (not yet working). 

Former-commit-id: 5665dd1f24
tempestpy_adaptions
dehnert 10 years ago
parent
d787b80fec
commit
c8d8f75a10
3 changed files with 147 additions and 15 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 121
      src/storage/dd/CuddOdd.cpp
  2. 17
      src/storage/dd/CuddOdd.h
  3. 24
      test/functional/storage/CuddDdTest.cpp

121
src/storage/dd/CuddOdd.cpp
View File

@ -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));
}
}
}

17
src/storage/dd/CuddOdd.h
View File

@ -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;

24
test/functional/storage/CuddDdTest.cpp
View File

@ -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());
}
Write Preview
Loading…
Cancel
Save