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

ODDs can now also be constructed from BDDs directly (without a transformation step to ADDs). 

Former-commit-id: d19bbc3ff5
tempestpy_adaptions
dehnert 10 years ago
parent
c8d8f75a10
commit
e83d191be3
4 changed files with 59 additions and 54 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. 60
      src/storage/dd/CuddOdd.cpp
  2. 13
      src/storage/dd/CuddOdd.h
  3. 32
      test/functional/storage/CuddDdTest.cpp

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

@ -35,32 +35,17 @@ 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 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);
// Now construct the ODD structure from the BDD.
std::shared_ptr<Odd<DdType::CUDD>> 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;
}
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.
}
@ -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<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 = 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<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();
@ -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<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));
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<Odd<DdType::CUDD>> elseNode = buildOddFromBddRec(Cudd_Regular(elseDdNode), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd<DdType::CUDD>> thenNode = buildOddFromBddRec(Cudd_Regular(thenDdNode), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels);
return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()));
}
}
}

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

@ -121,6 +121,19 @@ namespace storm {
*/
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);
/*!
* 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<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.

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

@ -314,7 +314,7 @@ TEST(CuddDd, ForwardIteratorTest) {
EXPECT_EQ(1, numberOfValuations);
}
TEST(CuddDd, OddTest) {
TEST(CuddDd, AddOddTest) {
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);
@ -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<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));
EXPECT_EQ(9, odd.getTotalOffset());
EXPECT_EQ(12, odd.getNodeCount());
std::vector<double> ddAsVector;
ASSERT_NO_THROW(ddAsVector = dd.toVector<double>());
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<storm::dd::DdType::CUDD> rowOdd;
ASSERT_NO_THROW(rowOdd = storm::dd::Odd<storm::dd::DdType::CUDD>(manager->getRange(x.first)));
storm::dd::Odd<storm::dd::DdType::CUDD> columnOdd;
ASSERT_NO_THROW(columnOdd = storm::dd::Odd<storm::dd::DdType::CUDD>(manager->getRange(x.second)));
// Try to translate the matrix.
storm::storage::SparseMatrix<double> 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));

Write Preview
Loading…
Cancel
Save