From f57782686d434695bcd4d3676c3de97c6d02e9fc Mon Sep 17 00:00:00 2001 From: Florian Renkin Date: Tue, 16 Apr 2024 16:37:00 +0200 Subject: [PATCH] Rename minimize_obligation_garanteed_to_work minimize_obligation_garanteed_to_work is now minimize_obligation_guaranteed_to_work * spot/twaalgos/minimize.hh, spot/twaalgos/minimize.cc: change name. * spot/twaalgos/postproc.cc: update call * NEWS: Mention it. --- NEWS | 9 ++++++--- spot/twaalgos/minimize.cc | 4 ++-- spot/twaalgos/minimize.hh | 2 +- spot/twaalgos/postproc.cc | 2 +- 4 files changed, 10 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index 4bc2f452e..38b832611 100644 --- a/NEWS +++ b/NEWS @@ -109,10 +109,10 @@ New in spot 2.11.6.dev (not yet released) - spot::translate() has a new -x option "relabel-overlap=M" that augments the existing "relabel-bool=N". By default, N=4, M=8. When the formula to translate has more than N atomic propositions, - relabel_bse() is first called to attempt to rename non-overlaping + relabel_bse() is first called to attempt to rename non-overlapping boolean subexpressions (i.e., no shared atomic proposition) in order to reduce the number of atomic proposition, a source of - explonential explosion in several places of the translation + exponential explosion in several places of the translation pipeline. This relabel-bool optimization exists since Spot 2.4. The new feature is that if, after relabel-bool, the formula still has more than M atomic propositions, then spot::translate() now @@ -159,7 +159,7 @@ New in spot 2.11.6.dev (not yet released) t or co-Büchi). In case where the input automaton had no rejecting cycle, the Büchi acceptance was overkill: scc_filter will now use "t" acceptance. This change may have unexpected - conseqences in code paths that assume running scc_filter on a + consequences in code paths that assume running scc_filter on a Büchi automaton will always return a Büchi automaton. For those, a "keep_one_color" option has been added to scc_filter. @@ -195,6 +195,9 @@ New in spot 2.11.6.dev (not yet released) the acceptance, was sometimes able to simplify co-Büchi to "t", causing surprizes. + - Rename minimize_obligation_garanteed_to_work to + minimize_obligation_guaranteed_to_work. + Python: - The spot.automata() and spot.automaton() functions now accept a diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc index 399cc2541..97b182566 100644 --- a/spot/twaalgos/minimize.cc +++ b/spot/twaalgos/minimize.cc @@ -607,7 +607,7 @@ namespace spot return product(min_aut, aut_neg)->is_empty(); } - bool minimize_obligation_garanteed_to_work(const const_twa_graph_ptr& aut_f, + bool minimize_obligation_guaranteed_to_work(const const_twa_graph_ptr& aut_f, formula f) { // WDBA-minimization necessarily work for obligations @@ -644,7 +644,7 @@ namespace spot ("minimize_obligation() does not support alternation"); bool minimization_will_be_correct = false; - if (minimize_obligation_garanteed_to_work(aut_f, f)) + if (minimize_obligation_guaranteed_to_work(aut_f, f)) { minimization_will_be_correct = true; } diff --git a/spot/twaalgos/minimize.hh b/spot/twaalgos/minimize.hh index 0b5c11bf2..276da5149 100644 --- a/spot/twaalgos/minimize.hh +++ b/spot/twaalgos/minimize.hh @@ -130,7 +130,7 @@ namespace spot /// minimize_obligation(), but as it is less likely, you might /// decide to save time. SPOT_API - bool minimize_obligation_garanteed_to_work(const const_twa_graph_ptr& aut_f, + bool minimize_obligation_guaranteed_to_work(const const_twa_graph_ptr& aut_f, formula f = nullptr); /// @} diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index eabde299b..b7f6d27de 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -474,7 +474,7 @@ namespace spot wdba_minimize = 0; } if (wdba_minimize == 2) - wdba_minimize = minimize_obligation_garanteed_to_work(a, f); + wdba_minimize = minimize_obligation_guaranteed_to_work(a, f); if (wdba_minimize) { bool reject_bigger = (PREF_ == Small) && (level_ <= Medium);