From 22a9703524bf5b336e89bb9f9fd33511476a069b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Basg=C3=B6ze?= Date: Wed, 25 Aug 2021 13:09:51 +0200 Subject: [PATCH] Remove erroneous mutex lock in sylvan_wrapper Also remove trailing whitespace --- .../3rdparty/sylvan/src/storm_wrapper.cpp | 178 ++++++++---------- 1 file changed, 77 insertions(+), 101 deletions(-) diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp index b0a10c1b8..44f406f1f 100644 --- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp @@ -42,7 +42,7 @@ void storm_rational_number_init(storm_rational_number_ptr* a) { #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm_rational_number_ptr srn_ptr = new storm::RationalNumber(*((storm::RationalNumber*)(*a))); *a = srn_ptr; } @@ -51,7 +51,7 @@ void storm_rational_number_destroy(storm_rational_number_ptr a) { #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber* srn_ptr = (storm::RationalNumber*)a; delete srn_ptr; } @@ -60,10 +60,10 @@ int storm_rational_number_equals(storm_rational_number_ptr a, storm_rational_num #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber const& srn_a = *(storm::RationalNumber*)a; storm::RationalNumber const& srn_b = *(storm::RationalNumber*)b; - + return (srn_a == srn_b) ? 1 : 0; } @@ -71,7 +71,7 @@ char* storm_rational_number_to_str(storm_rational_number_ptr val, char *buf, siz #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + std::stringstream ss; storm::RationalNumber const& srn_a = *(storm::RationalNumber*)val; ss << srn_a; @@ -90,7 +90,7 @@ storm_rational_number_ptr storm_rational_number_clone(storm_rational_number_ptr #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber* result_srn = new storm::RationalNumber(*((storm::RationalNumber const*)a)); return (storm_rational_number_ptr)result_srn; } @@ -99,7 +99,7 @@ storm_rational_number_ptr storm_rational_number_get_zero() { #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::zero()); return (storm_rational_number_ptr)result_srn; } @@ -108,7 +108,7 @@ storm_rational_number_ptr storm_rational_number_get_one() { #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::one()); return (storm_rational_number_ptr)result_srn; } @@ -117,7 +117,7 @@ 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; } @@ -126,7 +126,7 @@ int storm_rational_number_is_zero(storm_rational_number_ptr a) { #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + return storm::utility::isZero(*(storm::RationalNumber const*)a) ? 1 : 0; } @@ -134,9 +134,9 @@ uint64_t storm_rational_number_hash(storm_rational_number_ptr const a, uint64_t #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; - + // Taken from boost::hash_combine that we do not call here for the lack of boost headers. return seed ^ (std::hash()(srn_a) + 0x9e3779b9 + (seed<<6) + (seed>>2)); } @@ -145,7 +145,7 @@ double storm_rational_number_get_value_double(storm_rational_number_ptr a) { #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; return storm::utility::convertNumber(srn_a); } @@ -154,7 +154,7 @@ storm_rational_number_ptr storm_rational_number_from_double(double value) { #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber* number = new storm::RationalNumber(storm::utility::convertNumber(value)); return number; } @@ -163,10 +163,10 @@ storm_rational_number_ptr storm_rational_number_plus(storm_rational_number_ptr a #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; - + storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a + srn_b); return (storm_rational_number_ptr)result_srn; } @@ -175,10 +175,10 @@ storm_rational_number_ptr storm_rational_number_minus(storm_rational_number_ptr #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; - + storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a - srn_b); return (storm_rational_number_ptr)result_srn; } @@ -187,10 +187,10 @@ storm_rational_number_ptr storm_rational_number_times(storm_rational_number_ptr #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; - + storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a * srn_b); return (storm_rational_number_ptr)result_srn; } @@ -199,10 +199,10 @@ storm_rational_number_ptr storm_rational_number_divide(storm_rational_number_ptr #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; - + storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a / srn_b); return (storm_rational_number_ptr)result_srn; } @@ -211,7 +211,7 @@ storm_rational_number_ptr storm_rational_number_pow(storm_rational_number_ptr a, #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; @@ -224,7 +224,7 @@ storm_rational_number_ptr storm_rational_number_mod(storm_rational_number_ptr a, #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; if (carl::isInteger(srn_a) && carl::isInteger(srn_b)) { @@ -235,18 +235,10 @@ storm_rational_number_ptr storm_rational_number_mod(storm_rational_number_ptr a, } storm_rational_number_ptr storm_rational_number_min(storm_rational_number_ptr a, storm_rational_number_ptr b) { -#ifndef RATIONAL_NUMBER_THREAD_SAFE - std::lock_guard lock(rationalNumberMutex); -#endif - return storm_rational_number_less_or_equal(a, b) ? storm_rational_number_clone(a) : storm_rational_number_clone(b); } storm_rational_number_ptr storm_rational_number_max(storm_rational_number_ptr a, storm_rational_number_ptr b) { -#ifndef RATIONAL_NUMBER_THREAD_SAFE - std::lock_guard lock(rationalNumberMutex); -#endif - return storm_rational_number_less(a, b) ? storm_rational_number_clone(b) : storm_rational_number_clone(a); } @@ -254,16 +246,16 @@ int storm_rational_number_less(storm_rational_number_ptr a, storm_rational_numbe #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; - + if (storm::utility::isInfinity(srn_b)) { return storm::utility::isInfinity(srn_a) ? 0 : 1; } else if (storm::utility::isInfinity(srn_a)) { return 0; } - + return srn_a < srn_b ? 1 : 0; } @@ -271,16 +263,16 @@ int storm_rational_number_less_or_equal(storm_rational_number_ptr a, storm_ratio #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; - + if (storm::utility::isInfinity(srn_b)) { return 1; } else if (storm::utility::isInfinity(srn_a)) { return 0; } - + return srn_a <= srn_b ? 1 : 0; } @@ -288,7 +280,7 @@ storm_rational_number_ptr storm_rational_number_negate(storm_rational_number_ptr #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber* result_srn = new storm::RationalNumber(-srn_a); return (storm_rational_number_ptr)result_srn; @@ -298,7 +290,7 @@ storm_rational_number_ptr storm_rational_number_floor(storm_rational_number_ptr #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber* result_srn = new storm::RationalNumber(carl::floor(srn_a)); return (storm_rational_number_ptr)result_srn; @@ -308,7 +300,7 @@ storm_rational_number_ptr storm_rational_number_ceil(storm_rational_number_ptr a #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber* result_srn = new storm::RationalNumber(carl::ceil(srn_a)); return (storm_rational_number_ptr)result_srn; @@ -363,7 +355,7 @@ void print_storm_rational_number(storm_rational_number_ptr a) { #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; } @@ -371,7 +363,7 @@ void print_storm_rational_number_to_file(storm_rational_number_ptr a, FILE* out) #ifndef RATIONAL_NUMBER_THREAD_SAFE std::lock_guard lock(rationalNumberMutex); #endif - + std::stringstream ss; storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; ss << srn_a; @@ -387,7 +379,7 @@ void storm_rational_function_init(storm_rational_function_ptr* a) { #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a))); *a = srf_ptr; } @@ -396,7 +388,7 @@ void storm_rational_function_destroy(storm_rational_function_ptr a) { #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction* srf = (storm::RationalFunction*)a; delete srf; } @@ -405,10 +397,10 @@ int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction*)a; storm::RationalFunction const& srf_b = *(storm::RationalFunction*)b; - + return (srf_a == srf_b) ? 1 : 0; } @@ -416,7 +408,7 @@ char* storm_rational_function_to_str(storm_rational_function_ptr val, char* buf, #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + std::stringstream ss; storm::RationalFunction const& srf_a = *(storm::RationalFunction*)val; ss << srf_a; @@ -435,7 +427,7 @@ storm_rational_function_ptr storm_rational_function_clone(storm_rational_functio #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction* result_srf = new storm::RationalFunction(*((storm::RationalFunction const*)a)); return (storm_rational_function_ptr)result_srf; } @@ -444,7 +436,7 @@ storm_rational_function_ptr storm_rational_function_get_zero() { #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::zero()); return (storm_rational_function_ptr)result_srf; } @@ -453,7 +445,7 @@ storm_rational_function_ptr storm_rational_function_get_one() { #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::one()); return (storm_rational_function_ptr)result_srf; } @@ -462,7 +454,7 @@ 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; } @@ -472,7 +464,7 @@ int storm_rational_function_is_zero(storm_rational_function_ptr a) { #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + return storm::utility::isZero(*(storm::RationalFunction const*)a) ? 1 : 0; } @@ -480,9 +472,9 @@ uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint6 #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; - + // Taken from boost::hash_combine that we do not call here for the lack of boost headers. return seed ^ (std::hash()(srf_a) + 0x9e3779b9 + (seed<<6) + (seed>>2)); } @@ -491,7 +483,7 @@ double storm_rational_function_get_value_double(storm_rational_function_ptr a) { #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; if (srf_a.isConstant()) { return storm::utility::convertNumber(srf_a); @@ -504,10 +496,10 @@ storm_rational_function_ptr storm_rational_function_plus(storm_rational_function #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; - + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); *result_srf += srf_b; return (storm_rational_function_ptr)result_srf; @@ -517,10 +509,10 @@ storm_rational_function_ptr storm_rational_function_minus(storm_rational_functio #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; - + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); *result_srf -= srf_b; return (storm_rational_function_ptr)result_srf; @@ -530,10 +522,10 @@ storm_rational_function_ptr storm_rational_function_times(storm_rational_functio #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; - + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); *result_srf *= srf_b; return (storm_rational_function_ptr)result_srf; @@ -543,10 +535,10 @@ storm_rational_function_ptr storm_rational_function_divide(storm_rational_functi #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; - + storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); *result_srf /= srf_b; return (storm_rational_function_ptr)result_srf; @@ -556,10 +548,10 @@ storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; - + carl::uint exponentAsInteger = carl::toInt(srf_b.nominatorAsNumber()); storm::RationalFunction* result_srf = new storm::RationalFunction(carl::pow(srf_a, exponentAsInteger)); return (storm_rational_function_ptr)result_srf; @@ -569,10 +561,10 @@ storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; - + if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) { throw storm::exceptions::InvalidOperationException() << "Operands of mod must not be non-constant rational functions."; } @@ -580,43 +572,27 @@ storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ } storm_rational_function_ptr storm_rational_function_min(storm_rational_function_ptr a, storm_rational_function_ptr b) { -#ifndef RATIONAL_FUNCTION_THREAD_SAFE - std::lock_guard lock(rationalFunctionMutex); -#endif - - if (storm_rational_function_less_or_equal(a, b)) { - return storm_rational_function_clone(a); - } else { - return storm_rational_function_clone(b); - } + return storm_rational_function_less_or_equal(a, b) ? storm_rational_function_clone(a) : storm_rational_function_clone(b); } storm_rational_function_ptr storm_rational_function_max(storm_rational_function_ptr a, storm_rational_function_ptr b) { -#ifndef RATIONAL_FUNCTION_THREAD_SAFE - std::lock_guard lock(rationalFunctionMutex); -#endif - - if (storm_rational_function_less(a, b)) { - return storm_rational_function_clone(b); - } else { - return storm_rational_function_clone(a); - } + return storm_rational_function_less(a, b) ? storm_rational_function_clone(b) : storm_rational_function_clone(a); } int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_function_ptr b) { #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) { throw storm::exceptions::InvalidOperationException() << "Operands of less must not be non-constant rational functions."; } - + storm::RationalFunctionCoefficient srn_a = storm::utility::convertNumber(srf_a); storm::RationalFunctionCoefficient srn_b = storm::utility::convertNumber(srf_b); - + if (storm::utility::isInfinity(srn_b)) { return storm::utility::isInfinity(srn_a) ? 0 : 1; } else if (storm::utility::isInfinity(srn_a)) { @@ -630,22 +606,22 @@ int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_r #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) { throw storm::exceptions::InvalidOperationException() << "Operands of less-or-equal must not be non-constant rational functions."; } - + storm::RationalFunctionCoefficient srn_a = storm::utility::convertNumber(srf_a); storm::RationalFunctionCoefficient srn_b = storm::utility::convertNumber(srf_b); - + if (storm::utility::isInfinity(srn_b)) { return 1; } else if (storm::utility::isInfinity(srn_a)) { return 0; } - + return (srn_a <= srn_b) ? 1 : 0; } @@ -653,7 +629,7 @@ storm_rational_function_ptr storm_rational_function_negate(storm_rational_functi #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction* result_srf = new storm::RationalFunction(-srf_a); return (storm_rational_function_ptr)result_srf; @@ -663,7 +639,7 @@ storm_rational_function_ptr storm_rational_function_floor(storm_rational_functio #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; if (!storm::utility::isConstant(srf_a)) { throw storm::exceptions::InvalidOperationException() << "Operand of floor must not be non-constant rational function."; @@ -676,7 +652,7 @@ storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; if (!storm::utility::isConstant(srf_a)) { throw storm::exceptions::InvalidOperationException() << "Operand of ceil must not be non-constant rational function."; @@ -689,15 +665,15 @@ int storm_rational_function_equal_modulo_precision(int relative, storm_rational_ #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; storm::RationalFunction const& srf_p = *(storm::RationalFunction const*)precision; - + if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b) || !storm::utility::isConstant(srf_p)) { throw storm::exceptions::InvalidOperationException() << "Operands of equal-modulo-precision must not be non-constant rational functions."; } - + storm::RationalFunctionCoefficient srn_a = storm::utility::convertNumber(srf_a); storm::RationalFunctionCoefficient srn_b = storm::utility::convertNumber(srf_b); storm::RationalFunctionCoefficient srn_p = storm::utility::convertNumber(srf_p); @@ -713,7 +689,7 @@ void print_storm_rational_function(storm_rational_function_ptr a) { #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; std::cout << srf_a << std::flush; } @@ -722,7 +698,7 @@ void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE* #ifndef RATIONAL_FUNCTION_THREAD_SAFE std::lock_guard lock(rationalFunctionMutex); #endif - + std::stringstream ss; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; ss << srf_a;