diff --git a/CMakeLists.txt b/CMakeLists.txt index c53d049b3..6f1c9d174 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -124,7 +124,20 @@ if(CMAKE_COMPILER_IS_GNUCC) set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops") set(CMAKE_C_FLAGS_RELEASE "${CMAKE_C_FLAGS_RELEASE} -funroll-loops") add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE) - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -Wall -pedantic -Wno-deprecated-declarations -Wno-unused-local-typedefs -Wno-unknown-pragmas") + + set(STORM_CXX_STD_COMMAND "-std=c++14") + if (CMAKE_CXX_COMPILER_VERSION VERSION_GREATER 5.1) + message(STATUS "GCC Version is greater then 5.1, using -std=c++14") + set(STORM_CXX_STD_COMMAND "-std=c++14") + elseif(CMAKE_CXX_COMPILER_VERSION VERSION_LESS 4.9.2) + message(WARNING "GCC Version is less then 4.9.2 - your compiler is probably too old for StoRM!") + set(STORM_CXX_STD_COMMAND "-std=c++1y") + else() + message(STATUS "GCC Version is between 4.9.2 and 5.1, using -std=c++1y") + set(STORM_CXX_STD_COMMAND "-std=c++1y") + endif() + + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${STORM_CXX_STD_COMMAND} -Wall -pedantic -Wno-deprecated-declarations -Wno-unused-local-typedefs -Wno-unknown-pragmas") set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic -Wno-deprecated-declarations") if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 5.0) message(FATAL_ERROR "GCC version must be at least 5.0!") diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c index 118badbba..e768f3f66 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c @@ -549,7 +549,6 @@ cuddBddExistAbstractRepresentativeRecur( res1 = cuddUniqueInter(manager, (int) cube->index, zero, res); if (res1 == NULL) { Cudd_IterDerefBdd(manager,res); - Cudd_IterDerefBdd(manager,zero); return(NULL); } cuddDeref(res); @@ -573,7 +572,6 @@ cuddBddExistAbstractRepresentativeRecur( if (res1 == NULL) { Cudd_IterDerefBdd(manager,res); - Cudd_IterDerefBdd(manager,zero); return(NULL); } cuddDeref(res); diff --git a/resources/3rdparty/sylvan/CMakeLists.txt b/resources/3rdparty/sylvan/CMakeLists.txt index d9999a0f3..1007c5917 100644 --- a/resources/3rdparty/sylvan/CMakeLists.txt +++ b/resources/3rdparty/sylvan/CMakeLists.txt @@ -5,6 +5,7 @@ enable_testing() set(CMAKE_C_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11 -fPIC") set(CMAKE_CXX_FLAGS "-O3 -Wextra -Wall -Werror -fno-strict-aliasing -Wno-deprecated-register -std=gnu++11 -fPIC") +option(USE_CARL "Sets whether carl should be included." ON) option(WITH_COVERAGE "Add generation of test coverage" OFF) if(WITH_COVERAGE) set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -O0 -g -coverage") @@ -28,9 +29,26 @@ if(WITH_COVERAGE) ) endif() +if(USE_CARL) + find_package(carl QUIET REQUIRED) + if(carl_FOUND) + add_definitions(-DSYLVAN_HAVE_CARL) + include_directories("${carl_INCLUDE_DIR}") + list(APPEND STORM_LINK_LIBRARIES ${carl_LIBRARIES}) + message(STATUS "Sylvan - using CARL.") + else() + message(FATAL_ERROR "Sylvan - CARL was requested but not found") + endif() +else() + message(STATUS "Sylvan - not using CARL.") +endif() + + set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake) find_package(GMP REQUIRED) include_directories(${GMP_INCLUDE_DIR}) +include_directories("${PROJECT_SOURCE_DIR}/../../../") +include_directories("${PROJECT_BINARY_DIR}/../include") include_directories(src) include_directories(src) diff --git a/resources/3rdparty/sylvan/examples/CMakeLists.txt b/resources/3rdparty/sylvan/examples/CMakeLists.txt index bb335935d..ce2d0d740 100644 --- a/resources/3rdparty/sylvan/examples/CMakeLists.txt +++ b/resources/3rdparty/sylvan/examples/CMakeLists.txt @@ -12,6 +12,12 @@ target_link_libraries(lddmc sylvan) add_executable(simple simple.cpp) target_link_libraries(simple sylvan stdc++) +if(USE_CARL) + message(STATUS "Sylvan - Example for Storm enabled.") + add_executable(storm-rf storm.cpp) + target_link_libraries(storm-rf sylvan stdc++ ${carl_LIBRARIES}) +endif(USE_CARL) + include(CheckIncludeFiles) check_include_files("gperftools/profiler.h" HAVE_PROFILER) diff --git a/resources/3rdparty/sylvan/examples/storm.cpp b/resources/3rdparty/sylvan/examples/storm.cpp new file mode 100644 index 000000000..c9bcfb032 --- /dev/null +++ b/resources/3rdparty/sylvan/examples/storm.cpp @@ -0,0 +1,127 @@ +#ifdef NDEBUG +#undef NDEBUG +#endif + +#include +#include +#include + +#include +#include +#include +#include + +using namespace sylvan; + +VOID_TASK_0(storm_rf) +{ + Bdd one = Bdd::bddOne(); // the True terminal + Bdd zero = Bdd::bddZero(); // the False terminal + + // check if they really are the True/False terminal + assert(one.GetBDD() == sylvan_true); + assert(zero.GetBDD() == sylvan_false); + + Bdd a = Bdd::bddVar(0); // create a BDD variable x_0 + Bdd b = Bdd::bddVar(1); // create a BDD variable x_1 + + // check if a really is the Boolean formula "x_0" + assert(!a.isConstant()); + assert(a.TopVar() == 0); + assert(a.Then() == one); + assert(a.Else() == zero); + + // check if b really is the Boolean formula "x_1" + assert(!b.isConstant()); + assert(b.TopVar() == 1); + assert(b.Then() == one); + assert(b.Else() == zero); + + // compute !a + Bdd not_a = !a; + + // check if !!a is really a + assert((!not_a) == a); + + // compute a * b and !(!a + !b) and check if they are equivalent + Bdd a_and_b = a * b; + Bdd not_not_a_or_not_b = !(!a + !b); + assert(a_and_b == not_not_a_or_not_b); + + // perform some simple quantification and check the results + Bdd ex = a_and_b.ExistAbstract(a); // \exists a . a * b + assert(ex == b); + Bdd andabs = a.AndAbstract(b, a); // \exists a . a * b using AndAbstract + assert(ex == andabs); + Bdd univ = a_and_b.UnivAbstract(a); // \forall a . a * b + assert(univ == zero); + + // alternative method to get the cube "ab" using bddCube + BddSet variables = a * b; + std::vector vec = {1, 1}; + assert(a_and_b == Bdd::bddCube(variables, vec)); + + // test the bddCube method for all combinations + assert((!a * !b) == Bdd::bddCube(variables, std::vector({0, 0}))); + assert((!a * b) == Bdd::bddCube(variables, std::vector({0, 1}))); + assert((!a) == Bdd::bddCube(variables, std::vector({0, 2}))); + assert((a * !b) == Bdd::bddCube(variables, std::vector({1, 0}))); + assert((a * b) == Bdd::bddCube(variables, std::vector({1, 1}))); + assert((a) == Bdd::bddCube(variables, std::vector({1, 2}))); + assert((!b) == Bdd::bddCube(variables, std::vector({2, 0}))); + assert((b) == Bdd::bddCube(variables, std::vector({2, 1}))); + assert(one == Bdd::bddCube(variables, std::vector({2, 2}))); +} + +VOID_TASK_1(_main, void*, arg) +{ + // Initialize Sylvan + // With starting size of the nodes table 1 << 21, and maximum size 1 << 27. + // With starting size of the cache table 1 << 20, and maximum size 1 << 20. + // Memory usage: 24 bytes per node, and 36 bytes per cache bucket + // - 1<<24 nodes: 384 MB + // - 1<<25 nodes: 768 MB + // - 1<<26 nodes: 1536 MB + // - 1<<27 nodes: 3072 MB + // - 1<<24 cache: 576 MB + // - 1<<25 cache: 1152 MB + // - 1<<26 cache: 2304 MB + // - 1<<27 cache: 4608 MB + sylvan_init_package(1LL<<22, 1LL<<26, 1LL<<22, 1LL<<26); + + // Initialize the BDD module with granularity 1 (cache every operation) + // A higher granularity (e.g. 6) often results in better performance in practice + sylvan_init_bdd(1); + + // Now we can do some simple stuff using the C++ objects. + CALL(storm_rf); + + // Report statistics (if SYLVAN_STATS is 1 in the configuration) + sylvan_stats_report(stdout, 1); + + // And quit, freeing memory + sylvan_quit(); + + // We didn't use arg + (void)arg; +} + +int +main (int argc, char *argv[]) +{ + int n_workers = 0; // automatically detect number of workers + size_t deque_size = 0; // default value for the size of task deques for the workers + size_t program_stack_size = 0; // default value for the program stack of each pthread + + // Initialize the Lace framework for workers. + lace_init(n_workers, deque_size); + + // Spawn and start all worker pthreads; suspends current thread until done. + lace_startup(program_stack_size, TASK(_main), NULL); + + // The lace_startup command also exits Lace after _main is completed. + + return 0; + (void)argc; // unused variable + (void)argv; // unused variable +} diff --git a/resources/3rdparty/sylvan/src/CMakeLists.txt b/resources/3rdparty/sylvan/src/CMakeLists.txt index 50a645f22..eb27a6fc4 100644 --- a/resources/3rdparty/sylvan/src/CMakeLists.txt +++ b/resources/3rdparty/sylvan/src/CMakeLists.txt @@ -13,6 +13,8 @@ add_library(sylvan sha2.c stats.h stats.c + storm_function_wrapper.h + storm_function_wrapper.cpp sylvan.h sylvan_bdd.h sylvan_bdd.c @@ -30,6 +32,8 @@ add_library(sylvan sylvan_mtbdd_int.h sylvan_obj.hpp sylvan_obj.cpp + sylvan_storm_rational_function.h + sylvan_storm_rational_function.c tls.h ) @@ -42,6 +46,11 @@ set_target_properties(sylvan PROPERTIES target_link_libraries(sylvan m pthread) +if(USE_CARL) + message(STATUS "Sylvan - linking CARL.") + target_link_libraries(sylvan ${carl_LIBRARIES}) +endif(USE_CARL) + if(UNIX AND NOT APPLE) target_link_libraries(sylvan rt) endif() diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp new file mode 100644 index 000000000..6cd79305e --- /dev/null +++ b/resources/3rdparty/sylvan/src/storm_function_wrapper.cpp @@ -0,0 +1,206 @@ +#include "storm_function_wrapper.h" + +#include +#include +#include +#include "src/adapters/CarlAdapter.h" + +#undef DEBUG_STORM_FUNCTION_WRAPPER + +#ifdef DEBUG_STORM_FUNCTION_WRAPPER +#define LOG_I(funcName) std::cout << "Entering function " << funcName << std::endl; +#define LOG_O(funcName) std::cout << "Leaving function " << funcName << std::endl; +#else +#define LOG_I(funcName) +#define LOG_O(funcName) +#endif + +void storm_rational_function_init(storm_rational_function_ptr* a) { + LOG_I("init") +#ifdef DEBUG_STORM_FUNCTION_WRAPPER + std::cout << "storm_rational_function_init - ptr of old = " << *a << ", value = " << *((storm::RationalFunction*)(*a)) << std::endl; +#endif + storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a))); + + if (srf_ptr == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_init()!" << std::endl; + return; + } + + *a = srf_ptr; +#ifdef DEBUG_STORM_FUNCTION_WRAPPER + std::cout << "storm_rational_function_init - ptr of new = " << *a << ", value = " << *((storm::RationalFunction*)(*a)) << std::endl; +#endif + LOG_O("init") +} + +void storm_rational_function_destroy(storm_rational_function_ptr a) { + LOG_I("destroy") + delete (storm::RationalFunction*)a; + LOG_O("destroy") +} + +int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b) { + LOG_I("equals") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + + LOG_O("equals") + + int result = 0; + if (srf_a == srf_b) { + result = 1; + } + +#ifdef DEBUG_STORM_FUNCTION_WRAPPER + std::cout << "storm_rational_function_equals called with ptr = " << a << " value a = " << srf_a << " and ptr = " << b << " value b = " << srf_b << " result = " << result << "." << std::endl; +#endif + + return result; +} + +storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b) { + LOG_I("plus") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_plus()!" << std::endl; + return (storm_rational_function_ptr)nullptr; + } + + *result_srf += srf_b; + + storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; + + LOG_O("plus") + return result; +} + +storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b) { + LOG_I("minus") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_minus()!" << std::endl; + return (storm_rational_function_ptr)nullptr; + } + + *result_srf -= srf_b; + + storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; + + LOG_O("minus") + return result; +} + +storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b) { + LOG_I("times") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_times()!" << std::endl; + return (storm_rational_function_ptr)nullptr; + } + + *result_srf *= srf_b; + + storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; + + LOG_O("times") + return result; +} + +storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b) { + LOG_I("divide") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + storm::RationalFunction& srf_b = *(storm::RationalFunction*)b; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_divide()!" << std::endl; + return (storm_rational_function_ptr)nullptr; + } + + *result_srf /= srf_b; + + storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; + + LOG_O("divide") + return result; +} + +uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) { + LOG_I("hash") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + + size_t hash = carl::hash_value(srf_a); + +#ifdef DEBUG_STORM_FUNCTION_WRAPPER + std::cout << "storm_rational_function_hash of value " << srf_a << " is " << hash << std::endl; +#endif + + uint64_t result = hash ^ seed; + + LOG_O("hash") + return result; +} + +storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a) { + LOG_I("negate") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); + if (result_srf == nullptr) { + std::cerr << "Could not allocate memory in storm_rational_function_negate()!" << std::endl; + return (storm_rational_function_ptr)nullptr; + } + + *result_srf = -srf_a; + + storm_rational_function_ptr result = (storm_rational_function_ptr)result_srf; + + LOG_O("negate") + return result; +} + +int storm_rational_function_is_zero(storm_rational_function_ptr a) { + LOG_I("isZero") + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + + if (srf_a.isZero()) { + return 1; + } else { + return 0; + } +} + +storm_rational_function_ptr storm_rational_function_get_zero() { + static storm::RationalFunction zeroFunction(0); + LOG_I("getZero") + return (storm_rational_function_ptr)(&zeroFunction); +} + +storm_rational_function_ptr storm_rational_function_get_one() { + static storm::RationalFunction oneFunction(1); + LOG_I("getOne") + return (storm_rational_function_ptr)(&oneFunction); +} + +void print_storm_rational_function(storm_rational_function_ptr a) { + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + std::cout << srf_a << std::flush; +} + +void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out) { + std::stringstream ss; + storm::RationalFunction& srf_a = *(storm::RationalFunction*)a; + ss << srf_a; + std::string s = ss.str(); + fprintf(out, "%s", s.c_str()); +} diff --git a/resources/3rdparty/sylvan/src/storm_function_wrapper.h b/resources/3rdparty/sylvan/src/storm_function_wrapper.h new file mode 100644 index 000000000..ca5107dcb --- /dev/null +++ b/resources/3rdparty/sylvan/src/storm_function_wrapper.h @@ -0,0 +1,37 @@ +#ifndef SYLVAN_STORM_FUNCTION_WRAPPER_H +#define SYLVAN_STORM_FUNCTION_WRAPPER_H + +#include +#include + +#ifdef __cplusplus +extern "C" { +#endif + +typedef void* storm_rational_function_ptr; + +// equals, plus, minus, divide, times, create, destroy +void storm_rational_function_init(storm_rational_function_ptr* a); +void storm_rational_function_destroy(storm_rational_function_ptr a); +int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational_function_ptr b); +storm_rational_function_ptr storm_rational_function_plus(storm_rational_function_ptr a, storm_rational_function_ptr b); +storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b); +storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b); +storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b); +storm_rational_function_ptr storm_rational_function_negate(storm_rational_function_ptr a); +uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed); +int storm_rational_function_is_zero(storm_rational_function_ptr a); + +storm_rational_function_ptr storm_rational_function_get_zero(); +storm_rational_function_ptr storm_rational_function_get_one(); + +void print_storm_rational_function(storm_rational_function_ptr a); +void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* out); + +int storm_rational_function_is_zero(storm_rational_function_ptr a); + +#ifdef __cplusplus +} +#endif + +#endif // SYLVAN_STORM_FUNCTION_WRAPPER_H diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd.c b/resources/3rdparty/sylvan/src/sylvan_bdd.c index 74936a62d..6b6b3f74f 100644 --- a/resources/3rdparty/sylvan/src/sylvan_bdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_bdd.c @@ -2818,3 +2818,5 @@ TASK_IMPL_1(int, sylvan_test_isbdd, BDD, bdd) if (!SYNC(sylvan_test_isbdd_rec)) result = 0; return result; } + +#include "sylvan_bdd_storm.c" diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c new file mode 100644 index 000000000..ff9fddc48 --- /dev/null +++ b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c @@ -0,0 +1,171 @@ +/* */ + +/** + * Calculates \exists variables . a + */ +TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, prev_level) +{ + int aIsNegated = (a & sylvan_complement) == ((uint64_t)0) ? 0 : 1; + + BDD aRegular = (aIsNegated) ? sylvan_not(a) : a; + + if (aRegular == sylvan_false) { + if (aIsNegated) { + if (sylvan_set_isempty(variables)) { + //printf("return in preprocessing...2\n"); + return sylvan_true; + } else { + //printf("return in preprocessing...3\n"); + BDD _v = sylvan_set_next(variables); + BDD res = CALL(sylvan_existsRepresentative, a, _v, prev_level); + if (res == sylvan_invalid) { + return sylvan_invalid; + } + sylvan_ref(res); + + BDD res1 = sylvan_ite(sylvan_ithvar(bddnode_getvariable(GETNODE(variables))), sylvan_false, res); + if (res1 == sylvan_invalid) { + sylvan_deref(res); + return sylvan_invalid; + } + sylvan_deref(res); + return res1; + } + } else { + return a; + } + } else if (sylvan_set_isempty(variables)) { + //printf("return in preprocessing...4\n"); + return a; + } + /* From now on, f and cube are non-constant. */ + bddnode_t na = GETNODE(a); + BDDVAR level = bddnode_getvariable(na); + + bddnode_t nv = GETNODE(variables); + BDDVAR vv = bddnode_getvariable(nv); + + //printf("a level %i and cube level %i\n", level, vv); + + /* Abstract a variable that does not appear in f. */ + if (level > vv) { + BDD _v = sylvan_set_next(variables); + BDD res = CALL(sylvan_existsRepresentative, a, _v, level); + if (res == sylvan_invalid) { + return sylvan_invalid; + } + sylvan_ref(res); + + BDD res1 = sylvan_ite(sylvan_ithvar(vv), sylvan_false, res); + + if (res1 == sylvan_invalid) { + sylvan_deref(res); + return sylvan_invalid; + } + sylvan_deref(res); + + //printf("return after abstr. var that does not appear in f...\n"); + return res1; + } + + /* Compute the cofactors of a. */ + BDD aLow = node_low(a, na); // ELSE + BDD aHigh = node_high(a, na); // THEN + + /* If the two indices are the same, so are their levels. */ + if (level == vv) { + BDD _v = sylvan_set_next(variables); + BDD res1 = CALL(sylvan_existsRepresentative, aLow, _v, level); + if (res1 == sylvan_invalid) { + return sylvan_invalid; + } + if (res1 == sylvan_true) { + return sylvan_not(variables); + } + sylvan_ref(res1); + + BDD res2 = CALL(sylvan_existsRepresentative, aHigh, _v, level); + if (res2 == sylvan_invalid) { + sylvan_deref(res1); + return sylvan_invalid; + } + sylvan_ref(res2); + + BDD left = CALL(sylvan_exists, aLow, _v, 0); + if (left == sylvan_invalid) { + sylvan_deref(res1); + sylvan_deref(res2); + return sylvan_invalid; + } + sylvan_ref(left); + + BDD res1Inf = sylvan_ite(left, res1, sylvan_false); + if (res1Inf == sylvan_invalid) { + sylvan_deref(res1); + sylvan_deref(res2); + sylvan_deref(left); + return sylvan_invalid; + } + sylvan_ref(res1Inf); + sylvan_deref(res1); + + BDD res2Inf = sylvan_ite(left, sylvan_false, res2); + if (res2Inf == sylvan_invalid) { + sylvan_deref(res2); + sylvan_deref(left); + sylvan_deref(res1Inf); + return sylvan_invalid; + } + sylvan_ref(res2Inf); + sylvan_deref(res2); + sylvan_deref(left); + + assert(res1Inf != res2Inf); + BDD res = sylvan_ite(sylvan_ithvar(level), res2Inf, res1Inf); + if (res == sylvan_invalid) { + sylvan_deref(res1Inf); + sylvan_deref(res2Inf); + return sylvan_invalid; + } + + // cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, res); + // TODO: CACHING HERE + + sylvan_deref(res1Inf); + sylvan_deref(res2Inf); + + //printf("return properly computed result...\n"); + return res; + } else { /* if (level == vv) */ + BDD res1 = CALL(sylvan_existsRepresentative, aLow, variables, level); + if (res1 == sylvan_invalid){ + return sylvan_invalid; + } + sylvan_ref(res1); + + BDD res2 = CALL(sylvan_existsRepresentative, aHigh, variables, level); + if (res2 == sylvan_invalid) { + sylvan_deref(res1); + return sylvan_invalid; + } + sylvan_ref(res2); + + /* ITE takes care of possible complementation of res1 and of the + ** case in which res1 == res2. */ + BDD res = sylvan_ite(sylvan_ithvar(level), res2, res1); + if (res == sylvan_invalid) { + sylvan_deref(res1); + sylvan_deref(res2); + return sylvan_invalid; + } + + sylvan_deref(res1); + sylvan_deref(res2); + + //printf("return of last case...\n"); + return res; + } + + // Prevent unused variable warning + (void)prev_level; +} diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd_storm.h b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.h index 5806fba5d..f28259a84 100644 --- a/resources/3rdparty/sylvan/src/sylvan_bdd_storm.h +++ b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.h @@ -1,3 +1,6 @@ #define bdd_isnegated(dd) ((dd & sylvan_complement) ? 1 : 0) #define bdd_regular(dd) (dd & ~sylvan_complement) -#define bdd_isterminal(dd) (dd == sylvan_false || dd == sylvan_true) \ No newline at end of file +#define bdd_isterminal(dd) (dd == sylvan_false || dd == sylvan_true) + +TASK_DECL_3(BDD, sylvan_existsRepresentative, BDD, BDD, BDDVAR); +#define sylvan_existsRepresentative(a, vars) (CALL(sylvan_existsRepresentative, a, vars, 0)) diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index a4eb1bd62..ac5a8261f 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -31,6 +31,11 @@ #include #include +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) +#include +#include +#endif + /* Primitives */ int mtbdd_isleaf(MTBDD bdd) @@ -264,9 +269,15 @@ _mtbdd_create_cb(uint64_t *a, uint64_t *b) // for leaf if ((*a & 0x4000000000000000) == 0) return; // huh? uint32_t type = *a & 0xffffffff; - if (type >= cl_registry_count) return; // not in registry + if (type >= cl_registry_count) { // not in registry + printf("ERROR: type >= cl_registry_count!"); + return; + } customleaf_t *c = cl_registry + type; - if (c->create_cb == NULL) return; // not in registry + if (c->create_cb == NULL) { // not in registry + printf("ERROR: create_cb is NULL!"); + return; + } c->create_cb(b); } @@ -276,9 +287,15 @@ _mtbdd_destroy_cb(uint64_t a, uint64_t b) // for leaf if ((a & 0x4000000000000000) == 0) return; // huh? uint32_t type = a & 0xffffffff; - if (type >= cl_registry_count) return; // not in registry + if (type >= cl_registry_count) { // not in registry + printf("ERROR: type >= cl_registry_count! (2)"); + return; + } customleaf_t *c = cl_registry + type; - if (c->destroy_cb == NULL) return; // not in registry + if (c->destroy_cb == NULL) { // not in registry + printf("ERROR: destroy_cb is NULL!"); + return; + } c->destroy_cb(b); } @@ -833,6 +850,11 @@ TASK_2(MTBDD, mtbdd_uop_times_uint, MTBDD, a, size_t, k) uint32_t c = gcd(d, (uint32_t)k); return mtbdd_fraction(n*(k/c), d/c); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_uop_times_uint type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + } +#endif } return mtbdd_invalid; @@ -857,6 +879,11 @@ TASK_2(MTBDD, mtbdd_uop_pow_uint, MTBDD, a, size_t, k) uint64_t v = mtbddnode_getvalue(na); return mtbdd_fraction(pow((int32_t)(v>>32), k), (uint32_t)v); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_uop_pow_uint type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + } +#endif } return mtbdd_invalid; @@ -1017,6 +1044,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_plus, MTBDD*, pa, MTBDD*, pb) // add return mtbdd_fraction(nom_a + nom_b, denom_a); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_plus type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + } +#endif } if (a < b) { @@ -1066,6 +1098,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_minus, MTBDD*, pa, MTBDD*, pb) // subtract return mtbdd_fraction(nom_a - nom_b, denom_a); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) && (mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_minus type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + } +#endif } return mtbdd_invalid; @@ -1113,6 +1150,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_times, MTBDD*, pa, MTBDD*, pb) denom_a *= (denom_b/d); return mtbdd_fraction(nom_a, denom_a); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) && (mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_times type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + } +#endif } if (a < b) { @@ -1169,6 +1211,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_min, MTBDD*, pa, MTBDD*, pb) // compute lowest return nom_a < nom_b ? a : b; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) && (mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_min type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + } +#endif } if (a < b) { @@ -1223,6 +1270,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_max, MTBDD*, pa, MTBDD*, pb) // compute highest return nom_a > nom_b ? a : b; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) && (mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_max type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + } +#endif } if (a < b) { @@ -1252,6 +1304,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_negate, MTBDD, a, size_t, k) uint64_t v = mtbddnode_getvalue(na); return mtbdd_fraction(-(int32_t)(v>>32), (uint32_t)v); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_negate type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + } +#endif } return mtbdd_invalid; @@ -1335,6 +1392,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_threshold_double, MTBDD, a, size_t, svalue) d /= mtbdd_getdenom(a); return d >= value ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_threshold_double type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + } +#endif } return mtbdd_invalid; @@ -1361,6 +1423,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_strict_threshold_double, MTBDD, a, size_t, svalue) d /= mtbdd_getdenom(a); return d > value ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_strict_threshold_double type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + } +#endif } return mtbdd_invalid; @@ -1566,6 +1633,11 @@ TASK_3(MTBDD, mtbdd_leq_rec, MTBDD, a, MTBDD, b, int*, shortcircuit) nom_b *= da/c; result = nom_a <= nom_b ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR: mtbdd_leq_rec type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n"); + } +#endif } else { /* Get top variable */ uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); @@ -1651,6 +1723,11 @@ TASK_3(MTBDD, mtbdd_less_rec, MTBDD, a, MTBDD, b, int*, shortcircuit) nom_b *= da/c; result = nom_a < nom_b ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR: mtbdd_less_rec type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n"); + } +#endif } else { /* Get top variable */ uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); @@ -1736,6 +1813,11 @@ TASK_3(MTBDD, mtbdd_geq_rec, MTBDD, a, MTBDD, b, int*, shortcircuit) nom_b *= da/c; result = nom_a >= nom_b ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR: mtbdd_geq_rec type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n"); + } +#endif } else { /* Get top variable */ uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); @@ -1821,6 +1903,11 @@ TASK_3(MTBDD, mtbdd_greater_rec, MTBDD, a, MTBDD, b, int*, shortcircuit) nom_b *= da/c; result = nom_a > nom_b ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR: mtbdd_greater_rec type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n"); + } +#endif } else { /* Get top variable */ uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); @@ -2041,6 +2128,11 @@ TASK_IMPL_1(MTBDD, mtbdd_minimum, MTBDD, a) nom_h *= denom_l/c; result = nom_l < nom_h ? low : high; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(nl) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nh) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR: mtbdd_minimum type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n"); + } +#endif /* Store in cache */ cache_put3(CACHE_MTBDD_MINIMUM, a, 0, 0, result); @@ -2089,6 +2181,11 @@ TASK_IMPL_1(MTBDD, mtbdd_maximum, MTBDD, a) nom_h *= denom_l/c; result = nom_l > nom_h ? low : high; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(nl) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nh) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR: mtbdd_maximum type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\n"); + } +#endif /* Store in cache */ cache_put3(CACHE_MTBDD_MAXIMUM, a, 0, 0, result); @@ -2237,12 +2334,20 @@ mtbdd_unmark_rec(MTBDD mtbdd) static size_t mtbdd_leafcount_mark(MTBDD mtbdd) { - if (mtbdd == mtbdd_true) return 0; // do not count true/false leaf - if (mtbdd == mtbdd_false) return 0; // do not count true/false leaf + if (mtbdd == mtbdd_true) { // do not count true/false leaf + return 0; + } + if (mtbdd == mtbdd_false) { // do not count true/false leaf + return 0; + } mtbddnode_t n = GETNODE(mtbdd); - if (mtbddnode_getmark(n)) return 0; + if (mtbddnode_getmark(n)) { + return 0; + } mtbddnode_setmark(n, 1); - if (mtbddnode_isleaf(n)) return 1; // count leaf as 1 + if (mtbddnode_isleaf(n)) { // count leaf as 1 + return 1; + } return mtbdd_leafcount_mark(mtbddnode_getlow(n)) + mtbdd_leafcount_mark(mtbddnode_gethigh(n)); } @@ -2372,6 +2477,12 @@ mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd, print_terminal_label_cb cb) case 2: fprintf(out, "%u/%u", (uint32_t)(value>>32), (uint32_t)value); break; +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + case SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID: + fprintf(out, "srf::"); + print_storm_rational_function_to_file((storm_rational_function_ptr)value, out); + break; +#endif default: cb(out, type, value); break; diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h index 1a7de3f57..60d484f50 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h @@ -307,7 +307,7 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_max, MTBDD, MTBDD, int); * must be a Boolean MTBDD (or standard BDD). */ TASK_DECL_3(MTBDD, mtbdd_ite, MTBDD, MTBDD, MTBDD); -#define mtbdd_ite(f, g, h) CALL(mtbdd_ite, f, g, h); +#define mtbdd_ite(f, g, h) CALL(mtbdd_ite, f, g, h) /** * Multiply and , and abstract variables using summation. diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c index dab4860c0..87e9bb590 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c @@ -97,6 +97,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb) MTBDD result = mtbdd_fraction(nom_a, denom_a); return result; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_divide type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } return mtbdd_invalid; @@ -140,6 +146,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_equals, MTBDD*, pa, MTBDD*, pb) if (nom_a == nom_b && denom_a == denom_b) return mtbdd_true; return mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_equals type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } if (a < b) { @@ -187,6 +199,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less, MTBDD*, pa, MTBDD*, pb) uint64_t denom_b = val_b&0xffffffff; return nom_a * denom_b < nom_b * denom_a ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_less type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } return mtbdd_invalid; @@ -230,6 +248,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, pa, MTBDD*, pb) nom_b *= denom_a; return nom_a <= nom_b ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_less_or_equal type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } return mtbdd_invalid; @@ -261,6 +285,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_pow, MTBDD*, pa, MTBDD*, pb) } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) { assert(0); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_pow type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } return mtbdd_invalid; @@ -292,6 +322,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_mod, MTBDD*, pa, MTBDD*, pb) } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) { assert(0); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_mod type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } return mtbdd_invalid; @@ -323,6 +359,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_logxy, MTBDD*, pa, MTBDD*, pb) } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) { assert(0); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID && mtbddnode_gettype(nb) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_logxy type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } return mtbdd_invalid; @@ -345,6 +387,11 @@ TASK_IMPL_2(MTBDD, mtbdd_op_not_zero, MTBDD, a, size_t, v) } else if (mtbddnode_gettype(na) == 2) { return mtbdd_getnumer(a) != 0 ? mtbdd_true : mtbdd_false; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + return storm_rational_function_is_zero((storm_rational_function_ptr)mtbdd_getvalue(a)) == 0 ? mtbdd_true : mtbdd_false; + } +#endif } // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). @@ -377,6 +424,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_floor, MTBDD, a, size_t, v) MTBDD result = mtbdd_fraction(mtbdd_getnumer(a) / mtbdd_getdenom(a), 1); return result; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_floor type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). @@ -409,6 +462,12 @@ TASK_IMPL_2(MTBDD, mtbdd_op_ceil, MTBDD, a, size_t, v) MTBDD result = mtbdd_fraction(mtbdd_getnumer(a) / mtbdd_getdenom(a) + 1, 1); return result; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + printf("ERROR mtbdd_op_ceil type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID"); + assert(0); + } +#endif } // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). @@ -474,6 +533,11 @@ TASK_IMPL_2(double, mtbdd_non_zero_count, MTBDD, dd, size_t, nvars) } else if (mtbddnode_gettype(na) == 2) { return mtbdd_getnumer(dd) != 0 ? powl(2.0L, nvars) : 0.0; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + return storm_rational_function_is_zero((storm_rational_function_ptr)mtbdd_getvalue(dd)) == 0 ? powl(2.0L, nvars) : 0.0; + } +#endif } /* Perhaps execute garbage collection */ @@ -506,9 +570,237 @@ int mtbdd_iszero(MTBDD dd) { } else if (mtbdd_gettype(dd) == 2) { return mtbdd_getnumer(dd) == 0; } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if (mtbdd_gettype(dd) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID) { + return storm_rational_function_is_zero((storm_rational_function_ptr)mtbdd_getvalue(dd)) == 1 ? 1 : 0; + } +#endif return 0; } int mtbdd_isnonzero(MTBDD dd) { return mtbdd_iszero(dd) ? 0 : 1; -} \ No newline at end of file +} + +MTBDD +mtbdd_ithvar(uint32_t level) { + return mtbdd_makenode(level, mtbdd_false, mtbdd_true); +} + +TASK_IMPL_2(MTBDD, mtbdd_op_complement, MTBDD, a, size_t, k) +{ + // if a is false, then it is a partial function. Keep partial! + if (a == mtbdd_false) return mtbdd_false; + + // a != constant + mtbddnode_t na = GETNODE(a); + + if (mtbddnode_isleaf(na)) { + if (mtbddnode_gettype(na) == 0) { + int64_t v = mtbdd_getint64(a); + if (v == 0) { + return mtbdd_int64(1); + } else { + return mtbdd_int64(0); + } + } else if (mtbddnode_gettype(na) == 1) { + double d = mtbdd_getdouble(a); + if (d == 0.0) { + return mtbdd_double(1.0); + } else { + return mtbdd_double(0.0); + } + } else if (mtbddnode_gettype(na) == 2) { + printf("ERROR: mtbdd_op_complement type FRACTION.\n"); + assert(0); + } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + else if ((mtbddnode_gettype(na) == SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID)) { + printf("ERROR: mtbdd_op_complement type SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID.\n"); + assert(0); + } +#endif + } + + return mtbdd_invalid; + (void)k; // unused variable +} + +TASK_IMPL_3(MTBDD, mtbdd_minExistsRepresentative, MTBDD, a, MTBDD, variables, uint32_t, prev_level) { + MTBDD zero = mtbdd_false; + + /* Maybe perform garbage collection */ + sylvan_gc_test(); + + /* Cube is guaranteed to be a cube at this point. */ + if (mtbdd_isleaf(a)) { + if (mtbdd_set_isempty(variables)) { + return a; // FIXME? + } else { + return variables; + } + } + + mtbddnode_t na = GETNODE(a); + uint32_t va = mtbddnode_getvariable(na); + mtbddnode_t nv = GETNODE(variables); + uint32_t vv = mtbddnode_getvariable(nv); + + /* Abstract a variable that does not appear in a. */ + if (va > vv) { + MTBDD _v = mtbdd_set_next(variables); + MTBDD res = CALL(mtbdd_minExistsRepresentative, a, _v, va); + if (res == mtbdd_invalid) { + return mtbdd_invalid; + } + + // Fill in the missing variables to make representative unique. + mtbdd_ref(res); + MTBDD res1 = mtbdd_ite(mtbdd_ithvar(vv), zero, res); + if (res1 == mtbdd_invalid) { + mtbdd_deref(res); + return mtbdd_invalid; + } + mtbdd_deref(res); + return res1; + } + + /* TODO: Caching here. */ + /*if ((res = cuddCacheLookup2(manager, Cudd_addMinAbstractRepresentative, f, cube)) != NULL) { + return(res); + }*/ + + + MTBDD E = mtbdd_getlow(a); + MTBDD T = mtbdd_gethigh(a); + + /* If the two indices are the same, so are their levels. */ + if (va == vv) { + MTBDD _v = mtbdd_set_next(variables); + MTBDD res1 = CALL(mtbdd_minExistsRepresentative, E, _v, va); + if (res1 == mtbdd_invalid) { + return mtbdd_invalid; + } + mtbdd_ref(res1); + + MTBDD res2 = CALL(mtbdd_minExistsRepresentative, T, _v, va); + if (res2 == mtbdd_invalid) { + mtbdd_deref(res1); + return mtbdd_invalid; + } + mtbdd_ref(res2); + + MTBDD left = mtbdd_abstract_min(E, _v); + if (left == mtbdd_invalid) { + mtbdd_deref(res1); + mtbdd_deref(res2); + return mtbdd_invalid; + } + mtbdd_ref(left); + + MTBDD right = mtbdd_abstract_min(T, _v); + if (right == mtbdd_invalid) { + mtbdd_deref(res1); + mtbdd_deref(res2); + mtbdd_deref(left); + return mtbdd_invalid; + } + mtbdd_ref(right); + + MTBDD tmp = mtbdd_less_or_equal_as_bdd(left, right); + if (tmp == mtbdd_invalid) { + mtbdd_deref(res1); + mtbdd_deref(res2); + mtbdd_deref(left); + mtbdd_deref(right); + return mtbdd_invalid; + } + mtbdd_ref(tmp); + + mtbdd_deref(left); + mtbdd_deref(right); + + MTBDD res1Inf = mtbdd_ite(tmp, res1, zero); + if (res1Inf == mtbdd_invalid) { + mtbdd_deref(res1); + mtbdd_deref(res2); + mtbdd_deref(tmp); + return mtbdd_invalid; + } + mtbdd_ref(res1Inf); + mtbdd_deref(res1); + + MTBDD tmp2 = mtbdd_get_complement(tmp); + if (tmp2 == mtbdd_invalid) { + mtbdd_deref(res2); + mtbdd_deref(left); + mtbdd_deref(right); + mtbdd_deref(tmp); + return mtbdd_invalid; + } + mtbdd_ref(tmp2); + mtbdd_deref(tmp); + + MTBDD res2Inf = mtbdd_ite(tmp2, res2, zero); + if (res2Inf == mtbdd_invalid) { + mtbdd_deref(res2); + mtbdd_deref(res1Inf); + mtbdd_deref(tmp2); + return mtbdd_invalid; + } + mtbdd_ref(res2Inf); + mtbdd_deref(res2); + mtbdd_deref(tmp2); + + MTBDD res = (res1Inf == res2Inf) ? mtbdd_ite(mtbdd_ithvar(va), zero, res1Inf) : mtbdd_ite(mtbdd_ithvar(va), res2Inf, res1Inf); + + if (res == mtbdd_invalid) { + mtbdd_deref(res1Inf); + mtbdd_deref(res2Inf); + return mtbdd_invalid; + } + mtbdd_ref(res); + mtbdd_deref(res1Inf); + mtbdd_deref(res2Inf); + + /* TODO: Caching here. */ + //cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res); + + mtbdd_deref(res); + return res; + } + else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */ + MTBDD res1 = CALL(mtbdd_minExistsRepresentative, E, variables, va); + if (res1 == mtbdd_invalid) { + return mtbdd_invalid; + } + mtbdd_ref(res1); + MTBDD res2 = CALL(mtbdd_minExistsRepresentative, T, variables, va); + if (res2 == mtbdd_invalid) { + mtbdd_deref(res1); + return mtbdd_invalid; + } + mtbdd_ref(res2); + + MTBDD res = (res1 == res2) ? mtbdd_ite(mtbdd_ithvar(va), zero, res1) : mtbdd_ite(mtbdd_ithvar(va), res2, res1); + if (res == mtbdd_invalid) { + mtbdd_deref(res1); + mtbdd_deref(res2); + return mtbdd_invalid; + } + mtbdd_deref(res1); + mtbdd_deref(res2); + /* TODO: Caching here. */ + //cuddCacheInsert2(manager, Cudd_addMinAbstractRepresentative, f, cube, res); + return res; + } + + // Prevent unused variable warning + (void)prev_level; +} + +TASK_IMPL_3(MTBDD, mtbdd_maxExistsRepresentative, MTBDD, a, MTBDD, variables, uint32_t, prev_level) { + (void)variables; + (void)prev_level; + return a; +} diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h index 38fa6668b..d1119438b 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h @@ -6,7 +6,7 @@ void mtbdd_getsha(MTBDD mtbdd, char *target); // target must be at least 65 byte * If either operand is mtbdd_false (not defined), * then the result is mtbdd_false (i.e. not defined). */ -TASK_DECL_2(MTBDD, mtbdd_op_divide, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, mtbdd_op_divide, MTBDD*, MTBDD*) #define mtbdd_divide(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_divide)) /** @@ -15,7 +15,7 @@ TASK_DECL_2(MTBDD, mtbdd_op_divide, MTBDD*, MTBDD*); * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), * then the result is the other operand. */ -TASK_DECL_2(MTBDD, mtbdd_op_equals, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, mtbdd_op_equals, MTBDD*, MTBDD*) #define mtbdd_equals(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_equals)) /** @@ -24,7 +24,7 @@ TASK_DECL_2(MTBDD, mtbdd_op_equals, MTBDD*, MTBDD*); * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), * then the result is the other operand. */ -TASK_DECL_2(MTBDD, mtbdd_op_less, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, mtbdd_op_less, MTBDD*, MTBDD*) #define mtbdd_less_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less)) /** @@ -33,7 +33,7 @@ TASK_DECL_2(MTBDD, mtbdd_op_less, MTBDD*, MTBDD*); * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), * then the result is the other operand. */ -TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*) #define mtbdd_less_or_equal_as_bdd(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_less_or_equal)) /** @@ -42,7 +42,7 @@ TASK_DECL_2(MTBDD, mtbdd_op_less_or_equal, MTBDD*, MTBDD*); * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), * then the result is the other operand. */ -TASK_DECL_2(MTBDD, mtbdd_op_pow, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, mtbdd_op_pow, MTBDD*, MTBDD*) #define mtbdd_pow(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_pow)) /** @@ -51,7 +51,7 @@ TASK_DECL_2(MTBDD, mtbdd_op_pow, MTBDD*, MTBDD*); * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), * then the result is the other operand. */ -TASK_DECL_2(MTBDD, mtbdd_op_mod, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, mtbdd_op_mod, MTBDD*, MTBDD*) #define mtbdd_mod(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_mod)) /** @@ -60,7 +60,7 @@ TASK_DECL_2(MTBDD, mtbdd_op_mod, MTBDD*, MTBDD*); * For Integer/Double MTBDD, if either operand is mtbdd_false (not defined), * then the result is the other operand. */ -TASK_DECL_2(MTBDD, mtbdd_op_logxy, MTBDD*, MTBDD*); +TASK_DECL_2(MTBDD, mtbdd_op_logxy, MTBDD*, MTBDD*) #define mtbdd_logxy(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_logxy)) /** @@ -71,14 +71,14 @@ TASK_DECL_1(MTBDD, mtbdd_not_zero, MTBDD) #define mtbdd_not_zero(dd) CALL(mtbdd_not_zero, dd) /** - * Monad that floors all values Double and Fraction values. + * Monad that floors all Double and Fraction values. */ TASK_DECL_2(MTBDD, mtbdd_op_floor, MTBDD, size_t) TASK_DECL_1(MTBDD, mtbdd_floor, MTBDD) #define mtbdd_floor(dd) CALL(mtbdd_floor, dd) /** - * Monad that ceils all values Double and Fraction values. + * Monad that ceils all Double and Fraction values. */ TASK_DECL_2(MTBDD, mtbdd_op_ceil, MTBDD, size_t) TASK_DECL_1(MTBDD, mtbdd_ceil, MTBDD) @@ -101,7 +101,7 @@ TASK_DECL_1(MTBDD, mtbdd_bool_to_int64, MTBDD) /** * Count the number of assignments (minterms) leading to a non-zero */ -TASK_DECL_2(double, mtbdd_non_zero_count, MTBDD, size_t); +TASK_DECL_2(double, mtbdd_non_zero_count, MTBDD, size_t) #define mtbdd_non_zero_count(dd, nvars) CALL(mtbdd_non_zero_count, dd, nvars) // Checks whether the given MTBDD (does represents a zero leaf. @@ -109,3 +109,33 @@ int mtbdd_iszero(MTBDD); int mtbdd_isnonzero(MTBDD); #define mtbdd_regular(dd) (dd & ~mtbdd_complement) + +#define mtbdd_set_next(set) (mtbdd_gethigh(set)) +#define mtbdd_set_isempty(set) (set == mtbdd_true) + +/* Create a MTBDD representing just or the negation of */ +MTBDD mtbdd_ithvar(uint32_t var); + +/** + * Unary operation Complement. + * Supported domains: Integer, Real + */ +TASK_DECL_2(MTBDD, mtbdd_op_complement, MTBDD, size_t); + +/** + * Compute the complement of a. + */ +#define mtbdd_get_complement(a) mtbdd_uapply(a, TASK(mtbdd_op_complement), 0) + +/** + * 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(MTBDD, mtbdd_minExistsRepresentative, MTBDD, MTBDD, uint32_t); +#define mtbdd_minExistsRepresentative(a, vars) (CALL(mtbdd_minExistsRepresentative, 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(MTBDD, mtbdd_maxExistsRepresentative, MTBDD, MTBDD, uint32_t); +#define mtbdd_maxExistsRepresentative(a, vars) (CALL(mtbdd_maxExistsRepresentative, a, vars, 0)) + diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.cpp b/resources/3rdparty/sylvan/src/sylvan_obj.cpp index a573c7a49..b9d0c77f2 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.cpp @@ -15,6 +15,7 @@ */ #include +#include using namespace sylvan; @@ -604,6 +605,15 @@ Mtbdd::doubleTerminal(double value) return mtbdd_double(value); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) +Mtbdd +Mtbdd::stormRationalFunctionTerminal(storm::RationalFunction const& value) +{ + storm_rational_function_ptr ptr = (storm_rational_function_ptr)(&value); + return mtbdd_storm_rational_function(ptr); +} +#endif + Mtbdd Mtbdd::fractionTerminal(int64_t nominator, uint64_t denominator) { @@ -1028,6 +1038,7 @@ void Sylvan::initMtbdd() { sylvan_init_mtbdd(); + sylvan_storm_rational_function_init(); } void diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp index e7f77f6ca..6cd81a2fb 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.hpp @@ -23,6 +23,8 @@ #include #include +#include "src/adapters/CarlAdapter.h" + namespace sylvan { class BddSet; @@ -542,6 +544,13 @@ public: */ static Mtbdd doubleTerminal(double value); +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + /** + * @brief Creates a Mtbdd leaf representing the rational function value + */ + static Mtbdd stormRationalFunctionTerminal(storm::RationalFunction const& value); +#endif + /** * @brief Creates a Mtbdd leaf representing the fraction value / * Internally, Sylvan uses 32-bit values and reports overflows to stderr. diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp index 393ce988c..afcc027e6 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_bdd_storm.hpp @@ -1,3 +1,7 @@ Mtbdd toDoubleMtbdd() const; Mtbdd toInt64Mtbdd() const; +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + Mtbdd toStormRationalFunctionMtbdd() const; +#endif Mtbdd Ite(Mtbdd const& thenDd, Mtbdd const& elseDd) const; + Bdd ExistAbstractRepresentative(const BddSet& cube) const; diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp index 26e5ea4be..87ab6735e 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp @@ -8,6 +8,40 @@ */ Mtbdd Divide(const Mtbdd &other) const; +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + /** + * @brief Computes f + g for Rational Functions + */ + Mtbdd PlusRF(const Mtbdd &other) const; + + /** + * @brief Computes f * g for Rational Functions + */ + Mtbdd TimesRF(const Mtbdd &other) const; + + /** + * @brief Computes f - g for Rational Functions + */ + Mtbdd MinusRF(const Mtbdd &other) const; + + /** + * @brief Computes f / g for Rational Functions + */ + Mtbdd DivideRF(const Mtbdd &other) const; + + Mtbdd AbstractPlusRF(const BddSet &variables) const; +#endif + + /** + * @brief Computes abstraction by minimum + */ + Mtbdd AbstractMinRepresentative(const BddSet &variables) const; + + /** + * @brief Computes abstraction by maximum + */ + Mtbdd AbstractMaxRepresentative(const BddSet &variables) const; + Bdd NotZero() const; Bdd Equals(const Mtbdd& other) const; diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index 27706dcdd..7ef934fbe 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -1,3 +1,9 @@ +Bdd +Bdd::ExistAbstractRepresentative(const BddSet& cube) const { + LACE_ME; + return sylvan_existsRepresentative(bdd, cube.set.bdd); +} + Mtbdd Bdd::toDoubleMtbdd() const { LACE_ME; @@ -10,6 +16,49 @@ Bdd::toInt64Mtbdd() const { return mtbdd_bool_to_int64(bdd); } +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) +Mtbdd +Bdd::toStormRationalFunctionMtbdd() const { + LACE_ME; + return mtbdd_bool_to_storm_rational_function(bdd); +} + +Mtbdd +Mtbdd::PlusRF(const Mtbdd &other) const +{ + LACE_ME; + return sylvan_storm_rational_function_plus(mtbdd, other.mtbdd); +} + + +Mtbdd +Mtbdd::TimesRF(const Mtbdd &other) const +{ + LACE_ME; + return sylvan_storm_rational_function_times(mtbdd, other.mtbdd); +} + +Mtbdd +Mtbdd::MinusRF(const Mtbdd &other) const +{ + LACE_ME; + return sylvan_storm_rational_function_minus(mtbdd, other.mtbdd); +} + +Mtbdd +Mtbdd::DivideRF(const Mtbdd &other) const +{ + LACE_ME; + return sylvan_storm_rational_function_divide(mtbdd, other.mtbdd); +} + +Mtbdd Mtbdd::AbstractPlusRF(const BddSet &variables) const { + LACE_ME; + return sylvan_storm_rational_function_abstract_plus(mtbdd, variables.set.bdd); +} + +#endif + Mtbdd Bdd::Ite(Mtbdd const& thenDd, Mtbdd const& elseDd) const { LACE_ME; @@ -139,3 +188,16 @@ Mtbdd::GetShaHash() const { return std::string(buf); } +Mtbdd +Mtbdd::AbstractMinRepresentative(const BddSet &variables) const +{ + LACE_ME; + return mtbdd_minExistsRepresentative(mtbdd, variables.set.bdd); +} + +Mtbdd +Mtbdd::AbstractMaxRepresentative(const BddSet &variables) const +{ + LACE_ME; + return mtbdd_maxExistsRepresentative(mtbdd, variables.set.bdd); +} diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c new file mode 100644 index 000000000..dd2afab1a --- /dev/null +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c @@ -0,0 +1,457 @@ +#include + +#include +#include +#include +#include +#include +#include +#include + +#include +#include +#include +#include + +#include + +#undef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG + +#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG +int depth = 0; + +#define LOG_I(funcName) do { for (int i = 0; i < depth; ++i) { printf(" "); } ++depth; printf("Entering function " funcName "\n"); } while (0 != 0); +#define LOG_O(funcName) do { --depth; for (int i = 0; i < depth; ++i) { printf(" "); } printf("Leaving function " funcName "\n"); } while (0 != 0); +#else +#define LOG_I(funcName) +#define LOG_O(funcName) +#endif + +/** + * helper function for hash + */ +#ifndef rotl64 +static inline uint64_t +rotl64(uint64_t x, int8_t r) +{ + return ((x<>(64-r))); +} +#endif + +static uint64_t +sylvan_storm_rational_function_hash(const uint64_t v, const uint64_t seed) +{ + LOG_I("i-hash") + /* Hash the storm::RationalFunction in pointer v */ + + storm_rational_function_ptr x = (storm_rational_function_ptr)v; + + uint64_t hash = storm_rational_function_hash(x, seed); + +#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG + printf("Hashing ptr %p with contents ", x); + print_storm_rational_function(x); + printf(" with seed %zu, hash = %zu\n", seed, hash); +#endif + + LOG_O("i-hash") + return hash; +} + +static int +sylvan_storm_rational_function_equals(const uint64_t left, const uint64_t right) +{ + LOG_I("i-equals") + /* This function is called by the unique table when comparing a new + leaf with an existing leaf */ + storm_rational_function_ptr a = (storm_rational_function_ptr)(size_t)left; + storm_rational_function_ptr b = (storm_rational_function_ptr)(size_t)right; + + /* Just compare x and y */ + int result = storm_rational_function_equals(a, b); + + LOG_O("i-equals") + return result; +} + +static void +sylvan_storm_rational_function_create(uint64_t *val) +{ + LOG_I("i-create") + +#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG + void* tmp = (void*)*val; + printf("sylvan_storm_rational_function_create(ptr = %p, value = ", tmp); + print_storm_rational_function(*((storm_rational_function_ptr*)(size_t)val)); + printf(")\n"); +#endif + + /* This function is called by the unique table when a leaf does not yet exist. + We make a copy, which will be stored in the hash table. */ + storm_rational_function_ptr* x = (storm_rational_function_ptr*)(size_t)val; + storm_rational_function_init(x); + +#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG + tmp = (void*)*val; + printf("sylvan_storm_rational_function_create_2(ptr = %p)\n", tmp); +#endif + + LOG_O("i-create") +} + +static void +sylvan_storm_rational_function_destroy(uint64_t val) +{ + LOG_I("i-destroy") + /* This function is called by the unique table + when a leaf is removed during garbage collection. */ + storm_rational_function_ptr x = (storm_rational_function_ptr)(size_t)val; + storm_rational_function_destroy(x); + LOG_O("i-destroy") +} + +static uint32_t sylvan_storm_rational_function_type; +static uint64_t CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS; + +/** + * Initialize storm::RationalFunction custom leaves + */ +void +sylvan_storm_rational_function_init() +{ + /* Register custom leaf 3 */ + sylvan_storm_rational_function_type = mtbdd_register_custom_leaf(sylvan_storm_rational_function_hash, sylvan_storm_rational_function_equals, sylvan_storm_rational_function_create, sylvan_storm_rational_function_destroy); + + if (SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID != sylvan_storm_rational_function_type) { + printf("ERROR - ERROR - ERROR\nThe Sylvan Type ID is NOT correct.\nIt was assumed to be %u, but it is actually %u!\nYou NEED to fix this by changing the macro \"SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID\" and recompiling StoRM!\n\n", SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID, sylvan_storm_rational_function_type); + assert(0); + } + + CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS = cache_next_opid(); +} + +uint32_t sylvan_storm_rational_function_get_type() { + return sylvan_storm_rational_function_type; +} + +/** + * Create storm::RationalFunction leaf + */ +MTBDD +mtbdd_storm_rational_function(storm_rational_function_ptr val) +{ + LOG_I("i-mtbdd_") + uint64_t terminalValue = (uint64_t)val; + +#ifdef SYLVAN_STORM_RATIONAL_FUNCTION_DEBUG + printf("mtbdd_storm_rational_function(ptr = %p, value = ", val); + print_storm_rational_function(val); + printf(")\n"); +#endif + + MTBDD result = mtbdd_makeleaf(sylvan_storm_rational_function_type, terminalValue); + + LOG_O("i-mtbdd_") + return result; +} + +/** + * Converts a BDD to a MTBDD with storm::RationalFunction leaves + */ +TASK_IMPL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, a, size_t, v) +{ + LOG_I("task_impl_2 to_srf") + if (a == mtbdd_false) { + MTBDD result = mtbdd_storm_rational_function(storm_rational_function_get_zero()); + LOG_O("task_impl_2 to_srf - ZERO") + return result; + } + if (a == mtbdd_true) { + MTBDD result = mtbdd_storm_rational_function(storm_rational_function_get_one()); + LOG_O("task_impl_2 to_srf - ONE") + return result; + } + + // Ugly hack to get rid of the error "unused variable v" (because there is no version of uapply without a parameter). + (void)v; + + LOG_O("task_impl_2 to_srf - INVALID") + return mtbdd_invalid; +} + +TASK_IMPL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD, dd) +{ + return mtbdd_uapply(dd, TASK(mtbdd_op_bool_to_storm_rational_function), 0); +} + +/** + * Operation "plus" for two storm::RationalFunction MTBDDs + * Interpret partial function as "0" + */ +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, pa, MTBDD*, pb) +{ + LOG_I("task_impl_2 op_plus") + MTBDD a = *pa, b = *pb; + + /* Check for partial functions */ + if (a == mtbdd_false) return b; + if (b == mtbdd_false) return a; + + /* If both leaves, compute plus */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); + storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + + storm_rational_function_ptr mres = storm_rational_function_plus(ma, mb); + MTBDD res = mtbdd_storm_rational_function(mres); + + // TODO: Delete mres? + + return res; + } + + /* Commutative, so swap a,b for better cache performance */ + if (a < b) { + *pa = b; + *pb = a; + } + + return mtbdd_invalid; +} + +/** + * Operation "minus" for two storm::RationalFunction MTBDDs + * Interpret partial function as "0" + */ +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, pa, MTBDD*, pb) +{ + LOG_I("task_impl_2 op_minus") + MTBDD a = *pa, b = *pb; + + /* Check for partial functions */ + if (a == mtbdd_false) return sylvan_storm_rational_function_neg(b); + if (b == mtbdd_false) return a; + + /* If both leaves, compute plus */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); + storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + + storm_rational_function_ptr mres = storm_rational_function_minus(ma, mb); + MTBDD res = mtbdd_storm_rational_function(mres); + + // TODO: Delete mres? + + return res; + } + + return mtbdd_invalid; +} + +/** + * Operation "times" for two storm::RationalFunction MTBDDs. + * One of the parameters can be a BDD, then it is interpreted as a filter. + * For partial functions, domain is intersection + */ +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, pa, MTBDD*, pb) +{ + LOG_I("task_impl_2 op_times") + MTBDD a = *pa, b = *pb; + + /* Check for partial functions and for Boolean (filter) */ + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + + /* If one of Boolean, interpret as filter */ + if (a == mtbdd_true) return b; + if (b == mtbdd_true) return a; + + /* Handle multiplication of leaves */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); + storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + + storm_rational_function_ptr mres = storm_rational_function_times(ma, mb); + MTBDD res = mtbdd_storm_rational_function(mres); + + // TODO: Delete mres? + + return res; + } + + /* Commutative, so make "a" the lowest for better cache performance */ + if (a < b) { + *pa = b; + *pb = a; + } + + return mtbdd_invalid; +} + +/** + * Operation "divide" for two storm::RationalFunction MTBDDs. + * For partial functions, domain is intersection + */ +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*, pb) +{ + LOG_I("task_impl_2 op_divide") + MTBDD a = *pa, b = *pb; + + /* Check for partial functions */ + if (a == mtbdd_false || b == mtbdd_false) return mtbdd_false; + + /* Handle division of leaves */ + if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { + storm_rational_function_ptr ma = (storm_rational_function_ptr)mtbdd_getvalue(a); + storm_rational_function_ptr mb = (storm_rational_function_ptr)mtbdd_getvalue(b); + + storm_rational_function_ptr mres = storm_rational_function_divide(ma, mb); + MTBDD res = mtbdd_storm_rational_function(mres); + + // TODO: Delete mres? + + return res; + } + + return mtbdd_invalid; +} + +/** + * The abstraction operators are called in either of two ways: + * - with k=0, then just calculate "a op b" + * - with k<>0, then just calculate "a := a op a", k times + */ + +TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, a, MTBDD, b, int, k) +{ + LOG_I("task_impl_3 abstract_op_plus") + if (k==0) { + return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_plus)); + } else { + MTBDD res = a; + for (int i=0; i and , and abstract variables using summation. + * This is similar to the "and_exists" operation in BDDs. + */ +TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, a, MTBDD, b, MTBDD, v) +{ + /* Check terminal cases */ + + /* If v == true, then is an empty set */ + if (v == mtbdd_true) return mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_times)); + + /* Try the times operator on a and b */ + MTBDD result = CALL(sylvan_storm_rational_function_op_times, &a, &b); + if (result != mtbdd_invalid) { + /* Times operator successful, store reference (for garbage collection) */ + mtbdd_refs_push(result); + /* ... and perform abstraction */ + result = mtbdd_abstract(result, v, TASK(sylvan_storm_rational_function_abstract_op_plus)); + mtbdd_refs_pop(1); + /* Note that the operation cache is used in mtbdd_abstract */ + return result; + } + + /* Maybe perform garbage collection */ + 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_STORM_RATIONAL_FUNCTION_AND_EXISTS, a, b, v, &result)) return result; + + /* Now, v is not a constant, and either a or b is not a constant */ + + /* Get top variable */ + int la = mtbdd_isleaf(a); + int lb = mtbdd_isleaf(b); + mtbddnode_t na = la ? 0 : GETNODE(a); + mtbddnode_t nb = lb ? 0 : GETNODE(b); + uint32_t va = la ? 0xffffffff : mtbddnode_getvariable(na); + uint32_t vb = lb ? 0xffffffff : mtbddnode_getvariable(nb); + uint32_t var = va < vb ? va : vb; + + mtbddnode_t nv = GETNODE(v); + uint32_t vv = mtbddnode_getvariable(nv); + + if (vv < var) { + /* Recursive, then abstract result */ + result = CALL(sylvan_storm_rational_function_and_exists, a, b, node_gethigh(v, nv)); + mtbdd_refs_push(result); + result = mtbdd_apply(result, result, TASK(sylvan_storm_rational_function_op_plus)); + mtbdd_refs_pop(1); + } else { + /* Get cofactors */ + MTBDD alow, ahigh, blow, bhigh; + alow = (!la && va == var) ? node_getlow(a, na) : a; + ahigh = (!la && va == var) ? node_gethigh(a, na) : a; + blow = (!lb && vb == var) ? node_getlow(b, nb) : b; + bhigh = (!lb && vb == var) ? node_gethigh(b, nb) : b; + + if (vv == var) { + /* Recursive, then abstract result */ + mtbdd_refs_spawn(SPAWN(sylvan_storm_rational_function_and_exists, ahigh, bhigh, node_gethigh(v, nv))); + MTBDD low = mtbdd_refs_push(CALL(sylvan_storm_rational_function_and_exists, alow, blow, node_gethigh(v, nv))); + MTBDD high = mtbdd_refs_push(mtbdd_refs_sync(SYNC(sylvan_storm_rational_function_and_exists))); + result = CALL(mtbdd_apply, low, high, TASK(sylvan_storm_rational_function_op_plus)); + mtbdd_refs_pop(2); + } else /* vv > v */ { + /* Recursive, then create node */ + mtbdd_refs_spawn(SPAWN(sylvan_storm_rational_function_and_exists, ahigh, bhigh, v)); + MTBDD low = mtbdd_refs_push(CALL(sylvan_storm_rational_function_and_exists, alow, blow, v)); + MTBDD high = mtbdd_refs_sync(SYNC(sylvan_storm_rational_function_and_exists)); + mtbdd_refs_pop(1); + result = mtbdd_makenode(var, low, high); + } + } + + /* Store in cache */ + cache_put3(CACHE_STORM_RATIONAL_FUNCTION_AND_EXISTS, a, b, v, result); + return result; +} diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h new file mode 100644 index 000000000..98a2fdffd --- /dev/null +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h @@ -0,0 +1,113 @@ +/** + * This is an implementation of storm::RationalFunction custom leaves of MTBDDs + */ + +#ifndef SYLVAN_STORM_RATIONAL_FUNCTION_H +#define SYLVAN_STORM_RATIONAL_FUNCTION_H + +#include +#include + +#define SYLVAN_HAVE_CARL 1 + +#if defined(SYLVAN_HAVE_CARL) || defined(STORM_HAVE_CARL) + +#define SYLVAN_STORM_RATIONAL_FUNCTION_TYPE_ID (3) + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +/** + * Initialize storm::RationalFunction custom leaves + */ +void sylvan_storm_rational_function_init(); + +/** + * Returns the identifier necessary to use these custom leaves. + */ +uint32_t sylvan_storm_rational_function_get_type(); + +/** + * Create storm::RationalFunction leaf + */ +MTBDD mtbdd_storm_rational_function(storm_rational_function_ptr val); + +/** + * Monad that converts Boolean to a storm::RationalFunction MTBDD, translate terminals true to 1 and to 0 otherwise; + */ +TASK_DECL_2(MTBDD, mtbdd_op_bool_to_storm_rational_function, MTBDD, size_t) +TASK_DECL_1(MTBDD, mtbdd_bool_to_storm_rational_function, MTBDD) +#define mtbdd_bool_to_storm_rational_function(dd) CALL(mtbdd_bool_to_storm_rational_function, dd) + +/** + * Operation "plus" for two storm::RationalFunction MTBDDs + */ +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_plus, MTBDD*, MTBDD*) +TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_plus, MTBDD, MTBDD, int) + +/** + * Operation "minus" for two storm::RationalFunction MTBDDs + */ +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_minus, MTBDD*, MTBDD*) + +/** + * Operation "times" for two storm::RationalFunction MTBDDs + */ +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_times, MTBDD*, MTBDD*) +TASK_DECL_3(MTBDD, sylvan_storm_rational_function_abstract_op_times, MTBDD, MTBDD, int) + +/** + * Operation "divide" for two storm::RationalFunction MTBDDs + */ +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, MTBDD*) + +/** + * Operation "negate" for one storm::RationalFunction MTBDD + */ +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_neg, MTBDD, size_t) + +/** + * Compute a + b + */ +#define sylvan_storm_rational_function_plus(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_plus)) + +/** + * Compute a - b + */ +#define sylvan_storm_rational_function_minus(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_minus)) + +/** + * Compute a * b + */ +#define sylvan_storm_rational_function_times(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_times)) + +/** + * Compute a / b + */ +#define sylvan_storm_rational_function_divide(a, b) mtbdd_apply(a, b, TASK(sylvan_storm_rational_function_op_divide)) + +/** + * Compute -a + */ +#define sylvan_storm_rational_function_neg(a) mtbdd_uapply(a, TASK(sylvan_storm_rational_function_op_neg), 0); + +/** + * Multiply and , and abstract variables using summation. + * This is similar to the "and_exists" operation in BDDs. + */ +TASK_DECL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, MTBDD, MTBDD); +#define sylvan_storm_rational_function_and_exists(a, b, vars) CALL(sylvan_storm_rational_function_and_exists, a, b, vars) + +/** + * Abstract the variables in from by taking the sum of all values + */ +#define sylvan_storm_rational_function_abstract_plus(dd, v) mtbdd_abstract(dd, v, TASK(sylvan_storm_rational_function_abstract_op_plus)) + +#ifdef __cplusplus +} +#endif /* __cplusplus */ + +#endif // SYLVAN_HAVE_CARL + +#endif // SYLVAN_STORM_RATIONAL_FUNCTION_H diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index 52f032d8c..8e0d44def 100644 --- a/src/abstraction/AbstractionInformation.cpp +++ b/src/abstraction/AbstractionInformation.cpp @@ -5,6 +5,9 @@ #include "src/utility/macros.h" #include "src/exceptions/InvalidOperationException.h" +#include "src/storage/expressions/Expression.h" +#include "src/storage/expressions/ExpressionManager.h" + namespace storm { namespace abstraction { @@ -394,4 +397,4 @@ namespace storm { template class AbstractionInformation; template class AbstractionInformation; } -} \ No newline at end of file +} diff --git a/src/abstraction/AbstractionInformation.h b/src/abstraction/AbstractionInformation.h index ddc359694..dcd35f52c 100644 --- a/src/abstraction/AbstractionInformation.h +++ b/src/abstraction/AbstractionInformation.h @@ -2,6 +2,7 @@ #include #include +#include #include "src/storage/dd/DdType.h" diff --git a/src/abstraction/MenuGame.cpp b/src/abstraction/MenuGame.cpp index ba47698e2..82ad3ebfe 100644 --- a/src/abstraction/MenuGame.cpp +++ b/src/abstraction/MenuGame.cpp @@ -9,6 +9,9 @@ #include "src/models/symbolic/StandardRewardModel.h" +#include "storm-config.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace abstraction { @@ -26,7 +29,7 @@ namespace storm { std::set const& player2Variables, std::set const& allNondeterminismVariables, std::set const& probabilisticBranchingVariables, - std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract(probabilisticBranchingVariables), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), extendedTransitionMatrix(transitionMatrix), probabilisticBranchingVariables(probabilisticBranchingVariables), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) { + std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract(probabilisticBranchingVariables), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), extendedTransitionMatrix(transitionMatrix), probabilisticBranchingVariables(probabilisticBranchingVariables), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) { // Intentionally left empty. } @@ -78,7 +81,9 @@ namespace storm { template class MenuGame; template class MenuGame; - +#ifdef STORM_HAVE_CARL + template class MenuGame; +#endif } } diff --git a/src/abstraction/StateSetAbstractor.cpp b/src/abstraction/StateSetAbstractor.cpp index 97874d080..77337751d 100644 --- a/src/abstraction/StateSetAbstractor.cpp +++ b/src/abstraction/StateSetAbstractor.cpp @@ -7,6 +7,9 @@ #include "src/utility/macros.h" #include "src/utility/solver.h" +#include "storm-config.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace abstraction { @@ -159,5 +162,8 @@ namespace storm { template class StateSetAbstractor; template class StateSetAbstractor; +#ifdef STORM_HAVE_CARL + template class StateSetAbstractor; +#endif } } diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp index 91f305d9b..a600f1792 100644 --- a/src/abstraction/prism/AbstractCommand.cpp +++ b/src/abstraction/prism/AbstractCommand.cpp @@ -14,6 +14,9 @@ #include "src/utility/solver.h" #include "src/utility/macros.h" +#include "storm-config.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace abstraction { namespace prism { @@ -359,6 +362,9 @@ namespace storm { template class AbstractCommand; template class AbstractCommand; +#ifdef STORM_HAVE_CARL + template class AbstractCommand; +#endif } } -} \ No newline at end of file +} diff --git a/src/abstraction/prism/AbstractModule.cpp b/src/abstraction/prism/AbstractModule.cpp index 72e354584..bd2d42d32 100644 --- a/src/abstraction/prism/AbstractModule.cpp +++ b/src/abstraction/prism/AbstractModule.cpp @@ -9,6 +9,9 @@ #include "src/storage/prism/Module.h" +#include "storm-config.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace abstraction { namespace prism { @@ -89,6 +92,9 @@ namespace storm { template class AbstractModule; template class AbstractModule; +#ifdef STORM_HAVE_CARL + template class AbstractModule; +#endif } } -} \ No newline at end of file +} diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index f3f8c45be..c68269870 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -17,6 +17,9 @@ #include "src/exceptions/WrongFormatException.h" #include "src/exceptions/InvalidArgumentException.h" +#include "storm-config.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace abstraction { namespace prism { @@ -237,7 +240,7 @@ namespace storm { } // Construct the transition matrix by cutting away the transitions of unreachable states. - storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; + storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; // If there are bottom states, we need to mark all other states as non-bottom now. if (hasBottomStates) { @@ -358,7 +361,9 @@ namespace storm { // Explicitly instantiate the class. template class AbstractProgram; template class AbstractProgram; - +#ifdef STORM_HAVE_CARL + template class AbstractProgram; +#endif } } -} \ No newline at end of file +} diff --git a/src/adapters/AddExpressionAdapter.cpp b/src/adapters/AddExpressionAdapter.cpp index e50620db8..682c26e7f 100644 --- a/src/adapters/AddExpressionAdapter.cpp +++ b/src/adapters/AddExpressionAdapter.cpp @@ -8,6 +8,9 @@ #include "src/storage/dd/Add.h" #include "src/storage/dd/Bdd.h" +#include "storm-config.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace adapters { @@ -201,6 +204,8 @@ namespace storm { // Explicitly instantiate the symbolic expression adapter template class AddExpressionAdapter; template class AddExpressionAdapter; - +#ifdef STORM_HAVE_CARL + template class AddExpressionAdapter; +#endif } // namespace adapters } // namespace storm diff --git a/src/modelchecker/DFTAnalyser.h b/src/modelchecker/DFTAnalyser.h index 24c1068ba..d822b036c 100644 --- a/src/modelchecker/DFTAnalyser.h +++ b/src/modelchecker/DFTAnalyser.h @@ -122,7 +122,7 @@ private: STORM_LOG_TRACE("Result for permutation:"<(1) << nrM) && permutation != 0); } if(invResults) { return storm::utility::one() - result; diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp index f3c4d29d4..0d97b87d0 100644 --- a/src/models/sparse/NondeterministicModel.cpp +++ b/src/models/sparse/NondeterministicModel.cpp @@ -72,7 +72,7 @@ namespace storm { std::cout << i++ << "/" << modifications.size() << std::endl; rewardModel.setStateActionReward(mod.first, mod.second); } - }; + } template template @@ -81,7 +81,7 @@ namespace storm { for(auto const& mod : modifications) { rewardModel.setStateReward(mod.first, mod.second); } - }; + } template void NondeterministicModel::reduceToStateBasedRewards() { diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 945faba47..97abf9581 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -13,6 +13,9 @@ #include "src/models/symbolic/StandardRewardModel.h" +#include "storm-config.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace models { namespace symbolic { @@ -248,7 +251,9 @@ namespace storm { // Explicitly instantiate the template class. template class Model; template class Model; - +#ifdef STORM_HAVE_CARL + template class Model; +#endif } // namespace symbolic } // namespace models } // namespace storm diff --git a/src/models/symbolic/NondeterministicModel.cpp b/src/models/symbolic/NondeterministicModel.cpp index da3607d02..53119fcab 100644 --- a/src/models/symbolic/NondeterministicModel.cpp +++ b/src/models/symbolic/NondeterministicModel.cpp @@ -6,6 +6,9 @@ #include "src/models/symbolic/StandardRewardModel.h" +#include "storm-config.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace models { namespace symbolic { @@ -76,7 +79,9 @@ namespace storm { // Explicitly instantiate the template class. template class NondeterministicModel; template class NondeterministicModel; - +#ifdef STORM_HAVE_CARL + template class NondeterministicModel; +#endif } // namespace symbolic } // namespace models } // namespace storm \ No newline at end of file diff --git a/src/models/symbolic/StochasticTwoPlayerGame.cpp b/src/models/symbolic/StochasticTwoPlayerGame.cpp index e945b85d6..6ee650314 100644 --- a/src/models/symbolic/StochasticTwoPlayerGame.cpp +++ b/src/models/symbolic/StochasticTwoPlayerGame.cpp @@ -6,6 +6,9 @@ #include "src/models/symbolic/StandardRewardModel.h" +#include "storm-config.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace models { namespace symbolic { @@ -60,9 +63,12 @@ namespace storm { } // Explicitly instantiate the template class. - template class StochasticTwoPlayerGame; - template class StochasticTwoPlayerGame; + template class StochasticTwoPlayerGame; + template class StochasticTwoPlayerGame; +#ifdef STORM_HAVE_CARL + template class StochasticTwoPlayerGame; +#endif } // namespace symbolic } // namespace models -} // namespace storm \ No newline at end of file +} // namespace storm diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index db781d2b7..0c65233b1 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -12,6 +12,9 @@ #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" +#include "storm-config.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace dd { template @@ -771,5 +774,8 @@ namespace storm { template class Add; template class Add; +#ifdef STORM_HAVE_CARL + template class Add; +#endif } } diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp index 0e64d80a8..96389fa20 100644 --- a/src/storage/dd/Bdd.cpp +++ b/src/storage/dd/Bdd.cpp @@ -15,6 +15,9 @@ #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" +#include "storm-config.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace dd { @@ -368,14 +371,27 @@ namespace storm { template Bdd Bdd::fromVector(DdManager const& ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); template Bdd Bdd::fromVector(DdManager const& ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); +#ifdef STORM_HAVE_CARL + template Bdd Bdd::fromVector(DdManager const& ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); +#endif template Add Bdd::toAdd() const; template Add Bdd::toAdd() const; +#ifdef STORM_HAVE_CARL + 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; +#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; +#endif } } diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp index 7b365baae..1f06fbfb5 100644 --- a/src/storage/dd/DdManager.cpp +++ b/src/storage/dd/DdManager.cpp @@ -7,7 +7,11 @@ #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/NotSupportedException.h" +#include "storm-config.h" +#include "src/adapters/CarlAdapter.h" + #include +#include namespace storm { namespace dd { @@ -103,7 +107,7 @@ namespace storm { } return result; } - + template Bdd DdManager::getCube(storm::expressions::Variable const& variable) const { storm::dd::DdMetaVariable const& metaVariable = this->getMetaVariable(variable); @@ -388,17 +392,32 @@ namespace storm { template Add DdManager::getAddZero() const; template Add DdManager::getAddZero() const; +#ifdef STORM_HAVE_CARL + 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; +#endif + template Add DdManager::getInfinity() const; template Add DdManager::getInfinity() const; +#ifdef STORM_HAVE_CARL + template Add DdManager::getInfinity() const; +#endif template Add DdManager::getConstant(double const& value) const; template Add DdManager::getConstant(uint_fast64_t const& value) const; - +#ifdef STORM_HAVE_CARL + template Add DdManager::getConstant(storm::RationalFunction const& value) const; +#endif + 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; +#endif } } diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index d7a424583..af7832945 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -10,6 +10,8 @@ #include "src/utility/constants.h" #include "src/exceptions/NotImplementedException.h" +#include "storm-config.h" + namespace storm { namespace dd { template @@ -31,126 +33,298 @@ namespace storm { InternalAdd InternalAdd::operator+(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Plus(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::operator+(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.PlusRF(other.sylvanMtbdd)); + } +#endif + template InternalAdd& InternalAdd::operator+=(InternalAdd const& other) { this->sylvanMtbdd = this->sylvanMtbdd.Plus(other.sylvanMtbdd); return *this; } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd& InternalAdd::operator+=(InternalAdd const& other) { + this->sylvanMtbdd = this->sylvanMtbdd.PlusRF(other.sylvanMtbdd); + return *this; + } +#endif + template InternalAdd InternalAdd::operator*(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Times(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::operator*(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.TimesRF(other.sylvanMtbdd)); + } +#endif + template InternalAdd& InternalAdd::operator*=(InternalAdd const& other) { this->sylvanMtbdd = this->sylvanMtbdd.Times(other.sylvanMtbdd); return *this; } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd& InternalAdd::operator*=(InternalAdd const& other) { + this->sylvanMtbdd = this->sylvanMtbdd.TimesRF(other.sylvanMtbdd); + return *this; + } +#endif + template InternalAdd InternalAdd::operator-(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Minus(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::operator-(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.MinusRF(other.sylvanMtbdd)); + } +#endif + template InternalAdd& InternalAdd::operator-=(InternalAdd const& other) { this->sylvanMtbdd = this->sylvanMtbdd.Minus(other.sylvanMtbdd); return *this; } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd& InternalAdd::operator-=(InternalAdd const& other) { + this->sylvanMtbdd = this->sylvanMtbdd.MinusRF(other.sylvanMtbdd); + return *this; + } +#endif + template InternalAdd InternalAdd::operator/(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Divide(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::operator/(InternalAdd const& other) const { + return InternalAdd(ddManager, this->sylvanMtbdd.DivideRF(other.sylvanMtbdd)); + } +#endif + template InternalAdd& InternalAdd::operator/=(InternalAdd const& other) { this->sylvanMtbdd = this->sylvanMtbdd.Divide(other.sylvanMtbdd); return *this; } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd& InternalAdd::operator/=(InternalAdd const& other) { + this->sylvanMtbdd = this->sylvanMtbdd.DivideRF(other.sylvanMtbdd); + return *this; + } +#endif + template InternalBdd InternalAdd::equals(InternalAdd const& other) const { return InternalBdd(ddManager, this->sylvanMtbdd.Equals(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalBdd InternalAdd::equals(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Equals"); + } +#endif + template InternalBdd InternalAdd::notEquals(InternalAdd const& other) const { return !this->equals(other); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalBdd InternalAdd::notEquals(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Not Equals"); + } +#endif + template InternalBdd InternalAdd::less(InternalAdd const& other) const { return InternalBdd(ddManager, this->sylvanMtbdd.Less(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalBdd InternalAdd::less(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Less"); + } +#endif + template InternalBdd InternalAdd::lessOrEqual(InternalAdd const& other) const { return InternalBdd(ddManager, this->sylvanMtbdd.LessOrEqual(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalBdd InternalAdd::lessOrEqual(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Less or Equal"); + } +#endif + template InternalBdd InternalAdd::greater(InternalAdd const& other) const { return !this->lessOrEqual(other); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalBdd InternalAdd::greater(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Greater"); + } +#endif + template InternalBdd InternalAdd::greaterOrEqual(InternalAdd const& other) const { return !this->less(other); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalBdd InternalAdd::greaterOrEqual(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Greater or Equal"); + } +#endif + template InternalAdd InternalAdd::pow(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Pow(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::pow(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Pow"); + } +#endif + template InternalAdd InternalAdd::mod(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Mod(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::mod(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Mod"); + } +#endif + template InternalAdd InternalAdd::logxy(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Logxy(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::logxy(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: logxy"); + } +#endif + template InternalAdd InternalAdd::floor() const { return InternalAdd(ddManager, this->sylvanMtbdd.Floor()); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::floor() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Floor"); + } +#endif + template InternalAdd InternalAdd::ceil() const { return InternalAdd(ddManager, this->sylvanMtbdd.Ceil()); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::ceil() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Ceil"); + } +#endif + template InternalAdd InternalAdd::minimum(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Min(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::minimum(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Minimum"); + } +#endif + template InternalAdd InternalAdd::maximum(InternalAdd const& other) const { return InternalAdd(ddManager, this->sylvanMtbdd.Max(other.sylvanMtbdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::maximum(InternalAdd const& other) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: Maximum"); + } +#endif + template InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractPlus(cube.sylvanBdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { + return InternalAdd(ddManager, this->sylvanMtbdd.AbstractPlusRF(cube.sylvanBdd)); + } +#endif + template InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMin(cube.sylvanBdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstract"); + } +#endif + template InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMax(cube.sylvanBdd)); } - + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: maxAbstract"); + } +#endif + template bool InternalAdd::equalModuloPrecision(InternalAdd const& other, double precision, bool relative) const { if (relative) { @@ -159,7 +333,14 @@ namespace storm { return this->sylvanMtbdd.EqualNorm(other.sylvanMtbdd, precision); } } - + +#ifdef STORM_HAVE_CARL + template<> + bool InternalAdd::equalModuloPrecision(InternalAdd const& other, double precision, bool relative) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: equalModuloPrecision"); + } +#endif + template InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { std::vector fromIndices; @@ -187,12 +368,22 @@ namespace storm { InternalBdd InternalAdd::greater(ValueType const& value) const { return InternalBdd(ddManager, this->sylvanMtbdd.BddStrictThreshold(value)); } + + template<> + InternalBdd InternalAdd::greater(storm::RationalFunction const& value) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } template InternalBdd InternalAdd::greaterOrEqual(ValueType const& value) const { return InternalBdd(ddManager, this->sylvanMtbdd.BddThreshold(value)); } + template<> + InternalBdd InternalAdd::greaterOrEqual(storm::RationalFunction const& value) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); + } + template InternalBdd InternalAdd::less(ValueType const& value) const { return !this->greaterOrEqual(value); @@ -605,6 +796,13 @@ namespace storm { MTBDD InternalAdd::getLeaf(uint_fast64_t value) { return mtbdd_int64(value); } + + template + MTBDD InternalAdd::getLeaf(storm::RationalFunction const& value) { + storm_rational_function_ptr ptr = (storm_rational_function_ptr)(&value); + + return mtbdd_storm_rational_function(ptr); + } template ValueType InternalAdd::getValue(MTBDD const& node) { @@ -619,11 +817,35 @@ namespace storm { } else if (std::is_same::value) { STORM_LOG_ASSERT(mtbdd_gettype(node) == 0, "Expected an unsigned value."); return negated ? -mtbdd_getint64(node) : mtbdd_getint64(node); - } else { + } +#ifdef STORM_HAVE_CARL + else if (std::is_same::value) { + STORM_LOG_ASSERT(false, "Non-specialized version of getValue() called for storm::RationalFunction value."); + } +#endif + else { STORM_LOG_ASSERT(false, "Illegal or unknown type in MTBDD."); } } +#ifdef STORM_HAVE_CARL + template<> + storm::RationalFunction InternalAdd::getValue(MTBDD const& node) { + STORM_LOG_ASSERT(mtbdd_isleaf(node), "Expected leaf, but got variable " << mtbdd_getvar(node) << "."); + + bool negated = mtbdd_hascomp(node); + MTBDD n = mtbdd_regular(node); + + STORM_LOG_ASSERT(mtbdd_gettype(node) == sylvan_storm_rational_function_get_type(), "Expected a storm::RationalFunction value."); + uint64_t value = mtbdd_getvalue(node); + storm_rational_function_ptr ptr = (storm_rational_function_ptr)value; + + storm::RationalFunction* rationalFunction = (storm::RationalFunction*)(ptr); + + return negated ? -(*rationalFunction) : (*rationalFunction); + } +#endif + template sylvan::Mtbdd InternalAdd::getSylvanMtbdd() const { return sylvanMtbdd; @@ -631,5 +853,8 @@ namespace storm { template class InternalAdd; template class InternalAdd; +#ifdef STORM_HAVE_CARL + template class InternalAdd; +#endif } } \ No newline at end of file diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.h b/src/storage/dd/sylvan/InternalSylvanAdd.h index 52dca6a7c..b073af6cb 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storage/dd/sylvan/InternalSylvanAdd.h @@ -13,6 +13,9 @@ #include "src/storage/expressions/Variable.h" +#include "src/adapters/CarlAdapter.h" +#include "storm-config.h" + namespace storm { namespace storage { template @@ -662,6 +665,15 @@ namespace storm { * @return The sylvan node for the given value. */ static MTBDD getLeaf(uint_fast64_t value); + +#ifdef STORM_HAVE_CARL + /*! + * Retrieves the sylvan representation of the given storm::RatíonalFunction value. + * + * @return The sylvan node for the given value. + */ + static MTBDD getLeaf(storm::RationalFunction const& value); +#endif /*! * Retrieves the value of the given node (that must be a leaf). @@ -686,4 +698,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANADD_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANADD_H_ */ diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp index 9e9c8c7b3..c173a1e51 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -13,6 +13,9 @@ #include "src/exceptions/InvalidOperationException.h" #include "src/exceptions/NotSupportedException.h" +#include "src/adapters/CarlAdapter.h" +#include "storm-config.h" + namespace storm { namespace dd { InternalBdd::InternalBdd(InternalDdManager const* ddManager, sylvan::Bdd const& sylvanBdd) : ddManager(ddManager), sylvanBdd(sylvanBdd) { @@ -158,7 +161,7 @@ namespace storm { } InternalBdd InternalBdd::existsAbstractRepresentative(InternalBdd const& cube) const { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is currently not supported by sylvan."); + return InternalBdd(ddManager, this->sylvanBdd.ExistAbstractRepresentative(cube.sylvanBdd)); } InternalBdd InternalBdd::universalAbstract(InternalBdd const& cube) const { @@ -247,7 +250,13 @@ namespace storm { return InternalAdd(ddManager, this->sylvanBdd.toDoubleMtbdd()); } else if (std::is_same::value) { return InternalAdd(ddManager, this->sylvanBdd.toInt64Mtbdd()); - } else { + } +#ifdef STORM_HAVE_CARL + else if (std::is_same::value) { + return InternalAdd(ddManager, this->sylvanBdd.toStormRationalFunctionMtbdd()); + } +#endif + else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal ADD type."); } } @@ -475,15 +484,18 @@ namespace storm { template InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter); template InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter); + template InternalBdd InternalBdd::fromVector(InternalDdManager const* ddManager, std::vector const& values, Odd const& odd, std::vector const& sortedDdVariableIndices, std::function const& filter); 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 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; } -} \ No newline at end of file +} diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp index 4d21599bd..ee795d08b 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -1,6 +1,7 @@ #include "src/storage/dd/sylvan/InternalSylvanDdManager.h" #include +#include #include "src/settings/SettingsManager.h" #include "src/settings/modules/SylvanSettings.h" @@ -9,6 +10,10 @@ #include "src/utility/macros.h" #include "src/exceptions/NotSupportedException.h" +#include "src/utility/sylvan.h" + +#include "storm-config.h" + namespace storm { namespace dd { uint_fast64_t InternalDdManager::numberOfInstances = 0; @@ -71,6 +76,13 @@ namespace storm { InternalAdd InternalDdManager::getAddOne() const { return InternalAdd(this, sylvan::Mtbdd::int64Terminal(storm::utility::one())); } + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalDdManager::getAddOne() const { + return InternalAdd(this, sylvan::Mtbdd::stormRationalFunctionTerminal(storm::utility::one())); + } +#endif InternalBdd InternalDdManager::getBddZero() const { return InternalBdd(this, sylvan::Bdd::bddZero()); @@ -85,6 +97,13 @@ namespace storm { InternalAdd InternalDdManager::getAddZero() const { return InternalAdd(this, sylvan::Mtbdd::int64Terminal(storm::utility::zero())); } + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalDdManager::getAddZero() const { + return InternalAdd(this, sylvan::Mtbdd::stormRationalFunctionTerminal(storm::utility::zero())); + } +#endif template<> InternalAdd InternalDdManager::getConstant(double const& value) const { @@ -96,8 +115,16 @@ namespace storm { return InternalAdd(this, sylvan::Mtbdd::int64Terminal(value)); } +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalDdManager::getConstant(storm::RationalFunction const& value) const { + return InternalAdd(this, sylvan::Mtbdd::stormRationalFunctionTerminal(value)); + } +#endif + std::pair, InternalBdd> InternalDdManager::createNewDdVariablePair(boost::optional const& position) { STORM_LOG_THROW(!position, storm::exceptions::NotSupportedException, "The manager does not support ordered insertion."); + InternalBdd first = InternalBdd(this, sylvan::Bdd::bddVar(nextFreeVariableIndex)); InternalBdd second = InternalBdd(this, sylvan::Bdd::bddVar(nextFreeVariableIndex + 1)); nextFreeVariableIndex += 2; @@ -126,11 +153,20 @@ namespace storm { template InternalAdd InternalDdManager::getAddOne() const; template InternalAdd InternalDdManager::getAddOne() const; +#ifdef STORM_HAVE_CARL + template InternalAdd InternalDdManager::getAddOne() const; +#endif template InternalAdd InternalDdManager::getAddZero() const; template InternalAdd InternalDdManager::getAddZero() const; +#ifdef STORM_HAVE_CARL + template InternalAdd InternalDdManager::getAddZero() const; +#endif template InternalAdd InternalDdManager::getConstant(double const& value) const; template InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const; +#ifdef STORM_HAVE_CARL + template InternalAdd InternalDdManager::getConstant(storm::RationalFunction const& value) const; +#endif } -} \ No newline at end of file +} diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.h b/src/storage/dd/sylvan/InternalSylvanDdManager.h index edbd11914..7919bd103 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.h +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.h @@ -1,151 +1,168 @@ -#ifndef STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ -#define STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ - -#include - -#include "src/storage/dd/DdType.h" -#include "src/storage/dd/InternalDdManager.h" - -#include "src/storage/dd/sylvan/InternalSylvanBdd.h" -#include "src/storage/dd/sylvan/InternalSylvanAdd.h" - -namespace storm { - namespace dd { - template - class InternalAdd; - - template - class InternalBdd; - - template<> - class InternalDdManager { - public: - friend class InternalBdd; - - template - friend class InternalAdd; - - /*! - * Creates a new internal manager for Sylvan DDs. - */ - InternalDdManager(); - - /*! - * Destroys the internal manager. - */ - ~InternalDdManager(); - - /*! - * Retrieves a BDD representing the constant one function. - * - * @return A BDD representing the constant one function. - */ - InternalBdd getBddOne() const; - - /*! - * Retrieves an ADD representing the constant one function. - * - * @return An ADD representing the constant one function. - */ - template - InternalAdd getAddOne() const; - - /*! - * Retrieves a BDD representing the constant zero function. - * - * @return A BDD representing the constant zero function. - */ - InternalBdd getBddZero() const; - - /*! - * Retrieves an ADD representing the constant zero function. - * - * @return An ADD representing the constant zero function. - */ - template - InternalAdd getAddZero() const; - - /*! - * Retrieves an ADD representing the constant function with the given value. - * - * @return An ADD representing the constant function with the given value. - */ - template - InternalAdd getConstant(ValueType const& value) const; - - /*! - * Creates a new pair of DD variables and returns the two cubes as a result. - * - * @param position An optional position at which to insert the new variable pair. This may only be given, if - * the manager supports ordered insertion. - * @return The two cubes belonging to the DD variables. - */ - std::pair, InternalBdd> createNewDdVariablePair(boost::optional const& position = boost::none); - - /*! - * Checks whether this manager supports the ordered insertion of variables, i.e. inserting variables at - * positions between already existing variables. - * - * @return True iff the manager supports ordered insertion. - */ - bool supportsOrderedInsertion() const; - - /*! - * Sets whether or not dynamic reordering is allowed for the DDs managed by this manager. - * - * @param value If set to true, dynamic reordering is allowed and forbidden otherwise. - */ - void allowDynamicReordering(bool value); - - /*! - * Retrieves whether dynamic reordering is currently allowed. - * - * @return True iff dynamic reordering is currently allowed. - */ - bool isDynamicReorderingAllowed() const; - - /*! - * Triggers a reordering of the DDs managed by this manager. - */ - void triggerReordering(); - - /*! - * Retrieves the number of DD variables managed by this manager. - * - * @return The number of managed variables. - */ - uint_fast64_t getNumberOfDdVariables() const; - - private: - // A counter for the number of instances of this class. This is used to determine when to initialize and - // quit the sylvan. This is because Sylvan does not know the concept of managers but implicitly has a - // 'global' manager. - static uint_fast64_t numberOfInstances; - - // The index of the next free variable index. This needs to be shared across all instances since the sylvan - // manager is implicitly 'global'. - static uint_fast64_t nextFreeVariableIndex; - }; - - template<> - InternalAdd InternalDdManager::getAddOne() const; - - template<> - InternalAdd InternalDdManager::getAddOne() const; - - template<> - InternalAdd InternalDdManager::getAddZero() const; - - template<> - InternalAdd InternalDdManager::getAddZero() const; - - template<> - InternalAdd InternalDdManager::getConstant(double const& value) const; - - template<> - InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const; - - } -} - -#endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ */ \ No newline at end of file +#ifndef STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ +#define STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ + +#include + +#include "src/storage/dd/DdType.h" +#include "src/storage/dd/InternalDdManager.h" + +#include "src/storage/dd/sylvan/InternalSylvanBdd.h" +#include "src/storage/dd/sylvan/InternalSylvanAdd.h" + +#include "src/adapters/CarlAdapter.h" +#include "storm-config.h" + +namespace storm { + namespace dd { + template + class InternalAdd; + + template + class InternalBdd; + + template<> + class InternalDdManager { + public: + friend class InternalBdd; + + template + friend class InternalAdd; + + /*! + * Creates a new internal manager for Sylvan DDs. + */ + InternalDdManager(); + + /*! + * Destroys the internal manager. + */ + ~InternalDdManager(); + + /*! + * Retrieves a BDD representing the constant one function. + * + * @return A BDD representing the constant one function. + */ + InternalBdd getBddOne() const; + + /*! + * Retrieves an ADD representing the constant one function. + * + * @return An ADD representing the constant one function. + */ + template + InternalAdd getAddOne() const; + + /*! + * Retrieves a BDD representing the constant zero function. + * + * @return A BDD representing the constant zero function. + */ + InternalBdd getBddZero() const; + + /*! + * Retrieves an ADD representing the constant zero function. + * + * @return An ADD representing the constant zero function. + */ + template + InternalAdd getAddZero() const; + + /*! + * Retrieves an ADD representing the constant function with the given value. + * + * @return An ADD representing the constant function with the given value. + */ + template + InternalAdd getConstant(ValueType const& value) const; + + /*! + * Creates a new pair of DD variables and returns the two cubes as a result. + * + * @param position An optional position at which to insert the new variable pair. This may only be given, if + * the manager supports ordered insertion. + * @return The two cubes belonging to the DD variables. + */ + std::pair, InternalBdd> createNewDdVariablePair(boost::optional const& position = boost::none); + + /*! + * Checks whether this manager supports the ordered insertion of variables, i.e. inserting variables at + * positions between already existing variables. + * + * @return True iff the manager supports ordered insertion. + */ + bool supportsOrderedInsertion() const; + + /*! + * Sets whether or not dynamic reordering is allowed for the DDs managed by this manager. + * + * @param value If set to true, dynamic reordering is allowed and forbidden otherwise. + */ + void allowDynamicReordering(bool value); + + /*! + * Retrieves whether dynamic reordering is currently allowed. + * + * @return True iff dynamic reordering is currently allowed. + */ + bool isDynamicReorderingAllowed() const; + + /*! + * Triggers a reordering of the DDs managed by this manager. + */ + void triggerReordering(); + + /*! + * Retrieves the number of DD variables managed by this manager. + * + * @return The number of managed variables. + */ + uint_fast64_t getNumberOfDdVariables() const; + + private: + // A counter for the number of instances of this class. This is used to determine when to initialize and + // quit the sylvan. This is because Sylvan does not know the concept of managers but implicitly has a + // 'global' manager. + static uint_fast64_t numberOfInstances; + + // The index of the next free variable index. This needs to be shared across all instances since the sylvan + // manager is implicitly 'global'. + static uint_fast64_t nextFreeVariableIndex; + }; + + template<> + InternalAdd InternalDdManager::getAddOne() const; + + template<> + InternalAdd InternalDdManager::getAddOne() const; + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalDdManager::getAddOne() const; +#endif + + template<> + InternalAdd InternalDdManager::getAddZero() const; + + template<> + InternalAdd InternalDdManager::getAddZero() const; + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalDdManager::getAddZero() const; +#endif + + template<> + InternalAdd InternalDdManager::getConstant(double const& value) const; + + template<> + InternalAdd InternalDdManager::getConstant(uint_fast64_t const& value) const; + +#ifdef STORM_HAVE_CARL + template<> + InternalAdd InternalDdManager::getConstant(storm::RationalFunction const& value) const; +#endif + } +} + +#endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANDDMANAGER_H_ */ diff --git a/src/storage/dd/sylvan/SylvanAddIterator.cpp b/src/storage/dd/sylvan/SylvanAddIterator.cpp index 8c97941a3..827d2937c 100644 --- a/src/storage/dd/sylvan/SylvanAddIterator.cpp +++ b/src/storage/dd/sylvan/SylvanAddIterator.cpp @@ -10,6 +10,9 @@ #include +#include "src/adapters/CarlAdapter.h" +#include "storm-config.h" + namespace storm { namespace dd { template @@ -187,5 +190,8 @@ namespace storm { template class AddIterator; template class AddIterator; +#ifdef STORM_HAVE_CARL + template class AddIterator; +#endif } } diff --git a/src/utility/sylvan.h b/src/utility/sylvan.h index babdc22fd..776b2640b 100644 --- a/src/utility/sylvan.h +++ b/src/utility/sylvan.h @@ -1,19 +1,20 @@ -#ifndef STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ -#define STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ - -#pragma clang diagnostic push -#pragma clang diagnostic ignored "-Wextra-semi" -#pragma clang diagnostic ignored "-Wzero-length-array" -#pragma clang diagnostic ignored "-Wgnu-zero-variadic-macro-arguments" -#pragma clang diagnostic ignored "-Wdeprecated-register" -#pragma clang diagnostic ignored "-Wc99-extensions" -#pragma clang diagnostic ignored "-Wunknown-pragmas" -#pragma GCC diagnostic push -#pragma GCC diagnostic ignored "-Wpedantic" - -#include "sylvan_obj.hpp" - -#pragma GCC diagnostic pop -#pragma clang diagnostic pop - +#ifndef STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ +#define STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ + +#pragma clang diagnostic push +#pragma clang diagnostic ignored "-Wextra-semi" +#pragma clang diagnostic ignored "-Wzero-length-array" +#pragma clang diagnostic ignored "-Wgnu-zero-variadic-macro-arguments" +#pragma clang diagnostic ignored "-Wdeprecated-register" +#pragma clang diagnostic ignored "-Wc99-extensions" +#pragma clang diagnostic ignored "-Wunknown-pragmas" +#pragma GCC diagnostic push +#pragma GCC diagnostic ignored "-Wpedantic" + +#include "sylvan_obj.hpp" +#include "sylvan_storm_rational_function.h" + +#pragma GCC diagnostic pop +#pragma clang diagnostic pop + #endif /* STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ */ \ No newline at end of file diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp index 35af85399..0d628fb75 100644 --- a/test/functional/abstraction/PrismMenuGameTest.cpp +++ b/test/functional/abstraction/PrismMenuGameTest.cpp @@ -16,6 +16,8 @@ #include "src/utility/solver.h" +#include "src/adapters/CarlAdapter.h" + TEST(PrismMenuGame, DieAbstractionTest_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); @@ -50,6 +52,25 @@ TEST(PrismMenuGame, DieAbstractionTest_Sylvan) { EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); } +#ifdef STORM_HAVE_CARL +TEST(PrismMenuGame, DieAbstractionTest_SylvanWithRationalFunction) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + + std::vector initialPredicates; + storm::expressions::ExpressionManager& manager = program.getManager(); + + initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); + + storm::abstraction::prism::AbstractProgram abstractProgram(program, initialPredicates, std::make_shared(), false); + + storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); + + EXPECT_EQ(26, game.getNumberOfTransitions()); + EXPECT_EQ(4, game.getNumberOfStates()); + EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); +} +#endif + TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); @@ -884,4 +905,4 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) { EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); } -#endif \ No newline at end of file +#endif diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 6edd36da3..33a58ab4c 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -11,7 +11,7 @@ #include "src/storage/SparseMatrix.h" -TEST(CuddDd, Constants) { +TEST(CuddDd, AddConstants) { std::shared_ptr> manager(new storm::dd::DdManager()); storm::dd::Add zero; ASSERT_NO_THROW(zero = manager->template getAddZero()); @@ -41,48 +41,221 @@ TEST(CuddDd, Constants) { EXPECT_EQ(2, two.getMax()); } -TEST(CuddDd, BddExistAbstractRepresentative) { +TEST(CuddDd, BddConstants) { std::shared_ptr> manager(new storm::dd::DdManager()); + storm::dd::Bdd zero; + ASSERT_NO_THROW(zero = manager->getBddZero()); + + EXPECT_EQ(0ul, zero.getNonZeroCount()); + EXPECT_EQ(1ul, zero.getLeafCount()); + EXPECT_EQ(1ul, zero.getNodeCount()); + + storm::dd::Bdd one; + ASSERT_NO_THROW(one = manager->getBddOne()); + + EXPECT_EQ(0ul, one.getNonZeroCount()); + EXPECT_EQ(1ul, one.getLeafCount()); + EXPECT_EQ(1ul, one.getNodeCount()); +} + +TEST(CuddDd, BddExistAbstractRepresentative) { + std::shared_ptr> manager(new storm::dd::DdManager()); + + storm::dd::Bdd zero; + ASSERT_NO_THROW(zero = manager->getBddZero()); + storm::dd::Bdd one; + ASSERT_NO_THROW(one = manager->getBddOne()); + std::pair x; std::pair y; std::pair z; - ASSERT_NO_THROW(x = manager->addMetaVariable("x", 0, 1)); + ASSERT_NO_THROW(x = manager->addMetaVariable("x", 0, 1)); ASSERT_NO_THROW(y = manager->addMetaVariable("y", 0, 1)); ASSERT_NO_THROW(z = manager->addMetaVariable("z", 0, 1)); - storm::dd::Bdd bddX = manager->getEncoding(x.first, 1); - //bddX.template toAdd().exportToDot("/opt/masterThesis/storm/build/test_cudd_add_x.dot"); - storm::dd::Bdd bddY = manager->getEncoding(y.first, 0); - //bddY.template toAdd().exportToDot("/opt/masterThesis/storm/build/test_cudd_add_y.dot"); - storm::dd::Bdd bddZ = manager->getEncoding(z.first, 0); - //bddZ.template toAdd().exportToDot("/opt/masterThesis/storm/build/test_cudd_add_z.dot"); - - storm::dd::Bdd bddX1Y0Z0 = (bddX && bddY) && bddZ; - //bddX1Y0Z0.template toAdd().exportToDot("/opt/masterThesis/storm/build/test_cudd_bddX1Y0Z0.dot"); - - EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount()); - EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount()); - EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount()); + storm::dd::Bdd bddX0 = manager->getEncoding(x.first, 0); + storm::dd::Bdd bddX1 = manager->getEncoding(x.first, 1); + storm::dd::Bdd bddY0 = manager->getEncoding(y.first, 0); + storm::dd::Bdd bddY1 = manager->getEncoding(y.first, 1); + storm::dd::Bdd bddZ0 = manager->getEncoding(z.first, 0); + storm::dd::Bdd bddZ1 = manager->getEncoding(z.first, 1); + + // Abstract from FALSE + storm::dd::Bdd representative_false_x = zero.existsAbstractRepresentative({x.first}); + EXPECT_EQ(0ul, representative_false_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_false_x.getLeafCount()); + EXPECT_EQ(1ul, representative_false_x.getNodeCount()); + EXPECT_TRUE(representative_false_x == zero); + // Abstract from TRUE + storm::dd::Bdd representative_true_x = one.existsAbstractRepresentative({x.first}); + EXPECT_EQ(0ul, representative_true_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_true_x.getLeafCount()); + EXPECT_EQ(2ul, representative_true_x.getNodeCount()); + EXPECT_TRUE(representative_true_x == bddX0); + + storm::dd::Bdd representative_true_xyz = one.existsAbstractRepresentative({x.first, y.first, z.first}); + EXPECT_EQ(0ul, representative_true_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_true_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_true_xyz.getNodeCount()); + EXPECT_TRUE(representative_true_xyz == ((bddX0 && bddY0) && bddZ0)); + + storm::dd::Bdd bddX1Y0Z0 = (bddX1 && bddY0) && bddZ0; + EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount()); + EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount()); + EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount()); + storm::dd::Bdd representative_x = bddX1Y0Z0.existsAbstractRepresentative({x.first}); EXPECT_EQ(1ul, representative_x.getNonZeroCount()); - EXPECT_EQ(1ul, representative_x.getLeafCount()); - EXPECT_EQ(4ul, representative_x.getNodeCount()); + EXPECT_EQ(1ul, representative_x.getLeafCount()); + EXPECT_EQ(4ul, representative_x.getNodeCount()); EXPECT_TRUE(bddX1Y0Z0 == representative_x); - //representative_x.template toAdd().exportToDot("/opt/masterThesis/storm/build/test_representativea_x.dot"); + storm::dd::Bdd representative_y = bddX1Y0Z0.existsAbstractRepresentative({y.first}); EXPECT_EQ(1ul, representative_y.getNonZeroCount()); - EXPECT_EQ(1ul, representative_y.getLeafCount()); - EXPECT_EQ(4ul, representative_y.getNodeCount()); + EXPECT_EQ(1ul, representative_y.getLeafCount()); + EXPECT_EQ(4ul, representative_y.getNodeCount()); EXPECT_TRUE(bddX1Y0Z0 == representative_y); - //representative_y.template toAdd().exportToDot("/opt/masterThesis/storm/build/test_representativea_y.dot"); + storm::dd::Bdd representative_z = bddX1Y0Z0.existsAbstractRepresentative({z.first}); EXPECT_EQ(1ul, representative_z.getNonZeroCount()); - EXPECT_EQ(1ul, representative_z.getLeafCount()); - EXPECT_EQ(4ul, representative_z.getNodeCount()); + EXPECT_EQ(1ul, representative_z.getLeafCount()); + EXPECT_EQ(4ul, representative_z.getNodeCount()); EXPECT_TRUE(bddX1Y0Z0 == representative_z); - //representative_z.template toAdd().exportToDot("/opt/masterThesis/storm/build/test_representativea_z.dot"); + + storm::dd::Bdd representative_xyz = bddX1Y0Z0.existsAbstractRepresentative({x.first, y.first, z.first}); + EXPECT_EQ(1ul, representative_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_xyz.getNodeCount()); + EXPECT_TRUE(bddX1Y0Z0 == representative_xyz); + + storm::dd::Bdd bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0; + storm::dd::Bdd bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1; + + storm::dd::Bdd bddAllTrueOrAllFalse = bddX0Y0Z0 || bddX1Y1Z1; + //bddAllTrueOrAllFalse.template toAdd().exportToDot("test_cudd_addAllTrueOrAllFalse.dot"); + + representative_x = bddAllTrueOrAllFalse.existsAbstractRepresentative({x.first}); + EXPECT_EQ(2ul, representative_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_x.getLeafCount()); + EXPECT_EQ(5ul, representative_x.getNodeCount()); + EXPECT_TRUE(bddAllTrueOrAllFalse == representative_x); + + representative_y = bddAllTrueOrAllFalse.existsAbstractRepresentative({y.first}); + EXPECT_EQ(2ul, representative_y.getNonZeroCount()); + EXPECT_EQ(1ul, representative_y.getLeafCount()); + EXPECT_EQ(5ul, representative_y.getNodeCount()); + EXPECT_TRUE(bddAllTrueOrAllFalse == representative_y); + + representative_z = bddAllTrueOrAllFalse.existsAbstractRepresentative({z.first}); + EXPECT_EQ(2ul, representative_z.getNonZeroCount()); + EXPECT_EQ(1ul, representative_z.getLeafCount()); + EXPECT_EQ(5ul, representative_z.getNodeCount()); + EXPECT_TRUE(bddAllTrueOrAllFalse == representative_z); + + representative_xyz = bddAllTrueOrAllFalse.existsAbstractRepresentative({x.first, y.first, z.first}); + EXPECT_EQ(1ul, representative_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_xyz.getNodeCount()); + EXPECT_TRUE(bddX0Y0Z0 == representative_xyz); } +/* +TEST(CuddDd, AddMinExistAbstractRepresentative) { + std::shared_ptr> manager(new storm::dd::DdManager()); + + storm::dd::Add zero; + ASSERT_NO_THROW(zero = manager->template getAddZero()); + storm::dd::Add one; + ASSERT_NO_THROW(one = manager->template getAddOne()); + + std::pair x; + std::pair y; + std::pair z; + ASSERT_NO_THROW(x = manager->addMetaVariable("x", 0, 1)); + ASSERT_NO_THROW(y = manager->addMetaVariable("y", 0, 1)); + ASSERT_NO_THROW(z = manager->addMetaVariable("z", 0, 1)); + + // Abstract from FALSE + storm::dd::Add representative_false_x = zero.existsAbstractRepresentative({x.first}); + EXPECT_EQ(0ul, representative_false_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_false_x.getLeafCount()); + EXPECT_EQ(1ul, representative_false_x.getNodeCount()); + EXPECT_TRUE(representative_false_x == zero); + + // Abstract from TRUE + storm::dd::Add representative_true_x = one.existsAbstractRepresentative({x.first}); + EXPECT_EQ(1ul, representative_true_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_true_x.getLeafCount()); + EXPECT_EQ(1ul, representative_true_x.getNodeCount()); + EXPECT_TRUE(representative_true_x == manager->getEncoding(x.first, 0)); + + storm::dd::Add bddX1 = manager->getEncoding(x.first, 1); + storm::dd::Add bddY0 = manager->getEncoding(y.first, 0); + storm::dd::Add bddZ0 = manager->getEncoding(z.first, 0); + + storm::dd::Add bddX1Y0Z0 = (bddX1 && bddY0) && bddZ0; + EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount()); + EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount()); + EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount()); + + storm::dd::Add representative_x = bddX1Y0Z0.existsAbstractRepresentative({x.first}); + EXPECT_EQ(1ul, representative_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_x.getLeafCount()); + EXPECT_EQ(4ul, representative_x.getNodeCount()); + EXPECT_TRUE(bddX1Y0Z0 == representative_x); + + storm::dd::Add representative_y = bddX1Y0Z0.existsAbstractRepresentative({y.first}); + EXPECT_EQ(1ul, representative_y.getNonZeroCount()); + EXPECT_EQ(1ul, representative_y.getLeafCount()); + EXPECT_EQ(4ul, representative_y.getNodeCount()); + EXPECT_TRUE(bddX1Y0Z0 == representative_y); + + storm::dd::Add representative_z = bddX1Y0Z0.existsAbstractRepresentative({z.first}); + EXPECT_EQ(1ul, representative_z.getNonZeroCount()); + EXPECT_EQ(1ul, representative_z.getLeafCount()); + EXPECT_EQ(4ul, representative_z.getNodeCount()); + EXPECT_TRUE(bddX1Y0Z0 == representative_z); + + storm::dd::Add representative_xyz = bddX1Y0Z0.existsAbstractRepresentative({x.first, y.first, z.first}); + EXPECT_EQ(1ul, representative_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_xyz.getNodeCount()); + EXPECT_TRUE(bddX1Y0Z0 == representative_xyz); + + storm::dd::Add bddX0 = manager->getEncoding(x.first, 0); + storm::dd::Add bddY1 = manager->getEncoding(y.first, 1); + storm::dd::Add bddZ1 = manager->getEncoding(z.first, 1); + + storm::dd::Add bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0; + storm::dd::Add bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1; + + storm::dd::Add bddAllTrueOrAllFalse = bddX0Y0Z0 || bddX1Y1Z1; + //bddAllTrueOrAllFalse.template toAdd().exportToDot("test_cudd_addAllTrueOrAllFalse.dot"); + + representative_x = bddAllTrueOrAllFalse.existsAbstractRepresentative({x.first}); + EXPECT_EQ(2ul, representative_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_x.getLeafCount()); + EXPECT_EQ(5ul, representative_x.getNodeCount()); + EXPECT_TRUE(bddAllTrueOrAllFalse == representative_x); + + representative_y = bddAllTrueOrAllFalse.existsAbstractRepresentative({y.first}); + EXPECT_EQ(2ul, representative_y.getNonZeroCount()); + EXPECT_EQ(1ul, representative_y.getLeafCount()); + EXPECT_EQ(5ul, representative_y.getNodeCount()); + EXPECT_TRUE(bddAllTrueOrAllFalse == representative_y); + + representative_z = bddAllTrueOrAllFalse.existsAbstractRepresentative({z.first}); + EXPECT_EQ(2ul, representative_z.getNonZeroCount()); + EXPECT_EQ(1ul, representative_z.getLeafCount()); + EXPECT_EQ(5ul, representative_z.getNodeCount()); + EXPECT_TRUE(bddAllTrueOrAllFalse == representative_z); + + representative_xyz = bddAllTrueOrAllFalse.existsAbstractRepresentative({x.first, y.first, z.first}); + EXPECT_EQ(1ul, representative_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_xyz.getNodeCount()); + EXPECT_TRUE(bddX0Y0Z0 == representative_xyz); +}*/ TEST(CuddDd, AddGetMetaVariableTest) { std::shared_ptr> manager(new storm::dd::DdManager()); diff --git a/test/functional/storage/PrismProgramTest.cpp b/test/functional/storage/PrismProgramTest.cpp index 3cffe21a1..31d171cfd 100644 --- a/test/functional/storage/PrismProgramTest.cpp +++ b/test/functional/storage/PrismProgramTest.cpp @@ -163,4 +163,4 @@ TEST(PrismProgramTest, ConvertToJani) { ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm")); ASSERT_NO_THROW(janiModel = prismProgram.toJani()); -} \ No newline at end of file +} diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index 386501de3..8b5c38859 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -1,6 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" +#include "src/adapters/CarlAdapter.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/storage/dd/DdManager.h" #include "src/storage/dd/Add.h" @@ -10,6 +11,9 @@ #include "src/storage/SparseMatrix.h" +#include +#include + TEST(SylvanDd, Constants) { std::shared_ptr> manager(new storm::dd::DdManager()); storm::dd::Add zero; @@ -40,6 +44,125 @@ TEST(SylvanDd, Constants) { EXPECT_EQ(2, two.getMax()); } +TEST(SylvanDd, BddConstants) { + std::shared_ptr> manager(new storm::dd::DdManager()); + storm::dd::Bdd zero; + ASSERT_NO_THROW(zero = manager->getBddZero()); + + EXPECT_EQ(0ul, zero.getNonZeroCount()); + EXPECT_EQ(1ul, zero.getLeafCount()); + EXPECT_EQ(1ul, zero.getNodeCount()); + + storm::dd::Bdd one; + ASSERT_NO_THROW(one = manager->getBddOne()); + + EXPECT_EQ(0ul, one.getNonZeroCount()); + EXPECT_EQ(1ul, one.getLeafCount()); + EXPECT_EQ(1ul, one.getNodeCount()); +} + +TEST(SylvanDd, BddExistAbstractRepresentative) { + std::shared_ptr> manager(new storm::dd::DdManager()); + + storm::dd::Bdd zero; + ASSERT_NO_THROW(zero = manager->getBddZero()); + storm::dd::Bdd one; + ASSERT_NO_THROW(one = manager->getBddOne()); + + std::pair x; + std::pair y; + std::pair z; + ASSERT_NO_THROW(x = manager->addMetaVariable("x", 0, 1)); + ASSERT_NO_THROW(y = manager->addMetaVariable("y", 0, 1)); + ASSERT_NO_THROW(z = manager->addMetaVariable("z", 0, 1)); + + storm::dd::Bdd bddX0 = manager->getEncoding(x.first, 0); + storm::dd::Bdd bddX1 = manager->getEncoding(x.first, 1); + storm::dd::Bdd bddY0 = manager->getEncoding(y.first, 0); + storm::dd::Bdd bddY1 = manager->getEncoding(y.first, 1); + storm::dd::Bdd bddZ0 = manager->getEncoding(z.first, 0); + storm::dd::Bdd bddZ1 = manager->getEncoding(z.first, 1); + + // Abstract from FALSE + storm::dd::Bdd representative_false_x = zero.existsAbstractRepresentative({x.first}); + EXPECT_EQ(0ul, representative_false_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_false_x.getLeafCount()); + EXPECT_EQ(1ul, representative_false_x.getNodeCount()); + EXPECT_TRUE(representative_false_x == zero); + + // Abstract from TRUE + storm::dd::Bdd representative_true_x = one.existsAbstractRepresentative({x.first}); + EXPECT_EQ(0ul, representative_true_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_true_x.getLeafCount()); + EXPECT_EQ(2ul, representative_true_x.getNodeCount()); + EXPECT_TRUE(representative_true_x == bddX0); + + storm::dd::Bdd representative_true_xyz = one.existsAbstractRepresentative({x.first, y.first, z.first}); + EXPECT_EQ(0ul, representative_true_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_true_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_true_xyz.getNodeCount()); + EXPECT_TRUE(representative_true_xyz == ((bddX0 && bddY0) && bddZ0)); + + storm::dd::Bdd bddX1Y0Z0 = (bddX1 && bddY0) && bddZ0; + EXPECT_EQ(1ul, bddX1Y0Z0.getNonZeroCount()); + EXPECT_EQ(1ul, bddX1Y0Z0.getLeafCount()); + EXPECT_EQ(4ul, bddX1Y0Z0.getNodeCount()); + + storm::dd::Bdd representative_x = bddX1Y0Z0.existsAbstractRepresentative({x.first}); + EXPECT_EQ(1ul, representative_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_x.getLeafCount()); + EXPECT_EQ(4ul, representative_x.getNodeCount()); + EXPECT_TRUE(bddX1Y0Z0 == representative_x); + + storm::dd::Bdd representative_y = bddX1Y0Z0.existsAbstractRepresentative({y.first}); + EXPECT_EQ(1ul, representative_y.getNonZeroCount()); + EXPECT_EQ(1ul, representative_y.getLeafCount()); + EXPECT_EQ(4ul, representative_y.getNodeCount()); + EXPECT_TRUE(bddX1Y0Z0 == representative_y); + + storm::dd::Bdd representative_z = bddX1Y0Z0.existsAbstractRepresentative({z.first}); + EXPECT_EQ(1ul, representative_z.getNonZeroCount()); + EXPECT_EQ(1ul, representative_z.getLeafCount()); + EXPECT_EQ(4ul, representative_z.getNodeCount()); + EXPECT_TRUE(bddX1Y0Z0 == representative_z); + + storm::dd::Bdd representative_xyz = bddX1Y0Z0.existsAbstractRepresentative({x.first, y.first, z.first}); + EXPECT_EQ(1ul, representative_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_xyz.getNodeCount()); + EXPECT_TRUE(bddX1Y0Z0 == representative_xyz); + + storm::dd::Bdd bddX0Y0Z0 = (bddX0 && bddY0) && bddZ0; + storm::dd::Bdd bddX1Y1Z1 = (bddX1 && bddY1) && bddZ1; + + storm::dd::Bdd bddAllTrueOrAllFalse = bddX0Y0Z0 || bddX1Y1Z1; + //bddAllTrueOrAllFalse.template toAdd().exportToDot("test_Sylvan_addAllTrueOrAllFalse.dot"); + + representative_x = bddAllTrueOrAllFalse.existsAbstractRepresentative({x.first}); + EXPECT_EQ(2ul, representative_x.getNonZeroCount()); + EXPECT_EQ(1ul, representative_x.getLeafCount()); + EXPECT_EQ(5ul, representative_x.getNodeCount()); + EXPECT_TRUE(bddAllTrueOrAllFalse == representative_x); + + representative_y = bddAllTrueOrAllFalse.existsAbstractRepresentative({y.first}); + EXPECT_EQ(2ul, representative_y.getNonZeroCount()); + EXPECT_EQ(1ul, representative_y.getLeafCount()); + EXPECT_EQ(5ul, representative_y.getNodeCount()); + EXPECT_TRUE(bddAllTrueOrAllFalse == representative_y); + + representative_z = bddAllTrueOrAllFalse.existsAbstractRepresentative({z.first}); + EXPECT_EQ(2ul, representative_z.getNonZeroCount()); + EXPECT_EQ(1ul, representative_z.getLeafCount()); + EXPECT_EQ(5ul, representative_z.getNodeCount()); + EXPECT_TRUE(bddAllTrueOrAllFalse == representative_z); + + representative_xyz = bddAllTrueOrAllFalse.existsAbstractRepresentative({x.first, y.first, z.first}); + EXPECT_EQ(1ul, representative_xyz.getNonZeroCount()); + EXPECT_EQ(1ul, representative_xyz.getLeafCount()); + EXPECT_EQ(4ul, representative_xyz.getNodeCount()); + EXPECT_TRUE(bddX0Y0Z0 == representative_xyz); +} + TEST(SylvanDd, AddGetMetaVariableTest) { std::shared_ptr> manager(new storm::dd::DdManager()); ASSERT_NO_THROW(manager->addMetaVariable("x", 1, 9)); @@ -80,23 +203,120 @@ TEST(SylvanDd, EncodingTest) { EXPECT_EQ(2ul, add.getLeafCount()); } +#ifdef STORM_HAVE_CARL +TEST(SylvanDd, RationalFunctionConstants) { + std::shared_ptr> manager(new storm::dd::DdManager()); + storm::dd::Add zero; + ASSERT_NO_THROW(zero = manager->template getAddZero()); + + EXPECT_EQ(0ul, zero.getNonZeroCount()); + EXPECT_EQ(1ul, zero.getLeafCount()); + EXPECT_EQ(1ul, zero.getNodeCount()); + + storm::dd::Add one; + ASSERT_NO_THROW(one = manager->template getAddOne()); + + EXPECT_EQ(0ul, one.getNonZeroCount()); + EXPECT_EQ(1ul, one.getLeafCount()); + EXPECT_EQ(1ul, one.getNodeCount()); + + storm::dd::Add two; + storm::RationalFunction constantTwo(2); + + ASSERT_NO_THROW(two = manager->template getConstant(constantTwo)); + + EXPECT_EQ(0ul, two.getNonZeroCount()); + EXPECT_EQ(1ul, two.getLeafCount()); + EXPECT_EQ(1ul, two.getNodeCount()); + + // The cache that is used in case the underlying type needs a cache. + std::shared_ptr>> cache = std::make_shared>>(); + + storm::dd::Add function; + carl::Variable x = carl::freshRealVariable("x"); + carl::Variable y = carl::freshRealVariable("y"); + carl::Variable z = carl::freshRealVariable("z"); + + storm::RationalFunction constantOne(1); + + storm::RationalFunction variableX = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(x), cache)); + storm::RationalFunction variableY = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(y), cache)); + storm::RationalFunction variableZ = storm::RationalFunction(typename storm::RationalFunction::PolyType(typename storm::RationalFunction::PolyType::PolyType(z), cache)); + + storm::RationalFunction constantOneDivTwo(constantOne / constantTwo); + storm::RationalFunction tmpFunctionA(constantOneDivTwo); + tmpFunctionA *= variableZ; + tmpFunctionA /= variableY; + storm::RationalFunction tmpFunctionB(variableX); + tmpFunctionB *= variableY; + + + //storm::RationalFunction rationalFunction(two * x + x*y + constantOneDivTwo * z / y); + storm::RationalFunction rationalFunction(constantTwo); + rationalFunction *= variableX; + rationalFunction += tmpFunctionB; + rationalFunction += tmpFunctionA; + + ASSERT_NO_THROW(function = manager->template getConstant(rationalFunction)); + + EXPECT_EQ(0ul, function.getNonZeroCount()); + EXPECT_EQ(1ul, function.getLeafCount()); + EXPECT_EQ(1ul, function.getNodeCount()); +} + +TEST(SylvanDd, RationalFunctionEncodingTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 1, 9); + + storm::dd::Bdd encoding; + ASSERT_THROW(encoding = manager->getEncoding(x.first, 0), storm::exceptions::InvalidArgumentException); + ASSERT_THROW(encoding = manager->getEncoding(x.first, 10), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(encoding = manager->getEncoding(x.first, 4)); + EXPECT_EQ(1ul, encoding.getNonZeroCount()); + + // As a BDD, this DD has one only leaf, because there does not exist a 0-leaf, and (consequently) one node less + // than the MTBDD. + EXPECT_EQ(5ul, encoding.getNodeCount()); + EXPECT_EQ(1ul, encoding.getLeafCount()); + + storm::dd::Add add; + ASSERT_NO_THROW(add = encoding.template toAdd()); + + // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6. + EXPECT_EQ(6ul, add.getNodeCount()); + EXPECT_EQ(2ul, add.getLeafCount()); +} + +TEST(SylvanDd, RationalFunctionIdentityTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 1, 9); + + storm::dd::Add identity; + ASSERT_NO_THROW(identity = manager->getIdentity(x.first)); + + EXPECT_EQ(9ul, identity.getNonZeroCount()); + EXPECT_EQ(10ul, identity.getLeafCount()); + EXPECT_EQ(21ul, identity.getNodeCount()); +} +#endif + TEST(SylvanDd, RangeTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x; ASSERT_NO_THROW(x = manager->addMetaVariable("x", 1, 9)); - + storm::dd::Bdd range; ASSERT_NO_THROW(range = manager->getRange(x.first)); - + EXPECT_EQ(9ul, range.getNonZeroCount()); EXPECT_EQ(1ul, range.getLeafCount()); EXPECT_EQ(5ul, range.getNodeCount()); } -TEST(SylvanDd, IdentityTest) { +TEST(SylvanDd, DoubleIdentityTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); - + storm::dd::Add identity; ASSERT_NO_THROW(identity = manager->getIdentity(x.first)); @@ -105,6 +325,18 @@ TEST(SylvanDd, IdentityTest) { EXPECT_EQ(21ul, identity.getNodeCount()); } +TEST(SylvanDd, UintIdentityTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 1, 9); + + storm::dd::Add identity; + ASSERT_NO_THROW(identity = manager->getIdentity(x.first)); + + EXPECT_EQ(9ul, identity.getNonZeroCount()); + EXPECT_EQ(10ul, identity.getLeafCount()); + EXPECT_EQ(21ul, identity.getNodeCount()); +} + TEST(SylvanDd, OperatorTest) { std::shared_ptr> manager(new storm::dd::DdManager()); std::pair x = manager->addMetaVariable("x", 1, 9); @@ -427,4 +659,4 @@ TEST(SylvanDd, BddToExpressionTest) { storm::expressions::Variable d = manager->declareBooleanVariable("d"); auto result = bdd.toExpression(*manager); -} \ No newline at end of file +} diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 9fb9a0589..7b431e67e 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -644,4 +644,4 @@ TEST(GraphTest, ExplicitProb01MinMax) { ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff"))); EXPECT_EQ(993ul, statesWithProbability01.first.getNumberOfSetBits()); EXPECT_EQ(16ul, statesWithProbability01.second.getNumberOfSetBits()); -} \ No newline at end of file +}