From c98d149d515e1c4353979d787a1ad3adbc5cc889 Mon Sep 17 00:00:00 2001
From: Filip Macak <filip.macak1999@gmail.com>
Date: Mon, 25 Nov 2024 12:52:30 +0100
Subject: [PATCH] Fix for MDP counter examples

---
 .../counterexamples/CounterexampleMdp.cpp       | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/payntbind/src/synthesis/counterexamples/CounterexampleMdp.cpp b/payntbind/src/synthesis/counterexamples/CounterexampleMdp.cpp
index f35d9c55b..a1a05dcb1 100644
--- 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;