alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Rename minimize_obligation_garanteed_to_work

Browse source 
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.
This commit is contained in:
Florian Renkin 2024-04-16 16:37:00 +02:00
parent 96ff2225e3
commit f57782686d
4 changed files with 10 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

9
NEWS
View file

@ -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 - spot::translate() has a new -x option "relabel-overlap=M" that
augments the existing "relabel-bool=N". By default, N=4, M=8. augments the existing "relabel-bool=N". By default, N=4, M=8.
When the formula to translate has more than N atomic propositions, 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 boolean subexpressions (i.e., no shared atomic proposition) in
order to reduce the number of atomic proposition, a source of 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. pipeline. This relabel-bool optimization exists since Spot 2.4.
The new feature is that if, after relabel-bool, the formula still The new feature is that if, after relabel-bool, the formula still
has more than M atomic propositions, then spot::translate() now 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 t or co-Büchi). In case where the input automaton had no
rejecting cycle, the Büchi acceptance was overkill: scc_filter rejecting cycle, the Büchi acceptance was overkill: scc_filter
will now use "t" acceptance. This change may have unexpected 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, Büchi automaton will always return a Büchi automaton. For those,
a "keep_one_color" option has been added to scc_filter. 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", the acceptance, was sometimes able to simplify co-Büchi to "t",
causing surprizes. causing surprizes.
- Rename minimize_obligation_garanteed_to_work to
minimize_obligation_guaranteed_to_work.
Python: Python:
- The spot.automata() and spot.automaton() functions now accept a - The spot.automata() and spot.automaton() functions now accept a

4
spot/twaalgos/minimize.cc
View file

@ -607,7 +607,7 @@ namespace spot
return product(min_aut, aut_neg)->is_empty(); 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) formula f)
{ {
// WDBA-minimization necessarily work for obligations // WDBA-minimization necessarily work for obligations
@ -644,7 +644,7 @@ namespace spot
("minimize_obligation() does not support alternation"); ("minimize_obligation() does not support alternation");
bool minimization_will_be_correct = false; 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; minimization_will_be_correct = true;
} }

2
spot/twaalgos/minimize.hh
View file

@ -130,7 +130,7 @@ namespace spot
/// minimize_obligation(), but as it is less likely, you might /// minimize_obligation(), but as it is less likely, you might
/// decide to save time. /// decide to save time.
SPOT_API 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); formula f = nullptr);
/// @} /// @}

2
spot/twaalgos/postproc.cc
View file

@ -474,7 +474,7 @@ namespace spot
wdba_minimize = 0; wdba_minimize = 0;
} }
if (wdba_minimize == 2) 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) if (wdba_minimize)
{ {
bool reject_bigger = (PREF_ == Small) && (level_ <= Medium); bool reject_bigger = (PREF_ == Small) && (level_ <= Medium);