diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c index 8cf8a5b88..a890e28a9 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c @@ -542,7 +542,7 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, a, MTBDD, b return result; } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, a, size_t, svalue) { +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, a, size_t*, svalue) { storm_rational_function_ptr value = (storm_rational_function_ptr)svalue; if (mtbdd_isleaf(a)) { @@ -553,7 +553,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, a, size_t return mtbdd_invalid; } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, a, size_t, svalue) { +TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, a, size_t*, svalue) { storm_rational_function_ptr value = (storm_rational_function_ptr)svalue; if (mtbdd_isleaf(a)) { @@ -567,12 +567,12 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, a, TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_threshold, MTBDD, dd, storm_rational_function_ptr, value) { - return mtbdd_uapply(dd, TASK(sylvan_storm_rational_function_op_threshold), *(size_t*)value); + return mtbdd_uapply(dd, TASK(sylvan_storm_rational_function_op_threshold), (size_t*)value); } TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_strict_threshold, MTBDD, dd, storm_rational_function_ptr, value) { - return mtbdd_uapply(dd, TASK(sylvan_storm_rational_function_op_strict_threshold), *(size_t*)value); + return mtbdd_uapply(dd, TASK(sylvan_storm_rational_function_op_strict_threshold), (size_t*)value); } TASK_IMPL_1(MTBDD, sylvan_storm_rational_function_minimum, MTBDD, a) { diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h index a47def0a1..888a80d51 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.h @@ -76,8 +76,8 @@ TASK_DECL_3(MTBDD, sylvan_storm_rational_function_and_exists, MTBDD, MTBDD, MTBD TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_to_double, MTBDD, size_t) #define sylvan_storm_rational_function_to_double(a) mtbdd_uapply_nocache(a, TASK(sylvan_storm_rational_function_op_to_double), 0) -TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, size_t) -TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, size_t) +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, size_t*) +TASK_DECL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, size_t*) TASK_DECL_2(MTBDD, sylvan_storm_rational_function_threshold, MTBDD, storm_rational_function_ptr); #define sylvan_storm_rational_function_threshold(dd, value) CALL(sylvan_storm_rational_function_strict_threshold, dd, value) diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c index 692a6f607..076e75442 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c @@ -576,7 +576,7 @@ TASK_IMPL_3(MTBDD, sylvan_storm_rational_number_and_exists, MTBDD, a, MTBDD, b, return result; } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, a, size_t, svalue) { +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, a, size_t*, svalue) { storm_rational_number_ptr value = (storm_rational_number_ptr)svalue; if (mtbdd_isleaf(a)) { @@ -587,7 +587,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, a, size_t, return mtbdd_invalid; } -TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, a, size_t, svalue) { +TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, a, size_t*, svalue) { storm_rational_number_ptr value = (storm_rational_number_ptr)svalue; if (mtbdd_isleaf(a)) { @@ -601,12 +601,12 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, a, s TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_threshold, MTBDD, dd, storm_rational_number_ptr, value) { - return mtbdd_uapply(dd, TASK(sylvan_storm_rational_number_op_threshold), *(size_t*)value); + return mtbdd_uapply(dd, TASK(sylvan_storm_rational_number_op_threshold), (size_t*)value); } TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_strict_threshold, MTBDD, dd, storm_rational_number_ptr, value) { - return mtbdd_uapply(dd, TASK(sylvan_storm_rational_number_op_strict_threshold), *(size_t*)value); + return mtbdd_uapply(dd, TASK(sylvan_storm_rational_number_op_strict_threshold), (size_t*)value); } TASK_IMPL_1(MTBDD, sylvan_storm_rational_number_minimum, MTBDD, a) { diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h index d7accd375..227a9831d 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.h @@ -76,8 +76,8 @@ TASK_DECL_3(MTBDD, sylvan_storm_rational_number_and_exists, MTBDD, MTBDD, MTBDD) TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_to_double, MTBDD, size_t) #define sylvan_storm_rational_number_to_double(a) mtbdd_uapply_nocache(a, TASK(sylvan_storm_rational_number_op_to_double), 0) -TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, size_t) -TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, size_t) +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, size_t*) +TASK_DECL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, size_t*) TASK_DECL_2(MTBDD, sylvan_storm_rational_number_threshold, MTBDD, storm_rational_number_ptr); #define sylvan_storm_rational_number_threshold(dd, value) CALL(sylvan_storm_rational_number_strict_threshold, dd, value) diff --git a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp index 324d8d1d6..ea6320bda 100644 --- a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -21,17 +21,17 @@ namespace storm { template std::unique_ptr HybridQuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const { - storm::dd::Bdd symbolicResult; - + storm::dd::Bdd symbolicResult = symbolicStates; + // First compute the symbolic part of the result. if (comparisonType == storm::logic::ComparisonType::Less) { - symbolicResult = symbolicValues.less(bound); + symbolicResult &= symbolicValues.less(bound); } else if (comparisonType == storm::logic::ComparisonType::LessEqual) { - symbolicResult = symbolicValues.lessOrEqual(bound); + symbolicResult &= symbolicValues.lessOrEqual(bound); } else if (comparisonType == storm::logic::ComparisonType::Greater) { - symbolicResult = symbolicValues.greater(bound); + symbolicResult &= symbolicValues.greater(bound); } else if (comparisonType == storm::logic::ComparisonType::GreaterEqual) { - symbolicResult = symbolicValues.greaterOrEqual(bound); + symbolicResult &= symbolicValues.greaterOrEqual(bound); } // Then translate the explicit part to a symbolic format and simultaneously to a qualitative result.