From e8fab0718c387baf732a949a9188b30a410f63bf Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 21 Jun 2017 20:37:24 +0200 Subject: [PATCH 1/5] fixed issues in division operations of sylvan for rational numbers and rational functions (division by zero not correctly handled) --- .../3rdparty/sylvan/src/storm_wrapper.cpp | 19 +++++++++++++++++++ resources/3rdparty/sylvan/src/storm_wrapper.h | 2 ++ .../3rdparty/sylvan/src/sylvan_mtbdd_storm.c | 12 +++++++++--- .../src/sylvan_storm_rational_function.c | 3 +++ .../sylvan/src/sylvan_storm_rational_number.c | 3 +++ 5 files changed, 36 insertions(+), 3 deletions(-) diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp index 4678bec87..b042227fd 100644 --- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp @@ -109,6 +109,15 @@ storm_rational_number_ptr storm_rational_number_get_one() { return (storm_rational_number_ptr)result_srn; } +storm_rational_number_ptr storm_rational_number_get_infinity() { +#ifndef RATIONAL_NUMBER_THREAD_SAFE + std::lock_guard lock(rationalNumberMutex); +#endif + + storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::infinity()); + return (storm_rational_number_ptr)result_srn; +} + int storm_rational_number_is_zero(storm_rational_number_ptr a) { #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); @@ -404,6 +413,16 @@ storm_rational_function_ptr storm_rational_function_get_one() { return (storm_rational_function_ptr)result_srf; } +storm_rational_function_ptr storm_rational_function_get_infinity() { +#ifndef RATIONAL_FUNCTION_THREAD_SAFE + std::lock_guard lock(rationalFunctionMutex); +#endif + + storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::infinity()); + return (storm_rational_function_ptr)result_srf; +} + + int storm_rational_function_is_zero(storm_rational_function_ptr a) { #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.h b/resources/3rdparty/sylvan/src/storm_wrapper.h index 810269ecc..2fb6bb214 100644 --- a/resources/3rdparty/sylvan/src/storm_wrapper.h +++ b/resources/3rdparty/sylvan/src/storm_wrapper.h @@ -25,6 +25,7 @@ extern "C" { storm_rational_number_ptr storm_rational_number_clone(storm_rational_number_ptr a); storm_rational_number_ptr storm_rational_number_get_zero(); storm_rational_number_ptr storm_rational_number_get_one(); + storm_rational_number_ptr storm_rational_number_get_infinity(); int storm_rational_number_is_zero(storm_rational_number_ptr a); uint64_t storm_rational_number_hash(storm_rational_number_ptr const a, uint64_t const seed); double storm_rational_number_get_value_double(storm_rational_number_ptr a); @@ -71,6 +72,7 @@ extern "C" { storm_rational_function_ptr storm_rational_function_clone(storm_rational_function_ptr a); storm_rational_function_ptr storm_rational_function_get_zero(); storm_rational_function_ptr storm_rational_function_get_one(); + storm_rational_number_ptr storm_rational_function_get_infinity(); int storm_rational_function_is_zero(storm_rational_function_ptr a); uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed); double storm_rational_function_get_value_double(storm_rational_function_ptr a); diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c index 1915886f1..76792affe 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c @@ -43,10 +43,16 @@ TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb) double vval_a = *(double*)&val_a; double vval_b = *(double*)&val_b; if (vval_a == 0.0) return a; - else if (vval_b == 0.0) return b; - else { + else if (vval_b == 0.0) { + if (vval_a > 0.0) { + return mtbdd_double(INFINITY); + } else { + return mtbdd_double(-INFINITY); + } + return b; + } else { MTBDD result; - if (vval_a == 0.0 || vval_b == 1.0) result = a; + if (vval_b == 1.0) result = a; result = mtbdd_double(vval_a / vval_b); return result; } diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c index a890e28a9..dc9e97aa2 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c @@ -194,9 +194,12 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_divide, MTBDD*, pa, MTBDD*, /* If both leaves, compute division */ if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); + storm_rational_function_ptr mb = mtbdd_getstorm_rational_function_ptr(b); storm_rational_function_ptr mres; if (storm_rational_function_is_zero(ma)) { mres = storm_rational_function_get_zero(); + } else if (storm_rational_function_is_zero(mb)) { + mres = storm_rational_function_get_infinity(); } else { storm_rational_function_ptr mb = mtbdd_getstorm_rational_function_ptr(b); mres = storm_rational_function_divide(ma, mb); diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c index 076e75442..d2f59450c 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c @@ -194,9 +194,12 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_divide, MTBDD*, pa, MTBDD*, p /* If both leaves, compute division */ if (mtbdd_isleaf(a) && mtbdd_isleaf(b)) { storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); + storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); storm_rational_number_ptr mres; if (storm_rational_number_is_zero(ma)) { mres = storm_rational_number_get_zero(); + } else if (storm_rational_number_is_zero(mb)) { + mres = storm_rational_number_get_infinity(); } else { storm_rational_number_ptr mb = mtbdd_getstorm_rational_number_ptr(b); mres = storm_rational_number_divide(ma, mb); From 6ef8cf3042ab3ad51dc923ffc353b1905efed58b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 22 Jun 2017 12:52:29 +0200 Subject: [PATCH 2/5] Fixed compile problem with ull --- src/storm/storage/Scheduler.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index b7e842951..a1dc1ecbd 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -96,7 +96,7 @@ namespace storm { if (stateValuationsGiven) { widthOfStates += model->getStateValuations().getStateInfo(schedulerChoices.front().size() - 1).length() + 5; } - widthOfStates = std::max(widthOfStates, 12ull); + widthOfStates = std::max(widthOfStates, (uint_fast64_t)12); uint_fast64_t numOfSkippedStatesWithUniqueChoice = 0; out << "___________________________________________________________________" << std::endl; @@ -184,4 +184,4 @@ namespace storm { template class Scheduler; } -} \ No newline at end of file +} From 0542d66620146fc1a8b5de94cfebcf9fd964661b Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 26 Jun 2017 18:22:24 +0200 Subject: [PATCH 3/5] improved checking for git revision information --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 024fc9689..9d8394166 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -383,7 +383,7 @@ string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-([a-z0-9]+).*" "\\1" string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\1" STORM_VERSION_APPENDIX "${STORM_GIT_VERSION_STRING}") # now check whether the git version lookup failed -if (STORM_VERSION_MAJOR STREQUAL "HEAD-HASH-NOTFOUND") +if (STORM_VERSION_MAJOR MATCHES "NOTFOUND") set(STORM_VERSION_MAJOR 1) set(STORM_VERSION_MINOR 0) set(STORM_VERSION_PATCH 0) From 3e7dd56defdee8d8c0a1945e16d92796b66659b7 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 26 Jun 2017 18:24:20 +0200 Subject: [PATCH 4/5] fixed static version information (used in the absence of git version information) --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 9d8394166..d5b905eb1 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -386,7 +386,7 @@ string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\ if (STORM_VERSION_MAJOR MATCHES "NOTFOUND") set(STORM_VERSION_MAJOR 1) set(STORM_VERSION_MINOR 0) - set(STORM_VERSION_PATCH 0) + set(STORM_VERSION_PATCH 2) set(STORM_VERSION_GIT_HASH "") set(STORM_VERSION_COMMITS_AHEAD 0) set(STORM_VERSION_DIRTY boost::none) From e5cbc25f00535dfc0c3de4a6bcd94cbad509be84 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 26 Jun 2017 18:46:07 +0200 Subject: [PATCH 5/5] properly installing dylib resulting from shipped carl build (now considers carl version) --- resources/3rdparty/CMakeLists.txt | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 75d8ec4d1..4148df10a 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -215,7 +215,7 @@ if(USE_CARL) set(STORM_SHIPPED_CARL OFF) set(STORM_HAVE_CARL ON) message(STATUS "Storm - Use system version of carl.") - message(STATUS "Storm - Linking with carl ${carl_VERSION} (include: ${carl_INCLUDE_DIR}, library ${carl_LIBRARIES}, CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}, CARL_USE_GINAC: ${CARL_USE_GINAC}).") + message(STATUS "Storm - Linking with preinstalled carl ${carl_VERSION} (include: ${carl_INCLUDE_DIR}, library ${carl_LIBRARIES}, CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}, CARL_USE_GINAC: ${CARL_USE_GINAC}).") set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS}) set(STORM_HAVE_GINAC ${CARL_USE_GINAC}) @@ -257,8 +257,6 @@ if(USE_CARL) BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT} ) include(${STORM_3RDPARTY_BINARY_DIR}/carl/carlExport/carlConfig.cmake) - message("CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}, CARL_USE_GINAC: ${CARL_USE_GINAC}") - set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS}) set(STORM_HAVE_GINAC ${CARL_USE_GINAC}) @@ -267,9 +265,12 @@ if(USE_CARL) set(carl_INCLUDE_DIR "${STORM_3RDPARTY_BINARY_DIR}/carl/include/") set(carl_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT}) set(STORM_HAVE_CARL ON) + + message(STATUS "Storm - Linking with shipped carl ${carl_VERSION} (include: ${carl_INCLUDE_DIR}, library ${carl_LIBRARIES}, CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}, CARL_USE_GINAC: ${CARL_USE_GINAC}).") + # install the carl dynamic library if we build it - install(FILES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl.1.0.0${DYNAMIC_EXT} DESTINATION lib) + install(FILES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl.${carl_VERSION}${DYNAMIC_EXT} DESTINATION lib) endif() if(STORM_USE_CLN_RF AND NOT STORM_HAVE_CLN)