diff --git a/payntbind/src/synthesis/counterexamples/Counterexample.cpp b/payntbind/src/synthesis/counterexamples/Counterexample.cpp index 2bcc08990..f23f952c0 100644 --- 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(env, subdtmc, task); this->timer_model_check.stop(); storm::modelchecker::ExplicitQuantitativeCheckResult& result = this->hint_result->template asExplicitQuantitativeCheckResult(); + + 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;