From e8fab0718c387baf732a949a9188b30a410f63bf Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 21 Jun 2017 20:37:24 +0200
Subject: [PATCH 1/2] 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<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);
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 <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 22 Jun 2017 12:52:29 +0200
Subject: [PATCH 2/2] 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<storm::RationalFunction>;
}
-}
\ No newline at end of file
+}