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

to_parity: Add an option to force degeneralization

Browse source 
* spot/twaalgos/toparity.cc, spot/twaalgos/toparity.hh:
Don't try to run the algorithm without degeneralization
with the option force_degen.
This commit is contained in:
Florian Renkin 2020-04-17 14:23:59 +02:00
parent 527b62c5ff
commit 685d6d8ba0
2 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

7
spot/twaalgos/toparity.cc
View file

@ -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());

5
spot/twaalgos/toparity.hh
View file

@ -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.