diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp index b5132f984..bf9e0fe69 100644 --- a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp @@ -8,8 +8,11 @@ #include #include "storm/adapters/CarlAdapter.h" +#include "storm/utility/constants.h" #include "sylvan_storm_rational_function.h" +#include "storm/exceptions/InvalidOperationException.h" + #include #include #include @@ -128,22 +131,140 @@ storm_rational_function_ptr storm_rational_function_divide(storm_rational_functi std::cerr << "Could not allocate memory in storm_rational_function_divide()!" << std::endl; return result; } - + *result_srf /= srf_b; result = (storm_rational_function_ptr)result_srf; } return result; } +storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ptr a, storm_rational_function_ptr b) { + std::lock_guard lock(carlMutex); + storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; + + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + + uint64_t exponentAsInteger = carl::toInt(srf_b.nominatorAsNumber()); + storm::RationalFunction* result_srf = new storm::RationalFunction(carl::pow(srf_a, exponentAsInteger)); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl; + return result; + } + result = (storm_rational_function_ptr)result_srf; + } + return result; +} + +storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ptr a, storm_rational_function_ptr b) { + std::lock_guard lock(carlMutex); + storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; + + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { + throw storm::exceptions::InvalidOperationException() << "Operands of mod must not be rational function."; + } + throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rationals."; + + // storm::RationalFunction* result_srf = new storm::RationalFunction(carl::mod(srf_a.nominatorAsNumber(), srf_b.nominatorAsNumber())); +// if (result_srf == nullptr) { +// std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl; +// return result; +// } +// result = (storm_rational_function_ptr)result_srf; + + } + return result; +} + +storm_rational_function_ptr storm_rational_function_min(storm_rational_function_ptr a, storm_rational_function_ptr b) { + std::lock_guard lock(carlMutex); + storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; + + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { + throw storm::exceptions::InvalidOperationException() << "Operands of min must not be rational function."; + } + + storm::RationalFunction* result_srf = new storm::RationalFunction(std::min(srf_a.nominatorAsNumber(), srf_b.nominatorAsNumber())); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl; + return result; + } + result = (storm_rational_function_ptr)result_srf; + + } + return result; +} + +storm_rational_function_ptr storm_rational_function_max(storm_rational_function_ptr a, storm_rational_function_ptr b) { + std::lock_guard lock(carlMutex); + storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; + + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { + throw storm::exceptions::InvalidOperationException() << "Operands of max must not be rational function."; + } + + storm::RationalFunction* result_srf = new storm::RationalFunction(std::max(srf_a.nominatorAsNumber(), srf_b.nominatorAsNumber())); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_pow()!" << std::endl; + return result; + } + result = (storm_rational_function_ptr)result_srf; + } + return result; +} + +int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_function_ptr b) { + std::lock_guard lock(carlMutex); + + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { + throw storm::exceptions::InvalidOperationException() << "Operands of less must not be rational functions."; + } + + if (srf_a.nominatorAsNumber() < srf_b.nominatorAsNumber()) { + return 1; + } else { + return 0; + } + return -1; +} + +int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_rational_function_ptr b) { + std::lock_guard lock(carlMutex); + + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + if (!storm::utility::isInteger(srf_a) || !storm::utility::isInteger(srf_b)) { + throw storm::exceptions::InvalidOperationException() << "Operands of less-or-equal must not be rational functions."; + } + if (srf_a.nominatorAsNumber() <= srf_b.nominatorAsNumber()) { + return 1; + } else { + return 0; + } + + return -1; +} + uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) { std::lock_guard lock(carlMutex); - uint64_t result = 0; + uint64_t result = seed; { storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; - size_t hash = carl::hash_value(srf_a); - - result = hash ^ seed; + // carl::hash_add(result, srf_a); + result = seed ^ (carl::hash_value(srf_a) + 0x9e3779b9 + (seed<<6) + (seed>>2)); } return result; } @@ -167,6 +288,51 @@ storm_rational_function_ptr storm_rational_function_negate(storm_rational_functi return result; } +storm_rational_function_ptr storm_rational_function_floor(storm_rational_function_ptr a) { + std::lock_guard lock(carlMutex); + storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; + + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + if (!storm::utility::isInteger(srf_a)) { + throw storm::exceptions::InvalidOperationException() << "Operand of floor must not be rational function."; + } + 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 result; + } + + *result_srf = storm::RationalFunction(carl::floor(srf_a.nominatorAsNumber())); + result = (storm_rational_function_ptr)result_srf; + + } + return result; +} + +storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function_ptr a) { + std::lock_guard lock(carlMutex); + storm_rational_function_ptr result = (storm_rational_function_ptr)nullptr; + + { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + if (!storm::utility::isInteger(srf_a)) { + throw storm::exceptions::InvalidOperationException() << "Operand of ceil must not be rational function."; + } + 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 result; + } + + *result_srf = storm::RationalFunction(carl::ceil(srf_a.nominatorAsNumber())); + result = (storm_rational_function_ptr)result_srf; + } + return result; +} + int storm_rational_function_is_zero(storm_rational_function_ptr a) { std::lock_guard lock(carlMutex); diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.h b/resources/3rdparty/sylvan/src/storm_function_wrapper.h index 104842972..2326ceeae 100644 --- a/resources/3rdparty/sylvan/src/storm_function_wrapper.h +++ b/resources/3rdparty/sylvan/src/storm_function_wrapper.h @@ -11,15 +11,31 @@ extern "C" { typedef void* storm_rational_function_ptr; -// equals, plus, minus, divide, times, create, destroy +// basic functions (for sylvan) void storm_rational_function_init(storm_rational_function_ptr* a); void storm_rational_function_destroy(storm_rational_function_ptr a); int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b); + +// binary storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b); storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b); storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b); storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b); +storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ptr a, storm_rational_function_ptr b); + +storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ptr a, storm_rational_function_ptr b); +storm_rational_function_ptr storm_rational_function_min(storm_rational_function_ptr a, storm_rational_function_ptr b); +storm_rational_function_ptr storm_rational_function_max(storm_rational_function_ptr a, storm_rational_function_ptr b); + +int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_function_ptr b); +int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_rational_function_ptr b); + +// unary storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a); + +storm_rational_function_ptr storm_rational_function_floor(storm_rational_function_ptr a); +storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function_ptr a); + uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed); int storm_rational_function_is_zero(storm_rational_function_ptr a); @@ -29,8 +45,6 @@ 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); - MTBDD storm_rational_function_leaf_parameter_replacement(MTBDD dd, storm_rational_function_ptr a, void* context); double storm_rational_function_get_constant(storm_rational_function_ptr a); diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index a603e44ef..603755c72 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -308,7 +308,7 @@ _mtbdd_hash_cb(uint64_t a, uint64_t b, uint64_t seed) if (type >= cl_registry_count) return llmsset_hash(a, b, seed); customleaf_t *c = cl_registry + type; if (c->hash_cb == NULL) return llmsset_hash(a, b, seed); - return c->hash_cb(b, seed ^ a); + return c->hash_cb(b, seed); } static int diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp index cb272dbbb..98caf6c57 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp @@ -9,6 +9,14 @@ Mtbdd Divide(const Mtbdd &other) const; #if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + + Bdd EqualsRF(const Mtbdd& other) const; + Bdd LessRF(const Mtbdd& other) const; + Bdd LessOrEqualRF(const Mtbdd& other) const; + + Mtbdd MinRF(const Mtbdd& other) const; + Mtbdd MaxRF(const Mtbdd& other) const; + /** * @brief Computes f + g for Rational Functions */ @@ -18,7 +26,9 @@ * @brief Computes f * g for Rational Functions */ Mtbdd TimesRF(const Mtbdd &other) const; - + + Mtbdd AndExistsRF(const Mtbdd &other, const BddSet &variables) const; + /** * @brief Computes f - g for Rational Functions */ @@ -28,11 +38,25 @@ * @brief Computes f / g for Rational Functions */ Mtbdd DivideRF(const Mtbdd &other) const; - + + Mtbdd PowRF(const Mtbdd& other) const; + Mtbdd AbstractPlusRF(const BddSet &variables) const; Mtbdd ReplaceLeavesRF(void* context) const; - + + Mtbdd FloorRF() const; + Mtbdd CeilRF() const; + + Mtbdd AbstractMinRF(const BddSet &variables) const; + Mtbdd AbstractMaxRF(const BddSet &variables) const; + + Bdd BddThresholdRF(storm::RationalFunction const& rf) const; + Bdd BddStrictThresholdRF(storm::RationalFunction const& rf) const; + + Mtbdd MinimumRF() const; + Mtbdd MaximumRF() const; + Mtbdd ToDoubleRF() const; #endif diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index bead06e8a..a853494bf 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -23,7 +23,37 @@ Bdd::toStormRationalFunctionMtbdd() const { return mtbdd_bool_to_storm_rational_function(bdd); } -Mtbdd +Bdd +Mtbdd::EqualsRF(const Mtbdd& other) const { + LACE_ME; + return mtbdd_equals_rational_function(mtbdd, other.mtbdd); +} + +Bdd +Mtbdd::LessRF(const Mtbdd& other) const { + LACE_ME; + return sylvan_storm_rational_function_less(mtbdd, other.mtbdd); +} + +Bdd +Mtbdd::LessOrEqualRF(const Mtbdd& other) const { + LACE_ME; + return sylvan_storm_rational_function_less_or_equal(mtbdd, other.mtbdd); +} + +Mtbdd +Mtbdd::MinRF(const Mtbdd& other) const { + LACE_ME; + return sylvan_storm_rational_function_min(mtbdd, other.mtbdd); +} + +Mtbdd +Mtbdd::MaxRF(const Mtbdd& other) const { + LACE_ME; + return sylvan_storm_rational_function_max(mtbdd, other.mtbdd); +} + +Mtbdd Mtbdd::ToDoubleRF() const { LACE_ME; return sylvan_storm_rational_function_to_double(mtbdd); @@ -44,6 +74,12 @@ Mtbdd::TimesRF(const Mtbdd &other) const return sylvan_storm_rational_function_times(mtbdd, other.mtbdd); } +Mtbdd +Mtbdd::AndExistsRF(const Mtbdd &other, const BddSet &variables) const { + LACE_ME; + return sylvan_storm_rational_function_and_exists(mtbdd, other.mtbdd, variables.set.bdd); +} + Mtbdd Mtbdd::MinusRF(const Mtbdd &other) const { @@ -58,6 +94,13 @@ Mtbdd::DivideRF(const Mtbdd &other) const return sylvan_storm_rational_function_divide(mtbdd, other.mtbdd); } +Mtbdd +Mtbdd::PowRF(const Mtbdd& other) const { + LACE_ME; + return sylvan_storm_rational_function_pow(mtbdd, other.mtbdd); +} + + Mtbdd Mtbdd::AbstractPlusRF(const BddSet &variables) const { LACE_ME; return sylvan_storm_rational_function_abstract_plus(mtbdd, variables.set.bdd); @@ -68,6 +111,53 @@ Mtbdd Mtbdd::ReplaceLeavesRF(void* context) const { return sylvan_storm_rational_function_replace_leaves(mtbdd, (size_t)context); } + +Mtbdd +Mtbdd::FloorRF() const { + LACE_ME; + return sylvan_storm_rational_function_floor(mtbdd); +} + +Mtbdd +Mtbdd::CeilRF() const { + LACE_ME; + return sylvan_storm_rational_function_ceil(mtbdd); +} + +Mtbdd Mtbdd::AbstractMinRF(const BddSet &variables) const { + LACE_ME; + return sylvan_storm_rational_function_abstract_min(mtbdd, variables.set.bdd); +} + +Mtbdd Mtbdd::AbstractMaxRF(const BddSet &variables) const { + LACE_ME; + return sylvan_storm_rational_function_abstract_max(mtbdd, variables.set.bdd); +} + +Bdd +Mtbdd::BddStrictThresholdRF(storm::RationalFunction const& rf) const { + LACE_ME; + return sylvan_storm_rational_function_strict_threshold(mtbdd, (void*)&rf); +} + +Bdd +Mtbdd::BddThresholdRF(storm::RationalFunction const& rf) const { + LACE_ME; + return sylvan_storm_rational_function_threshold(mtbdd, (void*)&rf); +} + +Mtbdd +Mtbdd::MinimumRF() const { + LACE_ME; + return sylvan_storm_rational_function_minimum(mtbdd); +} + +Mtbdd +Mtbdd::MaximumRF() const { + LACE_ME; + return sylvan_storm_rational_function_maximum(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 1453449d9..df66f3155 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c @@ -38,6 +38,11 @@ int depth = 0; //} #endif +storm_rational_function_ptr mtbdd_getstorm_rational_function_ptr(MTBDD terminal) { + uint64_t value = mtbdd_getvalue(terminal); + return (storm_rational_function_ptr*)value; +} + static uint64_t sylvan_storm_rational_function_hash(const uint64_t v, const uint64_t seed) { @@ -111,7 +116,10 @@ sylvan_storm_rational_function_destroy(uint64_t val) } static uint32_t sylvan_storm_rational_function_type; -static uint64_t CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS; + +static uint64_t CACHE_MTBDD_AND_EXISTS_RF; +static uint64_t CACHE_MTBDD_MINIMUM_RF; +static uint64_t CACHE_MTBDD_MAXIMUM_RF; /** * Initialize storm::RationalFunction custom leaves @@ -123,11 +131,13 @@ sylvan_storm_rational_function_init() 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); + 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(); + CACHE_MTBDD_AND_EXISTS_RF = cache_next_opid(); + CACHE_MTBDD_MINIMUM_RF = cache_next_opid(); + CACHE_MTBDD_MAXIMUM_RF = cache_next_opid(); } uint32_t sylvan_storm_rational_function_get_type() { @@ -184,6 +194,35 @@ TASK_IMPL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD, dd) return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_storm_rational_function), 0); } +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_equals, MTBDD*, pa, MTBDD*, pb) +{ + LOG_I("task_impl_2 op_equals") + MTBDD a = *pa, b = *pb; + + /* Check for partial functions */ + if (a == mtbdd_false) return b; + if (b == mtbdd_false) return a; + + /* If both leaves, compute plus */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); + storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + if (storm_rational_function_equals(ma, mb)) { + return mtbdd_true; + } else { + return mtbdd_false; + } + } + + /* Commutative, so swap a,b for better cache performance */ + if (a < b) { + *pa = b; + *pb = a; + } + + return mtbdd_invalid; +} + /** * Operation "plus" for two storm::RationalFunction MTBDDs * Interpret partial function as "0" @@ -302,11 +341,14 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*, /* Handle division of leaves */ if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { 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_divide(ma, mb); + storm_rational_function_ptr mres; + if (storm_rational_function_is_zero(ma)) { + mres = storm_rational_function_get_zero(); + } else { + storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + mres = storm_rational_function_divide(ma, mb); + } MTBDD res = mtbdd_storm_rational_function(mres); - storm_rational_function_destroy(mres); return res; @@ -315,6 +357,216 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*, return mtbdd_invalid; } +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_less, MTBDD*, pa, MTBDD*, pb) +{ + LOG_I("task_impl_2 op_less") + MTBDD a = *pa, b = *pb; + + /* Check for partial functions and for Boolean (filter) */ + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + + /* If one of Boolean, interpret as filter */ + if (a == mtbdd_true) return b; + if (b == mtbdd_true) return a; + + /* Handle multiplication of leaves */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); + storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + + if (storm_rational_function_less(ma, mb)) { + return mtbdd_true; + } else { + return mtbdd_false; + } + } + + return mtbdd_invalid; +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_less_or_equal, MTBDD*, pa, MTBDD*, pb) +{ + LOG_I("task_impl_2 op_less_or_equal") + MTBDD a = *pa, b = *pb; + + /* Check for partial functions and for Boolean (filter) */ + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + + /* If one of Boolean, interpret as filter */ + if (a == mtbdd_true) return b; + if (b == mtbdd_true) return a; + + /* Handle multiplication of leaves */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); + storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + + if (storm_rational_function_less_or_equal(ma, mb)) { + return mtbdd_true; + } else { + return mtbdd_false; + } + } + + return mtbdd_invalid; +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_mod, MTBDD*, pa, MTBDD*, pb) +{ + LOG_I("task_impl_2 op_mod") + MTBDD a = *pa, b = *pb; + + /* Check for partial functions and for Boolean (filter) */ + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + + /* If one of Boolean, interpret as filter */ + if (a == mtbdd_true) return b; + if (b == mtbdd_true) return a; + + /* Handle multiplication of leaves */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + 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_mod(ma, mb); + MTBDD res = mtbdd_storm_rational_function(mres); + + storm_rational_function_destroy(mres); + + return res; + } + + return mtbdd_invalid; +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_min, MTBDD*, pa, MTBDD*, pb) +{ + LOG_I("task_impl_2 op_mod") + MTBDD a = *pa, b = *pb; + + /* Check for partial functions and for Boolean (filter) */ + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + + /* If one of Boolean, interpret as filter */ + if (a == mtbdd_true) return b; + if (b == mtbdd_true) return a; + + /* Handle multiplication of leaves */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + 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_min(ma, mb); + MTBDD res = mtbdd_storm_rational_function(mres); + + storm_rational_function_destroy(mres); + + return res; + } + + /* Commutative, so make "a" the lowest for better cache performance */ + if (a < b) { + *pa = b; + *pb = a; + } + + return mtbdd_invalid; +} + +TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_min, MTBDD, a, MTBDD, b, int, k) +{ + LOG_I("task_impl_3 abstract_op_min") + if (k==0) { + return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_min)); + } else { + MTBDD res = a; + for (int i=0; i= value to 1 and to 0 otherwise; + */ +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, a, size_t, svalue) +{ + LOG_I("task_impl_2 op_threshold") + storm_rational_function_ptr value = (storm_rational_function_ptr)svalue; + + if (mtbdd_isleaf(a)) { + storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); + + if (storm_rational_function_less_or_equal(ma, value)) { + return mtbdd_false; + } else { + return mtbdd_true; + } + } + + return mtbdd_invalid; +} + +/** + * Monad that converts double/fraction to a Boolean BDD, translate terminals > value to 1 and to 0 otherwise; + */ +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, a, size_t, svalue) +{ + LOG_I("task_impl_2 op_strict_threshold") + storm_rational_function_ptr value = (storm_rational_function_ptr)svalue; + + if (mtbdd_isleaf(a)) { + storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); + + if (storm_rational_function_less(ma, value)) { + return mtbdd_false; + } else { + return mtbdd_true; + } + } + + return mtbdd_invalid; +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_threshold, MTBDD, dd, storm_rational_function_ptr, value) +{ + return mtbdd_uapply(dd, TASK(sylvan_storm_rational_function_op_threshold), *(size_t*)value); +} + +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_strict_threshold, MTBDD, dd, storm_rational_function_ptr, value) +{ + return mtbdd_uapply(dd, TASK(sylvan_storm_rational_function_op_strict_threshold), *(size_t*)value); +} + +TASK_IMPL_1(MTBDD, sylvan_storm_rational_function_minimum, MTBDD, a) +{ + /* Check terminal case */ + if (a == mtbdd_false) return mtbdd_false; + mtbddnode_t na = MTBDD_GETNODE(a); + if (mtbddnode_isleaf(na)) return a; + + /* Maybe perform garbage collection */ + sylvan_gc_test(); + + /* Check cache */ + MTBDD result; + if (cache_get3(CACHE_MTBDD_MINIMUM_RF, a, 0, 0, &result)) return result; + + /* Call recursive */ + SPAWN(mtbdd_minimum, node_getlow(a, na)); + MTBDD high = CALL(sylvan_storm_rational_function_minimum, node_gethigh(a, na)); + MTBDD low = SYNC(sylvan_storm_rational_function_minimum); + + storm_rational_function_ptr fl = mtbdd_getstorm_rational_function_ptr(low); + storm_rational_function_ptr fh = mtbdd_getstorm_rational_function_ptr(high); + + if (storm_rational_function_less_or_equal(fl, fh)) { + return low; + } else { + return high; + } + + /* Store in cache */ + cache_put3(CACHE_MTBDD_MINIMUM_RF, a, 0, 0, result); + return result; +} + +TASK_IMPL_1(MTBDD, sylvan_storm_rational_function_maximum, MTBDD, a) +{ + /* Check terminal case */ + if (a == mtbdd_false) return mtbdd_false; + mtbddnode_t na = MTBDD_GETNODE(a); + if (mtbddnode_isleaf(na)) return a; + + /* Maybe perform garbage collection */ + sylvan_gc_test(); + + /* Check cache */ + MTBDD result; + if (cache_get3(CACHE_MTBDD_MAXIMUM_RF, a, 0, 0, &result)) return result; + + /* Call recursive */ + SPAWN(mtbdd_minimum, node_getlow(a, na)); + MTBDD high = CALL(sylvan_storm_rational_function_maximum, node_gethigh(a, na)); + MTBDD low = SYNC(sylvan_storm_rational_function_maximum); + + storm_rational_function_ptr fl = mtbdd_getstorm_rational_function_ptr(low); + storm_rational_function_ptr fh = mtbdd_getstorm_rational_function_ptr(high); + + if (storm_rational_function_less(fl, fh)) { + return high; + } else { + return low; + } + + /* Store in cache */ + cache_put3(CACHE_MTBDD_MAXIMUM_RF, a, 0, 0, result); + return result; +} diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h index 0b06cdf0f..8543ade19 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h @@ -33,6 +33,8 @@ uint32_t sylvan_storm_rational_function_get_type(); */ MTBDD mtbdd_storm_rational_function(storm_rational_function_ptr val); +storm_rational_function_ptr mtbdd_getstorm_rational_function_ptr(MTBDD terminal); + /** * Monad that converts Boolean to a storm::RationalFunction MTBDD, translate terminals true to 1 and to 0 otherwise; */ @@ -40,6 +42,10 @@ TASK_DECL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, size_t) TASK_DECL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD) #define mtbdd_bool_to_storm_rational_function(dd) CALL(mtbdd_bool_to_storm_rational_function, dd) +// Operation "equals" +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_equals, MTBDD*, MTBDD*) +#define mtbdd_equals_rational_function(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_equals)) + /** * Operation "plus" for two storm::RationalFunction MTBDDs */ @@ -62,11 +68,23 @@ TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, MTBD */ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, MTBDD*) +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_less, MTBDD*, MTBDD*) +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_less_or_equal, MTBDD*, MTBDD*) + +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_mod, MTBDD*, MTBDD*) +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_min, MTBDD*, MTBDD*) +TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_min, MTBDD, MTBDD, int) +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_max, MTBDD*, MTBDD*) +TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_max, MTBDD, MTBDD, int) + /** * Operation "negate" for one storm::RationalFunction MTBDD */ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, size_t) +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_floor, MTBDD, size_t) +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_ceil, MTBDD, size_t) + /** * Compute a + b */ @@ -87,11 +105,53 @@ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, size_t) */ #define sylvan_storm_rational_function_divide(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_divide)) +/** + * Compute a < b + */ +#define sylvan_storm_rational_function_less(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_less)) + +/** + * Compute a <= b + */ +#define sylvan_storm_rational_function_less_or_equal(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_less_or_equal)) + +/** + * Compute a mod b + */ +#define sylvan_storm_rational_function_mod(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_less_or_equal)) + +/** + * Compute min(a, b) + */ +#define sylvan_storm_rational_function_min(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_min)) + +/** + * Compute max(a, b) + */ +#define sylvan_storm_rational_function_max(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_max)) + /** * Compute -a */ #define sylvan_storm_rational_function_neg(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_neg), 0) +/** + * Compute floor(a) + */ +#define sylvan_storm_rational_function_floor(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_floor), 0) + +/** + * Compute ceil(a) + */ +#define sylvan_storm_rational_function_ceil(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_ceil), 0) + +/** + * Compute a^b + */ +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_pow, MTBDD*, MTBDD*) +#define sylvan_storm_rational_function_pow(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_pow)) + + /** * Multiply and , and abstract variables using summation. * This is similar to the "and_exists" operation in BDDs. @@ -103,7 +163,9 @@ TASK_DECL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, MTBDD, MTBD * Abstract the variables in from by taking the sum of all values */ #define sylvan_storm_rational_function_abstract_plus(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_function_abstract_op_plus)) - +#define sylvan_storm_rational_function_abstract_min(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_function_abstract_op_min)) +#define sylvan_storm_rational_function_abstract_max(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_function_abstract_op_max)) + /** * Apply a unary operation to
. * Callback is consulted after the cache, thus the application to a terminal is cached. @@ -135,6 +197,24 @@ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_to_double, MTBDD, size_t) */ #define sylvan_storm_rational_function_to_double(a) mtbdd_uapply_nocache(a, TASK(sylvan_storm_rational_function_op_to_double), 0) + +TASK_DECL_1(MTBDD, sylvan_storm_rational_function_minimum, MTBDD); +#define sylvan_storm_rational_function_minimum(dd) CALL(sylvan_storm_rational_function_minimum, dd) + +TASK_DECL_1(MTBDD, sylvan_storm_rational_function_maximum, MTBDD); +#define sylvan_storm_rational_function_maximum(dd) CALL(sylvan_storm_rational_function_maximum, dd) + + +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, size_t) +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, size_t) + +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_threshold, MTBDD, storm_rational_function_ptr); +#define sylvan_storm_rational_function_threshold(dd, value) CALL(sylvan_storm_rational_function_strict_threshold, dd, value) + + +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_strict_threshold, MTBDD, storm_rational_function_ptr); +#define sylvan_storm_rational_function_strict_threshold(dd, value) CALL(sylvan_storm_rational_function_strict_threshold, dd, value) + #ifdef __cplusplus } #endif /* __cplusplus */ diff --git a/src/storm/adapters/AddExpressionAdapter.cpp b/src/storm/adapters/AddExpressionAdapter.cpp index d975c8e9e..db60c7050 100644 --- a/src/storm/adapters/AddExpressionAdapter.cpp +++ b/src/storm/adapters/AddExpressionAdapter.cpp @@ -34,6 +34,11 @@ namespace storm { return boost::any_cast>(expression.accept(*this, boost::none)); } + template + void AddExpressionAdapter::setValue(storm::expressions::Variable const& variable, ValueType const& value) { + valueMapping[variable] = value; + } + template boost::any AddExpressionAdapter::visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) { if (expression.hasBooleanType()) { @@ -143,12 +148,17 @@ namespace storm { template boost::any AddExpressionAdapter::visit(storm::expressions::VariableExpression const& expression, boost::any const&) { - auto const& variablePair = variableMapping->find(expression.getVariable()); - STORM_LOG_THROW(variablePair != variableMapping->end(), storm::exceptions::InvalidArgumentException, "Cannot translate the given expression, because it contains the variable '" << expression.getVariableName() << "' for which no DD counterpart is known."); - if (expression.hasBooleanType()) { - return ddManager->template getIdentity(variablePair->second).toBdd(); + auto valueIt = valueMapping.find(expression.getVariable()); + if (valueIt != valueMapping.end()) { + return ddManager->getConstant(valueIt->second); } else { - return ddManager->template getIdentity(variablePair->second); + auto const& variablePair = variableMapping->find(expression.getVariable()); + STORM_LOG_THROW(variablePair != variableMapping->end(), storm::exceptions::InvalidArgumentException, "Cannot translate the given expression, because it contains the variable '" << expression.getVariableName() << "' for which no DD counterpart is known."); + if (expression.hasBooleanType()) { + return ddManager->template getIdentity(variablePair->second).toBdd(); + } else { + return ddManager->template getIdentity(variablePair->second); + } } } diff --git a/src/storm/adapters/AddExpressionAdapter.h b/src/storm/adapters/AddExpressionAdapter.h index 0d1fae7d5..6dfe5e5b4 100644 --- a/src/storm/adapters/AddExpressionAdapter.h +++ b/src/storm/adapters/AddExpressionAdapter.h @@ -21,7 +21,9 @@ namespace storm { storm::dd::Add translateExpression(storm::expressions::Expression const& expression); storm::dd::Bdd translateBooleanExpression(storm::expressions::Expression const& expression); - + + void setValue(storm::expressions::Variable const& variable, ValueType const& value); + virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) override; virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; virtual boost::any visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) override; @@ -32,13 +34,16 @@ namespace storm { virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) override; virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) override; virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) override; - + private: // The manager responsible for the DDs built by this adapter. std::shared_ptr> ddManager; // This member maps the variables used in the expressions to the variables used by the DD manager. std::shared_ptr> variableMapping; + + // A mapping of variables to their values (if set). + std::unordered_map valueMapping; }; } // namespace adapters diff --git a/src/storm/adapters/EigenAdapter.h b/src/storm/adapters/EigenAdapter.h index aa08c857a..5fd1e832a 100644 --- a/src/storm/adapters/EigenAdapter.h +++ b/src/storm/adapters/EigenAdapter.h @@ -36,8 +36,8 @@ namespace std { struct hash> { std::size_t operator()(StormEigen::Matrix const &vector) const { size_t seed = 0; - for (uint_fast64_t i = 0; i < vector.rows(); ++i) { - carl::hash_add(seed, std::hash()(vector(i))); + for (uint_fast64_t i = 0; i < static_cast(vector.rows()); ++i) { + carl::hash_add(seed, std::hash()(vector(i))); } return seed; } diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index c3d91b533..ff59ec735 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -1845,7 +1845,7 @@ namespace storm { template std::shared_ptr> DdJaniModelBuilder::build(storm::jani::Model const& model, Options const& options) { - if (model.hasUndefinedConstants()) { + if (!std::is_same::value && model.hasUndefinedConstants()) { std::vector> undefinedConstants = model.getUndefinedConstants(); std::vector strings; for (auto const& constant : undefinedConstants) { diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index a8481e21b..ee6573f27 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -31,12 +31,60 @@ namespace storm { namespace builder { + template + class ParameterCreator { + public: + void create(storm::prism::Program const& program, storm::adapters::AddExpressionAdapter& rowExpressionAdapter, storm::adapters::AddExpressionAdapter& columnExpressionAdapter) { + // Intentionally left empty: no support for parameters for this data type. + } + }; + + template + class ParameterCreator { + public: + ParameterCreator() : cache(std::make_shared>>()) { + // Intentionally left empty. + } + + void create(storm::prism::Program const& program, storm::adapters::AddExpressionAdapter& rowExpressionAdapter, storm::adapters::AddExpressionAdapter& columnExpressionAdapter) { + for (auto const& constant : program.getConstants()) { + if (!constant.isDefined()) { + carl::Variable carlVariable = carl::freshRealVariable(constant.getExpressionVariable().getName()); + auto rf = convertVariableToPolynomial(carlVariable); + rowExpressionAdapter.setValue(constant.getExpressionVariable(), rf); + columnExpressionAdapter.setValue(constant.getExpressionVariable(), rf); + } + } + } + + template> = carl::dummy> + RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) { + return RationalFunctionType(typename RationalFunctionType::PolyType(typename RationalFunctionType::PolyType::PolyType(variable), cache)); + } + + template> = carl::dummy> + RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable) { + return RationalFunctionType(variable); + } + + // A mapping from our variables to carl's. + std::unordered_map variableToVariableMap; + + // The cache that is used in case the underlying type needs a cache. + std::shared_ptr>> cache; + }; + template class DdPrismModelBuilder::GenerationInformation { public: GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(std::make_shared>()), rowExpressionAdapter(std::make_shared>(manager, variableToRowMetaVariableMap)), columnMetaVariables(), variableToColumnMetaVariableMap((std::make_shared>())), columnExpressionAdapter(std::make_shared>(manager, variableToColumnMetaVariableMap)), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() { + // Initializes variables and identity DDs. createMetaVariablesAndIdentities(); + + // Initialize the parameters (if any). + ParameterCreator parameterCreator; + parameterCreator.create(this->program, *this->rowExpressionAdapter, *this->columnExpressionAdapter); } // The program that is currently translated. @@ -84,6 +132,10 @@ namespace storm { std::map> moduleToRangeMap; private: + void createParameters() { + + } + /*! * Creates the required meta variables and variable/module identities. */ @@ -663,6 +715,8 @@ namespace storm { commandDd += updateResultsIt->updateDd * probabilityDd; } + commandDd.exportToDot("command.dot"); + return ActionDecisionDiagram(guard, guard.template toAdd() * commandDd, globalVariablesInSomeUpdate); } else { return ActionDecisionDiagram(*generationInfo.manager); @@ -1245,7 +1299,7 @@ namespace storm { template std::shared_ptr> DdPrismModelBuilder::build(storm::prism::Program const& program, Options const& options) { - if (program.hasUndefinedConstants()) { + if (!std::is_same::value && program.hasUndefinedConstants()) { std::vector> undefinedConstants = program.getUndefinedConstants(); std::stringstream stream; bool printComma = false; @@ -1342,6 +1396,8 @@ namespace storm { storm::dd::Bdd statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables); storm::dd::Bdd deadlockStates = reachableStates && !statesWithTransition; + transitionMatrix.exportToDot("trans.dot"); + // If there are deadlocks, either fix them or raise an error. if (!deadlockStates.isZero()) { // If we need to fix deadlocks, we do so now. diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 2dd312a51..beb085081 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -381,12 +381,11 @@ namespace storm { auto ddlib = storm::settings::getModule().getDdLibraryType(); STORM_LOG_THROW(ddlib == storm::dd::DdType::Sylvan, storm::exceptions::InvalidSettingsException, "This data-type is only available when selecting sylvan."); buildAndCheckSymbolicModelWithSymbolicEngine(engine == storm::settings::modules::CoreSettings::Engine::Hybrid, model, formulas, onlyInitialStatesRelevant); - } else { - STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Illegal engine."); + } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) { buildAndCheckSymbolicModelWithSparseEngine(model, formulas, onlyInitialStatesRelevant); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot use this data type with this engine."); } - - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot use this data type with this engine."); } #endif diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index e564aa0f6..3f3729975 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -316,9 +316,12 @@ namespace storm { // DD template class AbstractModelChecker>; template class AbstractModelChecker>; + template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; + template class AbstractModelChecker>; template class AbstractModelChecker>; template class AbstractModelChecker>; + template class AbstractModelChecker>; } } diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index 1936e60bd..a9bba9eaf 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -118,5 +118,7 @@ namespace storm { template class HybridDtmcPrctlModelChecker>; template class HybridDtmcPrctlModelChecker>; + + template class HybridDtmcPrctlModelChecker>; } } diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index c52307315..4dbfb6d1d 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -28,7 +28,7 @@ namespace storm { } template - SymbolicDtmcPrctlModelChecker::SymbolicDtmcPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(new storm::utility::solver::SymbolicLinearEquationSolverFactory()) { + SymbolicDtmcPrctlModelChecker::SymbolicDtmcPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { // Intentionally left empty. } @@ -45,8 +45,8 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); - return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); + return std::make_unique>(this->getModel().getReachableStates(), numericResult); } template @@ -54,8 +54,8 @@ namespace storm { storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); - return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); + return std::make_unique>(this->getModel().getReachableStates(), numericResult); } template @@ -63,8 +63,8 @@ namespace storm { storm::logic::NextFormula const& pathFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); - return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector()); + return std::make_unique>(this->getModel().getReachableStates(), numericResult); } template @@ -76,24 +76,24 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); - return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound() + (pathFormula.isUpperBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); + return std::make_unique>(this->getModel().getReachableStates(), numericResult); } template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); - return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound() + (rewardPathFormula.isBoundStrict() ? 1ull : 0ull), *this->linearEquationSolverFactory); + return std::make_unique>(this->getModel().getReachableStates(), numericResult); } template std::unique_ptr SymbolicDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *this->linearEquationSolverFactory); - return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *this->linearEquationSolverFactory); + return std::make_unique>(this->getModel().getReachableStates(), numericResult); } template @@ -101,12 +101,14 @@ namespace storm { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); - return std::unique_ptr>(new SymbolicQuantitativeCheckResult(this->getModel().getReachableStates(), numericResult)); + storm::dd::Add numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); + return std::make_unique>(this->getModel().getReachableStates(), numericResult); } template class SymbolicDtmcPrctlModelChecker>; template class SymbolicDtmcPrctlModelChecker>; + + template class SymbolicDtmcPrctlModelChecker>; } } diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index af3bbc2cf..dd12b76e6 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -39,7 +39,7 @@ namespace storm { // Check whether we need to compute exact probabilities for some states. if (qualitative) { // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1. - return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), statesWithProbability01.second.template toAdd() + maybeStates.template toAdd() * model.getManager().getConstant(0.5))); + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), statesWithProbability01.second.template toAdd() + maybeStates.template toAdd() * model.getManager().template getConstant(storm::utility::convertNumber(0.5)))); } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { @@ -77,9 +77,9 @@ namespace storm { solver->solveEquations(x, b); // Return a hybrid check result that stores the numerical values explicitly. - return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, statesWithProbability01.second.template toAdd(), maybeStates, odd, x)); + return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, statesWithProbability01.second.template toAdd(), maybeStates, odd, x)); } else { - return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), statesWithProbability01.second.template toAdd())); + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), statesWithProbability01.second.template toAdd())); } } } @@ -94,7 +94,7 @@ namespace storm { template std::unique_ptr HybridDtmcPrctlHelper::computeNextProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates) { storm::dd::Add result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd(); - return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result.sumAbstract(model.getColumnVariables()))); + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result.sumAbstract(model.getColumnVariables()))); } template @@ -135,9 +135,9 @@ namespace storm { solver->repeatedMultiply(x, &b, stepBound); // Return a hybrid check result that stores the numerical values explicitly. - return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.template toAdd(), maybeStates, odd, x)); + return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.template toAdd(), maybeStates, odd, x)); } else { - return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.template toAdd())); + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.template toAdd())); } } @@ -160,7 +160,7 @@ namespace storm { solver->repeatedMultiply(x, nullptr, stepBound); // Return a hybrid check result that stores the numerical values explicitly. - return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, x)); + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, x)); } template @@ -186,7 +186,7 @@ namespace storm { solver->repeatedMultiply(x, &b, stepBound); // Return a hybrid check result that stores the numerical values explicitly. - return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, x)); + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, x)); } template @@ -207,7 +207,7 @@ namespace storm { if (qualitative) { // Set the values for all maybe-states to 1 to indicate that their reward values // are neither 0 nor infinity. - return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()) + maybeStates.template toAdd() * model.getManager().template getAddOne())); + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()) + maybeStates.template toAdd() * model.getManager().template getAddOne())); } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { @@ -242,9 +242,9 @@ namespace storm { solver->solveEquations(x, b); // Return a hybrid check result that stores the numerical values explicitly. - return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()), maybeStates, odd, x)); + return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()), maybeStates, odd, x)); } else { - return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()))); + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), model.getManager().template getAddZero()))); } } } @@ -256,7 +256,7 @@ namespace storm { storm::storage::SparseMatrix explicitProbabilityMatrix = model.getTransitionMatrix().toMatrix(odd, odd); std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, targetStates.toVector(odd), linearEquationSolverFactory); - return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); } template @@ -266,11 +266,13 @@ namespace storm { storm::storage::SparseMatrix explicitProbabilityMatrix = model.getTransitionMatrix().toMatrix(odd, odd); std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getTotalRewardVector(model.getTransitionMatrix(), model.getColumnVariables()).toVector(odd), linearEquationSolverFactory); - return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); } template class HybridDtmcPrctlHelper; template class HybridDtmcPrctlHelper; + + template class HybridDtmcPrctlHelper; } } } diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index ac1815d43..7f0618048 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -33,7 +33,7 @@ namespace storm { // Check whether we need to compute exact probabilities for some states. if (qualitative) { // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1. - return statesWithProbability01.second.template toAdd() + maybeStates.template toAdd() * model.getManager().getConstant(0.5); + return statesWithProbability01.second.template toAdd() + maybeStates.template toAdd() * model.getManager().getConstant(ValueType(0.5)); } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { @@ -58,7 +58,7 @@ namespace storm { // Solve the equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->solveEquations(model.getManager().getConstant(0.0), subvector); + storm::dd::Add result = solver->solveEquations(model.getManager().template getAddZero(), subvector); return statesWithProbability01.second.template toAdd() + result; } else { @@ -175,7 +175,7 @@ namespace storm { // Solve the equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->solveEquations(model.getManager().getConstant(0.0), subvector); + storm::dd::Add result = solver->solveEquations(model.getManager().template getAddZero(), subvector); return infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), result); } else { @@ -186,7 +186,8 @@ namespace storm { template class SymbolicDtmcPrctlHelper; template class SymbolicDtmcPrctlHelper; - + + template class SymbolicDtmcPrctlHelper; } } } diff --git a/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp index 1e355f7b2..2b668cde6 100644 --- a/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp +++ b/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp @@ -66,6 +66,9 @@ namespace storm { template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; + template class SymbolicPropositionalModelChecker>; } } diff --git a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp index ef52d6028..d5ada4794 100644 --- a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -35,7 +35,7 @@ namespace storm { } // Then translate the explicit part to a symbolic format and simultaneously to a qualitative result. - symbolicResult |= storm::dd::Bdd::fromVector(this->reachableStates.getDdManager(), this->explicitValues, this->odd, this->symbolicValues.getContainedMetaVariables(), comparisonType, bound); + symbolicResult |= storm::dd::Bdd::template fromVector(this->reachableStates.getDdManager(), this->explicitValues, this->odd, this->symbolicValues.getContainedMetaVariables(), comparisonType, storm::utility::convertNumber(bound)); return std::unique_ptr>(new SymbolicQualitativeCheckResult(reachableStates, symbolicResult)); } @@ -98,9 +98,9 @@ namespace storm { if (this->symbolicStates.isZero()) { out << *this->explicitValues.begin(); } else { - out << this->symbolicValues.getMax(); + out << this->symbolicValues.sumAbstract(this->symbolicValues.getContainedMetaVariables()).getValue(); } - } else if (totalNumberOfStates < 10) { + } else if (totalNumberOfStates < 10 || std::is_same::value) { out << "{"; bool first = true; if (!this->symbolicStates.isZero()) { @@ -165,7 +165,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.ite(this->symbolicValues, reachableStates.getDdManager().getConstant(storm::utility::infinity())); + storm::dd::Add tmp = symbolicStates.ite(this->symbolicValues, reachableStates.getDdManager().getConstant(storm::utility::infinity())); ValueType min = tmp.getMin(); if (!explicitStates.isZero()) { for (auto const& element : explicitValues) { @@ -202,8 +202,8 @@ namespace storm { template void HybridQuantitativeCheckResult::oneMinus() { - storm::dd::Add one = symbolicValues.getDdManager().template getAddOne(); - storm::dd::Add zero = symbolicValues.getDdManager().template getAddZero(); + storm::dd::Add one = symbolicValues.getDdManager().template getAddOne(); + storm::dd::Add zero = symbolicValues.getDdManager().template getAddZero(); symbolicValues = symbolicStates.ite(one - symbolicValues, zero); for (auto& element : explicitValues) { @@ -215,5 +215,7 @@ namespace storm { // Explicitly instantiate the class. template class HybridQuantitativeCheckResult; template class HybridQuantitativeCheckResult; + + template class HybridQuantitativeCheckResult; } } diff --git a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index 9dce5fe56..cc81da3cd 100644 --- a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -60,8 +60,8 @@ namespace storm { template std::ostream& SymbolicQuantitativeCheckResult::writeToStream(std::ostream& out) const { if (states.getNonZeroCount() == 1) { - out << this->values.getMax(); - } else if (states.getNonZeroCount() < 10) { + out << this->values.sumAbstract(this->values.getContainedMetaVariables()).getValue(); + } else if (states.getNonZeroCount() < 10 || std::is_same::value) { out << "{"; if (this->values.isZero()) { out << "0"; @@ -100,7 +100,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.ite(this->values, states.getDdManager().getConstant(storm::utility::infinity())).getMin(); + return states.ite(this->values, states.getDdManager().getConstant(storm::utility::infinity())).getMin(); } template @@ -120,12 +120,14 @@ namespace storm { template void SymbolicQuantitativeCheckResult::oneMinus() { - storm::dd::Add one = values.getDdManager().template getAddOne(); + storm::dd::Add one = values.getDdManager().template getAddOne(); values = one - values; } // Explicitly instantiate the class. template class SymbolicQuantitativeCheckResult; template class SymbolicQuantitativeCheckResult; + + template class SymbolicQuantitativeCheckResult; } } diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 521bc9f46..103659212 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -11,6 +11,7 @@ #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/InvalidOperationException.h" #include "storm-config.h" #include "storm/adapters/CarlAdapter.h" @@ -168,12 +169,6 @@ namespace storm { return Bdd(this->getDdManager(), internalAdd.minAbstractRepresentative(cube), this->getContainedMetaVariables()); } - template - Add Add::minAbstractExcept0(std::set const& metaVariables) const { - Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); - return Add(this->getDdManager(), internalAdd.minAbstractExcept0(cube), Dd::subtractMetaVariables(*this, cube)); - } - template Add Add::maxAbstract(std::set const& metaVariables) const { Bdd cube = Bdd::getCube(this->getDdManager(), metaVariables); @@ -859,13 +854,18 @@ namespace storm { } template - Add Add::toDouble() const { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Not yet implemented: replaceLeaves"); + template + Add Add::toValueType() const { + if (std::is_same::value) { + return *this; + } + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot convert this ADD to the target type."); } template<> - Add Add::toDouble() const { - return Add(this->getDdManager(), internalAdd.toDouble(), this->getContainedMetaVariables()); + template<> + Add Add::toValueType() const { + return Add(this->getDdManager(), internalAdd.toValueType(), this->getContainedMetaVariables()); } #endif diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index b3803bfc2..627d47de6 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -260,7 +260,8 @@ namespace storm { * * @return The resulting function represented as an ADD. */ - Add toDouble() const; + template + Add toValueType() const; #endif /*! @@ -277,13 +278,6 @@ namespace storm { */ Add minAbstract(std::set const& metaVariables) const; - /*! - * Min-abstracts from the given meta variables but treats 0 as the largest possible value. - * - * @param metaVariables The meta variables from which to abstract. - */ - Add minAbstractExcept0(std::set const& metaVariables) const; - /*! * Similar to minAbstract, but does not abstract from the variables but rather picks a * valuation of each of the meta variables "to abstract from" such that for this valuation, there exists a diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index 809d7d512..382709b0d 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -14,6 +14,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/InvalidOperationException.h" #include "storm-config.h" #include "storm/adapters/CarlAdapter.h" @@ -26,25 +27,39 @@ namespace storm { // Intentionally left empty. } + template + struct FromVectorHelper { + static Bdd fromVector(DdManager const& ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, ValueType value) { + switch (comparisonType) { + case storm::logic::ComparisonType::Less: + return fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater(), value, std::placeholders::_1)); + case storm::logic::ComparisonType::LessEqual: + return fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal(), value, std::placeholders::_1)); + case storm::logic::ComparisonType::Greater: + return fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::less(), value, std::placeholders::_1)); + case storm::logic::ComparisonType::GreaterEqual: + return fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal(), value, std::placeholders::_1)); + } + return Bdd(); + } + + static 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.getInternalDdManager(), values, odd, ddManager.getSortedVariableIndices(metaVariables), filter), metaVariables); + } + }; + template - 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)); - case storm::logic::ComparisonType::LessEqual: - return fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal(), value, std::placeholders::_1)); - case storm::logic::ComparisonType::Greater: - return fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::less(), value, std::placeholders::_1)); - case storm::logic::ComparisonType::GreaterEqual: - return fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal(), value, std::placeholders::_1)); + struct FromVectorHelper { + static Bdd fromVector(DdManager const& ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, storm::RationalFunction value) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot compare rational functions to bound."); + return Bdd(); } - return Bdd(); - } + }; template template - 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); + Bdd Bdd::fromVector(DdManager const& ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, ValueType value) { + return FromVectorHelper::fromVector(ddManager, explicitValues, odd, metaVariables, comparisonType, value); } template @@ -355,8 +370,7 @@ namespace storm { template class Bdd; - 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 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); template Add Bdd::toAdd() const; template Add Bdd::toAdd() const; @@ -370,10 +384,10 @@ namespace storm { template class Bdd; - 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 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); + #ifdef STORM_HAVE_CARL - 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& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, storm::RationalFunction value); #endif template Add Bdd::toAdd() const; diff --git a/src/storm/storage/dd/Bdd.h b/src/storm/storage/dd/Bdd.h index 1341a8e3b..14bd690a6 100644 --- a/src/storm/storage/dd/Bdd.h +++ b/src/storm/storage/dd/Bdd.h @@ -46,7 +46,8 @@ 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(DdManager const& ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, double value); + template + static Bdd fromVector(DdManager const& ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, ValueType value); /*! * Retrieves whether the two BDDs represent the same function. @@ -335,6 +336,9 @@ namespace storm { friend struct std::hash>; + template + friend struct FromVectorHelper; + private: /*! * We provide a conversion operator from the BDD to its internal type to ease calling the internal functions. @@ -350,19 +354,6 @@ namespace storm { */ 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. - * - * @param ddManager The manager responsible for the BDD. - * @param values The values that are to be checked against the filter function. - * @param odd The ODD used for the translation. - * @param metaVariables The meta variables used for the translation. - * @param filter The filter that evaluates whether an encoding is to be mapped to 0 or 1. - * @return The resulting BDD. - */ - template - 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/storm/storage/dd/Odd.cpp b/src/storm/storage/dd/Odd.cpp index 469b590b6..b89262fde 100644 --- a/src/storm/storage/dd/Odd.cpp +++ b/src/storm/storage/dd/Odd.cpp @@ -8,6 +8,8 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm/utility/file.h" +#include "storm/adapters/CarlAdapter.h" + namespace storm { namespace dd { Odd::Odd(std::shared_ptr elseNode, uint_fast64_t elseOffset, std::shared_ptr thenNode, uint_fast64_t thenOffset) : elseNode(elseNode), thenNode(thenNode), elseOffset(elseOffset), thenOffset(thenOffset) { @@ -69,11 +71,13 @@ namespace storm { return this->elseNode == nullptr && this->thenNode == nullptr; } - void Odd::expandExplicitVector(storm::dd::Odd const& newOdd, std::vector const& oldValues, std::vector& newValues) const { + template + void Odd::expandExplicitVector(storm::dd::Odd const& newOdd, std::vector const& oldValues, std::vector& newValues) const { expandValuesToVectorRec(0, *this, oldValues, 0, newOdd, newValues); } - void Odd::expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector const& oldValues, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::vector& newValues) { + template + void Odd::expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector const& oldValues, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::vector& newValues) { if (oldOdd.isTerminalNode()) { STORM_LOG_THROW(newOdd.isTerminalNode(), storm::exceptions::InvalidArgumentException, "The ODDs for the translation must have the same height."); if (oldOdd.getThenOffset() != 0) { @@ -140,5 +144,8 @@ namespace storm { this->getThenSuccessor().addToLevelToOddNodesMap(levelToOddNodesMap, level + 1); } } + + template void Odd::expandExplicitVector(storm::dd::Odd const& newOdd, std::vector const& oldValues, std::vector& newValues) const; + template void Odd::expandExplicitVector(storm::dd::Odd const& newOdd, std::vector const& oldValues, std::vector& newValues) const; } } diff --git a/src/storm/storage/dd/Odd.h b/src/storm/storage/dd/Odd.h index 7af761693..637e9ca6c 100644 --- a/src/storm/storage/dd/Odd.h +++ b/src/storm/storage/dd/Odd.h @@ -108,7 +108,8 @@ namespace storm { * @param oldValues The old vector of values (which is being read). * @param newValues The new vector of values (which is being written). */ - void expandExplicitVector(storm::dd::Odd const& newOdd, std::vector const& oldValues, std::vector& newValues) const; + template + void expandExplicitVector(storm::dd::Odd const& newOdd, std::vector const& oldValues, std::vector& newValues) const; /*! * Exports the ODD in the dot format to the given file. @@ -137,7 +138,8 @@ namespace storm { * @param newOdd The ODD to use for the new explicit values. * @param newValues The vector of new values. */ - static void expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector const& oldValues, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::vector& newValues); + template + static void expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector const& oldValues, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::vector& newValues); // The then- and else-nodes. std::shared_ptr elseNode; diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 723694fe1..5ac14aab8 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -152,11 +152,6 @@ namespace storm { return InternalBdd(ddManager, this->getCuddAdd().MinAbstractRepresentative(cube.toAdd().getCuddAdd())); } - template - InternalAdd InternalAdd::minAbstractExcept0(InternalBdd const& cube) const { - return InternalAdd(ddManager, this->getCuddAdd().MinAbstractExcept0(cube.toAdd().getCuddAdd())); - } - template InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->getCuddAdd().MaxAbstract(cube.toAdd().getCuddAdd())); diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.h b/src/storm/storage/dd/cudd/InternalCuddAdd.h index 096bbbcf3..893eaf06a 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.h @@ -260,13 +260,6 @@ namespace storm { */ InternalAdd minAbstract(InternalBdd const& cube) const; - /*! - * Min-abstracts from the given cube, but treats 0 as the largest possible value. - * - * @param cube The cube from which to abstract. - */ - InternalAdd minAbstractExcept0(InternalBdd const& cube) const; - /*! * Min-abstracts from the given cube and returns a representative. * diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 12d7d31f0..eca2fdfce 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -9,6 +9,7 @@ #include "storm/utility/macros.h" #include "storm/utility/constants.h" #include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/InvalidOperationException.h" #include "storm-config.h" @@ -24,6 +25,47 @@ namespace storm { // Intentionally left empty. } + template + ValueType InternalAdd::getValue(MTBDD const& node) { + STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << "."); + + bool negated = mtbdd_hascomp(node); + MTBDD n = mtbdd_regular(node); + + if (std::is_same::value) { + STORM_LOG_ASSERT(mtbdd_gettype(n) == 1, "Expected a double value."); + return negated ? -mtbdd_getdouble(n) : mtbdd_getdouble(n); + } else if (std::is_same::value) { + STORM_LOG_ASSERT(mtbdd_gettype(node) == 0, "Expected an unsigned value."); + return negated ? -mtbdd_getint64(node) : mtbdd_getint64(node); + } +#ifdef STORM_HAVE_CARL + else if (std::is_same::value) { + STORM_LOG_ASSERT(false, "Non-specialized version of getValue() called for storm::RationalFunction value."); + } +#endif + else { + STORM_LOG_ASSERT(false, "Illegal or unknown type in MTBDD."); + } + } + +#ifdef STORM_HAVE_CARL + template<> + storm::RationalFunction InternalAdd::getValue(MTBDD const& node) { + STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << "."); + + bool negated = mtbdd_hascomp(node); + + 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 ptr = (storm_rational_function_ptr)value; + + storm::RationalFunction* rationalFunction = (storm::RationalFunction*)(ptr); + + return negated ? -(*rationalFunction) : (*rationalFunction); + } +#endif + template bool InternalAdd::operator==(InternalAdd const& other) const { return this->sylvanMtbdd == other.sylvanMtbdd; @@ -145,8 +187,8 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalBdd InternalAdd::equals(InternalAdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Equals"); + InternalBdd InternalAdd::equals(InternalAdd const& other) const { + return InternalBdd(ddManager, this->sylvanMtbdd.EqualsRF(other.sylvanMtbdd)); } #endif @@ -155,13 +197,6 @@ namespace storm { return !this->equals(other); } -#ifdef STORM_HAVE_CARL - template<> - InternalBdd InternalAdd::notEquals(InternalAdd const&) 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)); @@ -169,8 +204,8 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalBdd InternalAdd::less(InternalAdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Less"); + InternalBdd InternalAdd::less(InternalAdd const& other) const { + return InternalBdd(ddManager, this->sylvanMtbdd.LessRF(other.sylvanMtbdd)); } #endif @@ -181,8 +216,8 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalBdd InternalAdd::lessOrEqual(InternalAdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Less or Equal"); + InternalBdd InternalAdd::lessOrEqual(InternalAdd const& other) const { + return InternalBdd(ddManager, this->sylvanMtbdd.LessOrEqualRF(other.sylvanMtbdd)); } #endif @@ -191,25 +226,11 @@ namespace storm { return !this->lessOrEqual(other); } -#ifdef STORM_HAVE_CARL - template<> - InternalBdd InternalAdd::greater(InternalAdd const&) 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&) 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)); @@ -217,8 +238,8 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalAdd InternalAdd::pow(InternalAdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Pow"); + InternalAdd InternalAdd::pow(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.PowRF(other.sylvanMtbdd)); } #endif @@ -230,7 +251,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::mod(InternalAdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Mod"); + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (mod) not supported by rational functions."); } #endif @@ -242,7 +263,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::logxy(InternalAdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: logxy"); + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (logxy) not supported by rational functions."); } #endif @@ -254,7 +275,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::floor() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Floor"); + return InternalAdd(ddManager, this->sylvanMtbdd.FloorRF()); } #endif @@ -266,7 +287,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> InternalAdd InternalAdd::ceil() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Ceil"); + return InternalAdd(ddManager, this->sylvanMtbdd.CeilRF()); } #endif @@ -277,8 +298,8 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalAdd InternalAdd::minimum(InternalAdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Minimum"); + InternalAdd InternalAdd::minimum(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.MinRF(other.sylvanMtbdd)); } #endif @@ -289,14 +310,14 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalAdd InternalAdd::maximum(InternalAdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Maximum"); + InternalAdd InternalAdd::maximum(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.MaxRF(other.sylvanMtbdd)); } #endif template InternalAdd InternalAdd::replaceLeaves(std::map>> const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: replaceLeaves"); + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Replacing leaves is not supported for types other than rational functions."); } #ifdef STORM_HAVE_CARL @@ -307,13 +328,18 @@ namespace storm { #endif template - InternalAdd InternalAdd::toDouble() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: toDouble"); + template + InternalAdd InternalAdd::toValueType() const { + if (std::is_same::value) { + return *this; + } + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot convert this ADD to the target type."); } - + #ifdef STORM_HAVE_CARL template<> - InternalAdd InternalAdd::toDouble() const { + template<> + InternalAdd InternalAdd::toValueType() const { return InternalAdd(ddManager, this->sylvanMtbdd.ToDoubleRF()); } #endif @@ -342,20 +368,8 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalAdd InternalAdd::minAbstract(InternalBdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstract"); - } -#endif - - template - InternalAdd InternalAdd::minAbstractExcept0(InternalBdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractExcept0"); - } - -#ifdef STORM_HAVE_CARL - template<> - InternalAdd InternalAdd::minAbstractExcept0(InternalBdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractExcept0"); + InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { + return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMinRF(cube.sylvanBdd)); } #endif @@ -371,8 +385,8 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - InternalAdd InternalAdd::maxAbstract(InternalBdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: maxAbstract"); + InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { + return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMaxRF(cube.sylvanBdd)); } #endif @@ -388,7 +402,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> bool InternalAdd::equalModuloPrecision(InternalAdd const&, double, bool) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: equalModuloPrecision"); + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (equal modulo precision) not supported by rational functions."); } #endif @@ -426,14 +440,26 @@ namespace storm { return InternalAdd(ddManager, this->sylvanMtbdd.AndExists(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd())); } +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { + InternalBdd summationVariables = ddManager->getBddOne(); + for (auto const& ddVariable : summationDdVariables) { + summationVariables &= ddVariable; + } + + return InternalAdd(ddManager, this->sylvanMtbdd.AndExistsRF(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd())); + } +#endif + template InternalBdd InternalAdd::greater(ValueType const& value) const { return InternalBdd(ddManager, this->sylvanMtbdd.BddStrictThreshold(value)); } template<> - InternalBdd InternalAdd::greater(storm::RationalFunction const& ) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + InternalBdd InternalAdd::greater(storm::RationalFunction const& value) const { + return InternalBdd(ddManager, this->sylvanMtbdd.BddStrictThresholdRF(value)); } template @@ -442,8 +468,8 @@ namespace storm { } template<> - InternalBdd InternalAdd::greaterOrEqual(storm::RationalFunction const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + InternalBdd InternalAdd::greaterOrEqual(storm::RationalFunction const& value) const { + return InternalBdd(ddManager, this->sylvanMtbdd.BddThresholdRF(value)); } template @@ -463,12 +489,12 @@ namespace storm { template InternalAdd InternalAdd::constrain(InternalAdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Operation (constrain) not yet implemented."); } template InternalAdd InternalAdd::restrict(InternalAdd const&) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Operation (restrict) not yet implemented."); } template @@ -499,10 +525,20 @@ namespace storm { return getValue(this->sylvanMtbdd.Minimum().GetMTBDD()); } + template <> + storm::RationalFunction InternalAdd::getMin() const { + return getValue(this->sylvanMtbdd.MinimumRF().GetMTBDD()); + } + template ValueType InternalAdd::getMax() const { return getValue(this->sylvanMtbdd.Maximum().GetMTBDD()); } + + template<> + storm::RationalFunction InternalAdd::getMax() const { + return getValue(this->sylvanMtbdd.MaximumRF().GetMTBDD()); + } template ValueType InternalAdd::getValue() const { @@ -871,47 +907,6 @@ namespace storm { return mtbdd_storm_rational_function(ptr); } - - template - ValueType InternalAdd::getValue(MTBDD const& node) { - STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << "."); - - bool negated = mtbdd_hascomp(node); - MTBDD n = mtbdd_regular(node); - - if (std::is_same::value) { - STORM_LOG_ASSERT(mtbdd_gettype(n) == 1, "Expected a double value."); - return negated ? -mtbdd_getdouble(n) : mtbdd_getdouble(n); - } else if (std::is_same::value) { - STORM_LOG_ASSERT(mtbdd_gettype(node) == 0, "Expected an unsigned value."); - return negated ? -mtbdd_getint64(node) : mtbdd_getint64(node); - } -#ifdef STORM_HAVE_CARL - else if (std::is_same::value) { - STORM_LOG_ASSERT(false, "Non-specialized version of getValue() called for storm::RationalFunction value."); - } -#endif - else { - STORM_LOG_ASSERT(false, "Illegal or unknown type in MTBDD."); - } - } - -#ifdef STORM_HAVE_CARL - template<> - storm::RationalFunction InternalAdd::getValue(MTBDD const& node) { - STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << "."); - - bool negated = mtbdd_hascomp(node); - - 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 ptr = (storm_rational_function_ptr)value; - - storm::RationalFunction* rationalFunction = (storm::RationalFunction*)(ptr); - - return negated ? -(*rationalFunction) : (*rationalFunction); - } -#endif template sylvan::Mtbdd InternalAdd::getSylvanMtbdd() const { @@ -920,6 +915,7 @@ namespace storm { template class InternalAdd; template class InternalAdd; + #ifdef STORM_HAVE_CARL template class InternalAdd; #endif diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index 93f732acc..1dd0358ad 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -262,7 +262,8 @@ namespace storm { * * @return The resulting function represented as an ADD. */ - InternalAdd toDouble() const; + template + InternalAdd toValueType() const; #endif /*! @@ -278,13 +279,6 @@ namespace storm { * @param cube The cube from which to abstract. */ InternalAdd minAbstract(InternalBdd const& cube) const; - - /*! - * Min-abstracts from the given cube, but treats 0 as the largest possible value. - * - * @param cube The cube from which to abstract. - */ - InternalAdd minAbstractExcept0(InternalBdd const& cube) const; /*! * Min-abstracts from the given cube and returns a representative. diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index f2d2b98a8..821b25bdb 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -356,7 +356,7 @@ namespace storm { value.simplify(); return std::move(value); } - + template<> double convertNumber(RationalNumber const& number){ return carl::toDouble(number); @@ -414,6 +414,11 @@ namespace storm { uint_fast64_t convertNumber(RationalFunction const& func) { return carl::toInt(func.nominatorAsNumber()); } + + template<> + RationalFunction convertNumber(RationalFunction const& number){ + return number; + } template<> RationalNumber sqrt(RationalNumber const& number) { @@ -603,6 +608,8 @@ namespace storm { template RationalFunction zero(); template storm::RationalFunction infinity(); + template storm::RationalFunction convertNumber(storm::RationalFunction const& number); + template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent); template RationalFunction simplify(RationalFunction value); template RationalFunction& simplify(RationalFunction& value); diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 592167496..5d8754970 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -1411,7 +1411,7 @@ namespace storm { template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates); - // Instantiations for Sylvan. + // Instantiations for Sylvan (double). template storm::dd::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound = boost::optional()); @@ -1443,6 +1443,34 @@ namespace storm { template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional> const& player1Candidates); + // Instantiations for Sylvan (rational function). + + template storm::dd::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound = boost::optional()); + + template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0); + + template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + + template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + + template storm::dd::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + + template storm::dd::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + + template storm::dd::Bdd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + + template storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + + template storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A); + + template storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E); + + template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + + template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); + } // namespace graph } // namespace utility } // namespace storm diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp index 88280f306..21b73c9fe 100644 --- a/src/storm/utility/solver.cpp +++ b/src/storm/utility/solver.cpp @@ -33,12 +33,26 @@ namespace storm { case storm::solver::EquationSolverType::Elimination: return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); break; case storm::solver::EquationSolverType::Native: return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + break; default: STORM_LOG_WARN("The selected equation solver is not available in the DD setting. Falling back to native solver."); return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); } } - + + template + std::unique_ptr> SymbolicLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { + + storm::solver::EquationSolverType equationSolver = storm::settings::getModule().getEquationSolver(); + switch (equationSolver) { + case storm::solver::EquationSolverType::Elimination: return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + break; + default: + STORM_LOG_WARN("The selected equation solver is not available in the DD setting. Falling back to elimination solver."); + return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + } + } + template std::unique_ptr> SymbolicMinMaxLinearEquationSolverFactory::create(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) const { return std::unique_ptr>(new storm::solver::SymbolicMinMaxLinearEquationSolver(A, allRows, illegalMask, rowMetaVariables, columnMetaVariables, choiceVariables, rowColumnMetaVariablePairs)); @@ -114,6 +128,7 @@ namespace storm { template class SymbolicLinearEquationSolverFactory; template class SymbolicLinearEquationSolverFactory; + template class SymbolicLinearEquationSolverFactory; template class SymbolicMinMaxLinearEquationSolverFactory; template class SymbolicMinMaxLinearEquationSolverFactory; template class SymbolicGameSolverFactory; diff --git a/src/storm/utility/solver.h b/src/storm/utility/solver.h index 8dc736c75..ab3255f67 100644 --- a/src/storm/utility/solver.h +++ b/src/storm/utility/solver.h @@ -63,6 +63,12 @@ namespace storm { virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const; }; + template + class SymbolicLinearEquationSolverFactory { + public: + virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const; + }; + template class SymbolicMinMaxLinearEquationSolverFactory { public: diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index c03076915..6a38f7891 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -580,31 +580,16 @@ namespace storm { template std::unique_ptr verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { -// std::unique_ptr result; -// storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); -// if (model->getType() == storm::models::ModelType::Dtmc) { -// std::shared_ptr> dtmc = model->template as>(); -// storm::modelchecker::HybridDtmcPrctlModelChecker> modelchecker(*dtmc); -// if (modelchecker.canHandle(task)) { -// result = modelchecker.check(task); -// } -// } else if (model->getType() == storm::models::ModelType::Ctmc) { -// std::shared_ptr> ctmc = model->template as>(); -// storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc); -// if (modelchecker.canHandle(task)) { -// result = modelchecker.check(task); -// } -// } else if (model->getType() == storm::models::ModelType::Mdp) { -// std::shared_ptr> mdp = model->template as>(); -// storm::modelchecker::HybridMdpPrctlModelChecker> modelchecker(*mdp); -// if (modelchecker.canHandle(task)) { -// result = modelchecker.check(task); -// } -// } else { -// STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); -// } -// return result; - return nullptr; + std::unique_ptr result; + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + + STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::NotSupportedException, "Only DTMCs are supported by this engine (in parametric mode)."); + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::HybridDtmcPrctlModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + return result; } template @@ -631,25 +616,16 @@ namespace storm { template std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { -// std::unique_ptr result; -// storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); -// if (model->getType() == storm::models::ModelType::Dtmc) { -// std::shared_ptr> dtmc = model->template as>(); -// storm::modelchecker::SymbolicDtmcPrctlModelChecker> modelchecker(*dtmc); -// if (modelchecker.canHandle(task)) { -// result = modelchecker.check(task); -// } -// } else if (model->getType() == storm::models::ModelType::Mdp) { -// std::shared_ptr> mdp = model->template as>(); -// storm::modelchecker::SymbolicMdpPrctlModelChecker> modelchecker(*mdp); -// if (modelchecker.canHandle(task)) { -// result = modelchecker.check(task); -// } -// } else { -// STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented."); -// } -// return result; - return nullptr; + std::unique_ptr result; + storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + + STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::NotSupportedException, "Only DTMCs are supported by this engine (in parametric mode)."); + std::shared_ptr> dtmc = model->template as>(); + storm::modelchecker::SymbolicDtmcPrctlModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + return result; } template