fixed two bugs related to hybrid quantitative results

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

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)

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

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)

src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp

@@ -21,17 +21,17 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ValueType>
         std::unique_ptr<CheckResult> HybridQuantitativeCheckResult<Type, ValueType>::compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const {
-            storm::dd::Bdd<Type> symbolicResult;
-
+            storm::dd::Bdd<Type> 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.