diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 4daf835a6..bbce93902 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -25,7 +25,7 @@ namespace storm { metaVariableNames.insert(thenDd.getContainedMetaVariableNames().begin(), thenDd.getContainedMetaVariableNames().end()); metaVariableNames.insert(elseDd.getContainedMetaVariableNames().begin(), elseDd.getContainedMetaVariableNames().end()); - return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd())); + return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd()), metaVariableNames); } Dd<DdType::CUDD> Dd<DdType::CUDD>::operator+(Dd<DdType::CUDD> const& other) const { @@ -153,6 +153,20 @@ namespace storm { return result; } + Dd<DdType::CUDD> Dd<DdType::CUDD>::minimum(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().Minimum(other.getCuddAdd()), metaVariableNames); + } + + Dd<DdType::CUDD> Dd<DdType::CUDD>::maximum(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().Maximum(other.getCuddAdd()), metaVariableNames); + } + void Dd<DdType::CUDD>::existsAbstract(std::set<std::string> const& metaVariableNames) { Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne()); diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 32762b6cb..6c7bffd6a 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -210,6 +210,22 @@ namespace storm { */ Dd<DdType::CUDD> greaterOrEqual(Dd<DdType::CUDD> const& other) const; + /*! + * Retrieves the function that maps all evaluations to the minimum of the function values of the two DDs. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd<DdType::CUDD> minimum(Dd<DdType::CUDD> const& other) const; + + /*! + * Retrieves the function that maps all evaluations to the maximum of the function values of the two DDs. + * + * @param other The DD with which to perform the operation. + * @return The resulting function represented as a DD. + */ + Dd<DdType::CUDD> maximum(Dd<DdType::CUDD> const& other) const; + /*! * Existentially abstracts from the given meta variables. * diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 3ca7c0ce1..91d14f202 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -178,6 +178,20 @@ TEST(CuddDd, OperatorTest) { dd3 = dd1.greaterOrEqual(dd2); EXPECT_EQ(5, dd3.getNonZeroCount()); + dd3 = (manager->getEncoding("x", 2)).ite(dd2, dd1); + dd4 = dd3.less(dd2); + EXPECT_EQ(10, dd4.getNonZeroCount()); + + dd4 = dd3.minimum(dd1); + dd4 *= manager->getEncoding("x", 2); + dd4.sumAbstract({"x"}); + EXPECT_EQ(2, dd4.getValue()); + + dd4 = dd3.maximum(dd1); + dd4 *= manager->getEncoding("x", 2); + dd4.sumAbstract({"x"}); + EXPECT_EQ(5, dd4.getValue()); + dd1 = manager->getConstant(0.01); dd2 = manager->getConstant(0.01 + 1e-6); EXPECT_TRUE(dd1.equalModuloPrecision(dd2, 1e-6, false));