Fixed counter example generation for properties with leq/geq comparis…

…on operators
randriu · Nov 25, 2024 · 0fdece1 · 0fdece1
1 parent b7ecfd3
commit 0fdece1
Showing 1 changed file with 13 additions and 2 deletions.
diff --git a/payntbind/src/synthesis/counterexamples/Counterexample.cpp b/payntbind/src/synthesis/counterexamples/Counterexample.cpp
@@ -417,11 +417,22 @@ namespace synthesis {
         this->hint_result = storm::api::verifyWithSparseEngine<ValueType>(env, subdtmc, task);
         this->timer_model_check.stop();
         storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& result = this->hint_result->template asExplicitQuantitativeCheckResult<ValueType>();
+
+        auto comparisonType = this->formula_modified[index]->asOperatorFormula().getComparisonType();
+
         bool satisfied;
         if(this->formula_safety[index]) {
-            satisfied = result[initial_state] < formula_bound;
+            if (comparisonType == storm::logic::ComparisonType::Less) {
+                satisfied = result[initial_state] < formula_bound;
+            } else {
+                satisfied = result[initial_state] <= formula_bound;
+            }
         } else {
-            satisfied = result[initial_state] > formula_bound;
+            if (comparisonType == storm::logic::ComparisonType::Greater) {
+                satisfied = result[initial_state] > formula_bound;
+            } else {
+                satisfied = result[initial_state] >= formula_bound;
+            }
         }
 
         return satisfied;