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: 410d61d333

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)) {
+        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;
 	}
     }

src/storage/dd/CuddDd.cpp

@@ -55,6 +55,10 @@ namespace storm {
             return result;
         }
         
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::operator-() const {
+            return this->getDdManager()->getZero() - *this;
+        }
+        
         Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator-=(Dd<DdType::CUDD> const& other) {
             this->cuddAdd -= other.getCuddAdd();
             
@@ -85,6 +89,12 @@ namespace storm {
             return result;
         }
         
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::logicalOr(Dd<DdType::CUDD> const& other) const {
+            std::set<std::string> metaVariableNames(this->getContainedMetaVariableNames());
+            metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end());
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Or(other.getCuddAdd()), metaVariableNames);
+        }
+        
         Dd<DdType::CUDD>& Dd<DdType::CUDD>::complement() {
             this->cuddAdd = ~this->cuddAdd;
             return *this;
@@ -230,7 +240,7 @@ namespace storm {
             this->cuddAdd = this->cuddAdd.SwapVariables(from, to);
         }
         
-        Dd<DdType::CUDD> Dd<DdType::CUDD>::multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<std::string> const& summationMetaVariableNames) {
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<std::string> const& summationMetaVariableNames) const {
             std::vector<ADD> 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<char*> 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<std::string> ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames();
+                std::vector<char*> 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;
+                }
             }
         }
         

src/storage/dd/CuddDd.h

@@ -88,6 +88,13 @@ namespace storm {
              */
             Dd<DdType::CUDD> operator-(Dd<DdType::CUDD> const& other) const;
             
+            /*!
+             * Subtracts the DD from the constant zero function.
+             *
+             * @return The resulting function represented as a DD.
+             */
+            Dd<DdType::CUDD> 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<DdType::CUDD>& operator/=(Dd<DdType::CUDD> const& other);
             
-            /*!
-             * Subtracts the DD from the constant zero function.
-             *
-             * @return The resulting function represented as a DD.
-             */
-            Dd<DdType::CUDD> 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.
@@ -127,6 +127,13 @@ namespace storm {
              */
             Dd<DdType::CUDD> operator~() const;
 
+            /*!
+             * Performs a logical or of the current and the given DD.
+             *
+             * @return The logical or of the operands.
+             */
+            Dd<DdType::CUDD> logicalOr(Dd<DdType::CUDD> const& other) const;
+            
             /*!
              * Logically complements the current DD. The result will map all encodings with a value
              * unequal to zero to false and all others to true.
@@ -232,7 +239,7 @@ namespace storm {
              * matrix multiplication.
              * @return A DD representing the result of the matrix-matrix multiplication.
              */
-            Dd<DdType::CUDD> multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<std::string> const& summationMetaVariableNames);
+            Dd<DdType::CUDD> multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<std::string> const& summationMetaVariableNames) const;
             
             /*!
              * Retrieves the number of encodings that are mapped to a non-zero value.

src/storage/dd/CuddDdManager.cpp

@@ -1,4 +1,5 @@
 #include <cmath>
+#include <string>
 #include <algorithm>
 
 #include "src/storage/dd/CuddDdManager.h"
@@ -179,5 +180,27 @@ namespace storm {
         Cudd& DdManager<DdType::CUDD>::getCuddManager() {
             return this->cuddManager;
         }
+        
+        std::vector<std::string> DdManager<DdType::CUDD>::getDdVariableNames() const {
+            // First, we initialize a list DD variables and their names.
+            std::vector<std::pair<ADD, std::string>> variableNamePairs;
+            for (auto const& nameMetaVariablePair : this->metaVariableMap) {
+                DdMetaVariable<DdType::CUDD> 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<ADD, std::string> const& a, std::pair<ADD, std::string> const& b) { return a.first.getNode()->index < b.first.getNode()->index; });
+            
+            // Now, we project the sorted vector to its second component.
+            std::vector<std::string> result;
+            for (auto const& element : variableNamePairs) {
+                result.push_back(element.second);
+            }
+            
+            return result;
+        }
     }
 }

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<std::string> getDdVariableNames() const;
+            
             /*!
              * Retrieves the underlying CUDD manager.
              *

test/functional/storage/CuddDdTest.cpp

@@ -151,6 +151,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<storm::dd::DdType::CUDD> dd1 = manager->getOne();
     ASSERT_NO_THROW(dd1.setValue("x", 4, 2));
     EXPECT_EQ(2, dd1.getLeafCount());
-    dd1.exportToDot("dd1.dot");
     
     std::map<std::string, int_fast64_t> metaVariableToValueMap;
     metaVariableToValueMap.emplace("x", 1);