From 952776a05766713dc6a022de50ab0b25c30248a1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 27 Mar 2017 21:20:14 +0200 Subject: [PATCH] hybrid engine working for rational numbers --- resources/3rdparty/CMakeLists.txt | 3 - resources/3rdparty/cudd-3.0.0/Makefile.in | 1 + resources/3rdparty/cudd-3.0.0/configure | 14 +- .../3rdparty/sylvan/src/storm_wrapper.cpp | 80 +++++++-- resources/3rdparty/sylvan/src/storm_wrapper.h | 6 + resources/3rdparty/sylvan/src/sylvan_int.h | 15 +- .../3rdparty/sylvan/src/sylvan_mtbdd_storm.c | 28 +-- .../3rdparty/sylvan/src/sylvan_mtbdd_storm.h | 8 +- .../sylvan/src/sylvan_obj_mtbdd_storm.hpp | 6 + .../3rdparty/sylvan/src/sylvan_obj_storm.cpp | 39 ++++- .../src/sylvan_storm_rational_function.c | 148 ++++++++++++++++ .../src/sylvan_storm_rational_function.h | 6 + .../sylvan/src/sylvan_storm_rational_number.c | 163 +++++++++++++++++- .../sylvan/src/sylvan_storm_rational_number.h | 6 + src/storm/adapters/AddExpressionAdapter.cpp | 7 +- src/storm/builder/DdJaniModelBuilder.cpp | 1 + src/storm/builder/DdPrismModelBuilder.cpp | 3 +- src/storm/cli/entrypoints.h | 12 +- .../generator/PrismNextStateGenerator.cpp | 10 +- .../modelchecker/AbstractModelChecker.cpp | 3 + .../csl/HybridCtmcCslModelChecker.cpp | 37 ++-- .../csl/HybridCtmcCslModelChecker.h | 8 + .../csl/helper/HybridCtmcCslHelper.cpp | 103 ++++++++--- .../csl/helper/HybridCtmcCslHelper.h | 38 ++-- .../prctl/HybridDtmcPrctlModelChecker.cpp | 1 + .../prctl/HybridMdpPrctlModelChecker.cpp | 3 + .../prctl/SymbolicDtmcPrctlModelChecker.cpp | 5 +- .../prctl/SymbolicDtmcPrctlModelChecker.h | 7 +- .../prctl/SymbolicMdpPrctlModelChecker.cpp | 2 + .../prctl/helper/HybridDtmcPrctlHelper.cpp | 3 +- .../prctl/helper/HybridMdpPrctlHelper.cpp | 23 +-- .../prctl/helper/SparseDtmcPrctlHelper.cpp | 2 +- .../prctl/helper/SymbolicDtmcPrctlHelper.cpp | 13 +- .../prctl/helper/SymbolicDtmcPrctlHelper.h | 14 +- .../prctl/helper/SymbolicMdpPrctlHelper.cpp | 24 +-- .../SymbolicPropositionalModelChecker.cpp | 3 + .../results/HybridQuantitativeCheckResult.cpp | 71 ++++++-- .../SymbolicParetoCurveCheckResult.cpp | 2 + .../SymbolicQuantitativeCheckResult.cpp | 3 +- src/storm/models/symbolic/Ctmc.cpp | 1 + .../models/symbolic/DeterministicModel.cpp | 1 + src/storm/models/symbolic/Dtmc.cpp | 1 + src/storm/models/symbolic/Mdp.cpp | 1 + src/storm/models/symbolic/Model.cpp | 1 + .../models/symbolic/NondeterministicModel.cpp | 2 + .../models/symbolic/StandardRewardModel.cpp | 1 + ...ymbolicEliminationLinearEquationSolver.cpp | 27 ++- .../SymbolicEliminationLinearEquationSolver.h | 20 ++- .../solver/SymbolicLinearEquationSolver.cpp | 63 +++++-- .../solver/SymbolicLinearEquationSolver.h | 54 +++--- .../SymbolicMinMaxLinearEquationSolver.cpp | 3 +- .../SymbolicMinMaxLinearEquationSolver.h | 2 +- .../SymbolicNativeLinearEquationSolver.cpp | 80 ++++++++- .../SymbolicNativeLinearEquationSolver.h | 61 +++++-- src/storm/storage/dd/Add.cpp | 4 +- src/storm/storage/dd/Add.h | 2 +- src/storm/storage/dd/Bdd.cpp | 7 + src/storm/storage/dd/DdManager.cpp | 6 +- src/storm/storage/dd/Odd.cpp | 1 + src/storm/storage/dd/cudd/InternalCuddAdd.cpp | 2 +- src/storm/storage/dd/cudd/InternalCuddAdd.h | 2 +- .../storage/dd/sylvan/InternalSylvanAdd.cpp | 21 ++- .../storage/dd/sylvan/InternalSylvanAdd.h | 2 +- .../storage/dd/sylvan/InternalSylvanBdd.cpp | 6 + .../expressions/ExpressionEvaluator.cpp | 3 +- .../expressions/ToRationalNumberVisitor.cpp | 38 ++-- .../SymbolicToSparseTransformer.cpp | 14 +- .../transformer/SymbolicToSparseTransformer.h | 2 +- src/storm/utility/constants.cpp | 46 ++++- src/storm/utility/dd.cpp | 1 + src/storm/utility/graph.cpp | 28 +++ src/storm/utility/solver.cpp | 30 +--- src/storm/utility/solver.h | 12 -- src/storm/utility/storm.h | 96 +++++------ .../SymbolicDtmcPrctlModelCheckerTest.cpp | 12 +- 75 files changed, 1212 insertions(+), 362 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index b8ce069b2..b62cfb3d0 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -383,9 +383,6 @@ ExternalProject_Add( LOG_CONFIGURE ON LOG_BUILD ON BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/sylvan/src/libsylvan${STATIC_EXT} - - # TODO: REMOVE AFTER DEBUGGING - BUILD_ALWAYS 1 ) ExternalProject_Get_Property(sylvan source_dir) ExternalProject_Get_Property(sylvan binary_dir) diff --git a/resources/3rdparty/cudd-3.0.0/Makefile.in b/resources/3rdparty/cudd-3.0.0/Makefile.in index 75846bc4c..c18a9a946 100644 --- a/resources/3rdparty/cudd-3.0.0/Makefile.in +++ b/resources/3rdparty/cudd-3.0.0/Makefile.in @@ -795,6 +795,7 @@ pdfdir = @pdfdir@ prefix = @prefix@ program_transform_name = @program_transform_name@ psdir = @psdir@ +runstatedir = @runstatedir@ sbindir = @sbindir@ sharedstatedir = @sharedstatedir@ srcdir = @srcdir@ diff --git a/resources/3rdparty/cudd-3.0.0/configure b/resources/3rdparty/cudd-3.0.0/configure index 1494802d5..ef3832be0 100755 --- a/resources/3rdparty/cudd-3.0.0/configure +++ b/resources/3rdparty/cudd-3.0.0/configure @@ -754,6 +754,7 @@ infodir docdir oldincludedir includedir +runstatedir localstatedir sharedstatedir sysconfdir @@ -840,6 +841,7 @@ datadir='${datarootdir}' sysconfdir='${prefix}/etc' sharedstatedir='${prefix}/com' localstatedir='${prefix}/var' +runstatedir='${localstatedir}/run' includedir='${prefix}/include' oldincludedir='/usr/include' docdir='${datarootdir}/doc/${PACKAGE_TARNAME}' @@ -1092,6 +1094,15 @@ do | -silent | --silent | --silen | --sile | --sil) silent=yes ;; + -runstatedir | --runstatedir | --runstatedi | --runstated \ + | --runstate | --runstat | --runsta | --runst | --runs \ + | --run | --ru | --r) + ac_prev=runstatedir ;; + -runstatedir=* | --runstatedir=* | --runstatedi=* | --runstated=* \ + | --runstate=* | --runstat=* | --runsta=* | --runst=* | --runs=* \ + | --run=* | --ru=* | --r=*) + runstatedir=$ac_optarg ;; + -sbindir | --sbindir | --sbindi | --sbind | --sbin | --sbi | --sb) ac_prev=sbindir ;; -sbindir=* | --sbindir=* | --sbindi=* | --sbind=* | --sbin=* \ @@ -1229,7 +1240,7 @@ fi for ac_var in exec_prefix prefix bindir sbindir libexecdir datarootdir \ datadir sysconfdir sharedstatedir localstatedir includedir \ oldincludedir docdir infodir htmldir dvidir pdfdir psdir \ - libdir localedir mandir + libdir localedir mandir runstatedir do eval ac_val=\$$ac_var # Remove trailing slashes. @@ -1382,6 +1393,7 @@ Fine tuning of the installation directories: --sysconfdir=DIR read-only single-machine data [PREFIX/etc] --sharedstatedir=DIR modifiable architecture-independent data [PREFIX/com] --localstatedir=DIR modifiable single-machine data [PREFIX/var] + --runstatedir=DIR modifiable per-process data [LOCALSTATEDIR/run] --libdir=DIR object code libraries [EPREFIX/lib] --includedir=DIR C header files [PREFIX/include] --oldincludedir=DIR C header files for non-gcc [/usr/include] diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp index cfc39912c..2a89e0662 100644 --- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp @@ -16,8 +16,9 @@ #include #include -// TODO: remove and replace by proper detection in cmake +#if defined(STORM_HAVE_GMP) && !defined(STORM_USE_CLN_EA) #define RATIONAL_NUMBER_THREAD_SAFE +#endif // A mutex that is used to lock all operations accessing rational numbers as they are not necessarily thread-safe. #ifndef RATIONAL_NUMBER_THREAD_SAFE @@ -47,7 +48,7 @@ void storm_rational_number_destroy(storm_rational_number_ptr a) { std::lock_guard lock(rationalNumberMutex); #endif - storm::RationalFunction* srn_ptr = (storm::RationalFunction*)a; + storm::RationalNumber* srn_ptr = (storm::RationalNumber*)a; delete srn_ptr; } @@ -224,9 +225,6 @@ storm_rational_number_ptr storm_rational_number_max(storm_rational_number_ptr a, return storm_rational_number_less(a, b) ? storm_rational_number_clone(b) : storm_rational_number_clone(a); } - - - int storm_rational_number_less(storm_rational_number_ptr a, storm_rational_number_ptr b) { #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); @@ -235,6 +233,12 @@ int storm_rational_number_less(storm_rational_number_ptr a, storm_rational_numbe storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; + if (storm::utility::isInfinity(srn_b)) { + return storm::utility::isInfinity(srn_a) ? 0 : 1; + } else if (storm::utility::isInfinity(srn_a)) { + return 0; + } + return srn_a < srn_b ? 1 : 0; } @@ -246,6 +250,12 @@ int storm_rational_number_less_or_equal(storm_rational_number_ptr a, storm_ratio storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; + if (storm::utility::isInfinity(srn_b)) { + return 1; + } else if (storm::utility::isInfinity(srn_a)) { + return 0; + } + return srn_a <= srn_b ? 1 : 0; } @@ -279,6 +289,21 @@ storm_rational_number_ptr storm_rational_number_ceil(storm_rational_number_ptr a return (storm_rational_number_ptr)result_srn; } +int storm_rational_number_equal_modulo_precision(int relative, storm_rational_number_ptr a, storm_rational_number_ptr b, storm_rational_number_ptr precision) { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; + storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; + storm::RationalNumber const& srn_p = *(storm::RationalNumber const*)precision; + + if (relative) { + return carl::abs(srn_a - srn_b)/srn_a < srn_p ? 1 : 0; + } else { + return carl::abs(srn_a - srn_b) < srn_p ? 1 : 0; + } +} void print_storm_rational_number(storm_rational_number_ptr a) { #ifndef RATIONAL_NUMBER_THREAD_SAFE @@ -525,12 +550,16 @@ int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_f throw storm::exceptions::InvalidOperationException() << "Operands of less must not be non-constant rational functions."; } - if (storm::utility::convertNumber(srf_a) < storm::utility::convertNumber(srf_b)) { - return 1; - } else { + storm::RationalFunctionCoefficient srn_a = storm::utility::convertNumber(srf_a); + storm::RationalFunctionCoefficient srn_b = storm::utility::convertNumber(srf_b); + + if (storm::utility::isInfinity(srn_b)) { + return storm::utility::isInfinity(srn_a) ? 0 : 1; + } else if (storm::utility::isInfinity(srn_a)) { return 0; } - return -1; + + return (srn_a < srn_b) ? 1 : 0; } int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_rational_function_ptr b) { @@ -544,12 +573,16 @@ int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_r throw storm::exceptions::InvalidOperationException() << "Operands of less-or-equal must not be non-constant rational functions."; } - if (storm::utility::convertNumber(srf_a) <= storm::utility::convertNumber(srf_b)) { + storm::RationalFunctionCoefficient srn_a = storm::utility::convertNumber(srf_a); + storm::RationalFunctionCoefficient srn_b = storm::utility::convertNumber(srf_b); + + if (storm::utility::isInfinity(srn_b)) { return 1; - } else { + } else if (storm::utility::isInfinity(srn_a)) { return 0; } - return -1; + + return (srn_a <= srn_b) ? 1 : 0; } storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a) { @@ -588,6 +621,29 @@ storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function return (storm_rational_function_ptr)result_srf; } +int storm_rational_function_equal_modulo_precision(int relative, storm_rational_function_ptr a, storm_rational_function_ptr b, storm_rational_function_ptr precision) { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; + storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; + storm::RationalFunction const& srf_p = *(storm::RationalFunction const*)precision; + + if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b) || !storm::utility::isConstant(srf_p)) { + throw storm::exceptions::InvalidOperationException() << "Operands of equal-modulo-precision must not be non-constant rational functions."; + } + + storm::RationalFunctionCoefficient srn_a = storm::utility::convertNumber(srf_a); + storm::RationalFunctionCoefficient srn_b = storm::utility::convertNumber(srf_b); + storm::RationalFunctionCoefficient srn_p = storm::utility::convertNumber(srf_p); + + if (relative) { + return carl::abs(srn_a - srn_b)/srn_a < srn_p ? 1 : 0; + } else { + return carl::abs(srn_a - srn_b) < srn_p ? 1 : 0; + } +} void print_storm_rational_function(storm_rational_function_ptr a) { #ifndef RATIONAL_FUNCTION_THREAD_SAFE diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.h b/resources/3rdparty/sylvan/src/storm_wrapper.h index 537c33a40..810269ecc 100644 --- a/resources/3rdparty/sylvan/src/storm_wrapper.h +++ b/resources/3rdparty/sylvan/src/storm_wrapper.h @@ -48,6 +48,9 @@ extern "C" { storm_rational_number_ptr storm_rational_number_floor(storm_rational_number_ptr a); storm_rational_number_ptr storm_rational_number_ceil(storm_rational_number_ptr a); + // Other operations. + int storm_rational_number_equal_modulo_precision(int relative, storm_rational_number_ptr a, storm_rational_number_ptr b, storm_rational_number_ptr precision); + // Printing functions. void print_storm_rational_number(storm_rational_number_ptr a); void print_storm_rational_number_to_file(storm_rational_number_ptr a, FILE* out); @@ -91,6 +94,9 @@ extern "C" { 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); + // Other operations. + int storm_rational_function_equal_modulo_precision(int relative, storm_rational_function_ptr a, storm_rational_function_ptr b, storm_rational_function_ptr precision); + // Printing functions. void print_storm_rational_function(storm_rational_function_ptr a); void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out); diff --git a/resources/3rdparty/sylvan/src/sylvan_int.h b/resources/3rdparty/sylvan/src/sylvan_int.h index a68b800c1..df12c14f2 100755 --- a/resources/3rdparty/sylvan/src/sylvan_int.h +++ b/resources/3rdparty/sylvan/src/sylvan_int.h @@ -92,10 +92,17 @@ extern llmsset_t nodes; #define CACHE_MTBDD_GREATER (55LL<<40) #define CACHE_MTBDD_EVAL_COMPOSE (56LL<<40) #define CACHE_MTBDD_NONZERO_COUNT (57LL<<40) -#define CACHE_MTBDD_AND_EXISTS_RF (58LL<<40) -#define CACHE_MTBDD_MINIMUM_RF (59LL<<40) -#define CACHE_MTBDD_MAXIMUM_RF (60LL<<40) - +#define CACHE_MTBDD_AND_EXISTS_RN (58LL<<40) +#define CACHE_MTBDD_MINIMUM_RN (59LL<<40) +#define CACHE_MTBDD_MAXIMUM_RN (60LL<<40) +#define CACHE_MTBDD_EQUAL_NORM_RN (61LL<<40) +#define CACHE_MTBDD_EQUAL_NORM_REL_RN (62LL<<40) +#define CACHE_MTBDD_AND_EXISTS_RF (63LL<<40) +#define CACHE_MTBDD_MINIMUM_RF (64LL<<40) +#define CACHE_MTBDD_MAXIMUM_RF (65LL<<40) +#define CACHE_MTBDD_EQUAL_NORM_RF (66LL<<40) +#define CACHE_MTBDD_EQUAL_NORM_REL_RF (67LL<<40) + #ifdef __cplusplus } #endif /* __cplusplus */ diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c index af0dbc4aa..28d8e4e11 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c @@ -586,7 +586,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_complement, MTBDD, a, size_t, k) (void)k; // unused variable } -TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR, prev_level) { +TASK_IMPL_3(BDD, mtbdd_min_abstract_representative, MTBDD, a, BDD, variables, BDDVAR, prev_level) { /* Maybe perform garbage collection */ sylvan_gc_test(); @@ -597,7 +597,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR /* Cube is guaranteed to be a cube at this point. */ if (mtbdd_isleaf(a)) { BDD _v = sylvan_set_next(variables); - BDD res = CALL(mtbdd_minExistsRepresentative, a, _v, prev_level); + BDD res = CALL(mtbdd_min_abstract_representative, a, _v, prev_level); if (res == sylvan_invalid) { return sylvan_invalid; } @@ -620,7 +620,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR /* Abstract a variable that does not appear in a. */ if (va > vv) { BDD _v = sylvan_set_next(variables); - BDD res = CALL(mtbdd_minExistsRepresentative, a, _v, va); + BDD res = CALL(mtbdd_min_abstract_representative, a, _v, va); if (res == sylvan_invalid) { return sylvan_invalid; } @@ -648,13 +648,13 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR /* If the two indices are the same, so are their levels. */ if (va == vv) { BDD _v = sylvan_set_next(variables); - BDD res1 = CALL(mtbdd_minExistsRepresentative, E, _v, va); + BDD res1 = CALL(mtbdd_min_abstract_representative, E, _v, va); if (res1 == sylvan_invalid) { return sylvan_invalid; } sylvan_ref(res1); - BDD res2 = CALL(mtbdd_minExistsRepresentative, T, _v, va); + BDD res2 = CALL(mtbdd_min_abstract_representative, T, _v, va); if (res2 == sylvan_invalid) { sylvan_deref(res1); return sylvan_invalid; @@ -730,12 +730,12 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR return res; } else { /* if (va < vv) */ - BDD res1 = CALL(mtbdd_minExistsRepresentative, E, variables, va); + BDD res1 = CALL(mtbdd_min_abstract_representative, E, variables, va); if (res1 == sylvan_invalid) { return sylvan_invalid; } sylvan_ref(res1); - BDD res2 = CALL(mtbdd_minExistsRepresentative, T, variables, va); + BDD res2 = CALL(mtbdd_min_abstract_representative, T, variables, va); if (res2 == sylvan_invalid) { sylvan_deref(res1); return sylvan_invalid; @@ -756,7 +756,7 @@ TASK_IMPL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, a, BDD, variables, BDDVAR } } -TASK_IMPL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint32_t, prev_level) { +TASK_IMPL_3(BDD, mtbdd_max_abstract_representative, MTBDD, a, MTBDD, variables, uint32_t, prev_level) { /* Maybe perform garbage collection */ sylvan_gc_test(); @@ -767,7 +767,7 @@ TASK_IMPL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint /* Cube is guaranteed to be a cube at this point. */ if (mtbdd_isleaf(a)) { BDD _v = sylvan_set_next(variables); - BDD res = CALL(mtbdd_maxExistsRepresentative, a, _v, prev_level); + BDD res = CALL(mtbdd_max_abstract_representative, a, _v, prev_level); if (res == sylvan_invalid) { return sylvan_invalid; } @@ -790,7 +790,7 @@ TASK_IMPL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint /* Abstract a variable that does not appear in a. */ if (va > vv) { BDD _v = sylvan_set_next(variables); - BDD res = CALL(mtbdd_maxExistsRepresentative, a, _v, va); + BDD res = CALL(mtbdd_max_abstract_representative, a, _v, va); if (res == sylvan_invalid) { return sylvan_invalid; } @@ -818,13 +818,13 @@ TASK_IMPL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint /* If the two indices are the same, so are their levels. */ if (va == vv) { BDD _v = sylvan_set_next(variables); - BDD res1 = CALL(mtbdd_maxExistsRepresentative, E, _v, va); + BDD res1 = CALL(mtbdd_max_abstract_representative, E, _v, va); if (res1 == sylvan_invalid) { return sylvan_invalid; } sylvan_ref(res1); - BDD res2 = CALL(mtbdd_maxExistsRepresentative, T, _v, va); + BDD res2 = CALL(mtbdd_max_abstract_representative, T, _v, va); if (res2 == sylvan_invalid) { sylvan_deref(res1); return sylvan_invalid; @@ -900,12 +900,12 @@ TASK_IMPL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint return res; } else { /* if (va < vv) */ - BDD res1 = CALL(mtbdd_maxExistsRepresentative, E, variables, va); + BDD res1 = CALL(mtbdd_max_abstract_representative, E, variables, va); if (res1 == sylvan_invalid) { return sylvan_invalid; } sylvan_ref(res1); - BDD res2 = CALL(mtbdd_maxExistsRepresentative, T, variables, va); + BDD res2 = CALL(mtbdd_max_abstract_representative, T, variables, va); if (res2 == sylvan_invalid) { sylvan_deref(res1); return sylvan_invalid; diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h index 77497c0b0..33bfc9e4f 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h @@ -137,14 +137,14 @@ TASK_DECL_2(MTBDD, mtbdd_op_complement, MTBDD, size_t); /** * Just like mtbdd_abstract_min, but instead of abstracting the variables in the given cube, picks a unique representative that realizes the minimal function value. */ -TASK_DECL_3(BDD, mtbdd_minExistsRepresentative, MTBDD, MTBDD, uint32_t); -#define mtbdd_minExistsRepresentative(a, vars) (CALL(mtbdd_minExistsRepresentative, a, vars, 0)) +TASK_DECL_3(BDD, mtbdd_min_abstract_representative, MTBDD, MTBDD, uint32_t); +#define mtbdd_min_abstract_representative(a, vars) (CALL(mtbdd_min_abstract_representative, a, vars, 0)) /** * Just like mtbdd_abstract_max but instead of abstracting the variables in the given cube, picks a unique representative that realizes the maximal function value. */ -TASK_DECL_3(BDD, mtbdd_maxExistsRepresentative, MTBDD, MTBDD, uint32_t); -#define mtbdd_maxExistsRepresentative(a, vars) (CALL(mtbdd_maxExistsRepresentative, a, vars, 0)) +TASK_DECL_3(BDD, mtbdd_max_abstract_representative, MTBDD, MTBDD, uint32_t); +#define mtbdd_max_abstract_representative(a, vars) (CALL(mtbdd_max_abstract_representative, a, vars, 0)) TASK_DECL_3(MTBDD, mtbdd_uapply_nocache, MTBDD, mtbdd_uapply_op, size_t); #define mtbdd_uapply_nocache(dd, op, param) CALL(mtbdd_uapply_nocache, dd, op, param) diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp index eb2ec97de..59dda64fd 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp @@ -59,6 +59,9 @@ Mtbdd AbstractMaxRN(const BddSet &variables) const; Bdd BddThresholdRN(storm::RationalNumber const& rn) const; Bdd BddStrictThresholdRN(storm::RationalNumber const& rn) const; +bool EqualNormRN(const Mtbdd& other, storm::RationalNumber const& epsilon) const; +bool EqualNormRelRN(const Mtbdd& other, storm::RationalNumber const& epsilon) const; + Mtbdd ToDoubleRN() const; // Functions that operate on Mtbdds over rational functions. @@ -91,6 +94,9 @@ Mtbdd AbstractMaxRF(const BddSet &variables) const; Bdd BddThresholdRF(storm::RationalFunction const& rf) const; Bdd BddStrictThresholdRF(storm::RationalFunction const& rf) const; +bool EqualNormRF(const Mtbdd& other, storm::RationalFunction const& epsilon) const; +bool EqualNormRelRF(const Mtbdd& other, storm::RationalFunction const& epsilon) 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 00740768d..6e3b524c7 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -9,6 +9,7 @@ void Sylvan::initCustomMtbdd() { sylvan_init_mt(); + sylvan_storm_rational_number_init(); sylvan_storm_rational_function_init(); } @@ -131,14 +132,14 @@ Bdd Mtbdd::AbstractMinRepresentative(const BddSet &variables) const { LACE_ME; - return mtbdd_minExistsRepresentative(mtbdd, variables.set.bdd); + return mtbdd_min_abstract_representative(mtbdd, variables.set.bdd); } Bdd Mtbdd::AbstractMaxRepresentative(const BddSet &variables) const { LACE_ME; - return mtbdd_maxExistsRepresentative(mtbdd, variables.set.bdd); + return mtbdd_max_abstract_representative(mtbdd, variables.set.bdd); } Mtbdd @@ -315,13 +316,25 @@ Mtbdd Mtbdd::AbstractMaxRN(const BddSet &variables) const { Bdd Mtbdd::BddThresholdRN(storm::RationalNumber const& rn) const { LACE_ME; - return sylvan_storm_rational_number_threshold(mtbdd, (void*)&rn); + return sylvan_storm_rational_number_threshold(mtbdd, (storm_rational_number_ptr)&rn); } Bdd Mtbdd::BddStrictThresholdRN(storm::RationalNumber const& rn) const { LACE_ME; - return sylvan_storm_rational_number_strict_threshold(mtbdd, (void*)&rn); + return sylvan_storm_rational_number_strict_threshold(mtbdd, (storm_rational_number_ptr)&rn); +} + +bool +Mtbdd::EqualNormRN(const Mtbdd& other, storm::RationalNumber const& epsilon) const { + LACE_ME; + return sylvan_storm_rational_number_equal_norm_d(mtbdd, other.mtbdd, (storm_rational_number_ptr)&epsilon); +} + +bool +Mtbdd::EqualNormRelRN(const Mtbdd& other, storm::RationalNumber const& epsilon) const { + LACE_ME; + return sylvan_storm_rational_number_equal_norm_rel_d(mtbdd, other.mtbdd, (storm_rational_number_ptr)&epsilon); } Mtbdd @@ -330,8 +343,6 @@ Mtbdd::ToDoubleRN() const { return sylvan_storm_rational_number_to_double(mtbdd); } - - // Functions for Mtbdds over rational functions. #if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) Mtbdd @@ -453,13 +464,25 @@ Mtbdd Mtbdd::AbstractMaxRF(const BddSet &variables) const { Bdd Mtbdd::BddThresholdRF(storm::RationalFunction const& rf) const { LACE_ME; - return sylvan_storm_rational_function_threshold(mtbdd, (void*)&rf); + return sylvan_storm_rational_function_threshold(mtbdd, (storm_rational_function_ptr)&rf); } Bdd Mtbdd::BddStrictThresholdRF(storm::RationalFunction const& rf) const { LACE_ME; - return sylvan_storm_rational_function_strict_threshold(mtbdd, (void*)&rf); + return sylvan_storm_rational_function_strict_threshold(mtbdd, (storm_rational_function_ptr)&rf); +} + +bool +Mtbdd::EqualNormRF(const Mtbdd& other, storm::RationalFunction const& epsilon) const { + LACE_ME; + return sylvan_storm_rational_function_equal_norm_d(mtbdd, other.mtbdd, (storm_rational_number_ptr)&epsilon); +} + +bool +Mtbdd::EqualNormRelRF(const Mtbdd& other, storm::RationalFunction const& epsilon) const { + LACE_ME; + return sylvan_storm_rational_function_equal_norm_rel_d(mtbdd, other.mtbdd, (storm_rational_number_ptr)&epsilon); } Mtbdd diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c index 317361fe8..8cf8a5b88 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c @@ -639,3 +639,151 @@ TASK_IMPL_1(MTBDD, sylvan_storm_rational_function_maximum, MTBDD, a) cache_put3(CACHE_MTBDD_MAXIMUM_RF, a, 0, 0, result); return result; } + +TASK_4(MTBDD, sylvan_storm_rational_function_equal_norm_d2, MTBDD, a, MTBDD, b, storm_rational_function_ptr, svalue, int*, shortcircuit) +{ + /* Check short circuit */ + if (*shortcircuit) return mtbdd_false; + + /* Check terminal case */ + if (a == b) return mtbdd_true; + if (a == mtbdd_false) return mtbdd_false; + if (b == mtbdd_false) return mtbdd_false; + + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); + int la = mtbddnode_isleaf(na); + int lb = mtbddnode_isleaf(nb); + + if (la && lb) { + storm_rational_function_ptr fa = mtbdd_getstorm_rational_function_ptr(a); + storm_rational_function_ptr fb = mtbdd_getstorm_rational_function_ptr(b); + + return storm_rational_function_equal_modulo_precision(0, fa, fb, svalue) ? mtbdd_true : mtbdd_false; + } + + if (b < a) { + MTBDD t = a; + a = b; + b = t; + } + + /* Maybe perform garbage collection */ + sylvan_gc_test(); + + /* Count operation */ + sylvan_stats_count(MTBDD_EQUAL_NORM); + + /* Check cache */ + MTBDD result; + if (cache_get3(CACHE_MTBDD_EQUAL_NORM_RF, a, b, svalue, &result)) { + sylvan_stats_count(MTBDD_EQUAL_NORM_CACHED); + return result; + } + + /* Get top variable */ + uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); + uint32_t vb = lb ? 0xffffffff : mtbddnode_getvariable(nb); + uint32_t var = va < vb ? va : vb; + + /* Get cofactors */ + MTBDD alow, ahigh, blow, bhigh; + alow = va == var ? node_getlow(a, na) : a; + ahigh = va == var ? node_gethigh(a, na) : a; + blow = vb == var ? node_getlow(b, nb) : b; + bhigh = vb == var ? node_gethigh(b, nb) : b; + + SPAWN(sylvan_storm_rational_function_equal_norm_d2, ahigh, bhigh, svalue, shortcircuit); + result = CALL(sylvan_storm_rational_function_equal_norm_d2, alow, blow, svalue, shortcircuit); + if (result == mtbdd_false) *shortcircuit = 1; + if (result != SYNC(sylvan_storm_rational_function_equal_norm_d2)) result = mtbdd_false; + if (result == mtbdd_false) *shortcircuit = 1; + + /* Store in cache */ + if (cache_put3(CACHE_MTBDD_EQUAL_NORM_RF, a, b, svalue, result)) { + sylvan_stats_count(MTBDD_EQUAL_NORM_CACHEDPUT); + } + + return result; +} + +TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_equal_norm_d, MTBDD, a, MTBDD, b, storm_rational_function_ptr, d) +{ + /* the implementation checks shortcircuit in every task and if the two + MTBDDs are not equal module epsilon, then the computation tree quickly aborts */ + int shortcircuit = 0; + return CALL(sylvan_storm_rational_function_equal_norm_d2, a, b, d, &shortcircuit); +} + +/** + * Compare two Double MTBDDs, returns Boolean True if they are equal within some value epsilon + * This version computes the relative difference vs the value in a. + */ +TASK_4(MTBDD, sylvan_storm_rational_function_equal_norm_rel_d2, MTBDD, a, MTBDD, b, storm_rational_function_ptr, svalue, int*, shortcircuit) +{ + /* Check short circuit */ + if (*shortcircuit) return mtbdd_false; + + /* Check terminal case */ + if (a == b) return mtbdd_true; + if (a == mtbdd_false) return mtbdd_false; + if (b == mtbdd_false) return mtbdd_false; + + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); + int la = mtbddnode_isleaf(na); + int lb = mtbddnode_isleaf(nb); + + if (la && lb) { + storm_rational_function_ptr fa = mtbdd_getstorm_rational_function_ptr(a); + storm_rational_function_ptr fb = mtbdd_getstorm_rational_function_ptr(b); + + return storm_rational_function_equal_modulo_precision(1, fa, fb, svalue) ? mtbdd_true : mtbdd_false; + } + + /* Maybe perform garbage collection */ + sylvan_gc_test(); + + /* Count operation */ + sylvan_stats_count(MTBDD_EQUAL_NORM_REL); + + /* Check cache */ + MTBDD result; + if (cache_get3(CACHE_MTBDD_EQUAL_NORM_REL_RF, a, b, svalue, &result)) { + sylvan_stats_count(MTBDD_EQUAL_NORM_REL_CACHED); + return result; + } + + /* Get top variable */ + uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); + uint32_t vb = lb ? 0xffffffff : mtbddnode_getvariable(nb); + uint32_t var = va < vb ? va : vb; + + /* Get cofactors */ + MTBDD alow, ahigh, blow, bhigh; + alow = va == var ? node_getlow(a, na) : a; + ahigh = va == var ? node_gethigh(a, na) : a; + blow = vb == var ? node_getlow(b, nb) : b; + bhigh = vb == var ? node_gethigh(b, nb) : b; + + SPAWN(sylvan_storm_rational_function_equal_norm_rel_d2, ahigh, bhigh, svalue, shortcircuit); + result = CALL(sylvan_storm_rational_function_equal_norm_rel_d2, alow, blow, svalue, shortcircuit); + if (result == mtbdd_false) *shortcircuit = 1; + if (result != SYNC(sylvan_storm_rational_function_equal_norm_rel_d2)) result = mtbdd_false; + if (result == mtbdd_false) *shortcircuit = 1; + + /* Store in cache */ + if (cache_put3(CACHE_MTBDD_EQUAL_NORM_REL_RF, a, b, svalue, result)) { + sylvan_stats_count(MTBDD_EQUAL_NORM_REL_CACHEDPUT); + } + + return result; +} + +TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_equal_norm_rel_d, MTBDD, a, MTBDD, b, storm_rational_function_ptr, d) +{ + /* the implementation checks shortcircuit in every task and if the two + MTBDDs are not equal module epsilon, then the computation tree quickly aborts */ + int shortcircuit = 0; + return CALL(sylvan_storm_rational_function_equal_norm_rel_d2, a, b, d, &shortcircuit); +} diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h index 259e10a1d..a47def0a1 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h @@ -85,6 +85,12 @@ TASK_DECL_2(MTBDD, sylvan_storm_rational_function_threshold, MTBDD, storm_ration 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) +TASK_DECL_3(MTBDD, sylvan_storm_rational_function_equal_norm_d, MTBDD, MTBDD, storm_rational_function_ptr); +#define sylvan_storm_rational_function_equal_norm_d(a, b, epsilon) CALL(sylvan_storm_rational_function_equal_norm_d, a, b, epsilon) + +TASK_DECL_3(MTBDD, sylvan_storm_rational_function_equal_norm_rel_d, MTBDD, MTBDD, storm_rational_function_ptr); +#define sylvan_storm_rational_function_equal_norm_rel_d(a, b, epsilon) CALL(sylvan_storm_rational_function_equal_norm_rel_d, a, b, epsilon) + #ifdef __cplusplus } #endif /* __cplusplus */ diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c index 55f14b4d4..ef48ccab3 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c @@ -44,7 +44,7 @@ static char* sylvan_storm_rational_number_to_str(int comp, uint64_t val, char* b } void sylvan_storm_rational_number_init() { - // Register custom leaf type storing rational functions. + // Register custom leaf type storing rational numbers. srn_type = sylvan_mt_create_type(); sylvan_mt_set_hash(srn_type, sylvan_storm_rational_number_hash); sylvan_mt_set_equals(srn_type, sylvan_storm_rational_number_equals); @@ -490,7 +490,7 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_number_and_exists, MTBDD, a, MTBDD, b, sylvan_gc_test(); /* Check cache. Note that we do this now, since the times operator might swap a and b (commutative) */ - if (cache_get3(CACHE_MTBDD_AND_EXISTS_RF, a, b, v, &result)) return result; + if (cache_get3(CACHE_MTBDD_AND_EXISTS_RN, a, b, v, &result)) return result; /* Now, v is not a constant, and either a or b is not a constant */ @@ -538,7 +538,7 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_number_and_exists, MTBDD, a, MTBDD, b, } /* Store in cache */ - cache_put3(CACHE_MTBDD_AND_EXISTS_RF, a, b, v, result); + cache_put3(CACHE_MTBDD_AND_EXISTS_RN, a, b, v, result); return result; } @@ -586,7 +586,7 @@ TASK_IMPL_1(MTBDD, sylvan_storm_rational_number_minimum, MTBDD, a) { /* Check cache */ MTBDD result; - if (cache_get3(CACHE_MTBDD_MINIMUM_RF, a, 0, 0, &result)) return result; + if (cache_get3(CACHE_MTBDD_MINIMUM_RN, a, 0, 0, &result)) return result; /* Call recursive */ SPAWN(mtbdd_minimum, node_getlow(a, na)); @@ -603,7 +603,7 @@ TASK_IMPL_1(MTBDD, sylvan_storm_rational_number_minimum, MTBDD, a) { } /* Store in cache */ - cache_put3(CACHE_MTBDD_MINIMUM_RF, a, 0, 0, result); + cache_put3(CACHE_MTBDD_MINIMUM_RN, a, 0, 0, result); return result; } @@ -619,7 +619,7 @@ TASK_IMPL_1(MTBDD, sylvan_storm_rational_number_maximum, MTBDD, a) /* Check cache */ MTBDD result; - if (cache_get3(CACHE_MTBDD_MAXIMUM_RF, a, 0, 0, &result)) return result; + if (cache_get3(CACHE_MTBDD_MAXIMUM_RN, a, 0, 0, &result)) return result; /* Call recursive */ SPAWN(mtbdd_minimum, node_getlow(a, na)); @@ -636,6 +636,155 @@ TASK_IMPL_1(MTBDD, sylvan_storm_rational_number_maximum, MTBDD, a) } /* Store in cache */ - cache_put3(CACHE_MTBDD_MAXIMUM_RF, a, 0, 0, result); + cache_put3(CACHE_MTBDD_MAXIMUM_RN, a, 0, 0, result); return result; } + +TASK_4(MTBDD, sylvan_storm_rational_number_equal_norm_d2, MTBDD, a, MTBDD, b, storm_rational_number_ptr, svalue, int*, shortcircuit) +{ + /* Check short circuit */ + if (*shortcircuit) return mtbdd_false; + + /* Check terminal case */ + if (a == b) return mtbdd_true; + if (a == mtbdd_false) return mtbdd_false; + if (b == mtbdd_false) return mtbdd_false; + + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); + int la = mtbddnode_isleaf(na); + int lb = mtbddnode_isleaf(nb); + + if (la && lb) { + storm_rational_number_ptr fa = mtbdd_getstorm_rational_number_ptr(a); + storm_rational_number_ptr fb = mtbdd_getstorm_rational_number_ptr(b); + + return storm_rational_number_equal_modulo_precision(0, fa, fb, svalue) ? mtbdd_true : mtbdd_false; + } + + if (b < a) { + MTBDD t = a; + a = b; + b = t; + } + + /* Maybe perform garbage collection */ + sylvan_gc_test(); + + /* Count operation */ + sylvan_stats_count(MTBDD_EQUAL_NORM); + + /* Check cache */ + MTBDD result; + if (cache_get3(CACHE_MTBDD_EQUAL_NORM_RN, a, b, svalue, &result)) { + sylvan_stats_count(MTBDD_EQUAL_NORM_CACHED); + return result; + } + + /* Get top variable */ + uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); + uint32_t vb = lb ? 0xffffffff : mtbddnode_getvariable(nb); + uint32_t var = va < vb ? va : vb; + + /* Get cofactors */ + MTBDD alow, ahigh, blow, bhigh; + alow = va == var ? node_getlow(a, na) : a; + ahigh = va == var ? node_gethigh(a, na) : a; + blow = vb == var ? node_getlow(b, nb) : b; + bhigh = vb == var ? node_gethigh(b, nb) : b; + + SPAWN(sylvan_storm_rational_number_equal_norm_d2, ahigh, bhigh, svalue, shortcircuit); + result = CALL(sylvan_storm_rational_number_equal_norm_d2, alow, blow, svalue, shortcircuit); + if (result == mtbdd_false) *shortcircuit = 1; + if (result != SYNC(sylvan_storm_rational_number_equal_norm_d2)) result = mtbdd_false; + if (result == mtbdd_false) *shortcircuit = 1; + + /* Store in cache */ + if (cache_put3(CACHE_MTBDD_EQUAL_NORM_RN, a, b, svalue, result)) { + sylvan_stats_count(MTBDD_EQUAL_NORM_CACHEDPUT); + } + + return result; +} + +TASK_IMPL_3(MTBDD, sylvan_storm_rational_number_equal_norm_d, MTBDD, a, MTBDD, b, storm_rational_number_ptr, d) +{ + /* the implementation checks shortcircuit in every task and if the two + MTBDDs are not equal module epsilon, then the computation tree quickly aborts */ + int shortcircuit = 0; + return CALL(sylvan_storm_rational_number_equal_norm_d2, a, b, d, &shortcircuit); +} + +/** + * Compare two Double MTBDDs, returns Boolean True if they are equal within some value epsilon + * This version computes the relative difference vs the value in a. + */ +TASK_4(MTBDD, sylvan_storm_rational_number_equal_norm_rel_d2, MTBDD, a, MTBDD, b, storm_rational_number_ptr, svalue, int*, shortcircuit) +{ + /* Check short circuit */ + if (*shortcircuit) return mtbdd_false; + + /* Check terminal case */ + if (a == b) return mtbdd_true; + if (a == mtbdd_false) return mtbdd_false; + if (b == mtbdd_false) return mtbdd_false; + + mtbddnode_t na = MTBDD_GETNODE(a); + mtbddnode_t nb = MTBDD_GETNODE(b); + int la = mtbddnode_isleaf(na); + int lb = mtbddnode_isleaf(nb); + + if (la && lb) { + storm_rational_number_ptr fa = mtbdd_getstorm_rational_number_ptr(a); + storm_rational_number_ptr fb = mtbdd_getstorm_rational_number_ptr(b); + + return storm_rational_number_equal_modulo_precision(1, fa, fb, svalue) ? mtbdd_true : mtbdd_false; + } + + /* Maybe perform garbage collection */ + sylvan_gc_test(); + + /* Count operation */ + sylvan_stats_count(MTBDD_EQUAL_NORM_REL); + + /* Check cache */ + MTBDD result; + if (cache_get3(CACHE_MTBDD_EQUAL_NORM_REL_RN, a, b, svalue, &result)) { + sylvan_stats_count(MTBDD_EQUAL_NORM_REL_CACHED); + return result; + } + + /* Get top variable */ + uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); + uint32_t vb = lb ? 0xffffffff : mtbddnode_getvariable(nb); + uint32_t var = va < vb ? va : vb; + + /* Get cofactors */ + MTBDD alow, ahigh, blow, bhigh; + alow = va == var ? node_getlow(a, na) : a; + ahigh = va == var ? node_gethigh(a, na) : a; + blow = vb == var ? node_getlow(b, nb) : b; + bhigh = vb == var ? node_gethigh(b, nb) : b; + + SPAWN(sylvan_storm_rational_number_equal_norm_rel_d2, ahigh, bhigh, svalue, shortcircuit); + result = CALL(sylvan_storm_rational_number_equal_norm_rel_d2, alow, blow, svalue, shortcircuit); + if (result == mtbdd_false) *shortcircuit = 1; + if (result != SYNC(sylvan_storm_rational_number_equal_norm_rel_d2)) result = mtbdd_false; + if (result == mtbdd_false) *shortcircuit = 1; + + /* Store in cache */ + if (cache_put3(CACHE_MTBDD_EQUAL_NORM_REL_RN, a, b, svalue, result)) { + sylvan_stats_count(MTBDD_EQUAL_NORM_REL_CACHEDPUT); + } + + return result; +} + +TASK_IMPL_3(MTBDD, sylvan_storm_rational_number_equal_norm_rel_d, MTBDD, a, MTBDD, b, storm_rational_number_ptr, d) +{ + /* the implementation checks shortcircuit in every task and if the two + MTBDDs are not equal module epsilon, then the computation tree quickly aborts */ + int shortcircuit = 0; + return CALL(sylvan_storm_rational_number_equal_norm_rel_d2, a, b, d, &shortcircuit); +} + diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h index 6a5cc155f..1425e1bfc 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h @@ -81,6 +81,12 @@ TASK_DECL_2(MTBDD, sylvan_storm_rational_number_threshold, MTBDD, storm_rational TASK_DECL_2(MTBDD, sylvan_storm_rational_number_strict_threshold, MTBDD, storm_rational_number_ptr); #define sylvan_storm_rational_number_strict_threshold(dd, value) CALL(sylvan_storm_rational_number_strict_threshold, dd, value) +TASK_DECL_3(MTBDD, sylvan_storm_rational_number_equal_norm_d, MTBDD, MTBDD, storm_rational_number_ptr); +#define sylvan_storm_rational_number_equal_norm_d(a, b, epsilon) CALL(sylvan_storm_rational_number_equal_norm_d, a, b, epsilon) + +TASK_DECL_3(MTBDD, sylvan_storm_rational_number_equal_norm_rel_d, MTBDD, MTBDD, storm_rational_number_ptr); +#define sylvan_storm_rational_number_equal_norm_rel_d(a, b, epsilon) CALL(sylvan_storm_rational_number_equal_norm_rel_d, a, b, epsilon) + #ifdef __cplusplus } #endif /* __cplusplus */ diff --git a/src/storm/adapters/AddExpressionAdapter.cpp b/src/storm/adapters/AddExpressionAdapter.cpp index db60c7050..4ec8470e8 100644 --- a/src/storm/adapters/AddExpressionAdapter.cpp +++ b/src/storm/adapters/AddExpressionAdapter.cpp @@ -11,6 +11,8 @@ #include "storm-config.h" #include "storm/adapters/CarlAdapter.h" +#include "storm/utility/constants.h" + namespace storm { namespace adapters { @@ -203,12 +205,12 @@ namespace storm { template boost::any AddExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) { - return ddManager->getConstant(static_cast(expression.getValue())); + return ddManager->getConstant(storm::utility::convertNumber(expression.getValue())); } template boost::any AddExpressionAdapter::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) { - return ddManager->getConstant(static_cast(expression.getValueAsDouble())); + return ddManager->getConstant(storm::utility::convertNumber(expression.getValue())); } // Explicitly instantiate the symbolic expression adapter @@ -216,6 +218,7 @@ namespace storm { template class AddExpressionAdapter; #ifdef STORM_HAVE_CARL + template class AddExpressionAdapter; template class AddExpressionAdapter; #endif } // namespace adapters diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index ff59ec735..4b7a486bb 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -1928,6 +1928,7 @@ namespace storm { template class DdJaniModelBuilder; template class DdJaniModelBuilder; + template class DdJaniModelBuilder; template class DdJaniModelBuilder; } } diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index f8bc384c3..d5358c10f 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -1377,7 +1377,7 @@ namespace storm { // Cut the transitions and rewards to the reachable fragment of the state space. storm::dd::Bdd initialStates = createInitialStatesDecisionDiagram(generationInfo); - + storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); if (program.getModelType() == storm::prism::Program::ModelType::MDP) { transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables); @@ -1490,6 +1490,7 @@ namespace storm { template class DdPrismModelBuilder; template class DdPrismModelBuilder; + template class DdPrismModelBuilder; template class DdPrismModelBuilder; } // namespace adapters diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index beb085081..9d1052ca1 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -370,8 +370,16 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector const& formulas, bool onlyInitialStatesRelevant) { - STORM_LOG_THROW(storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); - buildAndCheckSymbolicModelWithSparseEngine(model, formulas, onlyInitialStatesRelevant); + auto engine = storm::settings::getModule().getEngine(); + if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { + 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 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."); + } } template<> diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index b3061db61..e15db2629 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -205,7 +205,7 @@ namespace storm { } } } - + // Get all choices for the state. result.setExpanded(); std::vector> allChoices = getUnlabeledChoices(*this->state, stateToIdCallback); @@ -439,7 +439,7 @@ namespace storm { template std::vector> PrismNextStateGenerator::getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) { std::vector> result; - + for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) { boost::optional>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(actionIndex); @@ -467,9 +467,9 @@ namespace storm { storm::prism::Update const& update = command.getUpdate(j); for (auto const& stateProbabilityPair : *currentTargetStates) { - auto probability = stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression()); - - if (probability != storm::utility::zero()) { + ValueType probability = stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression()); + + if (!storm::utility::isZero(probability)) { // Compute the new state under the current update and add it to the set of new target states. CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, update); diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 3f3729975..675adbaf4 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -316,12 +316,15 @@ 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>; template class AbstractModelChecker>; + template class AbstractModelChecker>; template class AbstractModelChecker>; } } diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index fc221147b..18deaedc1 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -26,12 +26,25 @@ namespace storm { // Intentionally left empty. } - template + template bool HybridCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { + return HybridCtmcCslModelChecker::canHandleImplementation(checkTask); + } + + template + template::SupportsExponential, int>::type> + bool HybridCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true)); } - + + template + template::SupportsExponential, int>::type> + bool HybridCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { + storm::logic::Formula const& formula = checkTask.getFormula(); + return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true)); + } + template std::unique_ptr HybridCtmcCslModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); @@ -40,7 +53,7 @@ namespace storm { SymbolicQualitativeCheckResult const& leftResult = leftResultPointer->asSymbolicQualitativeCheckResult(); SymbolicQualitativeCheckResult const& rightResult = rightResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *this->linearEquationSolverFactory); } template @@ -49,7 +62,7 @@ namespace storm { std::unique_ptr subResultPointer = this->check(pathFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector()); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeNextProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector()); } @@ -59,7 +72,7 @@ namespace storm { std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeReachabilityRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); } template @@ -82,7 +95,7 @@ namespace storm { upperBound = storm::utility::infinity(); } - return storm::modelchecker::helper::HybridCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), lowerBound, upperBound, *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeBoundedUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), lowerBound, upperBound, *linearEquationSolverFactory); } template @@ -90,7 +103,7 @@ namespace storm { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(!rewardPathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeInstantaneousRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); } template @@ -98,7 +111,7 @@ namespace storm { storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula(); STORM_LOG_THROW(!rewardPathFormula.isStepBounded(), storm::exceptions::NotImplementedException, "Currently step-bounded properties on CTMCs are not supported."); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeCumulativeRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getBound(), *linearEquationSolverFactory); } template @@ -107,17 +120,19 @@ namespace storm { std::unique_ptr subResultPointer = this->check(stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), *linearEquationSolverFactory); } template std::unique_ptr HybridCtmcCslModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { - return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), *linearEquationSolverFactory); + return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), *linearEquationSolverFactory); } // Explicitly instantiate the model checker. template class HybridCtmcCslModelChecker>; template class HybridCtmcCslModelChecker>; - + + template class HybridCtmcCslModelChecker>; + } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h index 202456f5b..4bb297c51 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h @@ -7,6 +7,8 @@ #include "storm/solver/LinearEquationSolver.h" +#include "storm/utility/NumberTraits.h" + namespace storm { namespace modelchecker { @@ -32,6 +34,12 @@ namespace storm { virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; private: + template::SupportsExponential, int>::type = 0> + bool canHandleImplementation(CheckTask const& checkTask) const; + + template::SupportsExponential, int>::type = 0> + bool canHandleImplementation(CheckTask const& checkTask) const; + // An object that is used for solving linear equations and performing matrix-vector multiplication. std::unique_ptr> linearEquationSolverFactory; }; diff --git a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index 592ecc460..cb046cfb1 100644 --- a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -20,29 +20,30 @@ #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/InvalidOperationException.h" namespace storm { namespace modelchecker { namespace helper { template - std::unique_ptr HybridCtmcCslHelper::computeReachabilityRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeReachabilityRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return HybridDtmcPrctlHelper::computeReachabilityRewards(model, computeProbabilityMatrix(rateMatrix, exitRateVector), rewardModel.divideStateRewardVector(exitRateVector), targetStates, qualitative, linearEquationSolverFactory); } template - std::unique_ptr HybridCtmcCslHelper::computeNextProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates) { + std::unique_ptr HybridCtmcCslHelper::computeNextProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates) { return HybridDtmcPrctlHelper::computeNextProbabilities(model, computeProbabilityMatrix(rateMatrix, exitRateVector), nextStates); } template - std::unique_ptr HybridCtmcCslHelper::computeUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { return HybridDtmcPrctlHelper::computeUntilProbabilities(model, computeProbabilityMatrix(rateMatrix, exitRateVector), phiStates, psiStates, qualitative, linearEquationSolverFactory); } - template - std::unique_ptr HybridCtmcCslHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + template::SupportsExponential, int>::type> + std::unique_ptr HybridCtmcCslHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // If the time bounds are [0, inf], we rather call untimed reachability. if (storm::utility::isZero(lowerBound) && upperBound == storm::utility::infinity()) { @@ -217,8 +218,13 @@ namespace storm { } } - template - std::unique_ptr HybridCtmcCslHelper::computeInstantaneousRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + template::SupportsExponential, int>::type> + std::unique_ptr HybridCtmcCslHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded until probabilities is unsupported for this value type."); + } + + template::SupportsExponential, int>::type> + std::unique_ptr HybridCtmcCslHelper::computeInstantaneousRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has a state-based reward model. STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -240,17 +246,22 @@ namespace storm { result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, result, linearEquationSolverFactory); } - return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, result)); + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), odd, result)); } - template - std::unique_ptr HybridCtmcCslHelper::computeCumulativeRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + template::SupportsExponential, int>::type> + std::unique_ptr HybridCtmcCslHelper::computeInstantaneousRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing instantaneous rewards is unsupported for this value type."); + } + + template::SupportsExponential, int>::type> + std::unique_ptr HybridCtmcCslHelper::computeCumulativeRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has a state-based reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); // If the time bound is zero, the result is the constant zero vector. if (timeBound == 0) { - return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), model.getManager().template getAddZero())); + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), model.getManager().template getAddZero())); } // Otherwise, we need to perform some computations. @@ -272,11 +283,16 @@ namespace storm { // Finally, compute the transient probabilities. std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, explicitTotalRewardVector, 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::SupportsExponential, int>::type> + std::unique_ptr HybridCtmcCslHelper::computeCumulativeRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing cumulative rewards is unsupported for this value type."); } template - std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { storm::dd::Add probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); // Create ODD for the translation. @@ -287,11 +303,11 @@ namespace storm { std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, psiStates.toVector(odd), &explicitExitRateVector, 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 - std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); storm::dd::Add probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); @@ -304,11 +320,11 @@ namespace storm { std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, model.getColumnVariables(), exitRateVector, true).toVector(odd), &explicitExitRateVector, 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 - storm::dd::Add HybridCtmcCslHelper::computeUniformizedMatrix(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, ValueType uniformizationRate) { + storm::dd::Add HybridCtmcCslHelper::computeUniformizedMatrix(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, ValueType uniformizationRate) { STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << "."); STORM_LOG_DEBUG("Keeping " << maybeStates.getNonZeroCount() << " rows."); @@ -326,13 +342,60 @@ namespace storm { } template - storm::dd::Add HybridCtmcCslHelper::computeProbabilityMatrix(storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector) { + storm::dd::Add HybridCtmcCslHelper::computeProbabilityMatrix(storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector) { return rateMatrix / exitRateVector; } - template class HybridCtmcCslHelper; - template class HybridCtmcCslHelper; + // Explicit instantiations. + // Cudd, double. + template std::unique_ptr HybridCtmcCslHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeInstantaneousRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeCumulativeRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeReachabilityRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeNextProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates); + template std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template storm::dd::Add HybridCtmcCslHelper::computeProbabilityMatrix(storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector); + template storm::dd::Add HybridCtmcCslHelper::computeUniformizedMatrix(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, double uniformizationRate); + + // Sylvan, double. + template std::unique_ptr HybridCtmcCslHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeInstantaneousRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeCumulativeRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeReachabilityRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeNextProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates); + template std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template storm::dd::Add HybridCtmcCslHelper::computeProbabilityMatrix(storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector); + template storm::dd::Add HybridCtmcCslHelper::computeUniformizedMatrix(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, double uniformizationRate); + + // Sylvan, rational number. + template std::unique_ptr HybridCtmcCslHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeInstantaneousRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeCumulativeRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeReachabilityRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeNextProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates); + template std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template storm::dd::Add HybridCtmcCslHelper::computeProbabilityMatrix(storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector); + template storm::dd::Add HybridCtmcCslHelper::computeUniformizedMatrix(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, storm::RationalNumber uniformizationRate); + + // Sylvan, rational function. + template std::unique_ptr HybridCtmcCslHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeInstantaneousRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeCumulativeRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeReachabilityRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::unique_ptr HybridCtmcCslHelper::computeNextProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates); + template std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template storm::dd::Add HybridCtmcCslHelper::computeProbabilityMatrix(storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector); + template storm::dd::Add HybridCtmcCslHelper::computeUniformizedMatrix(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, storm::RationalFunction uniformizationRate); + } } } diff --git a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h index 62eef6264..352abe14c 100644 --- a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h +++ b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h @@ -9,30 +9,46 @@ #include "storm/solver/LinearEquationSolver.h" +#include "storm/utility/NumberTraits.h" + namespace storm { namespace modelchecker { namespace helper { - template class HybridCtmcCslHelper { - public: - typedef typename storm::models::symbolic::Model::RewardModelType RewardModelType; + public: + template::SupportsExponential, int>::type = 0> + static std::unique_ptr computeBoundedUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template::SupportsExponential, int>::type = 0> static std::unique_ptr computeBoundedUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - - static std::unique_ptr computeInstantaneousRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - - static std::unique_ptr computeCumulativeRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - + + template::SupportsExponential, int>::type = 0> + static std::unique_ptr computeInstantaneousRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template::SupportsExponential, int>::type = 0> + static std::unique_ptr computeInstantaneousRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template::SupportsExponential, int>::type = 0> + static std::unique_ptr computeCumulativeRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template::SupportsExponential, int>::type = 0> + static std::unique_ptr computeCumulativeRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template static std::unique_ptr computeUntilProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::unique_ptr computeReachabilityRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template + static std::unique_ptr computeReachabilityRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template static std::unique_ptr computeLongRunAverageProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& psiStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template static std::unique_ptr computeNextProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates); - static std::unique_ptr computeLongRunAverageRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template + static std::unique_ptr computeLongRunAverageRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, typename storm::models::symbolic::Model::RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); /*! * Converts the given rate-matrix into a time-abstract probability matrix. @@ -42,6 +58,7 @@ namespace storm { * @param exitRateVector The exit rate vector of the model. * @return The probability matrix. */ + template static storm::dd::Add computeProbabilityMatrix(storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector); /*! @@ -53,6 +70,7 @@ namespace storm { * @param uniformizationRate The rate to be used for uniformization. * @return The uniformized matrix. */ + template static storm::dd::Add computeUniformizedMatrix(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, ValueType uniformizationRate); }; diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index a9bba9eaf..facf38fbe 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -119,6 +119,7 @@ namespace storm { template class HybridDtmcPrctlModelChecker>; template class HybridDtmcPrctlModelChecker>; + template class HybridDtmcPrctlModelChecker>; template class HybridDtmcPrctlModelChecker>; } } diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index d42de45dd..c773609af 100644 --- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -149,5 +149,8 @@ namespace storm { template class HybridMdpPrctlModelChecker>; template class HybridMdpPrctlModelChecker>; + + template class HybridMdpPrctlModelChecker>; + } } diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 4dbfb6d1d..9922c77d1 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -23,12 +23,12 @@ namespace storm { namespace modelchecker { template - SymbolicDtmcPrctlModelChecker::SymbolicDtmcPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { + SymbolicDtmcPrctlModelChecker::SymbolicDtmcPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::move(linearEquationSolverFactory)) { // Intentionally left empty. } template - SymbolicDtmcPrctlModelChecker::SymbolicDtmcPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { + SymbolicDtmcPrctlModelChecker::SymbolicDtmcPrctlModelChecker(ModelType const& model) : SymbolicPropositionalModelChecker(model), linearEquationSolverFactory(std::make_unique>()) { // Intentionally left empty. } @@ -109,6 +109,7 @@ namespace storm { template class SymbolicDtmcPrctlModelChecker>; template class SymbolicDtmcPrctlModelChecker>; + template class SymbolicDtmcPrctlModelChecker>; template class SymbolicDtmcPrctlModelChecker>; } } diff --git a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h index dceaa3e0b..dab6da4ad 100644 --- a/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h @@ -3,7 +3,8 @@ #include "storm/modelchecker/propositional/SymbolicPropositionalModelChecker.h" #include "storm/models/symbolic/Dtmc.h" -#include "storm/utility/solver.h" + +#include "storm/solver/SymbolicLinearEquationSolver.h" namespace storm { namespace modelchecker { @@ -14,7 +15,7 @@ namespace storm { static const storm::dd::DdType DdType = ModelType::DdType; explicit SymbolicDtmcPrctlModelChecker(ModelType const& model); - explicit SymbolicDtmcPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); + explicit SymbolicDtmcPrctlModelChecker(ModelType const& model, std::unique_ptr>&& linearEquationSolverFactory); // The implemented methods of the AbstractModelChecker interface. virtual bool canHandle(CheckTask const& checkTask) const override; @@ -28,7 +29,7 @@ namespace storm { private: // An object that is used for retrieving linear equation solvers. - std::unique_ptr> linearEquationSolverFactory; + std::unique_ptr> linearEquationSolverFactory; }; } // namespace modelchecker diff --git a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp index 2ac26509a..cf88dd848 100644 --- a/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp @@ -106,5 +106,7 @@ namespace storm { template class SymbolicMdpPrctlModelChecker>; template class SymbolicMdpPrctlModelChecker>; + + template class SymbolicMdpPrctlModelChecker>; } } diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index dd12b76e6..81cdce1f8 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -71,7 +71,7 @@ namespace storm { // Translate the symbolic matrix/vector to their explicit representations and solve the equation system. storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(odd, odd); std::vector b = subvector.toVector(odd); - + std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitSubmatrix)); solver->setBounds(storm::utility::zero(), storm::utility::one()); solver->solveEquations(x, b); @@ -272,6 +272,7 @@ namespace storm { template class HybridDtmcPrctlHelper; template class HybridDtmcPrctlHelper; + template class HybridDtmcPrctlHelper; template class HybridDtmcPrctlHelper; } } diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 1caae1606..81db71dfd 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -44,7 +44,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().getConstant(storm::utility::convertNumber(0.5)))); } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { @@ -81,9 +81,9 @@ namespace storm { solver->solveEquations(dir, x, explicitRepresentation.second); // 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())); } } } @@ -145,9 +145,9 @@ namespace storm { solver->repeatedMultiply(dir, x, &explicitRepresentation.second, 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())); } } @@ -170,7 +170,7 @@ namespace storm { solver->repeatedMultiply(dir, 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 @@ -199,7 +199,7 @@ namespace storm { solver->repeatedMultiply(dir, x, &explicitRepresentation.second, 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 @@ -227,7 +227,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().getConstant(storm::utility::one()))); + 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().getConstant(storm::utility::one()))); } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { @@ -272,15 +272,18 @@ namespace storm { solver->solveEquations(dir, x, explicitRepresentation.second); // 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()))); } } } template class HybridMdpPrctlHelper; template class HybridMdpPrctlHelper; + + template class HybridMdpPrctlHelper; + } } } diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index f768a2428..195dbc488 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -55,7 +55,7 @@ namespace storm { std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); - + // Perform some logging. storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); STORM_LOG_INFO("Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index 7f0618048..b57f6aa3b 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -19,7 +19,7 @@ namespace storm { namespace helper { template - storm::dd::Add SymbolicDtmcPrctlHelper::computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { + storm::dd::Add SymbolicDtmcPrctlHelper::computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 and 1 of satisfying the until-formula. std::pair, storm::dd::Bdd> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates); @@ -68,7 +68,7 @@ namespace storm { } template - storm::dd::Add SymbolicDtmcPrctlHelper::computeGloballyProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { + storm::dd::Add SymbolicDtmcPrctlHelper::computeGloballyProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { storm::dd::Add result = computeUntilProbabilities(model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory); result = result.getDdManager().template getAddOne() - result; return result; @@ -81,7 +81,7 @@ namespace storm { } template - storm::dd::Add SymbolicDtmcPrctlHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { + storm::dd::Add SymbolicDtmcPrctlHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 or 1 of satisfying the until-formula. storm::dd::Bdd statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(model, transitionMatrix.notZero(), phiStates, psiStates, stepBound); @@ -115,7 +115,7 @@ namespace storm { } template - storm::dd::Add SymbolicDtmcPrctlHelper::computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { + storm::dd::Add SymbolicDtmcPrctlHelper::computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -128,7 +128,7 @@ namespace storm { } template - storm::dd::Add SymbolicDtmcPrctlHelper::computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { + storm::dd::Add SymbolicDtmcPrctlHelper::computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if the model has at least one reward this->getModel(). STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -138,7 +138,7 @@ namespace storm { } template - storm::dd::Add SymbolicDtmcPrctlHelper::computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { + storm::dd::Add SymbolicDtmcPrctlHelper::computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { // Only compute the result if there is at least one reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); @@ -187,6 +187,7 @@ namespace storm { template class SymbolicDtmcPrctlHelper; template class SymbolicDtmcPrctlHelper; + template class SymbolicDtmcPrctlHelper; template class SymbolicDtmcPrctlHelper; } } diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h index 0e6bb7657..58b32b0dc 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h @@ -6,7 +6,7 @@ #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" -#include "storm/utility/solver.h" +#include "storm/solver/SymbolicLinearEquationSolver.h" namespace storm { namespace modelchecker { @@ -17,19 +17,19 @@ namespace storm { public: typedef typename storm::models::symbolic::Model::RewardModelType RewardModelType; - static storm::dd::Add computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); + static storm::dd::Add computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, uint_fast64_t stepBound, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); static storm::dd::Add computeNextProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& nextStates); - static storm::dd::Add computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); + static storm::dd::Add computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); - static storm::dd::Add computeGloballyProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); + static storm::dd::Add computeGloballyProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); - static storm::dd::Add computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); + static storm::dd::Add computeCumulativeRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); - static storm::dd::Add computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); + static storm::dd::Add computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); - static storm::dd::Add computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); + static storm::dd::Add computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory); }; } diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp index 95277500b..c2d86f663 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp @@ -43,7 +43,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().getConstant(storm::utility::convertNumber(0.5)))); } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { @@ -68,9 +68,9 @@ namespace storm { std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); storm::dd::Add result = solver->solveEquations(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), subvector); - return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), statesWithProbability01.second.template toAdd() + result)); + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), statesWithProbability01.second.template toAdd() + result)); } 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())); } } } @@ -90,7 +90,7 @@ namespace storm { } else { result = result.maxAbstract(model.getNondeterminismVariables()); } - return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result)); + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result)); } template @@ -125,9 +125,9 @@ namespace storm { std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); storm::dd::Add result = solver->multiply(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), &subvector, stepBound); - return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.template toAdd() + result)); + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.template toAdd() + result)); } 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())); } } @@ -140,7 +140,7 @@ namespace storm { std::unique_ptr> solver = linearEquationSolverFactory.create(transitionMatrix, model.getReachableStates(), model.getIllegalMask(), model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); storm::dd::Add result = solver->multiply(dir == OptimizationDirection::Minimize, rewardModel.getStateRewardVector(), nullptr, stepBound); - return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result)); + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result)); } template @@ -155,7 +155,7 @@ namespace storm { std::unique_ptr> solver = linearEquationSolverFactory.create(model.getTransitionMatrix(), model.getReachableStates(), model.getIllegalMask(), model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); storm::dd::Add result = solver->multiply(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), &totalRewardVector, stepBound); - return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result)); + return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), result)); } template @@ -184,7 +184,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().getConstant(storm::utility::one()))); + 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().getConstant(storm::utility::one()))); } else { // If there are maybe states, we need to solve an equation system. if (!maybeStates.isZero()) { @@ -210,15 +210,17 @@ namespace storm { std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs()); storm::dd::Add result = solver->solveEquations(dir == OptimizationDirection::Minimize, model.getManager().template getAddZero(), subvector); - return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), result))); + return std::unique_ptr(new storm::modelchecker::SymbolicQuantitativeCheckResult(model.getReachableStates(), infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), result))); } 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()))); } } } template class SymbolicMdpPrctlHelper; template class SymbolicMdpPrctlHelper; + + template class SymbolicMdpPrctlHelper; } } } diff --git a/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp index 2b668cde6..d7e93d372 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>; 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 d5ada4794..324d8d1d6 100644 --- a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -90,17 +90,66 @@ namespace storm { return explicitValues; } + template + void print(std::ostream& out, ValueType const& value) { + if (value == storm::utility::infinity()) { + out << "inf"; + } else { + out << value; + if (std::is_same::value) { + out << " (approx. " << storm::utility::convertNumber(value) << ")"; + } + } + } + + template + void printRange(std::ostream& out, ValueType const& min, ValueType const& max) { + out << "["; + if (min == storm::utility::infinity()) { + out << "inf"; + } else { + out << min; + } + out << ", "; + if (max == storm::utility::infinity()) { + out << "inf"; + } else { + out << max; + } + out << "]"; + if (std::is_same::value) { + out << " (approx. ["; + if (min == storm::utility::infinity()) { + out << "inf"; + } else { + out << storm::utility::convertNumber(min); + } + out << ", "; + if (max == storm::utility::infinity()) { + out << "inf"; + } else { + out << storm::utility::convertNumber(max); + } + out << "])"; + } + out << " (range)"; + } + template std::ostream& HybridQuantitativeCheckResult::writeToStream(std::ostream& out) const { uint64_t totalNumberOfStates = this->symbolicStates.getNonZeroCount() + this->explicitStates.getNonZeroCount(); - + bool minMaxSupported = std::is_same::value || std::is_same::value; + bool printAsRange = false; + if (totalNumberOfStates == 1) { if (this->symbolicStates.isZero()) { - out << *this->explicitValues.begin(); + print(out, *this->explicitValues.begin()); } else { - out << this->symbolicValues.sumAbstract(this->symbolicValues.getContainedMetaVariables()).getValue(); + print(out, this->symbolicValues.sumAbstract(this->symbolicValues.getContainedMetaVariables()).getValue()); } - } else if (totalNumberOfStates < 10 || std::is_same::value) { + } else if (totalNumberOfStates >= 10 && minMaxSupported) { + printAsRange = true; + } else { out << "{"; bool first = true; if (!this->symbolicStates.isZero()) { @@ -114,7 +163,7 @@ namespace storm { } else { first = false; } - out << valuationValuePair.second; + print(out, valuationValuePair.second); } if (symbolicStates.getNonZeroCount() != this->symbolicValues.getNonZeroCount()) { out << ", 0"; @@ -128,15 +177,16 @@ namespace storm { } else { first = false; } - out << element; + print(out, element); } } out << "}"; - } else { + } + + if (printAsRange) { ValueType min = this->getMin(); ValueType max = this->getMax(); - - out << "[" << min << ", " << max << "] (range)"; + printRange(out, min, max); } return out; } @@ -197,7 +247,7 @@ namespace storm { template ValueType HybridQuantitativeCheckResult::average() const { - return this->sum() / (symbolicStates || explicitStates).getNonZeroCount(); + return this->sum() / storm::utility::convertNumber((symbolicStates || explicitStates).getNonZeroCount()); } template @@ -216,6 +266,7 @@ namespace storm { template class HybridQuantitativeCheckResult; template class HybridQuantitativeCheckResult; + template class HybridQuantitativeCheckResult; template class HybridQuantitativeCheckResult; } } diff --git a/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp index 868116adf..37c8e3678 100644 --- a/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp @@ -53,5 +53,7 @@ namespace storm { template class SymbolicParetoCurveCheckResult; template class SymbolicParetoCurveCheckResult; + + template class SymbolicParetoCurveCheckResult; } } diff --git a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index cc81da3cd..87e8ff5d3 100644 --- a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -110,7 +110,7 @@ namespace storm { template ValueType SymbolicQuantitativeCheckResult::average() const { - return this->sum() / this->states.getNonZeroCount(); + return this->sum() / storm::utility::convertNumber(this->states.getNonZeroCount()); } template @@ -128,6 +128,7 @@ namespace storm { template class SymbolicQuantitativeCheckResult; template class SymbolicQuantitativeCheckResult; + template class SymbolicQuantitativeCheckResult; template class SymbolicQuantitativeCheckResult; } } diff --git a/src/storm/models/symbolic/Ctmc.cpp b/src/storm/models/symbolic/Ctmc.cpp index 9b8ceea68..543bc7d90 100644 --- a/src/storm/models/symbolic/Ctmc.cpp +++ b/src/storm/models/symbolic/Ctmc.cpp @@ -59,6 +59,7 @@ namespace storm { template class Ctmc; template class Ctmc; + template class Ctmc; template class Ctmc; } // namespace symbolic diff --git a/src/storm/models/symbolic/DeterministicModel.cpp b/src/storm/models/symbolic/DeterministicModel.cpp index 23dd73d90..a9d9c92df 100644 --- a/src/storm/models/symbolic/DeterministicModel.cpp +++ b/src/storm/models/symbolic/DeterministicModel.cpp @@ -34,6 +34,7 @@ namespace storm { template class DeterministicModel; template class DeterministicModel; + template class DeterministicModel; template class DeterministicModel; } // namespace symbolic diff --git a/src/storm/models/symbolic/Dtmc.cpp b/src/storm/models/symbolic/Dtmc.cpp index 584074481..3f7153ead 100644 --- a/src/storm/models/symbolic/Dtmc.cpp +++ b/src/storm/models/symbolic/Dtmc.cpp @@ -33,6 +33,7 @@ namespace storm { template class Dtmc; template class Dtmc; + template class Dtmc; template class Dtmc; } // namespace symbolic diff --git a/src/storm/models/symbolic/Mdp.cpp b/src/storm/models/symbolic/Mdp.cpp index a8260eb1b..20bd9ad2c 100644 --- a/src/storm/models/symbolic/Mdp.cpp +++ b/src/storm/models/symbolic/Mdp.cpp @@ -34,6 +34,7 @@ namespace storm { template class Mdp; template class Mdp; + template class Mdp; template class Mdp; } // namespace symbolic diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index fb61b4575..447867ea8 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -272,6 +272,7 @@ namespace storm { template class Model; template class Model; + template class Model; template class Model; } // namespace symbolic } // namespace models diff --git a/src/storm/models/symbolic/NondeterministicModel.cpp b/src/storm/models/symbolic/NondeterministicModel.cpp index dc6ffc07c..eb8c1a73d 100644 --- a/src/storm/models/symbolic/NondeterministicModel.cpp +++ b/src/storm/models/symbolic/NondeterministicModel.cpp @@ -79,7 +79,9 @@ namespace storm { // Explicitly instantiate the template class. template class NondeterministicModel; template class NondeterministicModel; + #ifdef STORM_HAVE_CARL + template class NondeterministicModel; template class NondeterministicModel; #endif } // namespace symbolic diff --git a/src/storm/models/symbolic/StandardRewardModel.cpp b/src/storm/models/symbolic/StandardRewardModel.cpp index 88d9fc3e0..1507b6dfc 100644 --- a/src/storm/models/symbolic/StandardRewardModel.cpp +++ b/src/storm/models/symbolic/StandardRewardModel.cpp @@ -160,6 +160,7 @@ namespace storm { template class StandardRewardModel; template class StandardRewardModel; + template class StandardRewardModel; template class StandardRewardModel; } diff --git a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp index 1f87a1ea3..0b515451a 100644 --- a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp @@ -15,11 +15,6 @@ namespace storm { // Intentionally left empty. } - template - SymbolicEliminationLinearEquationSolver::SymbolicEliminationLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : SymbolicLinearEquationSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, precision, maximalNumberOfIterations, relative) { - // Intentionally left empty. - } - template storm::dd::Add SymbolicEliminationLinearEquationSolver::solveEquations(storm::dd::Add const& x, storm::dd::Add const& b) const { storm::dd::DdManager& ddManager = x.getDdManager(); @@ -112,10 +107,30 @@ namespace storm { return solution.swapVariables(rowRowMetaVariablePairs); } + template + std::unique_ptr> SymbolicEliminationLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { + return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + } + + template + SymbolicEliminationLinearEquationSolverSettings& SymbolicEliminationLinearEquationSolverFactory::getSettings() { + return settings; + } + + template + SymbolicEliminationLinearEquationSolverSettings const& SymbolicEliminationLinearEquationSolverFactory::getSettings() const { + return settings; + } + template class SymbolicEliminationLinearEquationSolver; template class SymbolicEliminationLinearEquationSolver; - + template class SymbolicEliminationLinearEquationSolver; template class SymbolicEliminationLinearEquationSolver; + template class SymbolicEliminationLinearEquationSolverFactory; + template class SymbolicEliminationLinearEquationSolverFactory; + template class SymbolicEliminationLinearEquationSolverFactory; + template class SymbolicEliminationLinearEquationSolverFactory; + } } diff --git a/src/storm/solver/SymbolicEliminationLinearEquationSolver.h b/src/storm/solver/SymbolicEliminationLinearEquationSolver.h index cd7cd7ecf..0d96a3cd6 100644 --- a/src/storm/solver/SymbolicEliminationLinearEquationSolver.h +++ b/src/storm/solver/SymbolicEliminationLinearEquationSolver.h @@ -5,14 +5,30 @@ namespace storm { namespace solver { + template + class SymbolicEliminationLinearEquationSolverSettings { + public: + // Intentionally left empty. + }; + template class SymbolicEliminationLinearEquationSolver : public SymbolicLinearEquationSolver { public: SymbolicEliminationLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs); + + virtual storm::dd::Add solveEquations(storm::dd::Add const& x, storm::dd::Add const& b) const override; + }; + + template + class SymbolicEliminationLinearEquationSolverFactory { + 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; - SymbolicEliminationLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative); + SymbolicEliminationLinearEquationSolverSettings& getSettings(); + SymbolicEliminationLinearEquationSolverSettings const& getSettings() const; - virtual storm::dd::Add solveEquations(storm::dd::Add const& x, storm::dd::Add const& b) const override; + private: + SymbolicEliminationLinearEquationSolverSettings settings; }; } diff --git a/src/storm/solver/SymbolicLinearEquationSolver.cpp b/src/storm/solver/SymbolicLinearEquationSolver.cpp index 2d0895838..e5afcb08a 100644 --- a/src/storm/solver/SymbolicLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicLinearEquationSolver.cpp @@ -5,28 +5,23 @@ #include "storm/utility/dd.h" +#include "storm/solver/SymbolicEliminationLinearEquationSolver.h" +#include "storm/solver/SymbolicNativeLinearEquationSolver.h" +#include "storm/solver/SolverSelectionOptions.h" + #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/NativeEquationSolverSettings.h" +#include "storm/settings/modules/CoreSettings.h" + +#include "storm/utility/macros.h" #include "storm/adapters/CarlAdapter.h" namespace storm { namespace solver { - - template - SymbolicLinearEquationSolver::SymbolicLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : A(A), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) { - // Intentionally left empty. - } - + template SymbolicLinearEquationSolver::SymbolicLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) : A(A), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs) { - // Get the settings object to customize solving. - storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::getModule(); - - // Get appropriate settings. - maximalNumberOfIterations = settings.getMaximalIterationCount(); - precision = settings.getPrecision(); - relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; + // Intentionally left empty. } template @@ -45,10 +40,50 @@ namespace storm { return xCopy; } + + template + std::unique_ptr> GeneralSymbolicLinearEquationSolverFactory::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; + 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 engine. Falling back to native solver."); + return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs); + } + } + + + template + std::unique_ptr> GeneralSymbolicLinearEquationSolverFactory::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 class SymbolicLinearEquationSolver; template class SymbolicLinearEquationSolver; + template class SymbolicLinearEquationSolver; template class SymbolicLinearEquationSolver; + template class SymbolicLinearEquationSolverFactory; + template class SymbolicLinearEquationSolverFactory; + template class SymbolicLinearEquationSolverFactory; + template class SymbolicLinearEquationSolverFactory; + + template class GeneralSymbolicLinearEquationSolverFactory; + template class GeneralSymbolicLinearEquationSolverFactory; + template class GeneralSymbolicLinearEquationSolverFactory; + template class GeneralSymbolicLinearEquationSolverFactory; + } } diff --git a/src/storm/solver/SymbolicLinearEquationSolver.h b/src/storm/solver/SymbolicLinearEquationSolver.h index 25195c446..dddc80596 100644 --- a/src/storm/solver/SymbolicLinearEquationSolver.h +++ b/src/storm/solver/SymbolicLinearEquationSolver.h @@ -7,6 +7,8 @@ #include "storm/storage/expressions/Variable.h" #include "storm/storage/dd/DdType.h" +#include "storm/adapters/CarlAdapter.h" + namespace storm { namespace dd { template @@ -18,6 +20,13 @@ namespace storm { } namespace solver { + + template + class SymbolicLinearEquationSolverSettings { + public: + // Currently empty. + }; + /*! * An interface that represents an abstract symbolic linear equation solver. In addition to solving a system of * linear equations, the functionality to repeatedly multiply a matrix with a given vector is provided. @@ -38,22 +47,6 @@ namespace storm { */ SymbolicLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs); - /*! - * Constructs a symbolic linear equation solver with the given meta variable sets and pairs. - * - * @param A The matrix defining the coefficients of the linear equation system. - * @param allRows A BDD characterizing all rows of the equation system. - * @param rowMetaVariables The meta variables used to encode the rows of the matrix. - * @param columnMetaVariables The meta variables used to encode the columns of the matrix. - * @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta - * variables. - * @param precision The precision to achieve. - * @param maximalNumberOfIterations The maximal number of iterations to perform when solving a linear - * equation system iteratively. - * @param relative Sets whether or not to use a relativ stopping criterion rather than an absolute one. - */ - SymbolicLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative); - /*! * Solves the equation system A*x = b. The matrix A is required to be square and have a unique solution. * The solution of the set of linear equations will be written to the vector x. Note that the matrix A has @@ -83,7 +76,7 @@ namespace storm { storm::dd::Add A; // A BDD characterizing all rows of the equation system. - storm::dd::Bdd const& allRows; + storm::dd::Bdd allRows; // The row variables. std::set rowMetaVariables; @@ -93,15 +86,24 @@ namespace storm { // The pairs of meta variables used for renaming. std::vector> const& rowColumnMetaVariablePairs; - - // The precision to achive. - double precision; - - // The maximal number of iterations to perform. - uint_fast64_t maximalNumberOfIterations; - - // A flag indicating whether a relative or an absolute stopping criterion is to be used. - bool relative; + }; + + 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 = 0; + }; + + template + class GeneralSymbolicLinearEquationSolverFactory : public 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 GeneralSymbolicLinearEquationSolverFactory : public 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; }; } // namespace solver diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index 5ceb5b7d7..9eccde6d4 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -95,10 +95,11 @@ namespace storm { ValueType const& SymbolicMinMaxLinearEquationSolver::getPrecision() const { return precision; } - template class SymbolicMinMaxLinearEquationSolver; template class SymbolicMinMaxLinearEquationSolver; + + template class SymbolicMinMaxLinearEquationSolver; } } diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h index 2debcdd66..c343b281b 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.h @@ -113,7 +113,7 @@ namespace storm { std::vector> rowColumnMetaVariablePairs; // The precision to achieve. - double precision; + ValueType precision; // The maximal number of iterations to perform. uint_fast64_t maximalNumberOfIterations; diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp index c3613e3ea..612d29427 100644 --- a/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.cpp @@ -4,6 +4,7 @@ #include "storm/storage/dd/Add.h" #include "storm/utility/dd.h" +#include "storm/utility/constants.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/NativeEquationSolverSettings.h" @@ -11,13 +12,49 @@ namespace storm { namespace solver { - template - SymbolicNativeLinearEquationSolver::SymbolicNativeLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : SymbolicLinearEquationSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, precision, maximalNumberOfIterations, relative) { - // Intentionally left empty. + template + SymbolicNativeLinearEquationSolverSettings::SymbolicNativeLinearEquationSolverSettings() { + // Get the settings object to customize linear solving. + storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::getModule(); + + // Get appropriate settings. + maximalNumberOfIterations = settings.getMaximalIterationCount(); + precision = storm::utility::convertNumber(settings.getPrecision()); + relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; + } + + template + void SymbolicNativeLinearEquationSolverSettings::setPrecision(ValueType precision) { + this->precision = precision; + } + + template + void SymbolicNativeLinearEquationSolverSettings::setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations) { + this->maximalNumberOfIterations = maximalNumberOfIterations; + } + + template + void SymbolicNativeLinearEquationSolverSettings::setRelativeTerminationCriterion(bool value) { + this->relative = value; + } + + template + ValueType SymbolicNativeLinearEquationSolverSettings::getPrecision() const { + return precision; + } + + template + uint64_t SymbolicNativeLinearEquationSolverSettings::getMaximalNumberOfIterations() const { + return maximalNumberOfIterations; + } + + template + bool SymbolicNativeLinearEquationSolverSettings::getRelativeTerminationCriterion() const { + return relative; } template - SymbolicNativeLinearEquationSolver::SymbolicNativeLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) : SymbolicLinearEquationSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs) { + SymbolicNativeLinearEquationSolver::SymbolicNativeLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, SymbolicNativeLinearEquationSolverSettings const& settings) : SymbolicLinearEquationSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs), settings(settings) { // Intentionally left empty. } @@ -28,7 +65,7 @@ namespace storm { diagonal &= this->allRows; storm::dd::Add lu = diagonal.ite(this->A.getDdManager().template getAddZero(), this->A); - storm::dd::Add diagonalAdd = diagonal.template toAdd(); + storm::dd::Add diagonalAdd = diagonal.template toAdd(); storm::dd::Add diag = diagonalAdd.multiplyMatrix(this->A, this->columnMetaVariables); storm::dd::Add scaledLu = lu / diag; @@ -39,12 +76,12 @@ namespace storm { uint_fast64_t iterationCount = 0; bool converged = false; - while (!converged && iterationCount < this->maximalNumberOfIterations) { + while (!converged && iterationCount < this->getSettings().getMaximalNumberOfIterations()) { storm::dd::Add xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs); storm::dd::Add tmp = scaledB - scaledLu.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables); // Now check if the process already converged within our precision. - converged = tmp.equalModuloPrecision(xCopy, this->precision, this->relative); + converged = tmp.equalModuloPrecision(xCopy, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion()); xCopy = tmp; @@ -61,8 +98,35 @@ namespace storm { return xCopy; } + template + SymbolicNativeLinearEquationSolverSettings const& SymbolicNativeLinearEquationSolver::getSettings() const { + return settings; + } + + template + std::unique_ptr> SymbolicNativeLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { + return std::make_unique>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, settings); + } + + template + SymbolicNativeLinearEquationSolverSettings& SymbolicNativeLinearEquationSolverFactory::getSettings() { + return settings; + } + + template + SymbolicNativeLinearEquationSolverSettings const& SymbolicNativeLinearEquationSolverFactory::getSettings() const { + return settings; + } + + template class SymbolicNativeLinearEquationSolverSettings; + template class SymbolicNativeLinearEquationSolverSettings; + template class SymbolicNativeLinearEquationSolver; template class SymbolicNativeLinearEquationSolver; - + template class SymbolicNativeLinearEquationSolver; + + template class SymbolicNativeLinearEquationSolverFactory; + template class SymbolicNativeLinearEquationSolverFactory; + template class SymbolicNativeLinearEquationSolverFactory; } } diff --git a/src/storm/solver/SymbolicNativeLinearEquationSolver.h b/src/storm/solver/SymbolicNativeLinearEquationSolver.h index f83806a89..60e00ddf7 100644 --- a/src/storm/solver/SymbolicNativeLinearEquationSolver.h +++ b/src/storm/solver/SymbolicNativeLinearEquationSolver.h @@ -5,6 +5,31 @@ namespace storm { namespace solver { + template + class SymbolicNativeLinearEquationSolverSettings { + public: + SymbolicNativeLinearEquationSolverSettings(); + + void setPrecision(ValueType precision); + void setMaximalNumberOfIterations(uint64_t maximalNumberOfIterations); + void setRelativeTerminationCriterion(bool value); + + ValueType getPrecision() const; + uint64_t getMaximalNumberOfIterations() const; + bool getRelativeTerminationCriterion() const; + + private: + // The required precision for the iterative methods. + ValueType precision; + + // The maximal number of iterations to do before iteration is aborted. + uint_fast64_t maximalNumberOfIterations; + + // Sets whether the relative or absolute error is to be considered for convergence detection. Note that this + // only applies to the Jacobi method for this solver. + bool relative; + }; + /*! * An interface that represents an abstract symbolic linear equation solver. In addition to solving a system of * linear equations, the functionality to repeatedly multiply a matrix with a given vector is provided. @@ -22,24 +47,9 @@ namespace storm { * @param columnMetaVariables The meta variables used to encode the columns of the matrix. * @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta * variables. + * @param settings The settings to use. */ - SymbolicNativeLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs); - - /*! - * Constructs a symbolic linear equation solver with the given meta variable sets and pairs. - * - * @param A The matrix defining the coefficients of the linear equation system. - * @param allRows A BDD characterizing all rows of the equation system. - * @param rowMetaVariables The meta variables used to encode the rows of the matrix. - * @param columnMetaVariables The meta variables used to encode the columns of the matrix. - * @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta - * variables. - * @param precision The precision to achieve. - * @param maximalNumberOfIterations The maximal number of iterations to perform when solving a linear - * equation system iteratively. - * @param relative Sets whether or not to use a relativ stopping criterion rather than an absolute one. - */ - SymbolicNativeLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, double precision, uint_fast64_t maximalNumberOfIterations, bool relative); + SymbolicNativeLinearEquationSolver(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, SymbolicNativeLinearEquationSolverSettings const& settings = SymbolicNativeLinearEquationSolverSettings()); /*! * Solves the equation system A*x = b. The matrix A is required to be square and have a unique solution. @@ -52,6 +62,23 @@ namespace storm { */ virtual storm::dd::Add solveEquations(storm::dd::Add const& x, storm::dd::Add const& b) const; + SymbolicNativeLinearEquationSolverSettings const& getSettings() const; + + private: + // The settings to use. + SymbolicNativeLinearEquationSolverSettings settings; + }; + + template + class SymbolicNativeLinearEquationSolverFactory { + 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; + + SymbolicNativeLinearEquationSolverSettings& getSettings(); + SymbolicNativeLinearEquationSolverSettings const& getSettings() const; + + private: + SymbolicNativeLinearEquationSolverSettings settings; }; } // namespace solver diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index fd5f687a6..a3d374d23 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -182,7 +182,7 @@ namespace storm { } template - bool Add::equalModuloPrecision(Add const& other, double precision, bool relative) const { + bool Add::equalModuloPrecision(Add const& other, ValueType const& precision, bool relative) const { return internalAdd.equalModuloPrecision(other, precision, relative); } @@ -839,7 +839,9 @@ namespace storm { template class Add; template class Add; + #ifdef STORM_HAVE_CARL + template class Add; template class Add; #endif } diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index 62d6b999c..86f443ce3 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -302,7 +302,7 @@ namespace storm { * @param relative If set to true, not the absolute values have to be within the precision, but the relative * values. */ - bool equalModuloPrecision(Add const& other, double precision, bool relative = true) const; + bool equalModuloPrecision(Add const& other, ValueType const& precision, bool relative = true) const; /*! * Swaps the given pairs of meta variables in the ADD. The pairs of meta variables must be guaranteed to have diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index d4db6ede1..d58758b6e 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -395,25 +395,32 @@ namespace storm { 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& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, storm::RationalNumber value); 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; template Add Bdd::toAdd() const; + #ifdef STORM_HAVE_CARL + template Add Bdd::toAdd() const; template Add Bdd::toAdd() const; #endif template std::vector Bdd::filterExplicitVector(Odd const& odd, std::vector const& values) const; template std::vector Bdd::filterExplicitVector(Odd const& odd, std::vector const& values) const; + #ifdef STORM_HAVE_CARL + template std::vector Bdd::filterExplicitVector(Odd const& odd, std::vector const& values) const; template std::vector Bdd::filterExplicitVector(Odd const& odd, std::vector const& values) const; #endif template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; + #ifdef STORM_HAVE_CARL + template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; template Add Bdd::ite(Add const& thenAdd, Add const& elseAdd) const; #endif } diff --git a/src/storm/storage/dd/DdManager.cpp b/src/storm/storage/dd/DdManager.cpp index 0600ba1c3..361594a4b 100644 --- a/src/storm/storage/dd/DdManager.cpp +++ b/src/storm/storage/dd/DdManager.cpp @@ -104,7 +104,7 @@ namespace storm { Add result = this->getAddZero(); for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { - result += this->getEncoding(variable, value).template toAdd() * this->getConstant(static_cast(value)); + result += this->getEncoding(variable, value).template toAdd() * this->getConstant(storm::utility::convertNumber(value)); } return result; } @@ -446,18 +446,21 @@ namespace storm { template Add DdManager::getAddZero() const; template Add DdManager::getAddZero() const; #ifdef STORM_HAVE_CARL + template Add DdManager::getAddZero() const; template Add DdManager::getAddZero() const; #endif template Add DdManager::getAddOne() const; template Add DdManager::getAddOne() const; #ifdef STORM_HAVE_CARL + template Add DdManager::getAddOne() const; template Add DdManager::getAddOne() const; #endif template Add DdManager::getInfinity() const; template Add DdManager::getInfinity() const; #ifdef STORM_HAVE_CARL + template Add DdManager::getInfinity() const; template Add DdManager::getInfinity() const; #endif @@ -470,6 +473,7 @@ namespace storm { template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; #ifdef STORM_HAVE_CARL + template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; template Add DdManager::getIdentity(storm::expressions::Variable const& variable) const; #endif } diff --git a/src/storm/storage/dd/Odd.cpp b/src/storm/storage/dd/Odd.cpp index b89262fde..0973fe7a4 100644 --- a/src/storm/storage/dd/Odd.cpp +++ b/src/storm/storage/dd/Odd.cpp @@ -146,6 +146,7 @@ namespace storm { } 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; template void Odd::expandExplicitVector(storm::dd::Odd const& newOdd, std::vector const& oldValues, std::vector& newValues) const; } } diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 5ac14aab8..d02222df0 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -163,7 +163,7 @@ namespace storm { } template - bool InternalAdd::equalModuloPrecision(InternalAdd const& other, double precision, bool relative) const { + bool InternalAdd::equalModuloPrecision(InternalAdd const& other, ValueType const& precision, bool relative) const { if (relative) { return this->getCuddAdd().EqualSupNormRel(other.getCuddAdd(), precision); } else { diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.h b/src/storm/storage/dd/cudd/InternalCuddAdd.h index 893eaf06a..360a7b0f9 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.h @@ -290,7 +290,7 @@ namespace storm { * @param relative If set to true, not the absolute values have to be within the precision, but the relative * values. */ - bool equalModuloPrecision(InternalAdd const& other, double precision, bool relative = true) const; + bool equalModuloPrecision(InternalAdd const& other, ValueType const& precision, bool relative = true) const; /*! * Swaps the given pairs of DD variables in the ADD. The pairs of meta variables have to be represented by diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index 65933570c..e44433c3f 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -510,7 +510,7 @@ namespace storm { #endif template - bool InternalAdd::equalModuloPrecision(InternalAdd const& other, double precision, bool relative) const { + bool InternalAdd::equalModuloPrecision(InternalAdd const& other, ValueType const& precision, bool relative) const { if (relative) { return this->sylvanMtbdd.EqualNormRel(other.sylvanMtbdd, precision); } else { @@ -519,9 +519,22 @@ namespace storm { } #ifdef STORM_HAVE_CARL - template<> - bool InternalAdd::equalModuloPrecision(InternalAdd const&, double, bool) const { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Operation (equal modulo precision) not supported by rational functions."); + template<> + bool InternalAdd::equalModuloPrecision(InternalAdd const& other, storm::RationalNumber const& precision, bool relative) const { + if (relative) { + return this->sylvanMtbdd.EqualNormRelRN(other.sylvanMtbdd, precision); + } else { + return this->sylvanMtbdd.EqualNormRN(other.sylvanMtbdd, precision); + } + } + + template<> + bool InternalAdd::equalModuloPrecision(InternalAdd const& other, storm::RationalFunction const& precision, bool relative) const { + if (relative) { + return this->sylvanMtbdd.EqualNormRelRF(other.sylvanMtbdd, precision); + } else { + return this->sylvanMtbdd.EqualNormRF(other.sylvanMtbdd, precision); + } } #endif diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index b53fb0f76..13b96d25a 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -300,7 +300,7 @@ namespace storm { * @param relative If set to true, not the absolute values have to be within the precision, but the relative * values. */ - bool equalModuloPrecision(InternalAdd const& other, double precision, bool relative = true) const; + bool equalModuloPrecision(InternalAdd const& other, ValueType const& precision, bool relative = true) const; /*! * Swaps the given pairs of DD variables in the ADD. The pairs of meta variables have to be represented by diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp index 61a499248..db205268f 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -254,6 +254,9 @@ namespace storm { return InternalAdd(ddManager, this->sylvanBdd.toInt64Mtbdd()); } #ifdef STORM_HAVE_CARL + else if (std::is_same::value) { + return InternalAdd(ddManager, this->sylvanBdd.toStormRationalNumberMtbdd()); + } else if (std::is_same::value) { return InternalAdd(ddManager, this->sylvanBdd.toStormRationalFunctionMtbdd()); } @@ -526,14 +529,17 @@ namespace storm { template InternalAdd InternalBdd::toAdd() const; template InternalAdd InternalBdd::toAdd() const; + template InternalAdd InternalBdd::toAdd() const; template InternalAdd InternalBdd::toAdd() const; template void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; template void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; + template void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; template void InternalBdd::filterExplicitVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector const& sourceValues, std::vector& targetValues) const; template InternalAdd InternalBdd::ite(InternalAdd const& thenAdd, InternalAdd const& elseAdd) const; template InternalAdd InternalBdd::ite(InternalAdd const& thenAdd, InternalAdd const& elseAdd) const; + template InternalAdd InternalBdd::ite(InternalAdd const& thenAdd, InternalAdd const& elseAdd) const; template InternalAdd InternalBdd::ite(InternalAdd const& thenAdd, InternalAdd const& elseAdd) const; } } diff --git a/src/storm/storage/expressions/ExpressionEvaluator.cpp b/src/storm/storage/expressions/ExpressionEvaluator.cpp index 3305ec772..b167c6034 100644 --- a/src/storm/storage/expressions/ExpressionEvaluator.cpp +++ b/src/storm/storage/expressions/ExpressionEvaluator.cpp @@ -54,7 +54,8 @@ namespace storm { } RationalNumber ExpressionEvaluator::asRational(Expression const& expression) const { - return this->rationalNumberVisitor.toRationalNumber(expression); + RationalNumber result = this->rationalNumberVisitor.toRationalNumber(expression); + return result; } ExpressionEvaluator::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase(manager), rationalFunctionVisitor(*this) { diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp index c8931c7f3..9a82be279 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp @@ -47,29 +47,37 @@ namespace storm { boost::any ToRationalNumberVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { RationalNumberType firstOperandAsRationalNumber = boost::any_cast(expression.getFirstOperand()->accept(*this, data)); RationalNumberType secondOperandAsRationalNumber = boost::any_cast(expression.getSecondOperand()->accept(*this, data)); + RationalNumberType result; switch(expression.getOperatorType()) { case BinaryNumericalFunctionExpression::OperatorType::Plus: - return firstOperandAsRationalNumber + secondOperandAsRationalNumber; + result = firstOperandAsRationalNumber + secondOperandAsRationalNumber; + return result; break; case BinaryNumericalFunctionExpression::OperatorType::Minus: - return firstOperandAsRationalNumber - secondOperandAsRationalNumber; + result = firstOperandAsRationalNumber - secondOperandAsRationalNumber; + return result; break; case BinaryNumericalFunctionExpression::OperatorType::Times: - return firstOperandAsRationalNumber * secondOperandAsRationalNumber; + result = firstOperandAsRationalNumber * secondOperandAsRationalNumber; + return result; break; case BinaryNumericalFunctionExpression::OperatorType::Divide: - return firstOperandAsRationalNumber / secondOperandAsRationalNumber; + result = firstOperandAsRationalNumber / secondOperandAsRationalNumber; + return result; break; case BinaryNumericalFunctionExpression::OperatorType::Min: - return std::min(firstOperandAsRationalNumber, secondOperandAsRationalNumber); + result = std::min(firstOperandAsRationalNumber, secondOperandAsRationalNumber); + return result; break; case BinaryNumericalFunctionExpression::OperatorType::Max: - return std::max(firstOperandAsRationalNumber, secondOperandAsRationalNumber); + result = std::max(firstOperandAsRationalNumber, secondOperandAsRationalNumber); + return result; break; case BinaryNumericalFunctionExpression::OperatorType::Power: STORM_LOG_THROW(storm::utility::isInteger(secondOperandAsRationalNumber), storm::exceptions::InvalidArgumentException, "Exponent of power operator must be a positive integer."); uint_fast64_t exponentAsInteger = storm::utility::convertNumber(secondOperandAsRationalNumber); - return storm::utility::pow(firstOperandAsRationalNumber, exponentAsInteger); + result = storm::utility::pow(firstOperandAsRationalNumber, exponentAsInteger); + return result; break; } @@ -96,10 +104,20 @@ namespace storm { template boost::any ToRationalNumberVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { RationalNumberType operandAsRationalNumber = boost::any_cast(expression.getOperand()->accept(*this, data)); + RationalNumberType result; switch (expression.getOperatorType()) { - case UnaryNumericalFunctionExpression::OperatorType::Minus: return -operandAsRationalNumber; - case UnaryNumericalFunctionExpression::OperatorType::Floor: return storm::utility::floor(operandAsRationalNumber); - case UnaryNumericalFunctionExpression::OperatorType::Ceil: return storm::utility::ceil(operandAsRationalNumber); + case UnaryNumericalFunctionExpression::OperatorType::Minus: + result = -operandAsRationalNumber; + return result; + break; + case UnaryNumericalFunctionExpression::OperatorType::Floor: + result = storm::utility::floor(operandAsRationalNumber); + return result; + break; + case UnaryNumericalFunctionExpression::OperatorType::Ceil: + result = storm::utility::ceil(operandAsRationalNumber); + return result; + break; } } diff --git a/src/storm/transformer/SymbolicToSparseTransformer.cpp b/src/storm/transformer/SymbolicToSparseTransformer.cpp index 36e8a4918..b1d3813de 100644 --- a/src/storm/transformer/SymbolicToSparseTransformer.cpp +++ b/src/storm/transformer/SymbolicToSparseTransformer.cpp @@ -12,7 +12,7 @@ namespace storm { namespace transformer { template - std::shared_ptr> SymbolicMdpToSparseDtmcTransformer::translate(storm::models::symbolic::Dtmc const& symbolicDtmc) { + std::shared_ptr> SymbolicDtmcToSparseDtmcTransformer::translate(storm::models::symbolic::Dtmc const& symbolicDtmc) { this->odd = symbolicDtmc.getReachableStates().createOdd(); storm::storage::SparseMatrix transitionMatrix = symbolicDtmc.getTransitionMatrix().toMatrix(this->odd, this->odd); std::unordered_map> rewardModels; @@ -42,7 +42,7 @@ namespace storm { } template - storm::dd::Odd const& SymbolicMdpToSparseDtmcTransformer::getOdd() const { + storm::dd::Odd const& SymbolicDtmcToSparseDtmcTransformer::getOdd() const { return this->odd; } @@ -76,12 +76,16 @@ namespace storm { return std::make_shared>(transitionMatrix, labelling, rewardModels); } - template class SymbolicMdpToSparseDtmcTransformer; - template class SymbolicMdpToSparseDtmcTransformer; + template class SymbolicDtmcToSparseDtmcTransformer; + template class SymbolicDtmcToSparseDtmcTransformer; - template class SymbolicMdpToSparseDtmcTransformer; + template class SymbolicDtmcToSparseDtmcTransformer; + template class SymbolicDtmcToSparseDtmcTransformer; template class SymbolicMdpToSparseMdpTransformer; template class SymbolicMdpToSparseMdpTransformer; + + template class SymbolicMdpToSparseMdpTransformer; + } } diff --git a/src/storm/transformer/SymbolicToSparseTransformer.h b/src/storm/transformer/SymbolicToSparseTransformer.h index 2af78406b..eb1f973d6 100644 --- a/src/storm/transformer/SymbolicToSparseTransformer.h +++ b/src/storm/transformer/SymbolicToSparseTransformer.h @@ -12,7 +12,7 @@ namespace storm { namespace transformer { template - class SymbolicMdpToSparseDtmcTransformer { + class SymbolicDtmcToSparseDtmcTransformer { public: std::shared_ptr> translate(storm::models::symbolic::Dtmc const& symbolicDtmc); storm::dd::Odd const& getOdd() const; diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 3f3831293..7b2718e51 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -72,6 +72,11 @@ namespace storm { return true; } + template + TargetType convertNumber(SourceType const& number) { + return static_cast(number); + } + template<> uint_fast64_t convertNumber(double const& number){ return std::llround(number); @@ -86,7 +91,17 @@ namespace storm { double convertNumber(double const& number){ return number; } - + + template<> + double convertNumber(long long const& number){ + return static_cast(number); + } + + template<> + storm::storage::sparse::state_type convertNumber(long long const& number){ + return static_cast(number); + } + template ValueType simplify(ValueType value) { // In the general case, we don't do anything here, but merely return the value. If something else is @@ -240,39 +255,39 @@ namespace storm { } template<> - uint_fast64_t convertNumber(ClnRationalNumber const& number){ + uint_fast64_t convertNumber(ClnRationalNumber const& number) { return carl::toInt(number); } template<> - ClnRationalNumber convertNumber(ClnRationalNumber const& number){ + ClnRationalNumber convertNumber(ClnRationalNumber const& number) { return number; } template<> - ClnRationalNumber convertNumber(double const& number){ + ClnRationalNumber convertNumber(double const& number) { return carl::rationalize(number); } template<> - ClnRationalNumber convertNumber(int const& number){ + ClnRationalNumber convertNumber(int const& number) { return carl::rationalize(number); } template<> - ClnRationalNumber convertNumber(uint_fast64_t const& number){ + ClnRationalNumber convertNumber(uint_fast64_t const& number) { STORM_LOG_ASSERT(static_cast(number) == number, "Rationalizing failed, because the number is too large."); return carl::rationalize(static_cast(number)); } template<> - ClnRationalNumber convertNumber(int_fast64_t const& number){ + ClnRationalNumber convertNumber(int_fast64_t const& number) { STORM_LOG_ASSERT(static_cast(number) == number, "Rationalizing failed, because the number is too large."); return carl::rationalize(static_cast(number)); } template<> - double convertNumber(ClnRationalNumber const& number){ + double convertNumber(ClnRationalNumber const& number) { return carl::toDouble(number); } @@ -541,7 +556,12 @@ namespace storm { RationalFunctionCoefficient convertNumber(RationalFunction const& number){ return number.nominatorAsNumber() / number.denominatorAsNumber(); } - + + template<> + RationalFunction convertNumber(storm::storage::sparse::state_type const& number) { + return RationalFunction(convertNumber(number)); + } + template<> RationalFunction& simplify(RationalFunction& value); @@ -705,6 +725,12 @@ namespace storm { template bool isInfinity(storm::storage::sparse::state_type const& value); template bool isInteger(storm::storage::sparse::state_type const& number); + // other instantiations + template double convertNumber(long long const&); + template storm::storage::sparse::state_type convertNumber(long long const& number); + template unsigned long convertNumber(long const&); + template double convertNumber(long const&); + #if defined(STORM_HAVE_CLN) // Instantiations for (CLN) rational number. template storm::ClnRationalNumber one(); @@ -789,6 +815,8 @@ namespace storm { template storm::RationalFunction convertNumber(storm::RationalFunction const& number); template RationalFunctionCoefficient convertNumber(RationalFunction const& number); template RationalFunction convertNumber(storm::RationalFunctionCoefficient const& number); + template RationalFunction convertNumber(storm::storage::sparse::state_type const& number); + template RationalFunction convertNumber(double const& number); template RationalFunction simplify(RationalFunction value); template RationalFunction& simplify(RationalFunction& value); template RationalFunction&& simplify(RationalFunction&& value); diff --git a/src/storm/utility/dd.cpp b/src/storm/utility/dd.cpp index d1c75aeb4..26dde9bd5 100644 --- a/src/storm/utility/dd.cpp +++ b/src/storm/utility/dd.cpp @@ -74,6 +74,7 @@ namespace storm { template storm::dd::Bdd getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs); template storm::dd::Bdd getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs); + template storm::dd::Add getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs); template storm::dd::Add getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs); } diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 5d8754970..f64d46896 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -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 number). + + 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); + // 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()); diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp index 21b73c9fe..80a1db702 100644 --- a/src/storm/utility/solver.cpp +++ b/src/storm/utility/solver.cpp @@ -25,33 +25,7 @@ namespace storm { namespace utility { namespace solver { - 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; - 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 { @@ -126,11 +100,9 @@ namespace storm { return factory->create(manager); } - template class SymbolicLinearEquationSolverFactory; - template class SymbolicLinearEquationSolverFactory; - template class SymbolicLinearEquationSolverFactory; template class SymbolicMinMaxLinearEquationSolverFactory; template class SymbolicMinMaxLinearEquationSolverFactory; + template class SymbolicMinMaxLinearEquationSolverFactory; template class SymbolicGameSolverFactory; template class SymbolicGameSolverFactory; template class GameSolverFactory; diff --git a/src/storm/utility/solver.h b/src/storm/utility/solver.h index ab3255f67..1d3465e8c 100644 --- a/src/storm/utility/solver.h +++ b/src/storm/utility/solver.h @@ -57,18 +57,6 @@ namespace storm { namespace utility { namespace solver { - 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 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 de9660744..145583a61 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -103,16 +103,16 @@ #include "storm/utility/file.h" namespace storm { - + namespace parser { class FormulaParser; } - + template std::shared_ptr> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile = boost::none, boost::optional const& transitionRewardsFile = boost::none, boost::optional const& choiceLabelingFile = boost::none) { return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); } - + std::vector> extractFormulasFromProperties(std::vector const& properties); std::pair> parseJaniModel(std::string const& path); storm::prism::Program parseProgram(std::string const& path); @@ -123,7 +123,7 @@ namespace storm { std::vector parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional> const& propertyFilter = boost::none); boost::optional> parsePropertyFilter(boost::optional const& propertyFilter); std::vector filterProperties(std::vector const& properties, boost::optional> const& propertyFilter); - + template std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { storm::builder::BuilderOptions options(formulas); @@ -133,17 +133,17 @@ namespace storm { options.setBuildAllRewardModels(); options.clearTerminalStates(); } - + // Generate command labels if we are going to build a counterexample later. if (storm::settings::getModule().isMinimalCommandSetGenerationSet()) { options.setBuildChoiceLabels(true); } - + if (storm::settings::getModule().isJitSet()) { STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::NotSupportedException, "Cannot use JIT-based model builder for non-JANI model."); - + storm::builder::jit::ExplicitJitJaniModelBuilder builder(model.asJaniModel(), options); - + if (storm::settings::getModule().isDoctorSet()) { bool result = builder.doctor(); STORM_LOG_THROW(result, storm::exceptions::InvalidSettingsException, "The JIT-based model builder cannot be used on your system."); @@ -164,7 +164,7 @@ namespace storm { return builder.build(); } } - + template std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { if (model.isPrismProgram()) { @@ -207,7 +207,7 @@ namespace storm { options = typename storm::storage::NondeterministicModelBisimulationDecomposition::Options(*model, formulas); } options.setType(type); - + storm::storage::NondeterministicModelBisimulationDecomposition bisimulationDecomposition(*model, options); bisimulationDecomposition.computeBisimulationDecomposition(); model = bisimulationDecomposition.getQuotient(); @@ -221,16 +221,16 @@ namespace storm { STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs."); model->reduceToStateBasedRewards(); - + if (model->isOfType(storm::models::ModelType::Dtmc)) { return performDeterministicSparseBisimulationMinimization>(model->template as>(), formulas, type); } else if (model->isOfType(storm::models::ModelType::Ctmc)) { return performDeterministicSparseBisimulationMinimization>(model->template as>(), formulas, type); } else { return performNondeterministicSparseBisimulationMinimization>(model->template as>(), formulas, type); - } + } } - + template std::shared_ptr> performBisimulationMinimization(std::shared_ptr> const& model, std::shared_ptr const& formula, storm::storage::BisimulationType type) { std::vector> formulas = { formula }; @@ -252,7 +252,7 @@ namespace storm { model = ma->convertToCTMC(); } } - + if (model->isSparseModel() && storm::settings::getModule().isBisimulationSet()) { operationPerformed = true; storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; @@ -263,7 +263,7 @@ namespace storm { STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for sparse models."); model = performBisimulationMinimization(model->template as>(), formulas, bisimType); } - + preprocessingWatch.stop(); if (operationPerformed) { STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); @@ -271,7 +271,7 @@ namespace storm { return model; } - + template void generateCounterexample(storm::storage::SymbolicModelDescription const& model, std::shared_ptr> markovModel, std::shared_ptr const& formula) { if (storm::settings::getModule().isMinimalCommandSetGenerationSet()) { @@ -280,40 +280,40 @@ namespace storm { storm::prism::Program const& program = model.asPrismProgram(); std::shared_ptr> mdp = markovModel->template as>(); - + // Determine whether we are required to use the MILP-version or the SAT-version. bool useMILP = storm::settings::getModule().isUseMilpBasedMinimalCommandSetGenerationSet(); - + if (useMILP) { storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(program, *mdp, formula); } else { storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, storm::settings::getModule().getConstantDefinitionString(), *mdp, formula); } - + } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No suitable counterexample representation selected."); } } - + #ifdef STORM_HAVE_CARL template<> inline void generateCounterexample(storm::storage::SymbolicModelDescription const&, std::shared_ptr> , std::shared_ptr const& ) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for exact arithmetic model."); } - + template<> inline void generateCounterexample(storm::storage::SymbolicModelDescription const&, std::shared_ptr> , std::shared_ptr const& ) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); } #endif - + template void generateCounterexamples(storm::storage::SymbolicModelDescription const& model, std::shared_ptr> markovModel, std::vector> const& formulas) { for (auto const& formula : formulas) { generateCounterexample(model, markovModel, formula); } } - + template std::unique_ptr verifyModel(std::shared_ptr model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { switch(storm::settings::getModule().getEngine()) { @@ -337,7 +337,7 @@ namespace storm { } } } - + template std::unique_ptr verifySparseDtmc(std::shared_ptr> dtmc, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; @@ -358,7 +358,7 @@ namespace storm { } return result; } - + template std::unique_ptr verifySparseCtmc(std::shared_ptr> ctmc, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; @@ -370,7 +370,7 @@ namespace storm { } return result; } - + template std::unique_ptr verifySparseMdp(std::shared_ptr> mdp, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; @@ -382,7 +382,7 @@ namespace storm { } return result; } - + template std::unique_ptr verifySparseMarkovAutomaton(std::shared_ptr> ma, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; @@ -398,11 +398,11 @@ namespace storm { } return result; } - + template std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - + std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { result = verifySparseDtmc(model->template as>(), task); @@ -417,12 +417,12 @@ namespace storm { } return result; } - + #ifdef STORM_HAVE_CARL template<> inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - + std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { result = verifySparseDtmc(model->template as>(), task); @@ -435,7 +435,7 @@ namespace storm { } return result; } - + inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc::ConstraintCollector const& constraintCollector, std::string const& path) { std::ofstream filestream; storm::utility::openFile(path, filestream); @@ -451,11 +451,11 @@ namespace storm { std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator>(filestream, "\n")); storm::utility::closeFile(filestream); } - + template<> inline std::unique_ptr verifySparseModel(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - + std::unique_ptr result; if (model->getType() == storm::models::ModelType::Dtmc) { result = verifySparseDtmc(model->template as>(), task); @@ -469,7 +469,7 @@ namespace storm { } return result; } - + /*! * Initializes a region model checker. * @@ -480,9 +480,9 @@ namespace storm { * @return true when initialization was successful */ inline bool initializeRegionModelChecker(std::shared_ptr>& regionModelChecker, - std::string const& programFilePath, - std::string const& formulaString, - std::string const& constantsString=""){ + std::string const& programFilePath, + std::string const& formulaString, + std::string const& constantsString=""){ regionModelChecker.reset(); // Program and formula storm::prism::Program program = parseProgram(programFilePath); @@ -514,7 +514,7 @@ namespace storm { regionModelChecker->specifyFormula(formulas[0]); return true; } - + /*! * Computes the reachability value at the given point by instantiating the model. * @@ -526,7 +526,7 @@ namespace storm { std::map const& point){ return regionModelChecker->valueIsInBoundOfFormula(regionModelChecker->getReachabilityValue(point)); } - + /*! * Does an approximation of the reachability value for all parameters in the given region. * @param regionModelChecker the model checker object that is to be used @@ -549,10 +549,10 @@ namespace storm { storm::modelchecker::region::ParameterRegion region(lowerBoundaries, upperBoundaries); return regionModelChecker->checkRegionWithApproximation(region, proveAllSat); } - - + + #endif - + template std::unique_ptr verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { std::unique_ptr result; @@ -585,12 +585,12 @@ namespace storm { 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); - + 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>(); if (storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule().isUseDedicatedModelCheckerSet()) { - storm::transformer::SymbolicMdpToSparseDtmcTransformer transformer; + storm::transformer::SymbolicDtmcToSparseDtmcTransformer transformer; std::shared_ptr> sparseDtmc = transformer.translate(*dtmc); // Optimally, we could preprocess the model here and apply, for example, bisimulation minimization. However, @@ -600,7 +600,7 @@ namespace storm { storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*sparseDtmc); if (modelchecker.canHandle(task)) { result = modelchecker.check(task); - + // Now translate the sparse result to hybrid one, so it can be filtered with the symbolic initial states of the model later. if (result->isQualitative()) { storm::modelchecker::ExplicitQualitativeCheckResult const& explicitResult = result->asExplicitQualitativeCheckResult(); @@ -642,7 +642,7 @@ namespace storm { return result; } - + template std::unique_ptr verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant) { std::unique_ptr result; @@ -708,7 +708,7 @@ namespace storm { model->getTransitionMatrix().printAsMatlabMatrix(stream); storm::utility::closeFile(stream); } - + } #endif /* STORM_H */ diff --git a/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index e9819a2c7..05176b4f5 100644 --- a/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -41,7 +41,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); @@ -103,7 +103,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); @@ -158,7 +158,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); @@ -203,7 +203,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); @@ -259,7 +259,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); @@ -312,7 +312,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); + storm::modelchecker::SymbolicDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::solver::SymbolicLinearEquationSolverFactory())); std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");