From 8d3ed7d2fae31bd4022df5b942a5dacbea416e17 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 24 Apr 2014 14:03:36 +0200 Subject: [PATCH 1/3] Added min/max functions on DDs. Added tests for them and ite operation. Former-commit-id: 8e6df90a385c5d840a51288e6b23237f3b8dc11d --- src/storage/dd/CuddDd.cpp | 16 +++++++++++++++- src/storage/dd/CuddDd.h | 16 ++++++++++++++++ test/functional/storage/CuddDdTest.cpp | 14 ++++++++++++++ 3 files changed, 45 insertions(+), 1 deletion(-) 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(this->getDdManager(), this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd())); + return Dd(this->getDdManager(), this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd()), metaVariableNames); } Dd Dd::operator+(Dd const& other) const { @@ -153,6 +153,20 @@ namespace storm { return result; } + Dd Dd::minimum(Dd const& other) const { + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + + return Dd(this->getDdManager(), this->getCuddAdd().Minimum(other.getCuddAdd()), metaVariableNames); + } + + Dd Dd::maximum(Dd const& other) const { + std::set metaVariableNames(this->getContainedMetaVariableNames()); + metaVariableNames.insert(other.getContainedMetaVariableNames().begin(), other.getContainedMetaVariableNames().end()); + + return Dd(this->getDdManager(), this->getCuddAdd().Maximum(other.getCuddAdd()), metaVariableNames); + } + void Dd::existsAbstract(std::set const& metaVariableNames) { Dd 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 greaterOrEqual(Dd 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 minimum(Dd 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 maximum(Dd 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)); From 44ba492fe707d8e575c6844eb898f3a1361773d5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 25 Apr 2014 13:13:03 +0200 Subject: [PATCH 2/3] CuddDdManager now sets tolerance to 1e-15. Former-commit-id: bfc985b5defbfc33bf0337140c5a5f978ae5f4bb --- src/storage/dd/CuddDdManager.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index c75a7c211..6c8c66683 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -8,7 +8,8 @@ namespace storm { namespace dd { DdManager::DdManager() : metaVariableMap(), cuddManager() { - // Intentionally left empty. + + this->cuddManager.SetEpsilon(1.0e-15); } Dd DdManager::getOne() { From 5816bd8860d80777513957bbe1ae408e64169150 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 29 Apr 2014 16:37:53 +0200 Subject: [PATCH 3/3] Bugfix for explicit model adapter: empty choice labeling was not created for automatically added self-loops. Former-commit-id: 6c63c28f596905583d0695a7dcdad8bbdd57d7bd --- src/adapters/ExplicitModelAdapter.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 777807c06..e120f4a59 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -559,6 +559,8 @@ namespace storm { // requested and issue an error otherwise. if (totalNumberOfChoices == 0) { if (storm::settings::Settings::getInstance()->isSet("fixDeadlocks")) { + // Insert empty choice labeling for added self-loop transitions. + choiceLabels.push_back(boost::container::flat_set()); transitionMatrixBuilder.addNextValue(currentRow, currentState, storm::utility::constantOne()); ++currentRow; } else {