Fix for MDP counter examples

randriu · Nov 25, 2024 · c98d149 · c98d149
1 parent 0fdece1
commit c98d149
Showing 1 changed file with 13 additions and 4 deletions.
diff --git a/payntbind/src/synthesis/counterexamples/CounterexampleMdp.cpp b/payntbind/src/synthesis/counterexamples/CounterexampleMdp.cpp
@@ -465,13 +465,22 @@ std::pair<bool,bool> CounterexampleGeneratorMdp<ValueType,StateType>::expandAndC
     this->hint_result = storm::api::verifyWithSparseEngine<ValueType>(env, submdp, task);
     this->timer_model_check.stop();
     storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& model_check_result = this->hint_result->template asExplicitQuantitativeCheckResult<ValueType>();
+
+    auto comparisonType = this->formula_modified[index]->asOperatorFormula().getComparisonType();
+
     bool satisfied;
     if(this->formula_safety[formula_index]) {
-        satisfied = model_check_result[initial_state] < formula_bound;
-        // std::cout << model_check_result[initial_state] << " < " << formula_bound << std::endl;
+        if (comparisonType == storm::logic::ComparisonType::Less) {
+            satisfied = model_check_result[initial_state] < formula_bound;
+        } else {
+            satisfied = model_check_result[initial_state] <= formula_bound;
+        }
     } else {
-        satisfied = model_check_result[initial_state] > formula_bound;
-        // std::cout << model_check_result[initial_state] << " > " << formula_bound << std::endl;
+        if (comparisonType == storm::logic::ComparisonType::Greater) {
+            satisfied = model_check_result[initial_state] > formula_bound;
+        } else {
+            satisfied = model_check_result[initial_state] >= formula_bound;
+        }
     }
     result.second = satisfied;