From ebe9ccbb15f9a6ba1030411228bec7de1f4518e0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 3 Dec 2015 17:57:55 +0100 Subject: [PATCH] some work on DD stuff Former-commit-id: 50ca51d26468915d105b730643db65d7caccbda2 --- resources/3rdparty/sylvan/src/llmsset.h | 3 + resources/3rdparty/sylvan/src/sylvan_common.h | 1 + resources/3rdparty/sylvan/src/sylvan_mtbdd.c | 222 +++++++++++------- resources/3rdparty/sylvan/src/sylvan_mtbdd.h | 35 ++- resources/3rdparty/sylvan/src/sylvan_obj.cpp | 7 + resources/3rdparty/sylvan/src/sylvan_obj.hpp | 2 + .../sylvan/src/sylvan_obj_mtbdd_storm.hpp | 4 +- .../3rdparty/sylvan/src/sylvan_obj_storm.cpp | 6 + .../3rdparty/sylvan/src/sylvan_storm_custom.c | 6 +- src/builder/DdPrismModelBuilder.cpp | 2 +- .../results/HybridQuantitativeCheckResult.cpp | 2 +- .../SymbolicQuantitativeCheckResult.cpp | 2 +- src/models/symbolic/StandardRewardModel.cpp | 6 +- src/solver/SymbolicLinearEquationSolver.cpp | 8 +- .../SymbolicMinMaxLinearEquationSolver.cpp | 4 +- src/storage/dd/Add.cpp | 58 ++--- src/storage/dd/Add.h | 4 +- src/storage/dd/Bdd.cpp | 42 ++-- src/storage/dd/Bdd.h | 6 +- src/storage/dd/Dd.cpp | 8 +- src/storage/dd/Dd.h | 6 +- src/storage/dd/DdManager.cpp | 23 +- src/storage/dd/DdManager.h | 20 +- src/storage/dd/cudd/CuddAddIterator.cpp | 4 +- src/storage/dd/cudd/CuddAddIterator.h | 4 +- src/storage/dd/cudd/InternalCuddAdd.cpp | 4 +- src/storage/dd/cudd/InternalCuddAdd.h | 4 +- src/storage/dd/cudd/InternalCuddDdManager.cpp | 4 + src/storage/dd/cudd/InternalCuddDdManager.h | 5 + src/storage/dd/sylvan/InternalSylvanAdd.cpp | 4 +- src/storage/dd/sylvan/InternalSylvanAdd.h | 4 +- .../dd/sylvan/InternalSylvanDdManager.cpp | 2 + .../builder/DdPrismModelBuilderTest.cpp | 2 +- test/functional/storage/CuddDdTest.cpp | 2 +- test/functional/utility/GraphTest.cpp | 74 +++--- 35 files changed, 343 insertions(+), 247 deletions(-) diff --git a/resources/3rdparty/sylvan/src/llmsset.h b/resources/3rdparty/sylvan/src/llmsset.h index 0c3d5bc68..34feefaf0 100644 --- a/resources/3rdparty/sylvan/src/llmsset.h +++ b/resources/3rdparty/sylvan/src/llmsset.h @@ -20,6 +20,8 @@ #include "lace.h" +#include + #ifndef LLMSSET_H #define LLMSSET_H @@ -75,6 +77,7 @@ typedef struct llmsset /** * Retrieve a pointer to the data associated with the 42-bit value. */ + static inline void* llmsset_index_to_ptr(const llmsset_t dbs, size_t index) { diff --git a/resources/3rdparty/sylvan/src/sylvan_common.h b/resources/3rdparty/sylvan/src/sylvan_common.h index 61f34cc5b..7f512a904 100644 --- a/resources/3rdparty/sylvan/src/sylvan_common.h +++ b/resources/3rdparty/sylvan/src/sylvan_common.h @@ -70,6 +70,7 @@ extern "C" { #define CACHE_MTBDD_LESS (52LL<<40) #define CACHE_MTBDD_GEQ (53LL<<40) #define CACHE_MTBDD_GREATER (54LL<<40) +#define CACHE_MTBDD_NONZERO_COUNT (55LL<<40) /** * Registration of quit functions diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index 0c6da75c9..8824a64b2 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -90,7 +90,7 @@ VOID_TASK_IMPL_1(mtbdd_gc_mark_rec, MDD, mtbdd) if (mtbdd == mtbdd_true) return; if (mtbdd == mtbdd_false) return; - if (llmsset_mark(nodes, mtbdd&0x000000ffffffffff)) { + if (llmsset_mark(nodes, mtbdd&(~mtbdd_complement))) { mtbddnode_t n = GETNODE(mtbdd); if (!mtbddnode_isleaf(n)) { SPAWN(mtbdd_gc_mark_rec, mtbddnode_getlow(n)); @@ -699,8 +699,8 @@ TASK_IMPL_3(MTBDD, mtbdd_apply, MTBDD, a, MTBDD, b, mtbdd_apply_op, op) mtbdd_refs_spawn(SPAWN(mtbdd_apply, ahigh, bhigh, op)); MTBDD low = mtbdd_refs_push(CALL(mtbdd_apply, alow, blow, op)); MTBDD high = mtbdd_refs_sync(SYNC(mtbdd_apply)); - result = mtbdd_makenode(v, low, high); mtbdd_refs_pop(1); + result = mtbdd_makenode(v, low, high); /* Store in cache */ cache_put3(CACHE_MTBDD_APPLY, a, b, (size_t)op, result); @@ -764,8 +764,8 @@ TASK_IMPL_5(MTBDD, mtbdd_applyp, MTBDD, a, MTBDD, b, size_t, p, mtbdd_applyp_op, mtbdd_refs_spawn(SPAWN(mtbdd_applyp, ahigh, bhigh, p, op, opid)); MTBDD low = mtbdd_refs_push(CALL(mtbdd_applyp, alow, blow, p, op, opid)); MTBDD high = mtbdd_refs_sync(SYNC(mtbdd_applyp)); - result = mtbdd_makenode(v, low, high); mtbdd_refs_pop(1); + result = mtbdd_makenode(v, low, high); /* Store in cache */ cache_put3(opid, a, b, p, result); @@ -801,8 +801,8 @@ TASK_IMPL_3(MTBDD, mtbdd_uapply, MTBDD, dd, mtbdd_uapply_op, op, size_t, param) mtbdd_refs_spawn(SPAWN(mtbdd_uapply, ddhigh, op, param)); MTBDD low = mtbdd_refs_push(CALL(mtbdd_uapply, ddlow, op, param)); MTBDD high = mtbdd_refs_sync(SYNC(mtbdd_uapply)); - result = mtbdd_makenode(mtbddnode_getvariable(ndd), low, high); mtbdd_refs_pop(1); + result = mtbdd_makenode(mtbddnode_getvariable(ndd), low, high); /* Store in cache */ cache_put3(CACHE_MTBDD_UAPPLY, dd, (size_t)op, param, result); @@ -957,18 +957,15 @@ TASK_IMPL_3(MTBDD, mtbdd_abstract, MTBDD, a, MTBDD, v, mtbdd_abstract_op, op) if (v == mtbdd_true) { result = a; } else if (var_a < var_v) { - SPAWN(mtbdd_abstract, node_gethigh(a, na), v, op); - MTBDD low = CALL(mtbdd_abstract, node_getlow(a, na), v, op); - mtbdd_refs_push(low); - MTBDD high = SYNC(mtbdd_abstract); + mtbdd_refs_spawn(SPAWN(mtbdd_abstract, node_gethigh(a, na), v, op)); + MTBDD low = mtbdd_refs_push(CALL(mtbdd_abstract, node_getlow(a, na), v, op)); + MTBDD high = mtbdd_refs_sync(SYNC(mtbdd_abstract)); mtbdd_refs_pop(1); result = mtbdd_makenode(var_a, low, high); } else /* var_a == var_v */ { - SPAWN(mtbdd_abstract, node_gethigh(a, na), node_gethigh(v, nv), op); - MTBDD low = CALL(mtbdd_abstract, node_getlow(a, na), node_gethigh(v, nv), op); - mtbdd_refs_push(low); - MTBDD high = SYNC(mtbdd_abstract); - mtbdd_refs_push(high); + mtbdd_refs_spawn(SPAWN(mtbdd_abstract, node_gethigh(a, na), node_gethigh(v, nv), op)); + MTBDD low = mtbdd_refs_push(CALL(mtbdd_abstract, node_getlow(a, na), node_gethigh(v, nv), op)); + MTBDD high = mtbdd_refs_push(mtbdd_refs_sync(SYNC(mtbdd_abstract))); result = WRAP(op, low, high, 0); mtbdd_refs_pop(2); } @@ -1394,9 +1391,9 @@ TASK_IMPL_3(MTBDD, mtbdd_ite, MTBDD, f, MTBDD, g, MTBDD, h) /* Recursive calls */ mtbdd_refs_spawn(SPAWN(mtbdd_ite, fhigh, ghigh, hhigh)); MTBDD low = mtbdd_refs_push(CALL(mtbdd_ite, flow, glow, hlow)); - MTBDD high = mtbdd_refs_push(mtbdd_refs_sync(SYNC(mtbdd_ite))); + MTBDD high = mtbdd_refs_sync(SYNC(mtbdd_ite)); + mtbdd_refs_pop(1); result = mtbdd_makenode(v, low, high); - mtbdd_refs_pop(2); /* Store in cache */ cache_put3(CACHE_MTBDD_ITE, f, g, h, result); @@ -2326,108 +2323,93 @@ TASK_IMPL_2(double, mtbdd_satcount, MTBDD, dd, size_t, nvars) return hack.d; } -static MTBDD -mtbdd_enum_next_leaf(MTBDD dd, MTBDD variables, MTBDD prev) +MTBDD +mtbdd_enum_first(MTBDD dd, MTBDD variables, uint8_t *arr, mtbdd_enum_filter_cb filter_cb) { - // dd is a leaf - - if (variables == mtbdd_true) { - // if prev is not false, then it equals dd and we should return false (seen before) - if (prev != mtbdd_false) return mtbdd_false; - else return dd; + if (dd == mtbdd_false) { + // the leaf dd is skipped + return mtbdd_false; + } else if (mtbdd_isleaf(dd)) { + // a leaf for which the filter returns 0 is skipped + if (filter_cb != NULL && filter_cb(dd) == 0) return mtbdd_false; + // ok, we have a leaf that is not skipped, go for it! + while (variables != mtbdd_true) { + *arr++ = 2; + variables = mtbdd_gethigh(variables); + } + return dd; } else { + // if variables == true, then dd must be a leaf. But then this line is unreachable. + // if this assertion fails, then is not the support of
. + assert(variables != mtbdd_true); + // get next variable from uint32_t v = mtbdd_getvar(variables); variables = mtbdd_gethigh(variables); - // if prev is not false, get plow and phigh (one of these leads to "false") - MTBDD plow, phigh; - if (prev != mtbdd_false) { - mtbddnode_t pn = GETNODE(prev); - assert(!mtbdd_isleaf(prev) && mtbddnode_getvariable(pn) == v); - plow = node_getlow(prev, pn); - phigh = node_gethigh(prev, pn); - assert(plow == mtbdd_false || phigh == mtbdd_false); - } else { - plow = phigh = mtbdd_false; + // check if MTBDD is on this variable + mtbddnode_t n = GETNODE(dd); + if (mtbddnode_getvariable(n) != v) { + *arr = 2; + return mtbdd_enum_first(dd, variables, arr+1, filter_cb); } - MTBDD sub; - // first maybe follow low - if (phigh == mtbdd_false) { - sub = mtbdd_enum_next_leaf(dd, variables, plow); - if (sub != mtbdd_false) return mtbdd_makenode(v, sub, mtbdd_false); + MTBDD res = mtbdd_enum_first(node_getlow(dd, n), variables, arr+1, filter_cb); + if (res != mtbdd_false) { + *arr = 0; + return res; } // if not low, try following high - sub = mtbdd_enum_next_leaf(dd, variables, phigh); - if (sub != mtbdd_false) return mtbdd_makenode(v, mtbdd_false, sub); - + res = mtbdd_enum_first(node_gethigh(dd, n), variables, arr+1, filter_cb); + if (res != mtbdd_false) { + *arr = 1; + return res; + } + // we've tried low and high, return false return mtbdd_false; } } MTBDD -mtbdd_enum_next(MTBDD dd, MTBDD variables, MTBDD prev, mtbdd_enum_filter_cb filter_cb) +mtbdd_enum_next(MTBDD dd, MTBDD variables, uint8_t *arr, mtbdd_enum_filter_cb filter_cb) { - if (dd == mtbdd_false) { - // the leaf dd is skipped + if (mtbdd_isleaf(dd)) { + // we find the leaf in 'enum_next', then we've seen it before... return mtbdd_false; - } else if (mtbdd_isleaf(dd)) { - // a leaf for which the filter returns 0 is skipped - if (filter_cb != NULL && filter_cb(dd) == 0) return mtbdd_false; - // ok, we have a leaf that is not skipped, go for it! - return mtbdd_enum_next_leaf(dd, variables, prev); } else { // if variables == true, then dd must be a leaf. But then this line is unreachable. + // if this assertion fails, then is not the support of
. assert(variables != mtbdd_true); - // get next variable from - uint32_t v = mtbdd_getvar(variables); variables = mtbdd_gethigh(variables); - // if prev is not false, get plow and phigh (one of these leads to "false") - MTBDD plow, phigh; - if (prev != mtbdd_false) { - mtbddnode_t pn = GETNODE(prev); - assert(!mtbdd_isleaf(prev) && mtbddnode_getvariable(pn) == v); - plow = node_getlow(prev, pn); - phigh = node_gethigh(prev, pn); - assert(plow == mtbdd_false || phigh == mtbdd_false); - } else { - plow = phigh = mtbdd_false; - } - - // get cofactors ddlow and ddhigh - MTBDD ddlow, ddhigh; - if (!mtbdd_isleaf(dd)) { + if (*arr == 0) { + // previous was low mtbddnode_t n = GETNODE(dd); - if (mtbddnode_getvariable(n) == v) { - ddlow = node_getlow(dd, n); - ddhigh = node_gethigh(dd, n); + MTBDD res = mtbdd_enum_next(node_getlow(dd, n), variables, arr+1, filter_cb); + if (res != mtbdd_false) { + return res; } else { - ddlow = ddhigh = dd; + // try to find new in high branch + res = mtbdd_enum_first(node_gethigh(dd, n), variables, arr+1, filter_cb); + if (res != mtbdd_false) { + *arr = 1; + return res; + } else { + return mtbdd_false; + } } + } else if (*arr == 1) { + // previous was high + mtbddnode_t n = GETNODE(dd); + return mtbdd_enum_next(node_gethigh(dd, n), variables, arr+1, filter_cb); } else { - ddlow = ddhigh = dd; - } - - MTBDD sub; - - // first maybe follow low - if (phigh == mtbdd_false) { - sub = mtbdd_enum_next(ddlow, variables, plow, filter_cb); - if (sub != mtbdd_false) return mtbdd_makenode(v, sub, mtbdd_false); + // previous was either + return mtbdd_enum_next(dd, variables, arr+1, filter_cb); } - - // if not low, try following high - sub = mtbdd_enum_next(ddhigh, variables, phigh, filter_cb); - if (sub != mtbdd_false) return mtbdd_makenode(v, mtbdd_false, sub); - - // we've tried low and high, return false - return mtbdd_false; } } @@ -2493,6 +2475,73 @@ mtbdd_nodecount(MTBDD mtbdd) return result; } +TASK_2(int, mtbdd_test_isvalid_rec, MTBDD, dd, uint32_t, parent_var) +{ + // check if True/False leaf + if (dd == mtbdd_true || dd == mtbdd_false) return 1; + + // check if index is in array + uint64_t index = dd & (~mtbdd_complement); + assert(index > 1 && index < nodes->table_size); + if (index <= 1 || index >= nodes->table_size) return 0; + + // check if marked + int marked = llmsset_is_marked(nodes, index); + assert(marked); + if (marked == 0) return 0; + + // check if leaf + mtbddnode_t n = GETNODE(dd); + if (mtbddnode_isleaf(n)) return 1; // we're fine + + // check variable order + uint32_t var = mtbddnode_getvariable(n); + assert(var > parent_var); + if (var <= parent_var) return 0; + + // check cache + uint64_t result; + if (cache_get3(CACHE_BDD_ISBDD, dd, 0, 0, &result)) { + return result; + } + + // check recursively + SPAWN(mtbdd_test_isvalid_rec, node_getlow(dd, n), var); + result = (uint64_t)CALL(mtbdd_test_isvalid_rec, node_gethigh(dd, n), var); + if (!SYNC(mtbdd_test_isvalid_rec)) result = 0; + + // put in cache and return result + cache_put3(CACHE_BDD_ISBDD, dd, 0, 0, result); + return result; +} + +TASK_IMPL_1(int, mtbdd_test_isvalid, MTBDD, dd) +{ + // check if True/False leaf + if (dd == mtbdd_true || dd == mtbdd_false) return 1; + + // check if index is in array + uint64_t index = dd & (~mtbdd_complement); + assert(index > 1 && index < nodes->table_size); + if (index <= 1 || index >= nodes->table_size) return 0; + + // check if marked + int marked = llmsset_is_marked(nodes, index); + assert(marked); + if (marked == 0) return 0; + + // check if leaf + mtbddnode_t n = GETNODE(dd); + if (mtbddnode_isleaf(n)) return 1; // we're fine + + // check recursively + uint32_t var = mtbddnode_getvariable(n); + SPAWN(mtbdd_test_isvalid_rec, node_getlow(dd, n), var); + int result = CALL(mtbdd_test_isvalid_rec, node_gethigh(dd, n), var); + if (!SYNC(mtbdd_test_isvalid_rec)) result = 0; + return result; +} + /** * Export to .dot file */ @@ -2688,4 +2737,3 @@ mtbdd_map_removeall(MTBDDMAP map, MTBDD variables) } #include "sylvan_storm_custom.c" - diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h index b22ff3f67..19761ead7 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h @@ -250,7 +250,7 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_max, MTBDD, MTBDD, int); /** * Compute a - b */ -//#define mtbdd_minus(a, b) mtbdd_plus(a, mtbdd_negate(minus)) +#define mtbdd_minus(a, b) mtbdd_plus(a, mtbdd_negate(b)) /** * Compute a * b @@ -392,21 +392,36 @@ TASK_DECL_1(MTBDD, mtbdd_maximum, MTBDD); #define mtbdd_maximum(dd) CALL(mtbdd_maximum, dd) /** - * Enumeration. Get the next cube+terminal encoded by the MTBDD. - * The cube follows a variable assignment to each variable in the cube and - * ends with the terminal that the MTBDD assigns to that assignment. - * Terminal "false" is always skipped. + * Given a MTBDD
and a cube of variables expected in
, + * mtbdd_enum_first and mtbdd_enum_next enumerates the unique paths in
that lead to a non-False leaf. + * + * The function returns the leaf (or mtbdd_false if no new path is found) and encodes the path + * in the supplied array : 0 for a low edge, 1 for a high edge, and 2 if the variable is skipped. + * + * The supplied array must be large enough for all variables in . * * Usage: - * MTBDD cube = mtbdd_enum_next(dd, variables, mtbdd_false, NULL); - * while (cube != mtbdd_false) { - * .... - * cube = mtbdd_enum_next(dd, variables, cube, NULL); + * MTBDD leaf = mtbdd_enum_first(dd, variables, arr, NULL); + * while (leaf != mtbdd_false) { + * .... // do something with arr/leaf + * leaf = mtbdd_enum_next(dd, variables, arr, NULL); * } + * * The callback is an optional function that returns 0 when the given terminal node should be skipped. */ typedef int (*mtbdd_enum_filter_cb)(MTBDD); -MTBDD mtbdd_enum_next(MTBDD dd, MTBDD variables, MTBDD prev, mtbdd_enum_filter_cb filter_cb); +MTBDD mtbdd_enum_first(MTBDD dd, MTBDD variables, uint8_t *arr, mtbdd_enum_filter_cb filter_cb); +MTBDD mtbdd_enum_next(MTBDD dd, MTBDD variables, uint8_t *arr, mtbdd_enum_filter_cb filter_cb); + +/** + * For debugging. + * Tests if all nodes in the MTBDD are correctly ``marked'' in the nodes table. + * Tests if variables in the internal nodes appear in-order. + * In Debug mode, this will cause assertion failures instead of returning 0. + * Returns 1 if all is fine, or 0 otherwise. + */ +TASK_DECL_1(int, mtbdd_test_isvalid, MTBDD); +#define mtbdd_test_isvalid(mtbdd) CALL(mtbdd_test_isvalid, mtbdd) /** * Write a DOT representation of a MTBDD diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.cpp b/resources/3rdparty/sylvan/src/sylvan_obj.cpp index 143061704..60d95dcb2 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.cpp @@ -1035,4 +1035,11 @@ Sylvan::quitPackage() sylvan_quit(); } +void +Sylvan::triggerGarbageCollection() { +// LACE_ME; +// sylvan_gc(); +} + + #include "sylvan_obj_storm.cpp" diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp index e63cd0706..e59c30d06 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.hpp @@ -847,6 +847,8 @@ public: * Warning: if you have any Bdd objects which are not bddZero() or bddOne() after this, your program may crash! */ static void quitPackage(); + + static void triggerGarbageCollection(); }; } diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp index 90f62ffa3..4630d42b7 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp @@ -39,4 +39,6 @@ /** * @brief Compute the number of non-zero variable assignments, using variables in cube. */ - double NonZeroCount(size_t variableCount) const; \ No newline at end of file + double NonZeroCount(size_t variableCount) const; + + bool isValid() const; \ No newline at end of file diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index a080e5698..d2687ac8e 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -110,3 +110,9 @@ Mtbdd::NonZeroCount(size_t variableCount) const { LACE_ME; return mtbdd_non_zero_count(mtbdd, variableCount); } + +bool +Mtbdd::isValid() const { + LACE_ME; + return mtbdd_test_isvalid(mtbdd) == 1; +} diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_custom.c b/resources/3rdparty/sylvan/src/sylvan_storm_custom.c index 45283ae09..48d499184 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_custom.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_custom.c @@ -500,8 +500,8 @@ TASK_IMPL_2(double, mtbdd_non_zero_count, MTBDD, dd, size_t, nvars) } hack; /* Consult cache */ - if (cache_get3(CACHE_BDD_SATCOUNT, dd, 0, nvars, &hack.s)) { - sylvan_stats_count(BDD_SATCOUNT_CACHED); + if (cache_get3(CACHE_MTBDD_NONZERO_COUNT, dd, 0, nvars, &hack.s)) { + sylvan_stats_count(CACHE_MTBDD_NONZERO_COUNT); return hack.d; } @@ -509,6 +509,6 @@ TASK_IMPL_2(double, mtbdd_non_zero_count, MTBDD, dd, size_t, nvars) 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); + cache_put3(CACHE_MTBDD_NONZERO_COUNT, dd, 0, nvars, hack.s); return hack.d; } \ No newline at end of file diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 79616701c..1834d178c 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -916,7 +916,7 @@ namespace storm { ActionDecisionDiagram const& actionDd = stateActionReward.isLabeled() ? globalModule.synchronizingActionToDecisionDiagramMap.at(stateActionReward.getActionIndex()) : globalModule.independentAction; states *= actionDd.guardDd * reachableStatesAdd; storm::dd::Add stateActionRewardDd = synchronization * states * rewards; - + // If we are building the state-action rewards for an MDP, we need to make sure that the encoding // of the nondeterminism is present in the reward vector, so we ne need to multiply it with the // legal state-actions. diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp index 040379c42..dbb92f7e6 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -141,7 +141,7 @@ namespace storm { ValueType HybridQuantitativeCheckResult::getMin() const { // In order to not get false zeros, we need to set the values of all states whose values is not stored // symbolically to infinity. - storm::dd::Add tmp = symbolicStates.template toAdd().ite(this->symbolicValues, reachableStates.getDdManager()->getConstant(storm::utility::infinity())); + storm::dd::Add tmp = symbolicStates.template toAdd().ite(this->symbolicValues, reachableStates.getDdManager().getConstant(storm::utility::infinity())); ValueType min = tmp.getMin(); if (!explicitStates.isZero()) { for (auto const& element : explicitValues) { diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index 09ce1c9ee..f837876e4 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -81,7 +81,7 @@ namespace storm { ValueType SymbolicQuantitativeCheckResult::getMin() const { // In order to not get false zeros, we need to set the values of all states whose values is not stored // symbolically to infinity. - return states.template toAdd().ite(this->values, states.getDdManager()->getConstant(storm::utility::infinity())).getMin(); + return states.template toAdd().ite(this->values, states.getDdManager().getConstant(storm::utility::infinity())).getMin(); } template diff --git a/src/models/symbolic/StandardRewardModel.cpp b/src/models/symbolic/StandardRewardModel.cpp index f97caf293..4ec405405 100644 --- a/src/models/symbolic/StandardRewardModel.cpp +++ b/src/models/symbolic/StandardRewardModel.cpp @@ -84,7 +84,7 @@ namespace storm { template storm::dd::Add StandardRewardModel::getTotalRewardVector(storm::dd::Add const& filterAdd, storm::dd::Add const& transitionMatrix, std::set const& columnVariables) const { - storm::dd::Add result = transitionMatrix.getDdManager()->template getAddZero(); + storm::dd::Add result = transitionMatrix.getDdManager().template getAddZero(); if (this->hasStateRewards()) { result += filterAdd * optionalStateRewardVector.get(); } @@ -99,7 +99,7 @@ namespace storm { template storm::dd::Add StandardRewardModel::getTotalRewardVector(storm::dd::Add const& transitionMatrix, std::set const& columnVariables) const { - storm::dd::Add result = transitionMatrix.getDdManager()->template getAddZero(); + storm::dd::Add result = transitionMatrix.getDdManager().template getAddZero(); if (this->hasStateRewards()) { result += optionalStateRewardVector.get(); } @@ -114,7 +114,7 @@ namespace storm { template storm::dd::Add StandardRewardModel::getTotalRewardVector(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, storm::dd::Add const& weights) const { - storm::dd::Add result = transitionMatrix.getDdManager()->template getAddZero(); + storm::dd::Add result = transitionMatrix.getDdManager().template getAddZero(); if (this->hasStateRewards()) { result += optionalStateRewardVector.get(); } diff --git a/src/solver/SymbolicLinearEquationSolver.cpp b/src/solver/SymbolicLinearEquationSolver.cpp index e9427f0a5..acb2a9f91 100644 --- a/src/solver/SymbolicLinearEquationSolver.cpp +++ b/src/solver/SymbolicLinearEquationSolver.cpp @@ -28,14 +28,14 @@ namespace storm { template storm::dd::Add SymbolicLinearEquationSolver::solveEquationSystem(storm::dd::Add const& x, storm::dd::Add const& b) const { // Start by computing the Jacobi decomposition of the matrix A. - storm::dd::Add diagonal = x.getDdManager()->template getAddOne(); + storm::dd::Add diagonal = x.getDdManager().template getAddOne(); for (auto const& pair : rowColumnMetaVariablePairs) { - diagonal *= x.getDdManager()->template getIdentity(pair.first).equals(x.getDdManager()->template getIdentity(pair.second)).template toAdd(); - diagonal *= x.getDdManager()->getRange(pair.first).template toAdd() * x.getDdManager()->getRange(pair.second).template toAdd(); + diagonal *= x.getDdManager().template getIdentity(pair.first).equals(x.getDdManager().template getIdentity(pair.second)).template toAdd(); + diagonal *= x.getDdManager().getRange(pair.first).template toAdd() * x.getDdManager().getRange(pair.second).template toAdd(); } diagonal *= allRows.template toAdd(); - storm::dd::Add lu = diagonal.ite(this->A.getDdManager()->template getAddZero(), this->A); + storm::dd::Add lu = diagonal.ite(this->A.getDdManager().template getAddZero(), this->A); storm::dd::Add dinv = diagonal / (diagonal * this->A); // Set up additional environment variables. diff --git a/src/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/solver/SymbolicMinMaxLinearEquationSolver.cpp index 359267474..bffbfcb48 100644 --- a/src/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -14,12 +14,12 @@ namespace storm { namespace solver { template - SymbolicMinMaxLinearEquationSolver::SymbolicMinMaxLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), allRows(allRows), illegalMaskAdd(illegalMask.template toAdd() * A.getDdManager()->getConstant(storm::utility::infinity())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { + SymbolicMinMaxLinearEquationSolver::SymbolicMinMaxLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), allRows(allRows), illegalMaskAdd(illegalMask.template toAdd() * A.getDdManager().getConstant(storm::utility::infinity())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { // Intentionally left empty. } template - SymbolicMinMaxLinearEquationSolver::SymbolicMinMaxLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs) : A(A), allRows(allRows), illegalMaskAdd(illegalMask.template toAdd() * A.getDdManager()->getConstant(storm::utility::infinity())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs) { + SymbolicMinMaxLinearEquationSolver::SymbolicMinMaxLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalMask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& choiceVariables, std::vector> const& rowColumnMetaVariablePairs) : A(A), allRows(allRows), illegalMaskAdd(illegalMask.template toAdd() * A.getDdManager().getConstant(storm::utility::infinity())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs) { // Get the settings object to customize solving. storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index 876ccc808..4afc3fbc4 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -15,7 +15,7 @@ namespace storm { namespace dd { template - Add::Add(std::shared_ptr const> ddManager, InternalAdd const& internalAdd, std::set const& containedMetaVariables) : Dd(ddManager, containedMetaVariables), internalAdd(internalAdd) { + Add::Add(DdManager const& ddManager, InternalAdd const& internalAdd, std::set const& containedMetaVariables) : Dd(ddManager, containedMetaVariables), internalAdd(internalAdd) { // Intentionally left empty. } @@ -67,7 +67,7 @@ namespace storm { template Add Add::operator-() const { - return this->getDdManager()->template getAddZero() - *this; + return this->getDdManager().template getAddZero() - *this; } template @@ -161,19 +161,19 @@ namespace storm { template Add Add::sumAbstract(std::set const& metaVariables) const { - Bdd cube = Bdd::getCube(*this->getDdManager(), metaVariables); + Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); return Add(this->getDdManager(), internalAdd.sumAbstract(cube), Dd::subtractMetaVariables(*this, cube)); } template Add Add::minAbstract(std::set const& metaVariables) const { - Bdd cube = Bdd::getCube(*this->getDdManager(), metaVariables); + Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); return Add(this->getDdManager(), internalAdd.minAbstract(cube), Dd::subtractMetaVariables(*this, cube)); } template Add Add::maxAbstract(std::set const& metaVariables) const { - Bdd cube = Bdd::getCube(*this->getDdManager(), metaVariables); + Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); return Add(this->getDdManager(), internalAdd.maxAbstract(cube), Dd::subtractMetaVariables(*this, cube)); } @@ -188,8 +188,8 @@ namespace storm { 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); + DdMetaVariable const& variable1 = this->getDdManager().getMetaVariable(metaVariablePair.first); + DdMetaVariable const& variable2 = this->getDdManager().getMetaVariable(metaVariablePair.second); // Keep track of the contained meta variables in the DD. if (this->containsMetaVariable(metaVariablePair.first)) { @@ -215,7 +215,7 @@ namespace storm { // Create the CUDD summation variables. std::vector> summationDdVariables; for (auto const& metaVariable : summationMetaVariables) { - for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariable).getDdVariables()) { + for (auto const& ddVariable : this->getDdManager().getMetaVariable(metaVariable).getDdVariables()) { summationDdVariables.push_back(ddVariable); } } @@ -271,7 +271,7 @@ namespace storm { uint_fast64_t Add::getNonZeroCount() const { std::size_t numberOfDdVariables = 0; for (auto const& metaVariable : this->getContainedMetaVariables()) { - numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); + numberOfDdVariables += this->getDdManager().getMetaVariable(metaVariable).getNumberOfDdVariables(); } return internalAdd.getNonZeroCount(numberOfDdVariables); } @@ -313,22 +313,22 @@ namespace storm { template void Add::setValue(std::map const& metaVariableToValueMap, ValueType const& targetValue) { - Bdd valueEncoding = this->getDdManager()->getBddOne(); + Bdd valueEncoding = this->getDdManager().getBddOne(); for (auto const& nameValuePair : metaVariableToValueMap) { - valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); + valueEncoding &= this->getDdManager().getEncoding(nameValuePair.first, nameValuePair.second); // Also record that the DD now contains the meta variable. this->addMetaVariable(nameValuePair.first); } - internalAdd = valueEncoding.template toAdd().ite(this->getDdManager()->getConstant(targetValue), *this); + internalAdd = valueEncoding.template toAdd().ite(this->getDdManager().getConstant(targetValue), *this); } template ValueType Add::getValue(std::map const& metaVariableToValueMap) const { std::set remainingMetaVariables(this->getContainedMetaVariables()); - Bdd valueEncoding = this->getDdManager()->getBddOne(); + Bdd valueEncoding = this->getDdManager().getBddOne(); for (auto const& nameValuePair : metaVariableToValueMap) { - valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second); + valueEncoding &= this->getDdManager().getEncoding(nameValuePair.first, nameValuePair.second); if (this->containsMetaVariable(nameValuePair.first)) { remainingMetaVariables.erase(nameValuePair.first); } @@ -412,7 +412,7 @@ namespace storm { std::vector ddColumnVariableIndices; for (auto const& variable : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + DdMetaVariable const& metaVariable = this->getDdManager().getMetaVariable(variable); for (auto const& ddVariable : metaVariable.getDdVariables()) { ddRowVariableIndices.push_back(ddVariable.getIndex()); } @@ -420,7 +420,7 @@ namespace storm { std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); for (auto const& variable : columnMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + DdMetaVariable const& metaVariable = this->getDdManager().getMetaVariable(variable); for (auto const& ddVariable : metaVariable.getDdVariables()) { ddColumnVariableIndices.push_back(ddVariable.getIndex()); } @@ -499,7 +499,7 @@ namespace storm { std::set rowAndColumnMetaVariables; for (auto const& variable : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + DdMetaVariable const& metaVariable = this->getDdManager().getMetaVariable(variable); for (auto const& ddVariable : metaVariable.getDdVariables()) { ddRowVariableIndices.push_back(ddVariable.getIndex()); } @@ -507,7 +507,7 @@ namespace storm { } std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); for (auto const& variable : columnMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + DdMetaVariable const& metaVariable = this->getDdManager().getMetaVariable(variable); for (auto const& ddVariable : metaVariable.getDdVariables()) { ddColumnVariableIndices.push_back(ddVariable.getIndex()); } @@ -515,14 +515,14 @@ namespace storm { } std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); for (auto const& variable : groupMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + DdMetaVariable const& metaVariable = this->getDdManager().getMetaVariable(variable); for (auto const& ddVariable : metaVariable.getDdVariables()) { ddGroupVariableIndices.push_back(ddVariable.getIndex()); } } std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); - Bdd columnVariableCube = Bdd::getCube(*this->getDdManager(), columnMetaVariables); + Bdd columnVariableCube = Bdd::getCube(this->getDdManager(), columnMetaVariables); // Start by computing the offsets (in terms of rows) for each row group. Add stateToNumberOfChoices = this->notZero().existsAbstract(columnMetaVariables).template toAdd().sumAbstract(groupMetaVariables); @@ -548,7 +548,7 @@ namespace storm { std::vector rowIndications(rowGroupIndices.back() + 1); std::vector> statesWithGroupEnabled(groups.size()); - InternalAdd stateToRowGroupCount = this->getDdManager()->template getAddZero(); + InternalAdd stateToRowGroupCount = this->getDdManager().template getAddZero(); for (uint_fast64_t i = 0; i < groups.size(); ++i) { auto const& dd = groups[i]; @@ -623,7 +623,7 @@ namespace storm { std::set rowAndColumnMetaVariables; for (auto const& variable : rowMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + DdMetaVariable const& metaVariable = this->getDdManager().getMetaVariable(variable); for (auto const& ddVariable : metaVariable.getDdVariables()) { ddRowVariableIndices.push_back(ddVariable.getIndex()); } @@ -631,7 +631,7 @@ namespace storm { } std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); for (auto const& variable : columnMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + DdMetaVariable const& metaVariable = this->getDdManager().getMetaVariable(variable); for (auto const& ddVariable : metaVariable.getDdVariables()) { ddColumnVariableIndices.push_back(ddVariable.getIndex()); } @@ -639,14 +639,14 @@ namespace storm { } std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); for (auto const& variable : groupMetaVariables) { - DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + DdMetaVariable const& metaVariable = this->getDdManager().getMetaVariable(variable); for (auto const& ddVariable : metaVariable.getDdVariables()) { ddGroupVariableIndices.push_back(ddVariable.getIndex()); } } std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); - Bdd columnVariableCube = Bdd::getCube(*this->getDdManager(), columnMetaVariables); + Bdd columnVariableCube = Bdd::getCube(this->getDdManager(), columnMetaVariables); // Transform the row group sizes to the actual row group indices. rowGroupIndices.resize(rowGroupIndices.size() + 1); @@ -672,7 +672,7 @@ namespace storm { std::vector rowIndications(rowGroupIndices.back() + 1); std::vector> statesWithGroupEnabled(groups.size()); - InternalAdd stateToRowGroupCount = this->getDdManager()->template getAddZero(); + InternalAdd stateToRowGroupCount = this->getDdManager().template getAddZero(); for (uint_fast64_t i = 0; i < groups.size(); ++i) { std::pair, InternalAdd> const& ddPair = groups[i]; @@ -720,7 +720,7 @@ namespace storm { template void Add::exportToDot(std::string const& filename) const { - internalAdd.exportToDot(filename, this->getDdManager()->getDdVariableNames()); + internalAdd.exportToDot(filename, this->getDdManager().getDdVariableNames()); } template @@ -745,8 +745,8 @@ namespace storm { } template - Add Add::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables) { - return Add(ddManager, InternalAdd::fromVector(ddManager->getInternalDdManagerPointer(), values, odd, ddManager->getSortedVariableIndices(metaVariables)), metaVariables); + Add Add::fromVector(DdManager const& ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables) { + return Add(ddManager, InternalAdd::fromVector(ddManager.getInternalDdManagerPointer(), values, odd, ddManager.getSortedVariableIndices(metaVariables)), metaVariables); } template diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h index b90f4f1b0..2743b548c 100644 --- a/src/storage/dd/Add.h +++ b/src/storage/dd/Add.h @@ -47,7 +47,7 @@ namespace storm { * @param metaVariables The meta variables used for the translation. * @return The resulting (CUDD) ADD. */ - static Add fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables); + static Add fromVector(DdManager const& ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables); /*! * Retrieves whether the two DDs represent the same function. @@ -611,7 +611,7 @@ namespace storm { * @param internalAdd The internal ADD to store. * @param containedMetaVariables The meta variables that appear in the DD. */ - Add(std::shared_ptr const> ddManager, InternalAdd const& internalAdd, std::set const& containedMetaVariables = std::set()); + Add(DdManager const& ddManager, InternalAdd const& internalAdd, std::set const& containedMetaVariables = std::set()); /*! * We provide a conversion operator from the BDD to its internal type to ease calling the internal functions. diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index 7b30ccfed..407aa9761 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -17,12 +17,12 @@ namespace storm { namespace dd { template - Bdd::Bdd(std::shared_ptr const> ddManager, InternalBdd const& internalBdd, std::set const& containedMetaVariables) : Dd(ddManager, containedMetaVariables), internalBdd(internalBdd) { + Bdd::Bdd(DdManager const& ddManager, InternalBdd const& internalBdd, std::set const& containedMetaVariables) : Dd(ddManager, containedMetaVariables), internalBdd(internalBdd) { // Intentionally left empty. } template - Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, double value) { + Bdd Bdd::fromVector(DdManager const& ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, double value) { switch (comparisonType) { case storm::logic::ComparisonType::Less: return fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater(), value, std::placeholders::_1)); @@ -37,8 +37,8 @@ namespace storm { template template - Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter) { - return Bdd(ddManager, InternalBdd::fromVector(&ddManager->internalDdManager, values, odd, ddManager->getSortedVariableIndices(metaVariables), filter), metaVariables); + Bdd Bdd::fromVector(DdManager const& ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter) { + return Bdd(ddManager, InternalBdd::fromVector(&ddManager.internalDdManager, values, odd, ddManager.getSortedVariableIndices(metaVariables), filter), metaVariables); } template @@ -110,19 +110,19 @@ namespace storm { template Bdd Bdd::existsAbstract(std::set const& metaVariables) const { - Bdd cube = getCube(*this->getDdManager(), metaVariables); + Bdd cube = getCube(this->getDdManager(), metaVariables); return Bdd(this->getDdManager(), internalBdd.existsAbstract(cube), Dd::subtractMetaVariables(*this, cube)); } template Bdd Bdd::universalAbstract(std::set const& metaVariables) const { - Bdd cube = getCube(*this->getDdManager(), metaVariables); + Bdd cube = getCube(this->getDdManager(), metaVariables); return Bdd(this->getDdManager(), internalBdd.universalAbstract(cube), Dd::subtractMetaVariables(*this, cube)); } template Bdd Bdd::andExists(Bdd const& other, std::set const& existentialVariables) const { - Bdd cube = getCube(*this->getDdManager(), existentialVariables); + Bdd cube = getCube(this->getDdManager(), existentialVariables); std::set unionOfMetaVariables; std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin())); @@ -149,7 +149,7 @@ namespace storm { std::vector> rowVariables; for (auto const& metaVariable : rowMetaVariables) { - DdMetaVariable const& variable = this->getDdManager()->getMetaVariable(metaVariable); + DdMetaVariable const& variable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : variable.getDdVariables()) { rowVariables.push_back(ddVariable); } @@ -157,7 +157,7 @@ namespace storm { std::vector> columnVariables; for (auto const& metaVariable : columnMetaVariables) { - DdMetaVariable const& variable = this->getDdManager()->getMetaVariable(metaVariable); + DdMetaVariable const& variable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : variable.getDdVariables()) { columnVariables.push_back(ddVariable); } @@ -173,7 +173,7 @@ namespace storm { std::vector> rowVariables; for (auto const& metaVariable : rowMetaVariables) { - DdMetaVariable const& variable = this->getDdManager()->getMetaVariable(metaVariable); + DdMetaVariable const& variable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : variable.getDdVariables()) { rowVariables.push_back(ddVariable); } @@ -181,7 +181,7 @@ namespace storm { std::vector> columnVariables; for (auto const& metaVariable : columnMetaVariables) { - DdMetaVariable const& variable = this->getDdManager()->getMetaVariable(metaVariable); + DdMetaVariable const& variable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : variable.getDdVariables()) { columnVariables.push_back(ddVariable); } @@ -197,7 +197,7 @@ namespace storm { std::vector> rowVariables; for (auto const& metaVariable : rowMetaVariables) { - DdMetaVariable const& variable = this->getDdManager()->getMetaVariable(metaVariable); + DdMetaVariable const& variable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : variable.getDdVariables()) { rowVariables.push_back(ddVariable); } @@ -205,7 +205,7 @@ namespace storm { std::vector> columnVariables; for (auto const& metaVariable : columnMetaVariables) { - DdMetaVariable const& variable = this->getDdManager()->getMetaVariable(metaVariable); + DdMetaVariable const& variable = this->getDdManager().getMetaVariable(metaVariable); for (auto const& ddVariable : variable.getDdVariables()) { columnVariables.push_back(ddVariable); } @@ -220,8 +220,8 @@ namespace storm { 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); + DdMetaVariable const& variable1 = this->getDdManager().getMetaVariable(metaVariablePair.first); + DdMetaVariable const& variable2 = this->getDdManager().getMetaVariable(metaVariablePair.second); // Keep track of the contained meta variables in the DD. if (this->containsMetaVariable(metaVariablePair.first)) { @@ -261,7 +261,7 @@ namespace storm { uint_fast64_t Bdd::getNonZeroCount() const { std::size_t numberOfDdVariables = 0; for (auto const& metaVariable : this->getContainedMetaVariables()) { - numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); + numberOfDdVariables += this->getDdManager().getMetaVariable(metaVariable).getNumberOfDdVariables(); } return internalBdd.getNonZeroCount(numberOfDdVariables); } @@ -293,7 +293,7 @@ namespace storm { template void Bdd::exportToDot(std::string const& filename) const { - internalBdd.exportToDot(filename, this->getDdManager()->getDdVariableNames()); + internalBdd.exportToDot(filename, this->getDdManager().getDdVariableNames()); } template @@ -325,8 +325,8 @@ namespace storm { template class Bdd; - template Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); - template Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); + template Bdd Bdd::fromVector(DdManager const& ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); + template Bdd Bdd::fromVector(DdManager const& ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); template Add Bdd::toAdd() const; template Add Bdd::toAdd() const; @@ -337,8 +337,8 @@ namespace storm { template class Bdd; - template Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); - template Bdd Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); + template Bdd Bdd::fromVector(DdManager const& ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); + template Bdd Bdd::fromVector(DdManager const& ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); template Add Bdd::toAdd() const; template Add Bdd::toAdd() const; diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h index a9c9c906a..dbe1d3a0b 100644 --- a/src/storage/dd/Bdd.h +++ b/src/storage/dd/Bdd.h @@ -45,7 +45,7 @@ namespace storm { * @param comparisonType The relation that needs to hold for the values (wrt. to the given value). * @param value The value to compare with. */ - static Bdd fromVector(std::shared_ptr const> ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, double value); + static Bdd fromVector(DdManager const& ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, double value); /*! * Retrieves whether the two BDDs represent the same function. @@ -314,7 +314,7 @@ namespace storm { * @param internalBdd The internal BDD to store. * @param containedMetaVariables The meta variables that appear in the DD. */ - Bdd(std::shared_ptr const> ddManager, InternalBdd const& internalBdd, std::set const& containedMetaVariables = std::set()); + Bdd(DdManager const& ddManager, InternalBdd const& internalBdd, std::set const& containedMetaVariables = std::set()); /*! * Builds a BDD representing the values that make the given filter function evaluate to true. @@ -327,7 +327,7 @@ namespace storm { * @return The resulting (CUDD) BDD. */ template - static Bdd fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); + static Bdd fromVector(DdManager const& ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); // The internal BDD that depends on the chosen library. InternalBdd internalBdd; diff --git a/src/storage/dd/Dd.cpp b/src/storage/dd/Dd.cpp index ce477be7d..bae32c108 100644 --- a/src/storage/dd/Dd.cpp +++ b/src/storage/dd/Dd.cpp @@ -10,7 +10,7 @@ namespace storm { namespace dd { template - Dd::Dd(std::shared_ptr const> ddManager, std::set const& containedMetaVariables) : ddManager(ddManager), containedMetaVariables(containedMetaVariables) { + Dd::Dd(DdManager const& ddManager, std::set const& containedMetaVariables) : ddManager(&ddManager), containedMetaVariables(containedMetaVariables) { // Intentionally left empty. } @@ -35,8 +35,8 @@ namespace storm { } template - std::shared_ptr const> Dd::getDdManager() const { - return this->ddManager; + DdManager const& Dd::getDdManager() const { + return *this->ddManager; } template @@ -65,7 +65,7 @@ namespace storm { template std::vector Dd::getSortedVariableIndices() const { - return this->getDdManager()->getSortedVariableIndices(this->getContainedMetaVariables()); + return this->getDdManager().getSortedVariableIndices(this->getContainedMetaVariables()); } template diff --git a/src/storage/dd/Dd.h b/src/storage/dd/Dd.h index d91989d6a..30a0c3b97 100644 --- a/src/storage/dd/Dd.h +++ b/src/storage/dd/Dd.h @@ -100,7 +100,7 @@ namespace storm { * * A pointer to the manager that is responsible for this DD. */ - std::shared_ptr const> getDdManager() const; + DdManager const& getDdManager() const; /*! * Retrieves the set of all meta variables contained in the DD. @@ -151,7 +151,7 @@ namespace storm { * @param ddManager The manager responsible for this DD. * @param containedMetaVariables The meta variables that appear in the DD. */ - Dd(std::shared_ptr const> ddManager, std::set const& containedMetaVariables = std::set()); + Dd(DdManager const& ddManager, std::set const& containedMetaVariables = std::set()); /*! * Retrieves the set of meta variables contained in both DDs. @@ -173,7 +173,7 @@ namespace storm { private: // A pointer to the manager responsible for this DD. - std::shared_ptr const> ddManager; + DdManager const* ddManager; // The meta variables that appear in this DD. std::set containedMetaVariables; diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp index 41295db4b..c295629f3 100644 --- a/src/storage/dd/DdManager.cpp +++ b/src/storage/dd/DdManager.cpp @@ -14,30 +14,30 @@ namespace storm { template Bdd DdManager::getBddOne() const { - return Bdd(this->shared_from_this(), internalDdManager.getBddOne()); + return Bdd(*this, internalDdManager.getBddOne()); } template template Add DdManager::getAddOne() const { - return Add(this->shared_from_this(), internalDdManager.template getAddOne()); + return Add(*this, internalDdManager.template getAddOne()); } template Bdd DdManager::getBddZero() const { - return Bdd(this->shared_from_this(), internalDdManager.getBddZero()); + return Bdd(*this, internalDdManager.getBddZero()); } template template Add DdManager::getAddZero() const { - return Add(this->shared_from_this(), internalDdManager.template getAddZero()); + return Add(*this, internalDdManager.template getAddZero()); } template template Add DdManager::getConstant(ValueType const& value) const { - return Add(this->shared_from_this(), internalDdManager.getConstant(value)); + return Add(*this, internalDdManager.getConstant(value)); } template @@ -114,8 +114,8 @@ namespace storm { std::vector> variablesPrime; for (std::size_t i = 0; i < numberOfBits; ++i) { auto ddVariablePair = internalDdManager.createNewDdVariablePair(); - variables.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.first, {unprimed})); - variablesPrime.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.second, {primed})); + variables.emplace_back(Bdd(*this, ddVariablePair.first, {unprimed})); + variablesPrime.emplace_back(Bdd(*this, ddVariablePair.second, {primed})); } metaVariableMap.emplace(unprimed, DdMetaVariable(name, low, high, variables)); @@ -138,8 +138,8 @@ namespace storm { std::vector> variables; std::vector> variablesPrime; auto ddVariablePair = internalDdManager.createNewDdVariablePair(); - variables.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.first, {unprimed})); - variablesPrime.emplace_back(Bdd(this->shared_from_this(), ddVariablePair.second, {primed})); + variables.emplace_back(Bdd(*this, ddVariablePair.first, {unprimed})); + variablesPrime.emplace_back(Bdd(*this, ddVariablePair.second, {primed})); metaVariableMap.emplace(unprimed, DdMetaVariable(name, variables)); metaVariableMap.emplace(primed, DdMetaVariable(name + "'", variablesPrime)); @@ -259,11 +259,6 @@ namespace storm { internalDdManager.triggerReordering(); } - template - std::shared_ptr const> DdManager::asSharedPointer() const { - return this->shared_from_this(); - } - template std::set DdManager::getAllMetaVariables() const { std::set result; diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h index f882ea57e..ca7fd4ca0 100644 --- a/src/storage/dd/DdManager.h +++ b/src/storage/dd/DdManager.h @@ -19,7 +19,7 @@ namespace storm { namespace dd { // Declare DdManager class so we can then specialize it for the different DD types. template - class DdManager : public std::enable_shared_from_this> { + class DdManager { public: friend class Bdd; @@ -172,14 +172,7 @@ namespace storm { * @return The corresponding meta variable. */ DdMetaVariable const& getMetaVariable(storm::expressions::Variable const& variable) const; - - /*! - * Retrieves the manager as a shared pointer. - * - * @return A shared pointer to the manager. - */ - std::shared_ptr const> asSharedPointer() const; - + /*! * Retrieves the set of meta variables contained in the DD. * @@ -261,15 +254,18 @@ namespace storm { * @return A pointer to the internal DD manager. */ InternalDdManager const* getInternalDdManagerPointer() const; + + // ATTENTION: as the DD packages typically perform garbage collection, the order of members is crucial here: + // First, the references to the DDs of the meta variables need to be disposed of and *then* the manager. + + // The DD manager that is customized according to the selected library type. + InternalDdManager internalDdManager; // A mapping from variables to the meta variable information. std::unordered_map> metaVariableMap; // The manager responsible for the variables. std::shared_ptr manager; - - // The DD manager that is customized according to the selected library type. - InternalDdManager internalDdManager; }; } } diff --git a/src/storage/dd/cudd/CuddAddIterator.cpp b/src/storage/dd/cudd/CuddAddIterator.cpp index 3f8f1a75c..e11b75aec 100644 --- a/src/storage/dd/cudd/CuddAddIterator.cpp +++ b/src/storage/dd/cudd/CuddAddIterator.cpp @@ -12,7 +12,7 @@ namespace storm { } template - AddIterator::AddIterator(std::shared_ptr const> ddManager, DdGen* generator, int* cube, ValueType const& value, bool isAtEnd, std::set const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(ddManager), generator(generator), cube(cube), valueAsDouble(static_cast(value)), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager->getExpressionManager().getSharedPointer()) { + AddIterator::AddIterator(DdManager const& ddManager, DdGen* generator, int* cube, ValueType const& value, bool isAtEnd, std::set const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(&ddManager), generator(generator), cube(cube), valueAsDouble(static_cast(value)), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager.getExpressionManager().getSharedPointer()) { // If the given generator is not yet at its end, we need to create the current valuation from the cube from // scratch. if (!this->isAtEnd) { @@ -163,7 +163,7 @@ namespace storm { if (this->isAtEnd && other.isAtEnd) { return true; } else { - return this->ddManager.get() == other.ddManager.get() && this->generator == other.generator + return this->ddManager == other.ddManager && this->generator == other.generator && this->cube == other.cube && this->valueAsDouble == other.valueAsDouble && this->isAtEnd == other.isAtEnd && this->metaVariables == other.metaVariables && this->cubeCounter == other.cubeCounter && this->relevantDontCareDdVariables == other.relevantDontCareDdVariables diff --git a/src/storage/dd/cudd/CuddAddIterator.h b/src/storage/dd/cudd/CuddAddIterator.h index 615056505..b037bd5bb 100644 --- a/src/storage/dd/cudd/CuddAddIterator.h +++ b/src/storage/dd/cudd/CuddAddIterator.h @@ -88,7 +88,7 @@ namespace storm { * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even * if a meta variable does not at all influence the the function value. */ - AddIterator(std::shared_ptr const> ddManager, DdGen* generator, int* cube, ValueType const& value, bool isAtEnd, std::set const* metaVariables = nullptr, bool enumerateDontCareMetaVariables = true); + AddIterator(DdManager const& ddManager, DdGen* generator, int* cube, ValueType const& value, bool isAtEnd, std::set const* metaVariables = nullptr, bool enumerateDontCareMetaVariables = true); /*! * Recreates the internal information when a new cube needs to be treated. @@ -101,7 +101,7 @@ namespace storm { void treatNextInCube(); // The manager responsible for the meta variables (and therefore the underlying DD). - std::shared_ptr const> ddManager; + DdManager const* ddManager; // The CUDD generator used to enumerate the cubes of the DD. DdGen* generator; diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 773845043..79c14734c 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -311,7 +311,7 @@ namespace storm { } template - AddIterator InternalAdd::begin(std::shared_ptr const> fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { + AddIterator InternalAdd::begin(DdManager const& fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { int* cube; double value; DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value); @@ -319,7 +319,7 @@ namespace storm { } template - AddIterator InternalAdd::end(std::shared_ptr const> fullDdManager, bool enumerateDontCareMetaVariables) const { + AddIterator InternalAdd::end(DdManager const& fullDdManager, bool enumerateDontCareMetaVariables) const { return AddIterator(fullDdManager, nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables); } diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index ddd153215..8543ffda5 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -459,7 +459,7 @@ namespace storm { * if a meta variable does not at all influence the the function value. * @return An iterator that points to the first meta variable assignment with a non-zero function value. */ - AddIterator begin(std::shared_ptr const> fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables = true) const; + AddIterator begin(DdManager const& fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables = true) const; /*! * Retrieves an iterator that points past the end of the container. @@ -469,7 +469,7 @@ namespace storm { * if a meta variable does not at all influence the the function value. * @return An iterator that points past the end of the container. */ - AddIterator end(std::shared_ptr const> fullDdManager, bool enumerateDontCareMetaVariables = true) const; + AddIterator end(DdManager const& fullDdManager, bool enumerateDontCareMetaVariables = true) const; /*! * Composes the ADD with an explicit vector by performing a specified function between the entries of this diff --git a/src/storage/dd/cudd/InternalCuddDdManager.cpp b/src/storage/dd/cudd/InternalCuddDdManager.cpp index b6c7fdbb0..d097b332c 100644 --- a/src/storage/dd/cudd/InternalCuddDdManager.cpp +++ b/src/storage/dd/cudd/InternalCuddDdManager.cpp @@ -34,6 +34,10 @@ namespace storm { } } + InternalDdManager::~InternalDdManager() { + // Intentionally left empty. + } + InternalBdd InternalDdManager::getBddOne() const { return InternalBdd(this, cuddManager.bddOne()); } diff --git a/src/storage/dd/cudd/InternalCuddDdManager.h b/src/storage/dd/cudd/InternalCuddDdManager.h index 884b69abb..4db5717a5 100644 --- a/src/storage/dd/cudd/InternalCuddDdManager.h +++ b/src/storage/dd/cudd/InternalCuddDdManager.h @@ -30,6 +30,11 @@ namespace storm { */ InternalDdManager(); + /*! + * Destroys the CUDD manager. + */ + ~InternalDdManager(); + /*! * Retrieves a BDD representing the constant one function. * diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index 1c30f59b5..0d7a8ca46 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -282,12 +282,12 @@ namespace storm { } template - AddIterator InternalAdd::begin(std::shared_ptr const> fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { + AddIterator InternalAdd::begin(DdManager const& fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } template - AddIterator InternalAdd::end(std::shared_ptr const> fullDdManager, bool enumerateDontCareMetaVariables) const { + AddIterator InternalAdd::end(DdManager const& fullDdManager, bool enumerateDontCareMetaVariables) const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.h b/src/storage/dd/sylvan/InternalSylvanAdd.h index 1f1f12079..60425d45d 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storage/dd/sylvan/InternalSylvanAdd.h @@ -457,7 +457,7 @@ namespace storm { * if a meta variable does not at all influence the the function value. * @return An iterator that points to the first meta variable assignment with a non-zero function value. */ - AddIterator begin(std::shared_ptr const> fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables = true) const; + AddIterator begin(DdManager const& fullDdManager, std::set const& metaVariables, bool enumerateDontCareMetaVariables = true) const; /*! * Retrieves an iterator that points past the end of the container. @@ -467,7 +467,7 @@ namespace storm { * if a meta variable does not at all influence the the function value. * @return An iterator that points past the end of the container. */ - AddIterator end(std::shared_ptr const> fullDdManager, bool enumerateDontCareMetaVariables = true) const; + AddIterator end(DdManager const& fullDdManager, bool enumerateDontCareMetaVariables = true) const; /*! * Composes the ADD with an explicit vector by performing a specified function between the entries of this diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp index 77ed14982..9aaaa6585 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -5,6 +5,8 @@ #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/NotSupportedException.h" +#include + namespace storm { namespace dd { uint_fast64_t InternalDdManager::numberOfInstances = 0; diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp index 030226d69..f2974a8cd 100644 --- a/test/functional/builder/DdPrismModelBuilderTest.cpp +++ b/test/functional/builder/DdPrismModelBuilderTest.cpp @@ -86,7 +86,7 @@ TEST(DdPrismModelBuilderTest_Sylvan, Ctmc) { model = storm::builder::DdPrismModelBuilder::translateProgram(program); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); - + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); EXPECT_EQ(810ul, model->getNumberOfStates()); diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 1c3132be1..5efec66b8 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -380,7 +380,7 @@ TEST(CuddDd, BddOddTest) { EXPECT_TRUE(i+1 == ddAsVector[i]); } - storm::dd::Add vectorAdd = storm::dd::Add::fromVector(manager, ddAsVector, odd, {x.first}); + storm::dd::Add vectorAdd = storm::dd::Add::fromVector(*manager, ddAsVector, odd, {x.first}); // Create a non-trivial matrix. dd = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)).template toAdd() * manager->getRange(x.first).template toAdd(); diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index c6baf90b1..c99925afc 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -63,50 +63,60 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); - - std::pair, storm::dd::Bdd> statesWithProbability01; - - ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("elected"))); - EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); - ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("elected"))); - EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); + { + std::pair, storm::dd::Bdd> statesWithProbability01; + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("elected"))); + EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("elected"))); + EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); + } program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); - - ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_0"))); - EXPECT_EQ(77ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(149ul, statesWithProbability01.second.getNonZeroCount()); - - ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_0"))); - EXPECT_EQ(74ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(198ul, statesWithProbability01.second.getNonZeroCount()); - ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_1"))); - EXPECT_EQ(94ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(33ul, statesWithProbability01.second.getNonZeroCount()); - - ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_1"))); - EXPECT_EQ(83ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount()); - + { + std::pair, storm::dd::Bdd> statesWithProbability01; + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_0"))); + EXPECT_EQ(77ul, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(149ul, statesWithProbability01.second.getNonZeroCount()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_0"))); + EXPECT_EQ(74ul, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(198ul, statesWithProbability01.second.getNonZeroCount()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_1"))); + EXPECT_EQ(94ul, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(33ul, statesWithProbability01.second.getNonZeroCount()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_1"))); + EXPECT_EQ(83ul, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount()); + } + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); model = storm::builder::DdPrismModelBuilder::translateProgram(program); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); - ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("collision_max_backoff"))); - EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount()); - - ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("collision_max_backoff"))); - EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount()); + { + std::pair, storm::dd::Bdd> statesWithProbability01; + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("collision_max_backoff"))); + EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("collision_max_backoff"))); + EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount()); + } } TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {