sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Remove erroneous mutex lock in sylvan_wrapper 

Also remove trailing whitespace
tempestpy_adaptions
Daniel Basgöze 3 years ago
committed by Stefan Pranger
parent
12111a91bd
commit
22a9703524
1 changed files with 77 additions and 101 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 178
      resources/3rdparty/sylvan/src/storm_wrapper.cpp

178
resources/3rdparty/sylvan/src/storm_wrapper.cpp
View File

@ -42,7 +42,7 @@ void storm_rational_number_init(storm_rational_number_ptr* a) {
#ifndef RATIONAL_NUMBER_THREAD_SAFE #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm_rational_number_ptr srn_ptr = new storm::RationalNumber(*((storm::RationalNumber*)(*a))); storm_rational_number_ptr srn_ptr = new storm::RationalNumber(*((storm::RationalNumber*)(*a)));
*a = srn_ptr; *a = srn_ptr;
} }
@ -51,7 +51,7 @@ void storm_rational_number_destroy(storm_rational_number_ptr a) {
#ifndef RATIONAL_NUMBER_THREAD_SAFE #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber* srn_ptr = (storm::RationalNumber*)a; storm::RationalNumber* srn_ptr = (storm::RationalNumber*)a;
delete srn_ptr; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber*)a; storm::RationalNumber const& srn_a = *(storm::RationalNumber*)a;
storm::RationalNumber const& srn_b = *(storm::RationalNumber*)b; storm::RationalNumber const& srn_b = *(storm::RationalNumber*)b;
return (srn_a == srn_b) ? 1 : 0; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
std::stringstream ss; std::stringstream ss;
storm::RationalNumber const& srn_a = *(storm::RationalNumber*)val; storm::RationalNumber const& srn_a = *(storm::RationalNumber*)val;
ss << srn_a; ss << srn_a;
@ -90,7 +90,7 @@ storm_rational_number_ptr storm_rational_number_clone(storm_rational_number_ptr
#ifndef RATIONAL_NUMBER_THREAD_SAFE #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber* result_srn = new storm::RationalNumber(*((storm::RationalNumber const*)a)); storm::RationalNumber* result_srn = new storm::RationalNumber(*((storm::RationalNumber const*)a));
return (storm_rational_number_ptr)result_srn; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::zero<storm::RationalNumber>()); storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::zero<storm::RationalNumber>());
return (storm_rational_number_ptr)result_srn; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::one<storm::RationalNumber>()); storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::one<storm::RationalNumber>());
return (storm_rational_number_ptr)result_srn; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::infinity<storm::RationalNumber>()); storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::infinity<storm::RationalNumber>());
return (storm_rational_number_ptr)result_srn; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
return storm::utility::isZero(*(storm::RationalNumber const*)a) ? 1 : 0; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; 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. // Taken from boost::hash_combine that we do not call here for the lack of boost headers.
return seed ^ (std::hash<storm::RationalNumber>()(srn_a) + 0x9e3779b9 + (seed<<6) + (seed>>2)); return seed ^ (std::hash<storm::RationalNumber>()(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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
return storm::utility::convertNumber<double>(srn_a); return storm::utility::convertNumber<double>(srn_a);
} }
@ -154,7 +154,7 @@ storm_rational_number_ptr storm_rational_number_from_double(double value) {
#ifndef RATIONAL_NUMBER_THREAD_SAFE #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber* number = new storm::RationalNumber(storm::utility::convertNumber<storm::RationalNumber>(value)); storm::RationalNumber* number = new storm::RationalNumber(storm::utility::convertNumber<storm::RationalNumber>(value));
return number; return number;
} }
@ -163,10 +163,10 @@ storm_rational_number_ptr storm_rational_number_plus(storm_rational_number_ptr a
#ifndef RATIONAL_NUMBER_THREAD_SAFE #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a + srn_b); storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a + srn_b);
return (storm_rational_number_ptr)result_srn; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a - srn_b); storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a - srn_b);
return (storm_rational_number_ptr)result_srn; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a * srn_b); storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a * srn_b);
return (storm_rational_number_ptr)result_srn; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a / srn_b); storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a / srn_b);
return (storm_rational_number_ptr)result_srn; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
if (carl::isInteger(srn_a) && carl::isInteger(srn_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) { 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<std::mutex> lock(rationalNumberMutex);
#endif
return storm_rational_number_less_or_equal(a, b) ? storm_rational_number_clone(a) : storm_rational_number_clone(b); 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) { 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<std::mutex> lock(rationalNumberMutex);
#endif
return storm_rational_number_less(a, b) ? storm_rational_number_clone(b) : storm_rational_number_clone(a); 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
if (storm::utility::isInfinity<storm::RationalNumber>(srn_b)) { if (storm::utility::isInfinity<storm::RationalNumber>(srn_b)) {
return storm::utility::isInfinity<storm::RationalNumber>(srn_a) ? 0 : 1; return storm::utility::isInfinity<storm::RationalNumber>(srn_a) ? 0 : 1;
} else if (storm::utility::isInfinity<storm::RationalNumber>(srn_a)) { } else if (storm::utility::isInfinity<storm::RationalNumber>(srn_a)) {
return 0; return 0;
} }
return srn_a < srn_b ? 1 : 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b; storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
if (storm::utility::isInfinity<storm::RationalNumber>(srn_b)) { if (storm::utility::isInfinity<storm::RationalNumber>(srn_b)) {
return 1; return 1;
} else if (storm::utility::isInfinity<storm::RationalNumber>(srn_a)) { } else if (storm::utility::isInfinity<storm::RationalNumber>(srn_a)) {
return 0; return 0;
} }
return srn_a <= srn_b ? 1 : 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
storm::RationalNumber* result_srn = new storm::RationalNumber(-srn_a); storm::RationalNumber* result_srn = new storm::RationalNumber(-srn_a);
return (storm_rational_number_ptr)result_srn; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
storm::RationalNumber* result_srn = new storm::RationalNumber(carl::floor(srn_a)); storm::RationalNumber* result_srn = new storm::RationalNumber(carl::floor(srn_a));
return (storm_rational_number_ptr)result_srn; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
storm::RationalNumber* result_srn = new storm::RationalNumber(carl::ceil(srn_a)); storm::RationalNumber* result_srn = new storm::RationalNumber(carl::ceil(srn_a));
return (storm_rational_number_ptr)result_srn; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; 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 #ifndef RATIONAL_NUMBER_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalNumberMutex); std::lock_guard<std::mutex> lock(rationalNumberMutex);
#endif #endif
std::stringstream ss; std::stringstream ss;
storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a; storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
ss << srn_a; ss << srn_a;
@ -387,7 +379,7 @@ void storm_rational_function_init(storm_rational_function_ptr* a) {
#ifndef RATIONAL_FUNCTION_THREAD_SAFE #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a))); storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a)));
*a = srf_ptr; *a = srf_ptr;
} }
@ -396,7 +388,7 @@ void storm_rational_function_destroy(storm_rational_function_ptr a) {
#ifndef RATIONAL_FUNCTION_THREAD_SAFE #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction* srf = (storm::RationalFunction*)a; storm::RationalFunction* srf = (storm::RationalFunction*)a;
delete srf; delete srf;
} }
@ -405,10 +397,10 @@ int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational
#ifndef RATIONAL_FUNCTION_THREAD_SAFE #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction*)a;
storm::RationalFunction const& srf_b = *(storm::RationalFunction*)b; storm::RationalFunction const& srf_b = *(storm::RationalFunction*)b;
return (srf_a == srf_b) ? 1 : 0; 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
std::stringstream ss; std::stringstream ss;
storm::RationalFunction const& srf_a = *(storm::RationalFunction*)val; storm::RationalFunction const& srf_a = *(storm::RationalFunction*)val;
ss << srf_a; ss << srf_a;
@ -435,7 +427,7 @@ storm_rational_function_ptr storm_rational_function_clone(storm_rational_functio
#ifndef RATIONAL_FUNCTION_THREAD_SAFE #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction* result_srf = new storm::RationalFunction(*((storm::RationalFunction const*)a)); storm::RationalFunction* result_srf = new storm::RationalFunction(*((storm::RationalFunction const*)a));
return (storm_rational_function_ptr)result_srf; 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::zero<storm::RationalFunction>()); storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::zero<storm::RationalFunction>());
return (storm_rational_function_ptr)result_srf; 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::one<storm::RationalFunction>()); storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::one<storm::RationalFunction>());
return (storm_rational_function_ptr)result_srf; 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::infinity<storm::RationalFunction>()); storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::infinity<storm::RationalFunction>());
return (storm_rational_function_ptr)result_srf; 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
return storm::utility::isZero(*(storm::RationalFunction const*)a) ? 1 : 0; 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; 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. // Taken from boost::hash_combine that we do not call here for the lack of boost headers.
return seed ^ (std::hash<storm::RationalFunction>()(srf_a) + 0x9e3779b9 + (seed<<6) + (seed>>2)); return seed ^ (std::hash<storm::RationalFunction>()(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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
if (srf_a.isConstant()) { if (srf_a.isConstant()) {
return storm::utility::convertNumber<double>(srf_a); return storm::utility::convertNumber<double>(srf_a);
@ -504,10 +496,10 @@ storm_rational_function_ptr storm_rational_function_plus(storm_rational_function
#ifndef RATIONAL_FUNCTION_THREAD_SAFE #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
*result_srf += srf_b; *result_srf += srf_b;
return (storm_rational_function_ptr)result_srf; 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
*result_srf -= srf_b; *result_srf -= srf_b;
return (storm_rational_function_ptr)result_srf; 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
*result_srf *= srf_b; *result_srf *= srf_b;
return (storm_rational_function_ptr)result_srf; 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a); storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
*result_srf /= srf_b; *result_srf /= srf_b;
return (storm_rational_function_ptr)result_srf; 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
carl::uint exponentAsInteger = carl::toInt<carl::uint>(srf_b.nominatorAsNumber()); carl::uint exponentAsInteger = carl::toInt<carl::uint>(srf_b.nominatorAsNumber());
storm::RationalFunction* result_srf = new storm::RationalFunction(carl::pow(srf_a, exponentAsInteger)); storm::RationalFunction* result_srf = new storm::RationalFunction(carl::pow(srf_a, exponentAsInteger));
return (storm_rational_function_ptr)result_srf; 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_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."; 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) { 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<std::mutex> 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) { 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<std::mutex> 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) { int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_function_ptr b) {
#ifndef RATIONAL_FUNCTION_THREAD_SAFE #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_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."; throw storm::exceptions::InvalidOperationException() << "Operands of less must not be non-constant rational functions.";
} }
storm::RationalFunctionCoefficient srn_a = storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a); storm::RationalFunctionCoefficient srn_a = storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a);
storm::RationalFunctionCoefficient srn_b = storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_b); storm::RationalFunctionCoefficient srn_b = storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_b);
if (storm::utility::isInfinity<storm::RationalFunctionCoefficient>(srn_b)) { if (storm::utility::isInfinity<storm::RationalFunctionCoefficient>(srn_b)) {
return storm::utility::isInfinity<storm::RationalFunctionCoefficient>(srn_a) ? 0 : 1; return storm::utility::isInfinity<storm::RationalFunctionCoefficient>(srn_a) ? 0 : 1;
} else if (storm::utility::isInfinity<storm::RationalFunctionCoefficient>(srn_a)) { } else if (storm::utility::isInfinity<storm::RationalFunctionCoefficient>(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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_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."; throw storm::exceptions::InvalidOperationException() << "Operands of less-or-equal must not be non-constant rational functions.";
} }
storm::RationalFunctionCoefficient srn_a = storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a); storm::RationalFunctionCoefficient srn_a = storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a);
storm::RationalFunctionCoefficient srn_b = storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_b); storm::RationalFunctionCoefficient srn_b = storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_b);
if (storm::utility::isInfinity<storm::RationalFunctionCoefficient>(srn_b)) { if (storm::utility::isInfinity<storm::RationalFunctionCoefficient>(srn_b)) {
return 1; return 1;
} else if (storm::utility::isInfinity<storm::RationalFunctionCoefficient>(srn_a)) { } else if (storm::utility::isInfinity<storm::RationalFunctionCoefficient>(srn_a)) {
return 0; return 0;
} }
return (srn_a <= srn_b) ? 1 : 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
storm::RationalFunction* result_srf = new storm::RationalFunction(-srf_a); storm::RationalFunction* result_srf = new storm::RationalFunction(-srf_a);
return (storm_rational_function_ptr)result_srf; 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
if (!storm::utility::isConstant(srf_a)) { if (!storm::utility::isConstant(srf_a)) {
throw storm::exceptions::InvalidOperationException() << "Operand of floor must not be non-constant rational function."; 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
if (!storm::utility::isConstant(srf_a)) { if (!storm::utility::isConstant(srf_a)) {
throw storm::exceptions::InvalidOperationException() << "Operand of ceil must not be non-constant rational function."; 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b; storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
storm::RationalFunction const& srf_p = *(storm::RationalFunction const*)precision; 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)) { 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."; throw storm::exceptions::InvalidOperationException() << "Operands of equal-modulo-precision must not be non-constant rational functions.";
} }
storm::RationalFunctionCoefficient srn_a = storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a); storm::RationalFunctionCoefficient srn_a = storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a);
storm::RationalFunctionCoefficient srn_b = storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_b); storm::RationalFunctionCoefficient srn_b = storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_b);
storm::RationalFunctionCoefficient srn_p = storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_p); storm::RationalFunctionCoefficient srn_p = storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_p);
@ -713,7 +689,7 @@ void print_storm_rational_function(storm_rational_function_ptr a) {
#ifndef RATIONAL_FUNCTION_THREAD_SAFE #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
std::cout << srf_a << std::flush; 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 #ifndef RATIONAL_FUNCTION_THREAD_SAFE
std::lock_guard<std::mutex> lock(rationalFunctionMutex); std::lock_guard<std::mutex> lock(rationalFunctionMutex);
#endif #endif
std::stringstream ss; std::stringstream ss;
storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a; storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
ss << srf_a; ss << srf_a;

Write Preview
Loading…
Cancel
Save