From 10996b4ab56ebc0af5c608a7aea49beee3e6ab6b Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 27 Nov 2015 17:01:46 +0100 Subject: [PATCH] more work on sylvan Former-commit-id: c1bfcd83eea68424b94c0ab4a9e6999a1d359be3 --- resources/3rdparty/sylvan/src/sylvan_obj.cpp | 33 +++++- resources/3rdparty/sylvan/src/sylvan_obj.hpp | 13 ++- .../3rdparty/sylvan/src/sylvan_storm_custom.c | 60 ++++++++++- .../3rdparty/sylvan/src/sylvan_storm_custom.h | 7 ++ src/storage/dd/Add.cpp | 20 ++-- src/storage/dd/Bdd.cpp | 12 +-- src/storage/dd/cudd/InternalCuddAdd.cpp | 13 ++- src/storage/dd/cudd/InternalCuddAdd.h | 7 +- src/storage/dd/cudd/InternalCuddBdd.cpp | 2 +- src/storage/dd/cudd/InternalCuddBdd.h | 3 +- src/storage/dd/sylvan/InternalSylvanAdd.cpp | 23 ++-- src/storage/dd/sylvan/InternalSylvanAdd.h | 7 +- src/storage/dd/sylvan/InternalSylvanBdd.cpp | 7 +- src/storage/dd/sylvan/InternalSylvanBdd.h | 5 +- .../dd/sylvan/InternalSylvanDdManager.cpp | 3 +- test/functional/storage/CuddDdTest.cpp | 8 +- test/functional/storage/SylvanDdTest.cpp | 100 ++++++++++-------- 17 files changed, 211 insertions(+), 112 deletions(-) diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.cpp b/resources/3rdparty/sylvan/src/sylvan_obj.cpp index 2eadee308..649b6cfd4 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.cpp @@ -340,10 +340,10 @@ Bdd::GetShaHash() const } double -Bdd::SatCount(const Bdd &variables) const +Bdd::SatCount(size_t variableCount) const { LACE_ME; - return sylvan_satcount_cached(bdd, variables.bdd); + return mtbdd_satcount(bdd, variableCount); } void @@ -986,6 +986,30 @@ Mtbdd::Logxy(const Mtbdd& other) const { return mtbdd_logxy(mtbdd, other.mtbdd); } +size_t +Mtbdd::CountLeaves() const { + LACE_ME; + return mtbdd_leafcount(mtbdd); +} + +double +Mtbdd::NonZeroCount(size_t variableCount) const { + LACE_ME; + return mtbdd_non_zero_count(mtbdd, variableCount); +} + +Mtbdd +Mtbdd::Permute(const std::vector& from, const std::vector& to) const { + LACE_ME; + + /* Create a map */ + MtbddMap map; + for (int i=from.size()-1; i>=0; i--) { + map.put(from[i].TopVar(), to[i]); + } + + return sylvan_compose(mtbdd, map.mtbdd); +} Mtbdd Mtbdd::Support() const @@ -1008,10 +1032,10 @@ Mtbdd::Compose(MtbddMap &m) const } double -Mtbdd::SatCount(const Mtbdd &variables) const +Mtbdd::SatCount(size_t variableCount) const { LACE_ME; - return mtbdd_satcount(mtbdd, variables.mtbdd); + return mtbdd_satcount(mtbdd, variableCount); } size_t @@ -1021,7 +1045,6 @@ Mtbdd::NodeCount() const return mtbdd_nodecount(mtbdd); } - /*** * Implementation of class MtbddMap */ diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp index 907a22c38..6f926ec4b 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.hpp @@ -273,7 +273,7 @@ public: /** * @brief Computes the number of satisfying variable assignments, using variables in cube. */ - double SatCount(const Bdd &variables) const; + double SatCount(size_t variableCount) const; /** * @brief Gets one satisfying assignment according to the variables. @@ -617,6 +617,10 @@ public: Mtbdd Mod(const Mtbdd& other) const; Mtbdd Logxy(const Mtbdd& other) const; + + size_t CountLeaves() const; + + Mtbdd Permute(const std::vector& from, const std::vector& to) const; /** * @brief Computes the support of a Mtbdd. @@ -638,8 +642,13 @@ public: /** * @brief Compute the number of satisfying variable assignments, using variables in cube. */ - double SatCount(const Mtbdd &variables) const; + double SatCount(size_t variableCount) const; + /** + * @brief Compute the number of non-zero variable assignments, using variables in cube. + */ + double NonZeroCount(size_t variableCount) const; + /** * @brief Gets the number of nodes in this Bdd. Not thread-safe! */ diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_custom.c b/resources/3rdparty/sylvan/src/sylvan_storm_custom.c index 6cf7178d6..55b16ac32 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_custom.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_custom.c @@ -380,7 +380,9 @@ TASK_IMPL_2(MTBDD, mtbdd_op_not_zero, MTBDD, a, size_t, v) } // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). - return v > 0 ? mtbdd_invalid : mtbdd_invalid; + (void)v; + + return mtbdd_invalid; } TASK_IMPL_1(MTBDD, mtbdd_not_zero, MTBDD, dd) @@ -410,7 +412,9 @@ TASK_IMPL_2(MTBDD, mtbdd_op_floor, MTBDD, a, size_t, v) } // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). - return v > 0 ? mtbdd_invalid : mtbdd_invalid; + (void)v; + + return mtbdd_invalid; } TASK_IMPL_1(MTBDD, mtbdd_floor, MTBDD, dd) @@ -438,9 +442,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_ceil, MTBDD, a, size_t, v) return mtbdd_isnegated(a) ? mtbdd_negate(result) : result; } } - + // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). - return v > 0 ? mtbdd_invalid : mtbdd_invalid; + (void)v; + + return mtbdd_invalid; } TASK_IMPL_1(MTBDD, mtbdd_ceil, MTBDD, dd) @@ -455,10 +461,54 @@ TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_double, MTBDD, a, size_t, v) if (a == mtbdd_true) return mtbdd_double(1.0); // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). - return v > 0 ? mtbdd_invalid : mtbdd_invalid; + (void)v; + + return mtbdd_invalid; } TASK_IMPL_1(MTBDD, mtbdd_bool_to_double, MTBDD, dd) { return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_double), 0); } + +/** + * Calculate the number of satisfying variable assignments according to . + */ +TASK_IMPL_2(double, mtbdd_non_zero_count, MTBDD, dd, size_t, nvars) +{ + /* Trivial cases */ + if (dd == mtbdd_false) return 0.0; + + mtbddnode_t na = GETNODE(dd); + + if (mtbdd_isleaf(dd)) { + if (mtbddnode_gettype(na) == 0) { + return mtbdd_getuint64(dd) != 0 ? powl(2.0L, nvars) : 0.0; + } else if (mtbddnode_gettype(na) == 1) { + return mtbdd_getdouble(dd) != 0 ? powl(2.0L, nvars) : 0.0; + } else if (mtbddnode_gettype(na) == 2) { + return mtbdd_getnumer(dd) != 0 ? powl(2.0L, nvars) : 0.0; + } + } + + /* Perhaps execute garbage collection */ + sylvan_gc_test(); + + union { + double d; + uint64_t s; + } hack; + + /* Consult cache */ + if (cache_get3(CACHE_BDD_SATCOUNT, dd, 0, nvars, &hack.s)) { + sylvan_stats_count(BDD_SATCOUNT_CACHED); + return hack.d; + } + + SPAWN(mtbdd_non_zero_count, mtbdd_gethigh(dd), nvars-1); + double low = CALL(mtbdd_non_zero_count, mtbdd_getlow(dd), nvars-1); + hack.d = low + SYNC(mtbdd_non_zero_count); + + cache_put3(CACHE_BDD_SATCOUNT, dd, 0, nvars, hack.s); + return hack.d; +} \ No newline at end of file diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_custom.h b/resources/3rdparty/sylvan/src/sylvan_storm_custom.h index 0e6f736d6..eca626e14 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_custom.h +++ b/resources/3rdparty/sylvan/src/sylvan_storm_custom.h @@ -93,3 +93,10 @@ TASK_DECL_1(MTBDD, mtbdd_ceil, MTBDD) TASK_DECL_2(MTBDD, mtbdd_op_bool_to_double, MTBDD, size_t) TASK_DECL_1(MTBDD, mtbdd_bool_to_double, MTBDD) #define mtbdd_bool_to_double(dd) CALL(mtbdd_bool_to_double, dd) + +/** + * Count the number of assignments (minterms) leading to a non-zero + */ +TASK_DECL_2(double, mtbdd_non_zero_count, MTBDD, size_t); +#define mtbdd_non_zero_count(dd, nvars) CALL(mtbdd_non_zero_count, dd, nvars) + diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index f43740418..60a74f622 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -185,8 +185,8 @@ namespace storm { template Add Add::swapVariables(std::vector> const& metaVariablePairs) const { std::set newContainedMetaVariables; - std::vector> from; - std::vector> to; + std::vector> from; + std::vector> to; for (auto const& metaVariablePair : metaVariablePairs) { DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); @@ -200,10 +200,10 @@ namespace storm { } for (auto const& ddVariable : variable1.getDdVariables()) { - from.push_back(ddVariable.template toAdd()); + from.push_back(ddVariable); } for (auto const& ddVariable : variable2.getDdVariables()) { - to.push_back(ddVariable.template toAdd()); + to.push_back(ddVariable); } } STORM_LOG_THROW(from.size() == to.size(), storm::exceptions::InvalidArgumentException, "Unable to swap mismatching meta variables."); @@ -270,16 +270,10 @@ namespace storm { template uint_fast64_t Add::getNonZeroCount() const { std::size_t numberOfDdVariables = 0; - if (LibraryType == DdType::CUDD) { - for (auto const& metaVariable : this->getContainedMetaVariables()) { - numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); - } - } - Bdd cube; - if (LibraryType == DdType::Sylvan) { - cube = Bdd::getCube(*this->getDdManager(), this->getContainedMetaVariables()); + for (auto const& metaVariable : this->getContainedMetaVariables()) { + numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); } - return internalAdd.getNonZeroCount(cube, numberOfDdVariables); + return internalAdd.getNonZeroCount(numberOfDdVariables); } template diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index 7b344eae0..882471d8c 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -188,16 +188,10 @@ namespace storm { template uint_fast64_t Bdd::getNonZeroCount() const { std::size_t numberOfDdVariables = 0; - if (LibraryType == DdType::CUDD) { - for (auto const& metaVariable : this->getContainedMetaVariables()) { - numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); - } - } - Bdd cube; - if (LibraryType == DdType::Sylvan) { - cube = Bdd::getCube(*this->getDdManager(), this->getContainedMetaVariables()); + for (auto const& metaVariable : this->getContainedMetaVariables()) { + numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); } - return internalBdd.getNonZeroCount(cube, numberOfDdVariables); + return internalBdd.getNonZeroCount(numberOfDdVariables); } template diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 40defb627..2ede652f6 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -166,13 +166,13 @@ namespace storm { } template - InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { + InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { std::vector fromAdd; std::vector toAdd; STORM_LOG_ASSERT(fromAdd.size() == toAdd.size(), "Sizes of vectors do not match."); for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { - fromAdd.push_back(it1->getCuddAdd()); - toAdd.push_back(it2->getCuddAdd()); + fromAdd.push_back(it1->getCuddBdd().Add()); + toAdd.push_back(it2->getCuddBdd().Add()); } return InternalAdd(ddManager, this->getCuddAdd().SwapVariables(fromAdd, toAdd)); } @@ -229,7 +229,12 @@ namespace storm { } template - uint_fast64_t InternalAdd::getNonZeroCount(InternalBdd const& cube, uint_fast64_t numberOfDdVariables) const { + uint_fast64_t InternalAdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { + // If the number of DD variables is zero, CUDD returns a number greater 0 for constant nodes different from + // zero, which is not the behaviour we expect. + if (numberOfDdVariables == 0) { + return 0; + } return static_cast(this->getCuddAdd().CountMinterm(static_cast(numberOfDdVariables))); } diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index 44372e6aa..63fa308e7 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -287,13 +287,13 @@ namespace storm { /*! * Swaps the given pairs of DD variables in the ADD. The pairs of meta variables have to be represented by - * ADDs must have equal length. + * vectors of BDDs must have equal length. * * @param from The vector that specifies the 'from' part of the variable renaming. * @param to The vector that specifies the 'to' part of the variable renaming. * @return The resulting ADD. */ - InternalAdd swapVariables(std::vector> const& from, std::vector> const& to) const; + InternalAdd swapVariables(std::vector> const& from, std::vector> const& to) const; /*! * Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta @@ -379,11 +379,10 @@ namespace storm { /*! * Retrieves the number of encodings that are mapped to a non-zero value. * - * @param cube A cube of variables that is ignored. * @param numberOfDdVariables The number of DD variables contained in this BDD. * @return The number of encodings that are mapped to a non-zero value. */ - uint_fast64_t getNonZeroCount(InternalBdd const& cube, uint_fast64_t numberOfDdVariables) const; + uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const; /*! * Retrieves the number of leaves of the ADD. diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp index cad95faa5..5017852d1 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storage/dd/cudd/InternalCuddBdd.cpp @@ -110,7 +110,7 @@ namespace storm { return InternalBdd(ddManager, this->getCuddBdd().Support()); } - uint_fast64_t InternalBdd::getNonZeroCount(InternalBdd const& cube, uint_fast64_t numberOfDdVariables) const { + uint_fast64_t InternalBdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { return static_cast(this->getCuddBdd().CountMinterm(static_cast(numberOfDdVariables))); } diff --git a/src/storage/dd/cudd/InternalCuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h index 99b78808c..7d446e2ab 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.h +++ b/src/storage/dd/cudd/InternalCuddBdd.h @@ -220,11 +220,10 @@ namespace storm { /*! * Retrieves the number of encodings that are mapped to a non-zero value. * - * @param cube A cube of variables that is ignored. * @param numberOfDdVariables The number of DD variables contained in this BDD. * @return The number of encodings that are mapped to a non-zero value. */ - uint_fast64_t getNonZeroCount(InternalBdd const& cube, uint_fast64_t numberOfDdVariables) const; + uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const; /*! * Retrieves the number of leaves of the DD. diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index 993ec6925..9ebc66233 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -1,5 +1,7 @@ #include "src/storage/dd/sylvan/InternalSylvanAdd.h" +#include + #include "src/storage/dd/sylvan/InternalSylvanDdManager.h" #include "src/utility/macros.h" @@ -161,8 +163,14 @@ namespace storm { } template - InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { + std::vector fromBdd; + std::vector toBdd; + for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { + fromBdd.push_back(it1->getSylvanBdd()); + toBdd.push_back(it2->getSylvanBdd()); + } + return InternalAdd(ddManager, this->sylvanMtbdd.Permute(fromBdd, toBdd)); } template @@ -215,18 +223,21 @@ namespace storm { } template - uint_fast64_t InternalAdd::getNonZeroCount(InternalBdd const& cube, uint_fast64_t numberOfDdVariables) const { - return static_cast(this->sylvanMtbdd.SatCount(cube.sylvanBdd)); + uint_fast64_t InternalAdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { + if (numberOfDdVariables == 0) { + return 0; + } + return static_cast(this->sylvanMtbdd.NonZeroCount(numberOfDdVariables)); } template uint_fast64_t InternalAdd::getLeafCount() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + return static_cast(this->sylvanMtbdd.CountLeaves()); } template uint_fast64_t InternalAdd::getNodeCount() const { - return static_cast(this->sylvanMtbdd.NodeCount()) + this->getLeafCount(); + return static_cast(this->sylvanMtbdd.NodeCount()); } template diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.h b/src/storage/dd/sylvan/InternalSylvanAdd.h index 3cc68a761..c1dbe5b44 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storage/dd/sylvan/InternalSylvanAdd.h @@ -293,7 +293,7 @@ namespace storm { * @param to The vector that specifies the 'to' part of the variable renaming. * @return The resulting ADD. */ - InternalAdd swapVariables(std::vector> const& from, std::vector> const& to) const; + InternalAdd swapVariables(std::vector> const& from, std::vector> const& to) const; /*! * Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given meta @@ -379,11 +379,10 @@ namespace storm { /*! * Retrieves the number of encodings that are mapped to a non-zero value. * - * @param cube The cube of variables contained in this BDD. - * @param numberOfDdVariables The number of DD variables contained in this BDD. This is ignored. + * @param numberOfDdVariables The number of DD variables contained in this BDD. * @return The number of encodings that are mapped to a non-zero value. */ - virtual uint_fast64_t getNonZeroCount(InternalBdd const& cube, uint_fast64_t numberOfDdVariables) const; + virtual uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const; /*! * Retrieves the number of leaves of the ADD. diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp index d6124853a..12e1d32aa 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -104,8 +104,11 @@ namespace storm { return InternalBdd(ddManager, this->sylvanBdd.Support()); } - uint_fast64_t InternalBdd::getNonZeroCount(InternalBdd const& cube, uint_fast64_t numberOfDdVariables) const { - return static_cast(this->sylvanBdd.SatCount(cube.sylvanBdd)); + uint_fast64_t InternalBdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { + if (numberOfDdVariables == 0) { + return 0; + } + return static_cast(this->sylvanBdd.SatCount(numberOfDdVariables)); } uint_fast64_t InternalBdd::getLeafCount() const { diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.h b/src/storage/dd/sylvan/InternalSylvanBdd.h index 9b8a4c28e..3e294d031 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.h +++ b/src/storage/dd/sylvan/InternalSylvanBdd.h @@ -209,11 +209,10 @@ namespace storm { /*! * Retrieves the number of encodings that are mapped to a non-zero value. * - * @param cube The cube of variables contained in this BDD. - * @param numberOfDdVariables The number of DD variables contained in this BDD. This is ignored. + * @param numberOfDdVariables The number of DD variables contained in this BDD. * @return The number of encodings that are mapped to a non-zero value. */ - uint_fast64_t getNonZeroCount(InternalBdd const& cube, uint_fast64_t numberOfDdVariables) const; + uint_fast64_t getNonZeroCount(uint_fast64_t numberOfDdVariables) const; /*! * Retrieves the number of leaves of the DD. diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp index 93e7511b8..2840196cb 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -12,7 +12,7 @@ namespace storm { InternalDdManager::InternalDdManager() { if (numberOfInstances == 0) { - // Initialize lace: auto-detecting number of workers. + // Initialize lace: auto-detect number of workers. lace_init(0, 1000000); lace_startup(0, 0, 0); @@ -27,6 +27,7 @@ namespace storm { --numberOfInstances; if (numberOfInstances == 0) { sylvan::Sylvan::quitPackage(); + lace_exit(); } } diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index f5a7c1f6d..9bb57dc94 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -23,7 +23,7 @@ TEST(CuddDd, Constants) { storm::dd::Add one; ASSERT_NO_THROW(one = manager->template getAddOne()); - EXPECT_EQ(1ul, one.getNonZeroCount()); + EXPECT_EQ(0ul, one.getNonZeroCount()); EXPECT_EQ(1ul, one.getLeafCount()); EXPECT_EQ(1ul, one.getNodeCount()); EXPECT_EQ(1, one.getMin()); @@ -32,7 +32,7 @@ TEST(CuddDd, Constants) { storm::dd::Add two; ASSERT_NO_THROW(two = manager->template getConstant(2)); - EXPECT_EQ(1ul, two.getNonZeroCount()); + EXPECT_EQ(0ul, two.getNonZeroCount()); EXPECT_EQ(1ul, two.getLeafCount()); EXPECT_EQ(1ul, two.getNodeCount()); EXPECT_EQ(2, two.getMin()); @@ -212,7 +212,7 @@ TEST(CuddDd, AbstractionTest) { dd3 *= manager->template getConstant(3); ASSERT_THROW(dd3 = dd3.sumAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(dd3 = dd3.sumAbstract({x.first})); - EXPECT_EQ(1ul, dd3.getNonZeroCount()); + EXPECT_EQ(0ul, dd3.getNonZeroCount()); EXPECT_EQ(3, dd3.getMax()); dd3 = dd1.equals(dd2).template toAdd(); @@ -226,7 +226,7 @@ TEST(CuddDd, AbstractionTest) { dd3 *= manager->template getConstant(3); ASSERT_THROW(dd3 = dd3.maxAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(dd3 = dd3.maxAbstract({x.first})); - EXPECT_EQ(1ul, dd3.getNonZeroCount()); + EXPECT_EQ(0ul, dd3.getNonZeroCount()); EXPECT_EQ(3, dd3.getMax()); } diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index eab221a35..442a9f1d4 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -10,35 +10,35 @@ #include "src/storage/SparseMatrix.h" -//TEST(SylvanDd, Constants) { -// std::shared_ptr> manager(new storm::dd::DdManager()); -// storm::dd::Add zero; -// ASSERT_NO_THROW(zero = manager->template getAddZero()); -// -// EXPECT_EQ(0ul, zero.getNonZeroCount()); -// EXPECT_EQ(1ul, zero.getLeafCount()); -// EXPECT_EQ(1ul, zero.getNodeCount()); -// EXPECT_EQ(0, zero.getMin()); -// EXPECT_EQ(0, zero.getMax()); -// -// storm::dd::Add one; -// ASSERT_NO_THROW(one = manager->template getAddOne()); -// -// EXPECT_EQ(1ul, one.getNonZeroCount()); -// EXPECT_EQ(1ul, one.getLeafCount()); -// EXPECT_EQ(1ul, one.getNodeCount()); -// EXPECT_EQ(1, one.getMin()); -// EXPECT_EQ(1, one.getMax()); -// -// storm::dd::Add two; -// ASSERT_NO_THROW(two = manager->template getConstant(2)); -// -// EXPECT_EQ(1ul, two.getNonZeroCount()); -// EXPECT_EQ(1ul, two.getLeafCount()); -// EXPECT_EQ(1ul, two.getNodeCount()); -// EXPECT_EQ(2, two.getMin()); -// EXPECT_EQ(2, two.getMax()); -//} +TEST(SylvanDd, Constants) { + std::shared_ptr> manager(new storm::dd::DdManager()); + storm::dd::Add zero; + ASSERT_NO_THROW(zero = manager->template getAddZero()); + + EXPECT_EQ(0ul, zero.getNonZeroCount()); + EXPECT_EQ(1ul, zero.getLeafCount()); + EXPECT_EQ(1ul, zero.getNodeCount()); + EXPECT_EQ(0, zero.getMin()); + EXPECT_EQ(0, zero.getMax()); + + storm::dd::Add one; + ASSERT_NO_THROW(one = manager->template getAddOne()); + + EXPECT_EQ(0ul, one.getNonZeroCount()); + EXPECT_EQ(1ul, one.getLeafCount()); + EXPECT_EQ(1ul, one.getNodeCount()); + EXPECT_EQ(1, one.getMin()); + EXPECT_EQ(1, one.getMax()); + + storm::dd::Add two; + ASSERT_NO_THROW(two = manager->template getConstant(2)); + + EXPECT_EQ(0ul, two.getNonZeroCount()); + EXPECT_EQ(1ul, two.getLeafCount()); + EXPECT_EQ(1ul, two.getNodeCount()); + EXPECT_EQ(2, two.getMin()); + EXPECT_EQ(2, two.getMax()); +} TEST(SylvanDd, AddGetMetaVariableTest) { std::shared_ptr> manager(new storm::dd::DdManager()); @@ -72,11 +72,17 @@ TEST(SylvanDd, EncodingTest) { EXPECT_EQ(5ul, encoding.getNodeCount()); EXPECT_EQ(1ul, encoding.getLeafCount()); -// // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6. -// EXPECT_EQ(6ul, encoding.template toAdd().getNodeCount()); -// EXPECT_EQ(2ul, encoding.template toAdd().getLeafCount()); + encoding.exportToDot("encoding.dot"); + + storm::dd::Add add; + ASSERT_NO_THROW(add = encoding.template toAdd()); + + // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6. + add.exportToDot("add.dot"); + EXPECT_EQ(6ul, add.getNodeCount()); + EXPECT_EQ(2ul, add.getLeafCount()); } -// + TEST(SylvanDd, RangeTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x; @@ -90,18 +96,18 @@ TEST(SylvanDd, RangeTest) { EXPECT_EQ(5ul, range.getNodeCount()); } -//TEST(SylvanDd, IdentityTest) { -// std::shared_ptr> manager(new storm::dd::DdManager()); -// std::pair x = manager->addMetaVariable("x", 1, 9); -// -// storm::dd::Add identity; -// ASSERT_NO_THROW(identity = manager->getIdentity(x.first)); -// -// EXPECT_EQ(9ul, identity.getNonZeroCount()); -// EXPECT_EQ(10ul, identity.getLeafCount()); -// EXPECT_EQ(21ul, identity.getNodeCount()); -//} -// +TEST(SylvanDd, IdentityTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 1, 9); + + storm::dd::Add identity; + ASSERT_NO_THROW(identity = manager->getIdentity(x.first)); + + EXPECT_EQ(9ul, identity.getNonZeroCount()); + EXPECT_EQ(10ul, identity.getLeafCount()); + EXPECT_EQ(21ul, identity.getNodeCount()); +} + TEST(SylvanDd, OperatorTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); @@ -213,7 +219,7 @@ TEST(SylvanDd, OperatorTest) { // dd3 *= manager->template getConstant(3); // ASSERT_THROW(dd3 = dd3.sumAbstract({x.second}), storm::exceptions::InvalidArgumentException); // ASSERT_NO_THROW(dd3 = dd3.sumAbstract({x.first})); -// EXPECT_EQ(1ul, dd3.getNonZeroCount()); +// EXPECT_EQ(0ul, dd3.getNonZeroCount()); // EXPECT_EQ(3, dd3.getMax()); // // dd3 = dd1.equals(dd2); @@ -227,7 +233,7 @@ TEST(SylvanDd, OperatorTest) { // dd3 *= manager->template getConstant(3); // ASSERT_THROW(dd3 = dd3.maxAbstract({x.second}), storm::exceptions::InvalidArgumentException); // ASSERT_NO_THROW(dd3 = dd3.maxAbstract({x.first})); -// EXPECT_EQ(1ul, dd3.getNonZeroCount()); +// EXPECT_EQ(0ul, dd3.getNonZeroCount()); // EXPECT_EQ(3, dd3.getMax()); //} //