spot
2.9.1
|
Options to control various optimizations of to_parity(). More...
#include <spot/twaalgos/toparity.hh>
Public Attributes | |
bool | search_ex = true |
bool | use_last = true |
bool | force_order = true |
bool | partial_degen = true |
bool | force_degen = true |
bool | acc_clean = true |
bool | parity_equiv = true |
bool | parity_prefix = true |
bool | rabin_to_buchi = true |
bool | reduce_col_deg = false |
bool | propagate_col = true |
bool | pretty_print = false |
Options to control various optimizations of to_parity().
bool spot::to_parity_options::acc_clean = true |
If scc_acc_clean
is true, to_parity() will ignore colors no occoring in an SCC while processing this SCC.
bool spot::to_parity_options::force_degen = true |
If force_degen
is false, to_parity will checks if we can get a better result if we don't apply partial_degeneralize.
bool spot::to_parity_options::force_order = true |
If force_order
is true, we force to use an order when CAR or IAR is applied. Given a state s and a set E ({0}, {0 1}, {2} for example) we construct an order on colors. With the given example, we ask to have a permutation that start with [0 …], [0 1 …] or [2 …] in that order of preference.
bool spot::to_parity_options::parity_equiv = true |
If parity_equiv
is true, to_parity() will check if there exists a permutations of colors such that the acceptance condition is a parity condition.
bool spot::to_parity_options::parity_prefix = true |
If parity_prefix
is true, to_parity() will use a special handling for acceptance conditions of the form Inf(m0) | (Fin(m1) & (Inf(m2) | (… β)))
that start as a parity condition (modulo a renumbering of m0
, m1
, m2
, ...) but where β
can be an arbitrary formula. In this case, the paritization algorithm is really applied only to β
, and the marks of the prefix are appended after a suitable renumbering.
For technical reasons, activating this option (and this is the default) causes reduce_parity() to be called at the end to minimize the number of colors used. It is therefore recommended to disable this option when one wants to follow the output CAR/IAR constructions.
bool spot::to_parity_options::partial_degen = true |
If partial_degen
is true, apply a partial degeneralization to remove occurrences of acceptance subformulas such as Fin(x) | Fin(y)
or Inf(x) & Inf(y)
.
bool spot::to_parity_options::pretty_print = false |
If pretty_print
is true, states of the output automaton are named to help debugging.
bool spot::to_parity_options::propagate_col = true |
Use propagate_marks_here to increase the number of marks on transition in order to move more colors (and increase the number of compatible states) when we apply LAR.
bool spot::to_parity_options::rabin_to_buchi = true |
If rabin_to_buchi
is true, to_parity() tries to convert a Rabin or Streett condition to Büchi or co-Büchi with rabin_to_buchi_if_realizable().
bool spot::to_parity_options::reduce_col_deg = false |
Only allow degeneralization if it reduces the number of colors in the acceptance condition.
bool spot::to_parity_options::search_ex = true |
If search_ex
is true, whenever CAR or IAR have to move several elements in a record, it tries to find an order such that the new permutation already exists.
bool spot::to_parity_options::use_last = true |
If use_last
is true and search_ex are true, we use the most recent state when we find multiple existing state compatible with the current move.