diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp
index f12c4bfa8..e5f62f80d 100644
--- a/src/storage/dd/CuddDd.cpp
+++ b/src/storage/dd/CuddDd.cpp
@@ -518,6 +518,16 @@ namespace storm {
return toExpressionRecur(this->getCuddAdd().getNode(), this->getDdManager()->getDdVariableNames());
}
+ storm::expressions::Expression Dd<DdType::CUDD>::getMintermExpression() const {
+ // Note that we first transform the ADD into a BDD to convert all non-zero terminals to ones and therefore
+ // make the DD more compact.
+ Dd<DdType::CUDD> tmp(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariableNames());
+ tmp.exportToDot("tmp.dot");
+
+
+ return getMintermExpressionRecur(this->getDdManager()->getCuddManager().getManager(), this->getCuddAdd().BddPattern().getNode(), this->getDdManager()->getDdVariableNames());
+ }
+
storm::expressions::Expression Dd<DdType::CUDD>::toExpressionRecur(DdNode const* dd, std::vector<std::string> const& variableNames) {
// If the DD is a terminal node, we can simply return a constant expression.
if (Cudd_IsConstant(dd)) {
@@ -527,6 +537,30 @@ namespace storm {
}
}
+ storm::expressions::Expression Dd<DdType::CUDD>::getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector<std::string> const& variableNames) {
+ // If the DD is a terminal node, we can simply return a constant expression.
+ if (Cudd_IsConstant(dd)) {
+ if (Cudd_IsComplement(dd)) {
+ return storm::expressions::Expression::createBooleanLiteral(false);
+ } else {
+ return storm::expressions::Expression::createBooleanLiteral((dd == Cudd_ReadOne(manager)) ? true : false);
+ }
+ } else {
+ // Get regular versions of the pointers.
+ DdNode* regularDd = Cudd_Regular(dd);
+ DdNode* thenDd = Cudd_T(regularDd);
+ DdNode* elseDd = Cudd_E(regularDd);
+
+ // Compute expression recursively.
+ storm::expressions::Expression result = storm::expressions::Expression::createBooleanVariable(variableNames[dd->index]).ite(getMintermExpressionRecur(manager, thenDd, variableNames), getMintermExpressionRecur(manager, elseDd, variableNames));
+ if (Cudd_IsComplement(dd)) {
+ result = !result;
+ }
+
+ return result;
+ }
+ }
+
std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd) {
dd.exportToDot();
return out;
diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
index 279b2c2fa..b269c4dfd 100644
--- a/src/storage/dd/CuddDd.h
+++ b/src/storage/dd/CuddDd.h
@@ -518,6 +518,16 @@ namespace storm {
* @return The resulting expression.
*/
storm::expressions::Expression toExpression() const;
+
+ /*!
+ * Converts the DD into a (heavily nested) if-then-else (with negations) expression that evaluates to true
+ * if and only if the assignment is minterm of the DD. The variable names used in the expression are derived
+ * from the meta variable name and are extended with a suffix ".i" if the meta variable is integer-valued,
+ * expressing that the variable is the i-th bit of the meta variable.
+ *
+ * @return The resulting expression.
+ */
+ storm::expressions::Expression getMintermExpression() const;
friend std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd);
private:
@@ -558,6 +568,16 @@ namespace storm {
*/
static storm::expressions::Expression toExpressionRecur(DdNode const* dd, std::vector<std::string> const& variableNames);
+ /*!
+ * Performs the recursive step of getMintermExpression on the given DD.
+ *
+ * @param manager The manager of the DD.
+ * @param dd The dd whose minterms to translate into an expression.
+ * @param variableNames The names of the variables to use in the expression.
+ * @return The resulting expression.
+ */
+ static storm::expressions::Expression getMintermExpressionRecur(::DdManager* manager, DdNode const* dd, std::vector<std::string> const& variableNames);
+
/*!
* Creates a DD that encapsulates the given CUDD ADD.
*
diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp
index c84def017..e425bca51 100644
--- a/test/functional/storage/CuddDdTest.cpp
+++ b/test/functional/storage/CuddDdTest.cpp
@@ -340,4 +340,39 @@ TEST(CuddDd, ToExpressionTest) {
// same value as the current value obtained from the DD.
EXPECT_EQ(valuationValuePair.second, ddAsExpression.evaluateAsDouble(&valuation));
}
+
+ storm::expressions::Expression mintermExpression = dd.getMintermExpression();
+
+ // Check whether all minterms are covered.
+ for (auto valuationValuePair : dd) {
+ for (std::size_t i = 0; i < metaVariable.getNumberOfDdVariables(); ++i) {
+ // Check if the i-th bit is set or not and modify the valuation accordingly.
+ if (((valuationValuePair.first.getIntegerValue("x") - metaVariable.getLow()) & (1 << (metaVariable.getNumberOfDdVariables() - i - 1))) != 0) {
+ valuation.setBooleanValue("x." + std::to_string(i), true);
+ } else {
+ valuation.setBooleanValue("x." + std::to_string(i), false);
+ }
+ }
+
+ // At this point, the constructed valuation should make the expression obtained from the DD evaluate to the very
+ // same value as the current value obtained from the DD.
+ EXPECT_TRUE(mintermExpression.evaluateAsBool(&valuation));
+ }
+
+ // Now check no additional minterms are covered.
+ dd = !dd;
+ for (auto valuationValuePair : dd) {
+ for (std::size_t i = 0; i < metaVariable.getNumberOfDdVariables(); ++i) {
+ // Check if the i-th bit is set or not and modify the valuation accordingly.
+ if (((valuationValuePair.first.getIntegerValue("x") - metaVariable.getLow()) & (1 << (metaVariable.getNumberOfDdVariables() - i - 1))) != 0) {
+ valuation.setBooleanValue("x." + std::to_string(i), true);
+ } else {
+ valuation.setBooleanValue("x." + std::to_string(i), false);
+ }
+ }
+
+ // At this point, the constructed valuation should make the expression obtained from the DD evaluate to the very
+ // same value as the current value obtained from the DD.
+ EXPECT_FALSE(mintermExpression.evaluateAsBool(&valuation));
+ }
}
\ No newline at end of file