From b1f22c17478905e5305c416ef1e11ee65e2d664e Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 30 May 2014 17:34:09 +0200
Subject: [PATCH] Added shortcut DD interface to compute \'greaterZero\' on a
 DD.

Former-commit-id: 65585533fd8c50fabe9870e248b35361a6365e36
---
 src/storage/dd/CuddDd.cpp | 4 ++++
 src/storage/dd/CuddDd.h   | 8 ++++++++
 2 files changed, 12 insertions(+)

diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp
index 96bdc9e77..d3789d073 100644
--- a/src/storage/dd/CuddDd.cpp
+++ b/src/storage/dd/CuddDd.cpp
@@ -314,6 +314,10 @@ namespace storm {
             return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariableNames);
         }
         
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::greaterZero() const {
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().BddStrictThreshold(0).Add(), this->getContainedMetaVariableNames());
+        }
+        
         uint_fast64_t Dd<DdType::CUDD>::getNonZeroCount() const {
             std::size_t numberOfDdVariables = 0;
             for (auto const& metaVariableName : this->containedMetaVariableNames) {
diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h
index 9f638d329..4de29e513 100644
--- a/src/storage/dd/CuddDd.h
+++ b/src/storage/dd/CuddDd.h
@@ -291,6 +291,14 @@ namespace storm {
              */
             Dd<DdType::CUDD> multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<std::string> const& summationMetaVariableNames) const;
             
+            /*!
+             * Computes a DD that represents the function in which all assignments with a function value strictly larger
+             * than zero are mapped to one and all others to zero.
+             *
+             * @return The resulting DD.
+             */
+            Dd<DdType::CUDD> greaterZero() const;
+            
             /*!
              * Retrieves the number of encodings that are mapped to a non-zero value.
              *