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.