spot  2.9.4
Public Attributes | List of all members

Options to control various optimizations of to_parity(). More...

#include <spot/twaalgos/toparity.hh>

Collaboration diagram for spot::to_parity_options:

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
 

Detailed Description

Options to control various optimizations of to_parity().

Member Data Documentation

◆ acc_clean

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.

◆ force_degen

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.

◆ force_order

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.

◆ parity_equiv

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.

◆ parity_prefix

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.

◆ partial_degen

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

◆ pretty_print

bool spot::to_parity_options::pretty_print = false

If pretty_print is true, states of the output automaton are named to help debugging.

◆ propagate_col

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.

◆ rabin_to_buchi

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().

◆ reduce_col_deg

bool spot::to_parity_options::reduce_col_deg = false

Only allow degeneralization if it reduces the number of colors in the acceptance condition.

◆ search_ex

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.

◆ use_last

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.


The documentation for this struct was generated from the following file:

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.8.13