|
spot 2.13
|
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 | use_last_post_process = false |
| bool | force_order = true |
| bool | partial_degen = true |
| bool | acc_clean = true |
| bool | parity_equiv = true |
| bool | car = true |
| bool | tar = false |
| bool | iar = true |
If iar is true, to_parity will try to apply IAR. More... | |
| bool | lar_dfs = true |
| bool | bscc = true |
| bool | parity_prefix = true |
| bool | parity_prefix_general = false |
| bool | generic_emptiness = false |
| bool | rabin_to_buchi = true |
| bool | buchi_type_to_buchi = false |
| bool | parity_type_to_parity = false |
| bool | reduce_col_deg = false |
| bool | propagate_col = true |
| bool | use_generalized_rabin = false |
| bool | pretty_print = false |
| to_parity_data * | datas = nullptr |
| Structure used to store some information about the construction. More... | |
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 not occurring in an SCC while processing this SCC.
| bool spot::to_parity_options::bscc = true |
If bscc is true, to_parity() will only keep the bottommost automaton when it applies LAR.
| bool spot::to_parity_options::buchi_type_to_buchi = false |
If buchi_type_to_buchi is true, to_parity converts a (co-)Büchi type automaton to a (co-)Büchi automaton.
| bool spot::to_parity_options::car = true |
If Car is true, to_parity will try to apply CAR. It is a version of LAR that tracks colors.
| to_parity_data* spot::to_parity_options::datas = nullptr |
Structure used to store some information about the construction.
| 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::generic_emptiness = false |
If generic_emptiness is true, to_parity() will check if the automaton does not accept any word with an emptiness check algorithm.
| bool spot::to_parity_options::iar = true |
If iar is true, to_parity will try to apply IAR.
| bool spot::to_parity_options::lar_dfs = true |
if lar_dfs is true, then when LAR is used the next state of the result that will be processed is the last created state.
| bool spot::to_parity_options::parity_equiv = true |
If parity_equiv is true, to_parity() will check if there exists a way to see the acceptance condition as a parity max one.
| 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.
| bool spot::to_parity_options::parity_prefix_general = false |
If parity_prefix_general is true, to_parity() will rewrite the acceptance condition as Inf(m0) | (Fin(m1) & (Inf(m2) | (… β))) before applying the same construction as with the option parity_prefix.
| bool spot::to_parity_options::parity_type_to_parity = false |
If parity_type_to_parity is true, to_parity converts a parity type automaton to a parity automaton.
| 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 partial degeneralization if it reduces the number of colors in the acceptance condition or if it implies to apply IAR instead of CAR.
| 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::tar = false |
If tar is true, to_parity will try to apply TAR. It is a version of LAR that tracks transitions instead of colors.
| bool spot::to_parity_options::use_generalized_rabin = false |
If use_generalized_buchi is true, each SCC will use a generalized Rabin acceptance in order to avoid CAR.
| 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.
| bool spot::to_parity_options::use_last_post_process = false |
If use_last_post_process is true, then when LAR ends, it tries to replace the destination of an edge by the newest compatible state.
1.9.4