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(this->getDdManager(), this->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariableNames); } + Dd Dd::greaterZero() const { + return Dd(this->getDdManager(), this->getCuddAdd().BddStrictThreshold(0).Add(), this->getContainedMetaVariableNames()); + } + uint_fast64_t Dd::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 multiplyMatrix(Dd const& otherMatrix, std::set 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 greaterZero() const; + /*! * Retrieves the number of encodings that are mapped to a non-zero value. *