From b3f72c63c6b70dfa7dfea2049575980d1ae8eba8 Mon Sep 17 00:00:00 2001 From: Roman Andriushchenko Date: Fri, 27 Sep 2024 17:17:57 +0200 Subject: [PATCH] DT synthesis: fix termination condition --- paynt/synthesizer/decision_tree.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/paynt/synthesizer/decision_tree.py b/paynt/synthesizer/decision_tree.py index 29dfe15f..03c48357 100644 --- a/paynt/synthesizer/decision_tree.py +++ b/paynt/synthesizer/decision_tree.py @@ -209,7 +209,9 @@ def map_scheduler(self, scheduler_choices, opt_result_value): self.best_tree = self.quotient.decision_tree self.best_tree.root.associate_assignment(self.best_assignment) self.best_tree_value = self.best_assignment_value - if abs( (self.best_assignment_value-opt_result_value)/opt_result_value ) < 1e-4: + if consistent: + break + if not disable_counterexamples and abs( (self.best_assignment_value-opt_result_value)/opt_result_value ) < 1e-4: break if self.resource_limit_reached():