From 58eb54926c4980a90999423d3d7a33e316df6484 Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 3 Aug 2016 04:03:31 +0200 Subject: [PATCH] Fixed Sylvan bugs. Added a lot of debugging options and output, controlled by #define's. Added more template specializations for storm::RationalFunction. Former-commit-id: 416c32d196b0d848dbdaf1b292ccad198cfe1c74 --- .../sylvan/src/storm_function_wrapper.cpp | 324 ++++++++++------- .../sylvan/src/storm_function_wrapper.h | 15 +- resources/3rdparty/sylvan/src/sylvan_mtbdd.c | 127 ++++++- .../3rdparty/sylvan/src/sylvan_mtbdd_storm.c | 69 ++++ resources/3rdparty/sylvan/src/sylvan_obj.cpp | 6 +- .../sylvan/src/sylvan_obj_mtbdd_storm.hpp | 22 ++ .../3rdparty/sylvan/src/sylvan_obj_storm.cpp | 30 ++ .../src/sylvan_storm_rational_function.c | 99 ++++- .../src/sylvan_storm_rational_function.h | 4 +- src/storage/dd/DdManager.cpp | 16 +- src/storage/dd/sylvan/InternalSylvanAdd.cpp | 240 ++++++++++-- .../dd/sylvan/InternalSylvanDdManager.cpp | 341 +++++++++--------- test/functional/storage/SylvanDdTest.cpp | 21 +- 13 files changed, 925 insertions(+), 389 deletions(-) diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp index 15d2cdc66..74756d121 100644 --- a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp @@ -1,132 +1,192 @@ -#include "storm_function_wrapper.h" - -#include -#include "src/adapters/CarlAdapter.h" - -void storm_rational_function_init(storm_rational_function_ptr* a) { - storm_rational_function_ptr srf_ptr = static_cast(malloc(sizeof(storm_rational_function_ptr_struct))); - - if (srf_ptr == nullptr) { - return; - } - - srf_ptr->storm_rational_function = new storm::RationalFunction(*(storm::RationalFunction*)((*a)->storm_rational_function)); - - *a = srf_ptr; -} - -void storm_rational_function_destroy(storm_rational_function_ptr a) { - delete (storm::RationalFunction*)a->storm_rational_function; - a->storm_rational_function = nullptr; - free((void*)a); -} - -int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b) { - storm::RationalFunction* srf_a = (storm::RationalFunction*)a->storm_rational_function; - storm::RationalFunction* srf_b = (storm::RationalFunction*)b->storm_rational_function; - - if (*srf_a == *srf_b) { - return 0; - } - - return -1; -} - -storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b) { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b->storm_rational_function; - - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - *result_srf += srf_b; - - storm_rational_function_ptr result = (storm_rational_function_ptr)malloc(sizeof(storm_rational_function_ptr_struct)); - result->storm_rational_function = (void*)result_srf; - - return result; -} - -storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b) { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b->storm_rational_function; - - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - *result_srf -= srf_b; - - storm_rational_function_ptr result = (storm_rational_function_ptr)malloc(sizeof(storm_rational_function_ptr_struct)); - result->storm_rational_function = (void*)result_srf; - - return result; -} - -storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b) { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b->storm_rational_function; - - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - *result_srf *= srf_b; - - storm_rational_function_ptr result = (storm_rational_function_ptr)malloc(sizeof(storm_rational_function_ptr_struct)); - result->storm_rational_function = (void*)result_srf; - - return result; -} - -storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b) { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function; - storm::RationalFunction& srf_b = *(storm::RationalFunction*)b->storm_rational_function; - - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - *result_srf /= srf_b; - - storm_rational_function_ptr result = (storm_rational_function_ptr)malloc(sizeof(storm_rational_function_ptr_struct)); - result->storm_rational_function = (void*)result_srf; - - return result; -} - -uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function; - - size_t hash = carl::hash_value(srf_a); - uint64_t result = hash ^ seed; - - return result; -} - -storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a) { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function; - - storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); - *result_srf = -srf_a; - - storm_rational_function_ptr result = (storm_rational_function_ptr)malloc(sizeof(storm_rational_function_ptr_struct)); - result->storm_rational_function = (void*)result_srf; - - return result; -} - -int storm_rational_function_is_zero(storm_rational_function_ptr a) { - storm::RationalFunction& srf_a = *(storm::RationalFunction*)a->storm_rational_function; - - if (srf_a.isZero()) { - return 1; - } else { - return 0; - } -} - -storm_rational_function_ptr storm_rational_function_get_zero() { - static storm::RationalFunction zeroFunction(0); - static storm_rational_function_ptr_struct functionStruct; - functionStruct.storm_rational_function = (void*)&zeroFunction; - - return &functionStruct; -} - -storm_rational_function_ptr storm_rational_function_get_one() { - static storm::RationalFunction oneFunction(1); - static storm_rational_function_ptr_struct functionStruct; - functionStruct.storm_rational_function = (void*)&oneFunction; - - return &functionStruct; -} +#include "storm_function_wrapper.h" + +#include +#include +#include +#include "src/adapters/CarlAdapter.h" + +#undef DEBUG_STORM_FUNCTION_WRAPPER + +#ifdef DEBUG_STORM_FUNCTION_WRAPPER +#define LOG_I(funcName) std::cout << "Entering function " << funcName << std::endl; +#define LOG_O(funcName) std::cout << "Leaving function " << funcName << std::endl; +#else +#define LOG_I(funcName) +#define LOG_O(funcName) +#endif + +void storm_rational_function_init(storm_rational_function_ptr* a) { + LOG_I("init") + storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a))); + + if (srf_ptr == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_init()!" << std::endl; + return; + } + + *a = srf_ptr; + LOG_O("init") +} + +void storm_rational_function_destroy(storm_rational_function_ptr a) { + LOG_I("destroy") + delete (storm::RationalFunction*)a; + LOG_O("destroy") +} + +int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b) { + LOG_I("equals") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + + LOG_O("equals") + + int result = 0; + if (srf_a == srf_b) { + result = 1; + } + return result; +} + +storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b) { + LOG_I("plus") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_plus()!" << std::endl; + return (storm_rational_function_ptr)nullptr; + } + + *result_srf += srf_b; + + storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; + + LOG_O("plus") + return result; +} + +storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b) { + LOG_I("minus") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_minus()!" << std::endl; + return (storm_rational_function_ptr)nullptr; + } + + *result_srf -= srf_b; + + storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; + + LOG_O("minus") + return result; +} + +storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b) { + LOG_I("times") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_times()!" << std::endl; + return (storm_rational_function_ptr)nullptr; + } + + *result_srf *= srf_b; + + storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; + + LOG_O("times") + return result; +} + +storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b) { + LOG_I("divide") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_divide()!" << std::endl; + return (storm_rational_function_ptr)nullptr; + } + + *result_srf /= srf_b; + + storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; + + LOG_O("divide") + return result; +} + +uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) { + LOG_I("hash") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + + size_t hash = carl::hash_value(srf_a); + uint64_t result = hash ^ seed; + + LOG_O("hash") + return result; +} + +storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a) { + LOG_I("negate") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_negate()!" << std::endl; + return (storm_rational_function_ptr)nullptr; + } + + *result_srf = -srf_a; + + storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; + + LOG_O("negate") + return result; +} + +int storm_rational_function_is_zero(storm_rational_function_ptr a) { + LOG_I("isZero") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + + if (srf_a.isZero()) { + return 1; + } else { + return 0; + } +} + +storm_rational_function_ptr storm_rational_function_get_zero() { + static storm::RationalFunction zeroFunction(0); + LOG_I("getZero") + //return new storm::RationalFunction(0); + return (storm_rational_function_ptr)(&zeroFunction); +} + +storm_rational_function_ptr storm_rational_function_get_one() { + static storm::RationalFunction oneFunction(1); + LOG_I("getOne") + //return new storm::RationalFunction(1); + return (storm_rational_function_ptr)(&oneFunction); +} + +void print_storm_rational_function(storm_rational_function_ptr a) { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + std::cout << srf_a << std::flush; +} + +void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out) { + std::stringstream ss; + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + ss << srf_a; + std::string s = ss.str(); + fprintf(out, "%s", s.c_str()); +} diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.h b/resources/3rdparty/sylvan/src/storm_function_wrapper.h index 08b9f9471..ca5107dcb 100644 --- a/resources/3rdparty/sylvan/src/storm_function_wrapper.h +++ b/resources/3rdparty/sylvan/src/storm_function_wrapper.h @@ -2,17 +2,13 @@ #define SYLVAN_STORM_FUNCTION_WRAPPER_H #include +#include #ifdef __cplusplus extern "C" { #endif -typedef struct { - void* storm_rational_function; -} storm_rational_function_ptr_struct; -typedef storm_rational_function_ptr_struct storm_rational_function_t[1]; -typedef storm_rational_function_ptr_struct* storm_rational_function_ptr; - +typedef void* storm_rational_function_ptr; // equals, plus, minus, divide, times, create, destroy void storm_rational_function_init(storm_rational_function_ptr* a); @@ -29,8 +25,13 @@ int storm_rational_function_is_zero(storm_rational_function_ptr a); storm_rational_function_ptr storm_rational_function_get_zero(); storm_rational_function_ptr storm_rational_function_get_one(); +void print_storm_rational_function(storm_rational_function_ptr a); +void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out); + +int storm_rational_function_is_zero(storm_rational_function_ptr a); + #ifdef __cplusplus } #endif -#endif // SYLVAN_STORM_FUNCTION_WRAPPER_H \ No newline at end of file +#endif // SYLVAN_STORM_FUNCTION_WRAPPER_H diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index a4eb1bd62..ac5a8261f 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -31,6 +31,11 @@ #include #include +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) +#include +#include +#endif + /* Primitives */ int mtbdd_isleaf(MTBDD bdd) @@ -264,9 +269,15 @@ _mtbdd_create_cb(uint64_t *a, uint64_t *b) // for leaf if ((*a & 0x4000000000000000) == 0) return; // huh? uint32_t type = *a & 0xffffffff; - if (type >= cl_registry_count) return; // not in registry + if (type >= cl_registry_count) { // not in registry + printf("ERROR: type >= cl_registry_count!"); + return; + } customleaf_t *c = cl_registry + type; - if (c->create_cb == NULL) return; // not in registry + if (c->create_cb == NULL) { // not in registry + printf("ERROR: create_cb is NULL!"); + return; + } c->create_cb(b); } @@ -276,9 +287,15 @@ _mtbdd_destroy_cb(uint64_t a, uint64_t b) // for leaf if ((a & 0x4000000000000000) == 0) return; // huh? uint32_t type = a & 0xffffffff; - if (type >= cl_registry_count) return; // not in registry + if (type >= cl_registry_count) { // not in registry + printf("ERROR: type >= cl_registry_count! (2)"); + return; + } customleaf_t *c = cl_registry + type; - if (c->destroy_cb == NULL) return; // not in registry + if (c->destroy_cb == NULL) { // not in registry + printf("ERROR: destroy_cb is NULL!"); + return; + } c->destroy_cb(b); } @@ -833,6 +850,11 @@ TASK_2(MTBDD, mtbdd_uop_times_uint, MTBDD, a, size_t, k) uint32_t c = gcd(d, (uint32_t)k); return mtbdd_fraction(n*(k/c), d/c); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_uop_times_uint type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + } +#endif } return mtbdd_invalid; @@ -857,6 +879,11 @@ TASK_2(MTBDD, mtbdd_uop_pow_uint, MTBDD, a, size_t, k) uint64_t v = mtbddnode_getvalue(na); return mtbdd_fraction(pow((int32_t)(v>>32), k), (uint32_t)v); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_uop_pow_uint type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + } +#endif } return mtbdd_invalid; @@ -1017,6 +1044,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_plus, MTBDD*, pa, MTBDD*, pb) // add return mtbdd_fraction(nom_a + nom_b, denom_a); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_plus type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + } +#endif } if (a < b) { @@ -1066,6 +1098,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_minus, MTBDD*, pa, MTBDD*, pb) // subtract return mtbdd_fraction(nom_a - nom_b, denom_a); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) && (mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_minus type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + } +#endif } return mtbdd_invalid; @@ -1113,6 +1150,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_times, MTBDD*, pa, MTBDD*, pb) denom_a *= (denom_b/d); return mtbdd_fraction(nom_a, denom_a); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) && (mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_times type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + } +#endif } if (a < b) { @@ -1169,6 +1211,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_min, MTBDD*, pa, MTBDD*, pb) // compute lowest return nom_a < nom_b ? a : b; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) && (mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_min type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + } +#endif } if (a < b) { @@ -1223,6 +1270,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_max, MTBDD*, pa, MTBDD*, pb) // compute highest return nom_a > nom_b ? a : b; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) && (mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_max type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + } +#endif } if (a < b) { @@ -1252,6 +1304,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_negate, MTBDD, a, size_t, k) uint64_t v = mtbddnode_getvalue(na); return mtbdd_fraction(-(int32_t)(v>>32), (uint32_t)v); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_negate type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + } +#endif } return mtbdd_invalid; @@ -1335,6 +1392,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_threshold_double, MTBDD, a, size_t, svalue) d /= mtbdd_getdenom(a); return d >= value ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_threshold_double type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + } +#endif } return mtbdd_invalid; @@ -1361,6 +1423,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_strict_threshold_double, MTBDD, a, size_t, svalue) d /= mtbdd_getdenom(a); return d > value ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_strict_threshold_double type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + } +#endif } return mtbdd_invalid; @@ -1566,6 +1633,11 @@ TASK_3(MTBDD, mtbdd_leq_rec, MTBDD, a, MTBDD, b, int*, shortcircuit) nom_b *= da/c; result = nom_a <= nom_b ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR: mtbdd_leq_rec type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n"); + } +#endif } else { /* Get top variable */ uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); @@ -1651,6 +1723,11 @@ TASK_3(MTBDD, mtbdd_less_rec, MTBDD, a, MTBDD, b, int*, shortcircuit) nom_b *= da/c; result = nom_a < nom_b ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR: mtbdd_less_rec type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n"); + } +#endif } else { /* Get top variable */ uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); @@ -1736,6 +1813,11 @@ TASK_3(MTBDD, mtbdd_geq_rec, MTBDD, a, MTBDD, b, int*, shortcircuit) nom_b *= da/c; result = nom_a >= nom_b ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR: mtbdd_geq_rec type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n"); + } +#endif } else { /* Get top variable */ uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); @@ -1821,6 +1903,11 @@ TASK_3(MTBDD, mtbdd_greater_rec, MTBDD, a, MTBDD, b, int*, shortcircuit) nom_b *= da/c; result = nom_a > nom_b ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR: mtbdd_greater_rec type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n"); + } +#endif } else { /* Get top variable */ uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); @@ -2041,6 +2128,11 @@ TASK_IMPL_1(MTBDD, mtbdd_minimum, MTBDD, a) nom_h *= denom_l/c; result = nom_l < nom_h ? low : high; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(nl) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nh) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR: mtbdd_minimum type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n"); + } +#endif /* Store in cache */ cache_put3(CACHE_MTBDD_MINIMUM, a, 0, 0, result); @@ -2089,6 +2181,11 @@ TASK_IMPL_1(MTBDD, mtbdd_maximum, MTBDD, a) nom_h *= denom_l/c; result = nom_l > nom_h ? low : high; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(nl) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nh) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR: mtbdd_maximum type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n"); + } +#endif /* Store in cache */ cache_put3(CACHE_MTBDD_MAXIMUM, a, 0, 0, result); @@ -2237,12 +2334,20 @@ mtbdd_unmark_rec(MTBDD mtbdd) static size_t mtbdd_leafcount_mark(MTBDD mtbdd) { - if (mtbdd == mtbdd_true) return 0; // do not count true/false leaf - if (mtbdd == mtbdd_false) return 0; // do not count true/false leaf + if (mtbdd == mtbdd_true) { // do not count true/false leaf + return 0; + } + if (mtbdd == mtbdd_false) { // do not count true/false leaf + return 0; + } mtbddnode_t n = GETNODE(mtbdd); - if (mtbddnode_getmark(n)) return 0; + if (mtbddnode_getmark(n)) { + return 0; + } mtbddnode_setmark(n, 1); - if (mtbddnode_isleaf(n)) return 1; // count leaf as 1 + if (mtbddnode_isleaf(n)) { // count leaf as 1 + return 1; + } return mtbdd_leafcount_mark(mtbddnode_getlow(n)) + mtbdd_leafcount_mark(mtbddnode_gethigh(n)); } @@ -2372,6 +2477,12 @@ mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd, print_terminal_label_cb cb) case 2: fprintf(out, "%u/%u", (uint32_t)(value>>32), (uint32_t)value); break; +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + case SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID: + fprintf(out, "srf::"); + print_storm_rational_function_to_file((storm_rational_function_ptr)value, out); + break; +#endif default: cb(out, type, value); break; diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c index dab4860c0..2d0796a40 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c @@ -97,6 +97,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb) MTBDD result = mtbdd_fraction(nom_a, denom_a); return result; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_divide type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } return mtbdd_invalid; @@ -140,6 +146,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_equals, MTBDD*, pa, MTBDD*, pb) if (nom_a == nom_b && denom_a == denom_b) return mtbdd_true; return mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_equals type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } if (a < b) { @@ -187,6 +199,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less, MTBDD*, pa, MTBDD*, pb) uint64_t denom_b = val_b&0xffffffff; return nom_a * denom_b < nom_b * denom_a ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_less type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } return mtbdd_invalid; @@ -230,6 +248,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, pa, MTBDD*, pb) nom_b *= denom_a; return nom_a <= nom_b ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_less_or_equal type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } return mtbdd_invalid; @@ -261,6 +285,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_pow, MTBDD*, pa, MTBDD*, pb) } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) { assert(0); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_pow type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } return mtbdd_invalid; @@ -292,6 +322,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_mod, MTBDD*, pa, MTBDD*, pb) } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) { assert(0); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_mod type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } return mtbdd_invalid; @@ -323,6 +359,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_logxy, MTBDD*, pa, MTBDD*, pb) } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) { assert(0); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_logxy type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } return mtbdd_invalid; @@ -345,6 +387,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_not_zero, MTBDD, a, size_t, v) } else if (mtbddnode_gettype(na) == 2) { return mtbdd_getnumer(a) != 0 ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + return storm_rational_function_is_zero((storm_rational_function_ptr)mtbdd_getvalue(a)) == 0 ? mtbdd_true : mtbdd_false; + } +#endif } // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). @@ -377,6 +424,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_floor, MTBDD, a, size_t, v) MTBDD result = mtbdd_fraction(mtbdd_getnumer(a) / mtbdd_getdenom(a), 1); return result; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_floor type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). @@ -409,6 +462,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_ceil, MTBDD, a, size_t, v) MTBDD result = mtbdd_fraction(mtbdd_getnumer(a) / mtbdd_getdenom(a) + 1, 1); return result; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_ceil type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). @@ -474,6 +533,11 @@ TASK_IMPL_2(double, mtbdd_non_zero_count, MTBDD, dd, size_t, nvars) } else if (mtbddnode_gettype(na) == 2) { return mtbdd_getnumer(dd) != 0 ? powl(2.0L, nvars) : 0.0; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + return storm_rational_function_is_zero((storm_rational_function_ptr)mtbdd_getvalue(dd)) == 0 ? powl(2.0L, nvars) : 0.0; + } +#endif } /* Perhaps execute garbage collection */ @@ -506,6 +570,11 @@ int mtbdd_iszero(MTBDD dd) { } else if (mtbdd_gettype(dd) == 2) { return mtbdd_getnumer(dd) == 0; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbdd_gettype(dd) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + return storm_rational_function_is_zero((storm_rational_function_ptr)mtbdd_getvalue(dd)) == 1 ? 1 : 0; + } +#endif return 0; } diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.cpp b/resources/3rdparty/sylvan/src/sylvan_obj.cpp index b7b4484fb..b9d0c77f2 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.cpp @@ -609,9 +609,8 @@ Mtbdd::doubleTerminal(double value) Mtbdd Mtbdd::stormRationalFunctionTerminal(storm::RationalFunction const& value) { - storm_rational_function_ptr_struct functionStruct; - functionStruct.storm_rational_function = (void*)(&value); - return mtbdd_storm_rational_function(&functionStruct); + storm_rational_function_ptr ptr = (storm_rational_function_ptr)(&value); + return mtbdd_storm_rational_function(ptr); } #endif @@ -1039,6 +1038,7 @@ void Sylvan::initMtbdd() { sylvan_init_mtbdd(); + sylvan_storm_rational_function_init(); } void diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp index 26e5ea4be..83a89f138 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp @@ -8,6 +8,28 @@ */ Mtbdd Divide(const Mtbdd &other) const; +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + /** + * @brief Computes f + g for Rational Functions + */ + Mtbdd PlusRF(const Mtbdd &other) const; + + /** + * @brief Computes f * g for Rational Functions + */ + Mtbdd TimesRF(const Mtbdd &other) const; + + /** + * @brief Computes f - g for Rational Functions + */ + Mtbdd MinusRF(const Mtbdd &other) const; + + /** + * @brief Computes f / g for Rational Functions + */ + Mtbdd DivideRF(const Mtbdd &other) const; +#endif + Bdd NotZero() const; Bdd Equals(const Mtbdd& other) const; diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index f64ffeaa2..837e906a2 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -16,6 +16,36 @@ Bdd::toStormRationalFunctionMtbdd() const { LACE_ME; return mtbdd_bool_to_storm_rational_function(bdd); } + +Mtbdd +Mtbdd::PlusRF(const Mtbdd &other) const +{ + LACE_ME; + return sylvan_storm_rational_function_plus(mtbdd, other.mtbdd); +} + + +Mtbdd +Mtbdd::TimesRF(const Mtbdd &other) const +{ + LACE_ME; + return sylvan_storm_rational_function_times(mtbdd, other.mtbdd); +} + +Mtbdd +Mtbdd::MinusRF(const Mtbdd &other) const +{ + LACE_ME; + return sylvan_storm_rational_function_minus(mtbdd, other.mtbdd); +} + +Mtbdd +Mtbdd::DivideRF(const Mtbdd &other) const +{ + LACE_ME; + return sylvan_storm_rational_function_divide(mtbdd, other.mtbdd); +} + #endif Mtbdd diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c index 2b35ed91a..9ecc754b5 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c @@ -15,6 +15,18 @@ #include +#undef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG + +#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG +int depth = 0; + +#define LOG_I(funcName) do { for (int i = 0; i < depth; ++i) { printf(" "); } ++depth; printf("Entering function " funcName "\n"); } while (0 != 0); +#define LOG_O(funcName) do { --depth; for (int i = 0; i < depth; ++i) { printf(" "); } printf("Leaving function " funcName "\n"); } while (0 != 0); +#else +#define LOG_I(funcName) +#define LOG_O(funcName) +#endif + /** * helper function for hash */ @@ -29,42 +41,73 @@ rotl64(uint64_t x, int8_t r) static uint64_t sylvan_storm_rational_function_hash(const uint64_t v, const uint64_t seed) { + LOG_I("i-hash") /* Hash the storm::RationalFunction in pointer v */ - storm_rational_function_ptr x = (storm_rational_function_ptr)(size_t)v; + storm_rational_function_ptr x = (storm_rational_function_ptr)v; + + uint64_t hash = storm_rational_function_hash(x, seed); + +#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG + printf("Hashing ptr %p with contents ", x); + print_storm_rational_function(x); + printf(" with seed %zu, hash = %zu\n", seed, hash); +#endif - return storm_rational_function_hash(x, seed); + LOG_O("i-hash") + return hash; } static int sylvan_storm_rational_function_equals(const uint64_t left, const uint64_t right) { + LOG_I("i-equals") /* This function is called by the unique table when comparing a new leaf with an existing leaf */ storm_rational_function_ptr a = (storm_rational_function_ptr)(size_t)left; storm_rational_function_ptr b = (storm_rational_function_ptr)(size_t)right; /* Just compare x and y */ - return (storm_rational_function_equals(a, b) == 0) ? 1 : 0; + int result = storm_rational_function_equals(a, b); + + LOG_O("i-equals") + return result; } static void sylvan_storm_rational_function_create(uint64_t *val) { - printf("sylvan_storm_rational_function_create(val = %zu)\n", *val); + LOG_I("i-create") + +#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG + void* tmp = (void*)*val; + printf("sylvan_storm_rational_function_create(ptr = %p, value = ", tmp); + print_storm_rational_function(*((storm_rational_function_ptr*)(size_t)val)); + printf(")\n"); +#endif + /* This function is called by the unique table when a leaf does not yet exist. We make a copy, which will be stored in the hash table. */ storm_rational_function_ptr* x = (storm_rational_function_ptr*)(size_t)val; storm_rational_function_init(x); + +#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG + tmp = (void*)*val; + printf("sylvan_storm_rational_function_create_2(ptr = %p)\n", tmp); +#endif + + LOG_O("i-create") } static void sylvan_storm_rational_function_destroy(uint64_t val) { + LOG_I("i-destroy") /* This function is called by the unique table when a leaf is removed during garbage collection. */ storm_rational_function_ptr x = (storm_rational_function_ptr)(size_t)val; storm_rational_function_destroy(x); + LOG_O("i-destroy") } static uint32_t sylvan_storm_rational_function_type; @@ -78,6 +121,12 @@ sylvan_storm_rational_function_init() { /* Register custom leaf 3 */ sylvan_storm_rational_function_type = mtbdd_register_custom_leaf(sylvan_storm_rational_function_hash, sylvan_storm_rational_function_equals, sylvan_storm_rational_function_create, sylvan_storm_rational_function_destroy); + + if (SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID != sylvan_storm_rational_function_type) { + printf("ERROR - ERROR - ERROR\nThe Sylvan Type ID is NOT correct.\nIt was assumed to be %u, but it is actually %u!\nYou NEED to fix this by changing the macro \"SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\" and recompiling StoRM!\n\n", SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID, sylvan_storm_rational_function_type); + assert(0); + } + CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS = cache_next_opid(); } @@ -89,11 +138,21 @@ uint32_t sylvan_storm_rational_function_get_type() { * Create storm::RationalFunction leaf */ MTBDD -mtbdd_storm_rational_function(storm_rational_function_t val) +mtbdd_storm_rational_function(storm_rational_function_ptr val) { + LOG_I("i-mtbdd_") uint64_t terminalValue = (uint64_t)val; - printf("mtbdd_storm_rational_function(val = %zu)\n", terminalValue); - return mtbdd_makeleaf(sylvan_storm_rational_function_type, terminalValue); + +#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG + printf("mtbdd_storm_rational_function(ptr = %p, value = ", val); + print_storm_rational_function(val); + printf(")\n"); +#endif + + MTBDD result = mtbdd_makeleaf(sylvan_storm_rational_function_type, terminalValue); + + LOG_O("i-mtbdd_") + return result; } /** @@ -101,21 +160,30 @@ mtbdd_storm_rational_function(storm_rational_function_t val) */ TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, a, size_t, v) { + LOG_I("task_impl_2 to_srf") if (a == mtbdd_false) { - return mtbdd_storm_rational_function(storm_rational_function_get_zero()); + storm_rational_function_ptr srf_zero = storm_rational_function_get_zero(); + MTBDD result = mtbdd_storm_rational_function(srf_zero); + LOG_O("task_impl_2 to_srf - ZERO") + return result; } if (a == mtbdd_true) { - return mtbdd_storm_rational_function(storm_rational_function_get_one()); + storm_rational_function_ptr srf_one = storm_rational_function_get_one(); + MTBDD result = mtbdd_storm_rational_function(srf_one); + LOG_O("task_impl_2 to_srf - ONE") + return result; } // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). (void)v; - + + LOG_O("task_impl_2 to_srf - INVALID") return mtbdd_invalid; } TASK_IMPL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD, dd) { + LOG_I("task_impl_1 to_srf") return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_storm_rational_function), 0); } @@ -125,6 +193,7 @@ TASK_IMPL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD, dd) */ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, pa, MTBDD*, pb) { + LOG_I("task_impl_2 op_plus") MTBDD a = *pa, b = *pb; /* Check for partial functions */ @@ -159,7 +228,8 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, pa, MTBDD*, p */ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, pa, MTBDD*, pb) { - MTBDD a = *pa, b = *pb; + LOG_I("task_impl_2 op_minus") + MTBDD a = *pa, b = *pb; /* Check for partial functions */ if (a == mtbdd_false) return sylvan_storm_rational_function_neg(b); @@ -188,6 +258,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, pa, MTBDD*, */ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, pa, MTBDD*, pb) { + LOG_I("task_impl_2 op_times") MTBDD a = *pa, b = *pb; /* Check for partial functions and for Boolean (filter) */ @@ -202,7 +273,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, pa, MTBDD*, storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); - storm_rational_function_ptr mres = storm_rational_function_times(ma, mb); + storm_rational_function_ptr mres = storm_rational_function_times(ma, mb); MTBDD res = mtbdd_storm_rational_function(mres); // TODO: Delete mres? @@ -225,6 +296,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, pa, MTBDD*, */ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*, pb) { + LOG_I("task_impl_2 op_divide") MTBDD a = *pa, b = *pb; /* Check for partial functions */ @@ -254,6 +326,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*, TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, a, MTBDD, b, int, k) { + LOG_I("task_impl_3 abstract_op_plus") if (k==0) { return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_plus)); } else { @@ -269,6 +342,7 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, a, MT TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, a, MTBDD, b, int, k) { + LOG_I("task_impl_3 abstract_op_times") if (k==0) { return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_times)); } else { @@ -287,6 +361,7 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, a, M */ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, dd, size_t, p) { + LOG_I("task_impl_2 op_neg") /* Handle partial functions */ if (dd == mtbdd_false) return mtbdd_false; diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h index fd4ad7f3a..f6effbb66 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h @@ -12,6 +12,8 @@ #if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) +#define SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID (3) + #ifdef __cplusplus extern "C" { #endif /* __cplusplus */ @@ -29,7 +31,7 @@ uint32_t sylvan_storm_rational_function_get_type(); /** * Create storm::RationalFunction leaf */ -MTBDD mtbdd_storm_rational_function(storm_rational_function_t val); +MTBDD mtbdd_storm_rational_function(storm_rational_function_ptr val); /** * Monad that converts Boolean to a storm::RationalFunction MTBDD, translate terminals true to 1 and to 0 otherwise; diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp index 7a1a9ab8d..7a8df8f21 100644 --- a/src/storage/dd/DdManager.cpp +++ b/src/storage/dd/DdManager.cpp @@ -10,6 +10,7 @@ #include "src/adapters/CarlAdapter.h" #include +#include namespace storm { namespace dd { @@ -105,21 +106,6 @@ namespace storm { } return result; } - -#ifdef STORM_HAVE_CARL - template<> - template<> - Add DdManager::getIdentity(storm::expressions::Variable const& variable) const { - storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); - - Add result = this->getAddZero(); - for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { - storm::RationalFunction constantFunction(value); - result += this->getEncoding(variable, value).template toAdd() * this->getConstant(constantFunction); - } - return result; - } -#endif template std::pair DdManager::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high) { diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index 51c072126..4b301adf6 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -33,126 +33,298 @@ namespace storm { InternalAdd InternalAdd::operator+(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Plus(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::operator+(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.PlusRF(other.sylvanMtbdd)); + } +#endif + template InternalAdd& InternalAdd::operator+=(InternalAdd const& other) { this->sylvanMtbdd = this->sylvanMtbdd.Plus(other.sylvanMtbdd); return *this; } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd& InternalAdd::operator+=(InternalAdd const& other) { + this->sylvanMtbdd = this->sylvanMtbdd.PlusRF(other.sylvanMtbdd); + return *this; + } +#endif + template InternalAdd InternalAdd::operator*(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Times(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::operator*(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.TimesRF(other.sylvanMtbdd)); + } +#endif + template InternalAdd& InternalAdd::operator*=(InternalAdd const& other) { this->sylvanMtbdd = this->sylvanMtbdd.Times(other.sylvanMtbdd); return *this; } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd& InternalAdd::operator*=(InternalAdd const& other) { + this->sylvanMtbdd = this->sylvanMtbdd.TimesRF(other.sylvanMtbdd); + return *this; + } +#endif + template InternalAdd InternalAdd::operator-(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Minus(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::operator-(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.MinusRF(other.sylvanMtbdd)); + } +#endif + template InternalAdd& InternalAdd::operator-=(InternalAdd const& other) { this->sylvanMtbdd = this->sylvanMtbdd.Minus(other.sylvanMtbdd); return *this; } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd& InternalAdd::operator-=(InternalAdd const& other) { + this->sylvanMtbdd = this->sylvanMtbdd.MinusRF(other.sylvanMtbdd); + return *this; + } +#endif + template InternalAdd InternalAdd::operator/(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Divide(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::operator/(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.DivideRF(other.sylvanMtbdd)); + } +#endif + template InternalAdd& InternalAdd::operator/=(InternalAdd const& other) { this->sylvanMtbdd = this->sylvanMtbdd.Divide(other.sylvanMtbdd); return *this; } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd& InternalAdd::operator/=(InternalAdd const& other) { + this->sylvanMtbdd = this->sylvanMtbdd.DivideRF(other.sylvanMtbdd); + return *this; + } +#endif + template InternalBdd InternalAdd::equals(InternalAdd const& other) const { return InternalBdd(ddManager, this->sylvanMtbdd.Equals(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalBdd InternalAdd::equals(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Equals"); + } +#endif + template InternalBdd InternalAdd::notEquals(InternalAdd const& other) const { return !this->equals(other); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalBdd InternalAdd::notEquals(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Not Equals"); + } +#endif + template InternalBdd InternalAdd::less(InternalAdd const& other) const { return InternalBdd(ddManager, this->sylvanMtbdd.Less(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalBdd InternalAdd::less(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Less"); + } +#endif + template InternalBdd InternalAdd::lessOrEqual(InternalAdd const& other) const { return InternalBdd(ddManager, this->sylvanMtbdd.LessOrEqual(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalBdd InternalAdd::lessOrEqual(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Less or Equal"); + } +#endif + template InternalBdd InternalAdd::greater(InternalAdd const& other) const { return !this->lessOrEqual(other); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalBdd InternalAdd::greater(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Greater"); + } +#endif + template InternalBdd InternalAdd::greaterOrEqual(InternalAdd const& other) const { return !this->less(other); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalBdd InternalAdd::greaterOrEqual(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Greater or Equal"); + } +#endif + template InternalAdd InternalAdd::pow(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Pow(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::pow(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Pow"); + } +#endif + template InternalAdd InternalAdd::mod(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Mod(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::mod(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Mod"); + } +#endif + template InternalAdd InternalAdd::logxy(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Logxy(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::logxy(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: logxy"); + } +#endif + template InternalAdd InternalAdd::floor() const { return InternalAdd(ddManager, this->sylvanMtbdd.Floor()); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::floor() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Floor"); + } +#endif + template InternalAdd InternalAdd::ceil() const { return InternalAdd(ddManager, this->sylvanMtbdd.Ceil()); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::ceil() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Ceil"); + } +#endif + template InternalAdd InternalAdd::minimum(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Min(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::minimum(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Minimum"); + } +#endif + template InternalAdd InternalAdd::maximum(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Max(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::maximum(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Maximum"); + } +#endif + template InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractPlus(cube.sylvanBdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: sumAbstract"); + } +#endif + template InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMin(cube.sylvanBdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstract"); + } +#endif + template InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMax(cube.sylvanBdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: maxAbstract"); + } +#endif + template bool InternalAdd::equalModuloPrecision(InternalAdd const& other, double precision, bool relative) const { if (relative) { @@ -161,7 +333,14 @@ namespace storm { return this->sylvanMtbdd.EqualNorm(other.sylvanMtbdd, precision); } } - + +#ifdef STORM_HAVE_CARL + template<> + bool InternalAdd::equalModuloPrecision(InternalAdd const& other, double precision, bool relative) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: equalModuloPrecision"); + } +#endif + template InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { std::vector fromIndices; @@ -615,10 +794,9 @@ namespace storm { template MTBDD InternalAdd::getLeaf(storm::RationalFunction const& value) { - storm_rational_function_ptr_struct helperStruct; - helperStruct.storm_rational_function = (void*)(&value); + storm_rational_function_ptr ptr = (storm_rational_function_ptr)(&value); - return mtbdd_storm_rational_function(&helperStruct); + return mtbdd_storm_rational_function(ptr); } template @@ -639,7 +817,7 @@ namespace storm { else if (std::is_same::value) { STORM_LOG_ASSERT(false, "Non-specialized version of getValue() called for storm::RationalFunction value."); } -#endif +#endif else { STORM_LOG_ASSERT(false, "Illegal or unknown type in MTBDD."); } @@ -655,9 +833,9 @@ namespace storm { STORM_LOG_ASSERT(mtbdd_gettype(node) == sylvan_storm_rational_function_get_type(), "Expected a storm::RationalFunction value."); uint64_t value = mtbdd_getvalue(node); - storm_rational_function_ptr_struct* helperStructPtr = (storm_rational_function_ptr_struct*)value; + storm_rational_function_ptr ptr = (storm_rational_function_ptr)value; - storm::RationalFunction* rationalFunction = (storm::RationalFunction*)(helperStructPtr->storm_rational_function); + storm::RationalFunction* rationalFunction = (storm::RationalFunction*)(ptr); return negated ? -(*rationalFunction) : (*rationalFunction); } diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp index 287fe55c3..fffc82ec9 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -1,175 +1,166 @@ -#include "src/storage/dd/sylvan/InternalSylvanDdManager.h" - -#include - -#include "src/settings/SettingsManager.h" -#include "src/settings/modules/SylvanSettings.h" - -#include "src/utility/constants.h" -#include "src/utility/macros.h" -#include "src/exceptions/NotSupportedException.h" - -#include "src/utility/sylvan.h" - -#include "storm-config.h" -// TODO: Remove this later on. -#ifndef STORM_HAVE_CARL -#define STORM_HAVE_CARL 1 -#endif - -namespace storm { - namespace dd { - uint_fast64_t InternalDdManager::numberOfInstances = 0; - - // It is important that the variable pairs start at an even offset, because sylvan assumes this to be true for - // some operations. - uint_fast64_t InternalDdManager::nextFreeVariableIndex = 0; - - uint_fast64_t findLargestPowerOfTwoFitting(uint_fast64_t number) { - for (uint_fast64_t index = 0; index < 64; ++index) { - if ((number & (1ull << (63 - index))) != 0) { - return 63 - index; - } - } - return 0; - } - - InternalDdManager::InternalDdManager() { - if (numberOfInstances == 0) { - // Initialize lace: auto-detect number of workers. - lace_init(storm::settings::getModule().getNumberOfThreads(), 1000000); - lace_startup(0, 0, 0); - - // Each node takes 24 bytes and the maximal memory is specified in megabytes. - uint_fast64_t totalNodesToStore = storm::settings::getModule().getMaximalMemory() * 1024 * 1024 / 24; - - // Compute the power of two that still fits within the total numbers to store. - uint_fast64_t powerOfTwo = findLargestPowerOfTwoFitting(totalNodesToStore); - - sylvan::Sylvan::initPackage(1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 8 : 0ull), 1ull << (powerOfTwo - 1), 1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 12 : 0ull), 1ull << (powerOfTwo - 1)); - sylvan::Sylvan::initBdd(1); - sylvan::Sylvan::initMtbdd(); - } - ++numberOfInstances; - } - - InternalDdManager::~InternalDdManager() { - --numberOfInstances; - if (numberOfInstances == 0) { - // Enable this to print the sylvan statistics to a file. -// FILE* filePointer = fopen("sylvan.stats", "w"); -// sylvan_stats_report(filePointer, 0); -// fclose(filePointer); - - sylvan::Sylvan::quitPackage(); - lace_exit(); - } - } - - InternalBdd InternalDdManager::getBddOne() const { - return InternalBdd(this, sylvan::Bdd::bddOne()); - } - - template<> - InternalAdd InternalDdManager::getAddOne() const { - return InternalAdd(this, sylvan::Mtbdd::doubleTerminal(storm::utility::one())); - } - - template<> - InternalAdd InternalDdManager::getAddOne() const { - return InternalAdd(this, sylvan::Mtbdd::int64Terminal(storm::utility::one())); - } - -#ifdef STORM_HAVE_CARL - template<> - InternalAdd InternalDdManager::getAddOne() const { - storm::RationalFunction rationalFunction = storm::utility::one(); - storm_rational_function_ptr_struct helperStruct; - helperStruct.storm_rational_function = (void*)(&rationalFunction); - uint64_t value = (uint64_t)&helperStruct; - - return InternalAdd(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), value)); - } -#endif - - InternalBdd InternalDdManager::getBddZero() const { - return InternalBdd(this, sylvan::Bdd::bddZero()); - } - - template<> - InternalAdd InternalDdManager::getAddZero() const { - return InternalAdd(this, sylvan::Mtbdd::doubleTerminal(storm::utility::zero())); - } - - template<> - InternalAdd InternalDdManager::getAddZero() const { - return InternalAdd(this, sylvan::Mtbdd::int64Terminal(storm::utility::zero())); - } - -#ifdef STORM_HAVE_CARL - template<> - InternalAdd InternalDdManager::getAddZero() const { - storm::RationalFunction rationalFunction = storm::utility::zero(); - storm_rational_function_ptr_struct helperStruct; - helperStruct.storm_rational_function = (void*)(&rationalFunction); - uint64_t value = (uint64_t)&helperStruct; - - return InternalAdd(this, sylvan::Mtbdd::terminal(sylvan_storm_rational_function_get_type(), value)); - } -#endif - - template<> - InternalAdd InternalDdManager::getConstant(double const& value) const { - return InternalAdd(this, sylvan::Mtbdd::doubleTerminal(value)); - } - - template<> - InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const { - return InternalAdd(this, sylvan::Mtbdd::int64Terminal(value)); - } - -#ifdef STORM_HAVE_CARL - template<> - InternalAdd InternalDdManager::getConstant(storm::RationalFunction const& value) const { - return InternalAdd(this, sylvan::Mtbdd::stormRationalFunctionTerminal(value)); - } -#endif - - std::pair, InternalBdd> InternalDdManager::createNewDdVariablePair() { - InternalBdd first = InternalBdd(this, sylvan::Bdd::bddVar(nextFreeVariableIndex)); - InternalBdd second = InternalBdd(this, sylvan::Bdd::bddVar(nextFreeVariableIndex + 1)); - nextFreeVariableIndex += 2; - return std::make_pair(first, second); - } - - void InternalDdManager::allowDynamicReordering(bool value) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan."); - } - - bool InternalDdManager::isDynamicReorderingAllowed() const { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan."); - } - - void InternalDdManager::triggerReordering() { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan."); - } - - template InternalAdd InternalDdManager::getAddOne() const; - template InternalAdd InternalDdManager::getAddOne() const; -#ifdef STORM_HAVE_CARL - template InternalAdd InternalDdManager::getAddOne() const; -#endif - - template InternalAdd InternalDdManager::getAddZero() const; - template InternalAdd InternalDdManager::getAddZero() const; -#ifdef STORM_HAVE_CARL - template InternalAdd InternalDdManager::getAddZero() const; -#endif - - template InternalAdd InternalDdManager::getConstant(double const& value) const; - template InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const; -#ifdef STORM_HAVE_CARL - template InternalAdd InternalDdManager::getConstant(storm::RationalFunction const& value) const; -#endif - } -} \ No newline at end of file +#include "src/storage/dd/sylvan/InternalSylvanDdManager.h" + +#include +#include + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/SylvanSettings.h" + +#include "src/utility/constants.h" +#include "src/utility/macros.h" +#include "src/exceptions/NotSupportedException.h" + +#include "src/utility/sylvan.h" + +#include "storm-config.h" +// TODO: Remove this later on. +#ifndef STORM_HAVE_CARL +#define STORM_HAVE_CARL 1 +#endif + +namespace storm { + namespace dd { + uint_fast64_t InternalDdManager::numberOfInstances = 0; + + // It is important that the variable pairs start at an even offset, because sylvan assumes this to be true for + // some operations. + uint_fast64_t InternalDdManager::nextFreeVariableIndex = 0; + + uint_fast64_t findLargestPowerOfTwoFitting(uint_fast64_t number) { + for (uint_fast64_t index = 0; index < 64; ++index) { + if ((number & (1ull << (63 - index))) != 0) { + return 63 - index; + } + } + return 0; + } + + InternalDdManager::InternalDdManager() { + if (numberOfInstances == 0) { + // Initialize lace: auto-detect number of workers. + lace_init(storm::settings::getModule().getNumberOfThreads(), 1000000); + lace_startup(0, 0, 0); + + // Each node takes 24 bytes and the maximal memory is specified in megabytes. + uint_fast64_t totalNodesToStore = storm::settings::getModule().getMaximalMemory() * 1024 * 1024 / 24; + + // Compute the power of two that still fits within the total numbers to store. + uint_fast64_t powerOfTwo = findLargestPowerOfTwoFitting(totalNodesToStore); + + sylvan::Sylvan::initPackage(1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 8 : 0ull), 1ull << (powerOfTwo - 1), 1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 12 : 0ull), 1ull << (powerOfTwo - 1)); + sylvan::Sylvan::initBdd(1); + sylvan::Sylvan::initMtbdd(); + } + ++numberOfInstances; + } + + InternalDdManager::~InternalDdManager() { + --numberOfInstances; + if (numberOfInstances == 0) { + // Enable this to print the sylvan statistics to a file. +// FILE* filePointer = fopen("sylvan.stats", "w"); +// sylvan_stats_report(filePointer, 0); +// fclose(filePointer); + + sylvan::Sylvan::quitPackage(); + lace_exit(); + } + } + + InternalBdd InternalDdManager::getBddOne() const { + return InternalBdd(this, sylvan::Bdd::bddOne()); + } + + template<> + InternalAdd InternalDdManager::getAddOne() const { + return InternalAdd(this, sylvan::Mtbdd::doubleTerminal(storm::utility::one())); + } + + template<> + InternalAdd InternalDdManager::getAddOne() const { + return InternalAdd(this, sylvan::Mtbdd::int64Terminal(storm::utility::one())); + } + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalDdManager::getAddOne() const { + return InternalAdd(this, sylvan::Mtbdd::stormRationalFunctionTerminal(storm::utility::one())); + } +#endif + + InternalBdd InternalDdManager::getBddZero() const { + return InternalBdd(this, sylvan::Bdd::bddZero()); + } + + template<> + InternalAdd InternalDdManager::getAddZero() const { + return InternalAdd(this, sylvan::Mtbdd::doubleTerminal(storm::utility::zero())); + } + + template<> + InternalAdd InternalDdManager::getAddZero() const { + return InternalAdd(this, sylvan::Mtbdd::int64Terminal(storm::utility::zero())); + } + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalDdManager::getAddZero() const { + return InternalAdd(this, sylvan::Mtbdd::stormRationalFunctionTerminal(storm::utility::zero())); + } +#endif + + template<> + InternalAdd InternalDdManager::getConstant(double const& value) const { + return InternalAdd(this, sylvan::Mtbdd::doubleTerminal(value)); + } + + template<> + InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const { + return InternalAdd(this, sylvan::Mtbdd::int64Terminal(value)); + } + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalDdManager::getConstant(storm::RationalFunction const& value) const { + return InternalAdd(this, sylvan::Mtbdd::stormRationalFunctionTerminal(value)); + } +#endif + + std::pair, InternalBdd> InternalDdManager::createNewDdVariablePair() { + InternalBdd first = InternalBdd(this, sylvan::Bdd::bddVar(nextFreeVariableIndex)); + InternalBdd second = InternalBdd(this, sylvan::Bdd::bddVar(nextFreeVariableIndex + 1)); + nextFreeVariableIndex += 2; + return std::make_pair(first, second); + } + + void InternalDdManager::allowDynamicReordering(bool value) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan."); + } + + bool InternalDdManager::isDynamicReorderingAllowed() const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan."); + } + + void InternalDdManager::triggerReordering() { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation is not supported by sylvan."); + } + + template InternalAdd InternalDdManager::getAddOne() const; + template InternalAdd InternalDdManager::getAddOne() const; +#ifdef STORM_HAVE_CARL + template InternalAdd InternalDdManager::getAddOne() const; +#endif + + template InternalAdd InternalDdManager::getAddZero() const; + template InternalAdd InternalDdManager::getAddZero() const; +#ifdef STORM_HAVE_CARL + template InternalAdd InternalDdManager::getAddZero() const; +#endif + + template InternalAdd InternalDdManager::getConstant(double const& value) const; + template InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const; +#ifdef STORM_HAVE_CARL + template InternalAdd InternalDdManager::getConstant(storm::RationalFunction const& value) const; +#endif + } +} diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index ad5566050..8a5ca130e 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -142,26 +142,25 @@ TEST(SylvanDd, RationalFunctionIdentityTest) { EXPECT_EQ(10ul, identity.getLeafCount()); EXPECT_EQ(21ul, identity.getNodeCount()); } - #endif TEST(SylvanDd, RangeTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x; ASSERT_NO_THROW(x = manager->addMetaVariable("x", 1, 9)); - + storm::dd::Bdd range; ASSERT_NO_THROW(range = manager->getRange(x.first)); - + EXPECT_EQ(9ul, range.getNonZeroCount()); EXPECT_EQ(1ul, range.getLeafCount()); EXPECT_EQ(5ul, range.getNodeCount()); } -TEST(SylvanDd, IdentityTest) { +TEST(SylvanDd, DoubleIdentityTest) { 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)); @@ -170,6 +169,18 @@ TEST(SylvanDd, IdentityTest) { EXPECT_EQ(21ul, identity.getNodeCount()); } +TEST(SylvanDd, UintIdentityTest) { + 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);