From 5a4730ae22ddc1ce0e2c5e515792b40da2579399 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 16 Apr 2014 22:41:46 +0200 Subject: [PATCH] When exporting DDs to the dot format, edges leading to the zero node are now suppressed. Also, nodes in the dot file are now labeled with variable names (+ the number of the bit). Former-commit-id: 410d61d33331d5f9563172016aa8e9376509916c --- .../3rdparty/cudd-2.5.0/src/cudd/cuddExport.c | 19 ++++++++-- src/storage/dd/CuddDd.cpp | 37 ++++++++++++++++++- src/storage/dd/CuddDd.h | 23 ++++++++---- src/storage/dd/CuddDdManager.cpp | 23 ++++++++++++ src/storage/dd/CuddDdManager.h | 7 ++++ test/functional/storage/CuddDdTest.cpp | 4 +- 6 files changed, 99 insertions(+), 14 deletions(-) diff --git a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c index 3d8da77ac..2392da36a 100644 --- a/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c +++ b/resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c @@ -502,9 +502,11 @@ Cudd_DumpDot( scan = nodelist[j]; while (scan != NULL) { if (st_is_member(visited,(char *) scan)) { - retval = fprintf(fp,"\"%p\";\n", - (void *) ((mask & (ptrint) scan) / sizeof(DdNode))); - if (retval == EOF) goto failure; + if (scan != Cudd_ReadZero(dd)) { + retval = fprintf(fp,"\"%p\";\n", + (void *) ((mask & (ptrint) scan) / sizeof(DdNode))); + if (retval == EOF) goto failure; + } } scan = scan->next; } @@ -541,6 +543,12 @@ Cudd_DumpDot( scan = nodelist[j]; while (scan != NULL) { if (st_is_member(visited,(char *) scan)) { + retval = fprintf(fp, + "\"%p\" [label = \"%s\"];\n", + (void *) ((mask & (ptrint) scan) / + sizeof(DdNode)), inames[dd->invperm[i]]); + if (retval == EOF) goto failure; + if (cuddT(scan) != Cudd_ReadZero(dd)) { retval = fprintf(fp, "\"%p\" -> \"%p\";\n", (void *) ((mask & (ptrint) scan) / @@ -548,6 +556,8 @@ Cudd_DumpDot( (void *) ((mask & (ptrint) cuddT(scan)) / sizeof(DdNode))); if (retval == EOF) goto failure; + } + if (cuddE(scan) != Cudd_ReadZero(dd)) { if (Cudd_IsComplement(cuddE(scan))) { retval = fprintf(fp, "\"%p\" -> \"%p\" [style = dotted];\n", @@ -565,6 +575,7 @@ Cudd_DumpDot( } if (retval == EOF) goto failure; } + } scan = scan->next; } } @@ -578,11 +589,13 @@ Cudd_DumpDot( scan = nodelist[j]; while (scan != NULL) { if (st_is_member(visited,(char *) scan)) { + if (scan != Cudd_ReadZero(dd)) { retval = fprintf(fp,"\"%p\" [label = \"%g\"];\n", (void *) ((mask & (ptrint) scan) / sizeof(DdNode)), cuddV(scan)); if (retval == EOF) goto failure; } + } scan = scan->next; } } diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 0e163c5f7..ef204f790 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -55,6 +55,10 @@ namespace storm { return result; } + Dd Dd::operator-() const { + return this->getDdManager()->getZero() - *this; + } + Dd& Dd::operator-=(Dd const& other) { this->cuddAdd -= other.getCuddAdd(); @@ -85,6 +89,12 @@ namespace storm { return result; } + Dd Dd::logicalOr(Dd const& other) const { + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + return Dd(this->getDdManager(), this->getCuddAdd().Or(other.getCuddAdd()), metaVariableNames); + } + Dd& Dd::complement() { this->cuddAdd = ~this->cuddAdd; return *this; @@ -230,7 +240,7 @@ namespace storm { this->cuddAdd = this->cuddAdd.SwapVariables(from, to); } - Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames) { + Dd Dd::multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames) const { std::vector summationDdVariables; // Create the CUDD summation variables. @@ -358,9 +368,32 @@ namespace storm { if (filename.empty()) { this->getDdManager()->getCuddManager().DumpDot(cuddAddVector); } else { + // Build the name input of the DD. + std::vector ddNames; + std::string ddName("f"); + ddNames.push_back(new char[ddName.size() + 1]); + memcpy(ddNames.back(), ddName.c_str(), 2); + + // Now build the variables names. + std::vector ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames(); + std::vector ddVariableNames; + for (auto const& element : ddVariableNamesAsStrings) { + ddVariableNames.push_back(new char[element.size() + 1]); + memcpy(ddVariableNames.back(), element.c_str(), element.size() + 1); + } + + // Open the file, dump the DD and close it again. FILE* filePointer = fopen(filename.c_str() , "w"); - this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, nullptr, nullptr, filePointer); + this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer); fclose(filePointer); + + // Finally, delete the names. + for (char* element : ddNames) { + delete element; + } + for (char* element : ddVariableNames) { + delete element; + } } } diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 6da2dc9c3..8ca99614a 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -88,6 +88,13 @@ namespace storm { */ Dd operator-(Dd const& other) const; + /*! + * Subtracts the DD from the constant zero function. + * + * @return The resulting function represented as a DD. + */ + Dd operator-() const; + /*! * Subtracts the given DD from the current one and assigns the result to the current DD. * @@ -112,13 +119,6 @@ namespace storm { */ Dd& operator/=(Dd const& other); - /*! - * Subtracts the DD from the constant zero function. - * - * @return The resulting function represented as a DD. - */ - Dd minus() const; - /*! * Retrieves the logical complement of the current DD. The result will map all encodings with a value * unequal to zero to false and all others to true. @@ -126,6 +126,13 @@ namespace storm { * @return The logical complement of the current DD. */ Dd operator~() const; + + /*! + * Performs a logical or of the current and the given DD. + * + * @return The logical or of the operands. + */ + Dd logicalOr(Dd const& other) const; /*! * Logically complements the current DD. The result will map all encodings with a value @@ -232,7 +239,7 @@ namespace storm { * matrix multiplication. * @return A DD representing the result of the matrix-matrix multiplication. */ - Dd multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames); + Dd multiplyMatrix(Dd const& otherMatrix, std::set const& summationMetaVariableNames) const; /*! * Retrieves the number of encodings that are mapped to a non-zero value. diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 9843b5c92..cda474e7f 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -1,4 +1,5 @@ #include +#include #include #include "src/storage/dd/CuddDdManager.h" @@ -179,5 +180,27 @@ namespace storm { Cudd& DdManager::getCuddManager() { return this->cuddManager; } + + std::vector DdManager::getDdVariableNames() const { + // First, we initialize a list DD variables and their names. + std::vector> variableNamePairs; + for (auto const& nameMetaVariablePair : this->metaVariableMap) { + DdMetaVariable const& metaVariable = nameMetaVariablePair.second; + for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) { + variableNamePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), metaVariable.getName() + "." + std::to_string(variableIndex)); + } + } + + // Then, we sort this list according to the indices of the ADDs. + std::sort(variableNamePairs.begin(), variableNamePairs.end(), [](std::pair const& a, std::pair const& b) { return a.first.getNode()->index < b.first.getNode()->index; }); + + // Now, we project the sorted vector to its second component. + std::vector result; + for (auto const& element : variableNamePairs) { + result.push_back(element.second); + } + + return result; + } } } \ No newline at end of file diff --git a/src/storage/dd/CuddDdManager.h b/src/storage/dd/CuddDdManager.h index ca3f9c2c3..96daeb34a 100644 --- a/src/storage/dd/CuddDdManager.h +++ b/src/storage/dd/CuddDdManager.h @@ -131,6 +131,13 @@ namespace storm { bool hasMetaVariable(std::string const& metaVariableName) const; private: + /*! + * Retrieves a list of names of the DD variables in the order of their index. + * + * @return A list of DD variable names. + */ + std::vector getDdVariableNames() const; + /*! * Retrieves the underlying CUDD manager. * diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 8a5be849a..01d40164a 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -150,6 +150,9 @@ TEST(CuddDd, OperatorTest) { dd1 = ~dd3; EXPECT_TRUE(dd1 == manager->getOne()); + + dd3 = dd1.logicalOr(dd2); + EXPECT_TRUE(dd3 == manager->getOne()); dd1 = manager->getIdentity("x"); dd2 = manager->getConstant(5); @@ -253,7 +256,6 @@ TEST(CuddDd, GetSetValueTest) { storm::dd::Dd dd1 = manager->getOne(); ASSERT_NO_THROW(dd1.setValue("x", 4, 2)); EXPECT_EQ(2, dd1.getLeafCount()); - dd1.exportToDot("dd1.dot"); std::map metaVariableToValueMap; metaVariableToValueMap.emplace("x", 1);