Merge remote-tracking branch 'origin/master' into storm-pars

CMakeLists.txt

@@ -383,10 +383,10 @@ 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)
+	set(STORM_VERSION_PATCH 2)
 	set(STORM_VERSION_GIT_HASH "")
 	set(STORM_VERSION_COMMITS_AHEAD 0)
 	set(STORM_VERSION_DIRTY boost::none)

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})
@@ -268,8 +266,11 @@ if(USE_CARL)
 		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)

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<std::mutex> lock(rationalNumberMutex);
+#endif
+    
+    storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::infinity<storm::RationalNumber>());
+    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<std::mutex> 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<std::mutex> lock(rationalFunctionMutex);
+#endif
+    
+    storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::infinity<storm::RationalFunction>());
+    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<std::mutex> lock(rationalFunctionMutex);

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);

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;
             }

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);

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);

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;