From 685d6d8ba097b374033245d641a77df03b4297cc Mon Sep 17 00:00:00 2001 From: Florian Renkin Date: Fri, 17 Apr 2020 14:23:59 +0200 Subject: [PATCH] to_parity: Add an option to force degeneralization * spot/twaalgos/toparity.cc, spot/twaalgos/toparity.hh: Don't try to run the algorithm without degeneralization with the option force_degen. --- spot/twaalgos/toparity.cc | 7 ++++--- spot/twaalgos/toparity.hh | 5 ++++- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index 32f5c7570..09fa6a5c1 100644 --- a/spot/twaalgos/toparity.cc +++ b/spot/twaalgos/toparity.cc @@ -1606,9 +1606,10 @@ run() max_states_sub_car = 10000 + nb_states_deg - 1; } - nb_states_sub = - build_scc(sub_automaton, scc, state2car_sub, car2num_sub, - algo_sub, max_states_sub_car); + if (!options.force_degen || !has_degeneralized) + nb_states_sub = + build_scc(sub_automaton, scc, state2car_sub, car2num_sub, + algo_sub, max_states_sub_car); if (nb_states_deg < nb_states_sub) { state2car.insert(state2car_deg.begin(), state2car_deg.end()); diff --git a/spot/twaalgos/toparity.hh b/spot/twaalgos/toparity.hh index fb4984342..a8e631baa 100644 --- a/spot/twaalgos/toparity.hh +++ b/spot/twaalgos/toparity.hh @@ -45,9 +45,12 @@ namespace spot /// degeneralization to remove occurrences of acceptance /// subformulas such as `Fin(x) | Fin(y)` or `Inf(x) & Inf(y)`. bool partial_degen = true; + /// If \c force_degen is false, to_parity will checks if we can + /// get a better result if we don't apply partial_degeneralize. + bool force_degen = true; /// If \c scc_acc_clean is true, to_parity() will ignore colors /// no occoring in an SCC while processing this SCC. - bool acc_clean = true; + bool acc_clean = true; /// If \a parity_equiv is true, to_parity() will check if there /// exists a permutations of colors such that the acceptance /// condition is a parity condition.