spot
2.11.3

Modules  
Algorithms for parity acceptance  
Classes  
struct  spot::to_parity_options 
Options to control various optimizations of to_parity(). More...  
class  spot::zielonka_tree 
Zielonka Tree implementation. More...  
class  spot::acd 
Alternating Cycle Decomposition implementation. More...  
Enumerations  
enum class  spot::zielonka_tree_options { spot::NONE = 0 , spot::CHECK_RABIN = 1 , spot::CHECK_STREETT = 2 , spot::CHECK_PARITY = CHECK_RABIN  CHECK_STREETT , spot::ABORT_WRONG_SHAPE = 4 , spot::MERGE_SUBTREES = 8 } 
Options to alter the behavior of acd. More...  
enum class  spot::acd_options { spot::NONE = 0 , spot::CHECK_RABIN = 1 , spot::CHECK_STREETT = 2 , spot::CHECK_PARITY = CHECK_RABIN  CHECK_STREETT , spot::ABORT_WRONG_SHAPE = 4 , spot::ORDER_HEURISTIC = 8 } 
Options to alter the behavior of acd. More...  
Functions  
twa_graph_ptr  spot::degeneralize (const const_twa_graph_ptr &a, bool use_z_lvl=true, bool use_cust_acc_orders=false, int use_lvl_cache=1, bool skip_levels=true, bool ignaccsl=false, bool remove_extra_scc=true) 
Degeneralize a generalized (co)Büchi automaton into an equivalent (co)Büchi automaton. More...  
bool  spot::rabin_is_buchi_realizable (const const_twa_graph_ptr &aut) 
Check if aut is Rablinlike and Büchirealizable. More...  
twa_graph_ptr  spot::rabin_to_buchi_if_realizable (const const_twa_graph_ptr &aut) 
Convert a Rabinlike automaton into a Büchi automaton only when it can be done without changing the automaton structure. More...  
twa_graph_ptr  spot::rabin_to_buchi_maybe (const const_twa_graph_ptr &aut) 
Convert a Rabinlike automaton into a Büchi automaton, preserving determinism when possible. More...  
twa_graph_ptr  spot::remove_fin (const const_twa_graph_ptr &aut) 
Rewrite an automaton without Fin or f acceptance. More...  
bool  spot::has_separate_sets (const const_twa_graph_ptr &aut) 
Whether the Inf and Fin numbers are disjoints. More...  
twa_graph_ptr  spot::separate_sets_here (const twa_graph_ptr &aut) 
Separate the Fin and Inf sets used by an automaton. More...  
twa_graph_ptr  spot::to_parity (const const_twa_graph_ptr &aut, const to_parity_options options=to_parity_options()) 
Take an automaton with any acceptance condition and return an equivalent parity automaton. More...  
twa_graph_ptr  spot::to_parity_old (const const_twa_graph_ptr &aut, bool pretty_print=false) 
Take an automaton with any acceptance condition and return an equivalent parity automaton. More...  
spot::SPOT_DEPRECATED ("use to_parity() instead") twa_graph_ptr iar(const const_twa_graph_ptr &aut  
Turn a Rabinlike or Streettlike automaton into a parity automaton based on the index appearence record (IAR) More...  
spot::SPOT_DEPRECATED ("use to_parity() and spot::acc_cond::is_rabin_like() instead") twa_graph_ptr iar_maybe(const const_twa_graph_ptr &aut  
Turn a Rabinlike or Streettlike automaton into a parity automaton based on the index appearence record (IAR) More...  
twa_graph_ptr  spot::parity_type_to_parity (const twa_graph_ptr &aut) 
Convert an automaton into a parity max automaton preserving structure when possible. More...  
twa_graph_ptr  spot::buchi_type_to_buchi (const twa_graph_ptr &aut) 
Convert an automaton into a Büchi automaton preserving structure when possible. More...  
twa_graph_ptr  spot::co_buchi_type_to_co_buchi (const twa_graph_ptr &aut) 
Convert an automaton into a coBüchi automaton preserving structure when possible. More...  
twa_graph_ptr  spot::to_generalized_buchi (const const_twa_graph_ptr &aut) 
Take an automaton with any acceptance condition and return an equivalent Generalized Büchi automaton. More...  
twa_graph_ptr  spot::streett_to_generalized_buchi (const const_twa_graph_ptr &in) 
Convert Streett acceptance into generalized Büchi acceptance. More...  
twa_graph_ptr  spot::streett_to_generalized_buchi_maybe (const const_twa_graph_ptr &in) 
Convert Streett acceptance into generalized Büchi. More...  
twa_graph_ptr  spot::to_generalized_rabin (const const_twa_graph_ptr &aut, bool share_inf=false) 
Take an automaton with any acceptance condition and return an equivalent Generalized Rabin automaton. More...  
twa_graph_ptr  spot::to_generalized_streett (const const_twa_graph_ptr &aut, bool share_fin=false) 
Take an automaton with any acceptance condition and return an equivalent Generalized Streett automaton. More...  
twa_graph_ptr  spot::dnf_to_streett (const const_twa_graph_ptr &aut, bool original_states=false) 
Converts any DNF acceptance condition into Streettlike. More...  
twa_graph_ptr  spot::zielonka_tree_transform (const const_twa_graph_ptr &aut) 
Paritize an automaton using Zielonka tree. More...  
twa_graph_ptr  spot::cleanup_acceptance_here (twa_graph_ptr aut, bool strip=true) 
Remove useless acceptance sets. More...  
twa_graph_ptr  spot::cleanup_acceptance (const_twa_graph_ptr aut, bool strip=true) 
Remove useless acceptance sets. More...  
twa_graph_ptr  spot::simplify_acceptance_here (twa_graph_ptr aut) 
Simplify an acceptance condition. More...  
twa_graph_ptr  spot::simplify_acceptance (const_twa_graph_ptr aut) 
Simplify an acceptance condition. More...  
twa_graph_ptr  spot::partial_degeneralize (const const_twa_graph_ptr &a, acc_cond::mark_t todegen) 
@} More...  
twa_graph_ptr  spot::partial_degeneralize (twa_graph_ptr a) 
@} More...  
twa_graph_ptr  spot::acd_transform (const const_twa_graph_ptr &aut, bool colored=false) 
Paritize an automaton using ACD. More...  
twa_graph_ptr  spot::acd_transform_sbacc (const const_twa_graph_ptr &aut, bool colored=false, bool order_heuristic=true) 
Paritize an automaton using ACD. More...  

strong 
#include <spot/twaalgos/zlktree.hh>
Options to alter the behavior of acd.

strong 
#include <spot/twaalgos/zlktree.hh>
Options to alter the behavior of acd.
Enumerator  

NONE  Build the ZlkTree, without checking its shape. 
CHECK_RABIN  Check if the ZlkTree has Rabin shape. This actually has no effect unless ABORT_WRONG_SHAPE is set, because zielonka_tree always check the shape. 
CHECK_STREETT  Check if the ZlkTree has Streett shape. This actually has no effect unless ABORT_WRONG_SHAPE is set, because zielonka_tree always check the shape. 
CHECK_PARITY  Check if the ZlkTree has Parity shape This actually has no effect unless ABORT_WRONG_SHAPE is set, because zielonka_tree always check the shape. 
ABORT_WRONG_SHAPE  Abort the construction of the ZlkTree if it does not have the shape that is tested. When that happens, num_branches() is set to 0. 
MERGE_SUBTREES  Fuse identical substree. This cannot be used with zielonka_tree_transform(). However it saves memory if the only use of the zielonka_tree to check the shape. 
twa_graph_ptr spot::acd_transform  (  const const_twa_graph_ptr &  aut, 
bool  colored = false 

) 
#include <spot/twaalgos/zlktree.hh>
Paritize an automaton using ACD.
This corresponds to the application of Section 4 of [8]
The resulting automaton has a parity acceptance that is either "min odd" or "min even", depending on the original acceptance.
If colored is set, each output transition will have exactly one color, and the output automaton will use at most n+1 colors if the input has n colors. If colored is unsed (the default), output transitions will use at most one color, and output automaton will use at most n colors.
The acd_tranform() is the original function producing optimal transitionbased output (optimal in the sense of least number of duplicated states), while the acd_tansform_sbacc() variant produces statebased output from transitionbased input and without any optimality claim. The order_heuristics argument, enabled by default activates the ORDER_HEURISTICS option of the ACD.
twa_graph_ptr spot::acd_transform_sbacc  (  const const_twa_graph_ptr &  aut, 
bool  colored = false , 

bool  order_heuristic = true 

) 
#include <spot/twaalgos/zlktree.hh>
Paritize an automaton using ACD.
This corresponds to the application of Section 4 of [8]
The resulting automaton has a parity acceptance that is either "min odd" or "min even", depending on the original acceptance.
If colored is set, each output transition will have exactly one color, and the output automaton will use at most n+1 colors if the input has n colors. If colored is unsed (the default), output transitions will use at most one color, and output automaton will use at most n colors.
The acd_tranform() is the original function producing optimal transitionbased output (optimal in the sense of least number of duplicated states), while the acd_tansform_sbacc() variant produces statebased output from transitionbased input and without any optimality claim. The order_heuristics argument, enabled by default activates the ORDER_HEURISTICS option of the ACD.
twa_graph_ptr spot::buchi_type_to_buchi  (  const twa_graph_ptr &  aut  ) 
#include <spot/twaalgos/toparity.hh>
Convert an automaton into a Büchi automaton preserving structure when possible.
Return nullptr if no such automaton is found.
aut  Automaton that we want to convert 
twa_graph_ptr spot::cleanup_acceptance  (  const_twa_graph_ptr  aut, 
bool  strip = true 

) 
#include <spot/twaalgos/cleanacc.hh>
Remove useless acceptance sets.
Removes from aut the acceptance marks that are not used in its acceptance condition. Also removes from the acceptance conditions the terms that corresponds to empty or full sets.
If strip is true (the default), the remaining acceptance set numbers will be shifted down to reduce the maximal number of acceptance sets used.
cleanup_acceptance_here() works in place, cleanup_acceptance() returns a new automaton that has been simplified.
twa_graph_ptr spot::cleanup_acceptance_here  (  twa_graph_ptr  aut, 
bool  strip = true 

) 
#include <spot/twaalgos/cleanacc.hh>
Remove useless acceptance sets.
Removes from aut the acceptance marks that are not used in its acceptance condition. Also removes from the acceptance conditions the terms that corresponds to empty or full sets.
If strip is true (the default), the remaining acceptance set numbers will be shifted down to reduce the maximal number of acceptance sets used.
cleanup_acceptance_here() works in place, cleanup_acceptance() returns a new automaton that has been simplified.
twa_graph_ptr spot::co_buchi_type_to_co_buchi  (  const twa_graph_ptr &  aut  ) 
#include <spot/twaalgos/toparity.hh>
Convert an automaton into a coBüchi automaton preserving structure when possible.
Return nullptr if no such automaton is found.
aut  Automaton that we want to convert 
twa_graph_ptr spot::degeneralize  (  const const_twa_graph_ptr &  a, 
bool  use_z_lvl = true , 

bool  use_cust_acc_orders = false , 

int  use_lvl_cache = 1 , 

bool  skip_levels = true , 

bool  ignaccsl = false , 

bool  remove_extra_scc = true 

) 
#include <spot/twaalgos/degen.hh>
Degeneralize a generalized (co)Büchi automaton into an equivalent (co)Büchi automaton.
There are two variants of the function. If the generalizd (co)Büchi acceptance uses N colors, degeneralize() algorithm will builds a statebased (co)Büchi automaton that has at most (N+1) times the number of states of the original automaton. degeneralize_tba() builds a transitionbased (co)Büchi automaton that has at most N times the number of states of the original automaton.
Additional options control optimizations described in [1] . When use_z_lvl is set, the level of the degeneralized automaton is reset everytime an SCC is exited. If use_cust_acc_orders is set, the degeneralization will compute a custom acceptance order for each SCC (this option is disabled by default because our benchmarks show that it usually does more harm than good). If use_lvl_cache is set, everytime an SCC is entered on a state that as already been associated to some level elsewhere, reuse that level (set it to 2 to keep the smallest number, 3 to keep the largest level, and 1 to keep the first level found). If ignaccsl is set, we do not directly jump to the accepting level if the entering state has an accepting selfloop. If remove_extra_scc is set (the default) we ensure that the output automaton has as many SCCs as the input by removing superfluous SCCs.
Any of these three options will cause the SCCs of the automaton a to be computed prior to its actual degeneralization.
The mapping between each state of the resulting automaton and the original state of the input automaton is stored in the "originalstates" named property of the produced automaton. Call aut>get_named_prop<std::vector<unsigned>>("originalstates")
to retrieve it. However be aware that if the input automaton already defines the "originalstates" named property, it will be composed with the new one, so the "originalstates" of the degeneralized automaton will refer to the same automaton as the "originalstates" of the input automaton.
Note that these functions may return the original automaton asis if it is already degeneralized; in this case the "originalstates" property is not defined (or not changed).
Similarly, the property "degenlevels" keeps track of the degeneralization levels. To retrieve it, call aut>get_named_prop<std::vector<unsigned>>("degenlevels")
.
As an alternative method to degeneralization, one may also consider ACD transform. acd_transform() will never produce larger automata than degenaralize_tba(), and acd_transform_sbacc() produce smaller automata than degeneralize() on the average. See [9] for some comparisons.
@{
twa_graph_ptr spot::dnf_to_streett  (  const const_twa_graph_ptr &  aut, 
bool  original_states = false 

) 
#include <spot/twaalgos/totgba.hh>
Converts any DNF acceptance condition into Streettlike.
This function is an optimized version of the construction described by Lemma 4 and 5 of [5] .
In the described construction, as many copies as there are minterms in the acceptance condition are made and the union of all those copies is returned. Instead of cloning the automaton for each minterm and end up with many rejecting and useless SCC, we construct the automaton SCC by SCC. Each SCC is copied at most as many times as there are minterms for which it is not rejecting and at least one time if it is always rejecting (to be consistent with the recognized language).
aut The automaton to convert. original_states Enable mapping between each state of the resulting automaton and the original state of the input automaton. This is stored in the "originalstates" named property of the produced automaton. Call aut>get_named_prop<std::vector<unsigned>>("originalstates")
to retrieve it. Additionally, the correspondence between each created state and the associated DNF clause is recorded in the "originalclauses" property (also a vector of unsigned).
bool spot::has_separate_sets  (  const const_twa_graph_ptr &  aut  ) 
#include <spot/twaalgos/sepsets.hh>
Whether the Inf and Fin numbers are disjoints.
twa_graph_ptr spot::parity_type_to_parity  (  const twa_graph_ptr &  aut  ) 
#include <spot/twaalgos/toparity.hh>
Convert an automaton into a parity max automaton preserving structure when possible.
Return nullptr if no such automaton is found.
aut  Automaton that we want to convert 
twa_graph_ptr spot::partial_degeneralize  (  const const_twa_graph_ptr &  a, 
acc_cond::mark_t  todegen  
) 
#include <spot/twaalgos/degen.hh>
@}
Partial degeneralization of a TwA
Given an automaton whose acceptance contains a conjunction of Inf terms, perform a partial degeneralization to replace this conjunction by a single Inf term.
For instance if the input has acceptance (Fin(0)&Inf(1)&Inf(3))Fin(2) calling partial_degeneralize with todegen set to {1,3}
will build an equivalent automaton with acceptance (Fin(0)&Inf(2))Fin(1)
where Inf(2) tracks the acceptance of the original Inf(1)&Inf(3), and Fin(1) tracks the acceptance of the original Fin(2).
Cases where the sets listed in todegen also occur outside of the Infconjunction are also supported. Subformulas that are disjunctions of Fin(.) terms (e.g., Fin(1)Fin(2)) will be degeneralized as well.
If this functions is called with a value of todegen that does not match a conjunction of Inf(.), or a disjunction of Fin(.), an std::runtime_error exception is thrown.
The version of the function that has no todegen argument will perform all possible partial degeneralizations, and may return the input automaton unmodified if no partial degeneralization is possible.
The "originalstate" and "degenlevels" named properties are updated as for degeneralize() and degeneralize_tba().
twa_graph_ptr spot::partial_degeneralize  (  twa_graph_ptr  a  ) 
#include <spot/twaalgos/degen.hh>
@}
Partial degeneralization of a TwA
Given an automaton whose acceptance contains a conjunction of Inf terms, perform a partial degeneralization to replace this conjunction by a single Inf term.
For instance if the input has acceptance (Fin(0)&Inf(1)&Inf(3))Fin(2) calling partial_degeneralize with todegen set to {1,3}
will build an equivalent automaton with acceptance (Fin(0)&Inf(2))Fin(1)
where Inf(2) tracks the acceptance of the original Inf(1)&Inf(3), and Fin(1) tracks the acceptance of the original Fin(2).
Cases where the sets listed in todegen also occur outside of the Infconjunction are also supported. Subformulas that are disjunctions of Fin(.) terms (e.g., Fin(1)Fin(2)) will be degeneralized as well.
If this functions is called with a value of todegen that does not match a conjunction of Inf(.), or a disjunction of Fin(.), an std::runtime_error exception is thrown.
The version of the function that has no todegen argument will perform all possible partial degeneralizations, and may return the input automaton unmodified if no partial degeneralization is possible.
The "originalstate" and "degenlevels" named properties are updated as for degeneralize() and degeneralize_tba().
bool spot::rabin_is_buchi_realizable  (  const const_twa_graph_ptr &  aut  ) 
#include <spot/twaalgos/remfin.hh>
Check if aut is Rablinlike and Büchirealizable.
This is inspired from rabin_to_buchi_maybe()'s algorithm. The main difference is that here, no automaton is built.
If the input is nondeterministic, this algorithm may fail to detect Büchirealizability (falsenegative).
twa_graph_ptr spot::rabin_to_buchi_if_realizable  (  const const_twa_graph_ptr &  aut  ) 
#include <spot/twaalgos/remfin.hh>
Convert a Rabinlike automaton into a Büchi automaton only when it can be done without changing the automaton structure.
If aut is a Rabinlike automaton that is not Büchirealizable, this returns a Büchi automaton equivalent to aut that use exactly the same transition structure (the order of edges is even preserved). In particular, determinism is preserved.
If aut is not a Rabinlike automaton or is not Büchirealizable, return nullptr
.
If the input is nondeterministic, this algorithm may fail to detect Büchirealizability (falsenegative).
twa_graph_ptr spot::rabin_to_buchi_maybe  (  const const_twa_graph_ptr &  aut  ) 
#include <spot/twaalgos/remfin.hh>
Convert a Rabinlike automaton into a Büchi automaton, preserving determinism when possible.
Return nullptr if the input is not a Rabin (or Rabinlike) automaton.
This essentially applies the algorithm from "Deterministic ωautomata visavis Deterministic Büchi Automata", S. Krishnan, A. Puri, and R. Brayton (ISAAC'94), but SCCwise.
Unless you know what you are doing, you are probably better off calling remove_fin() instead, as this will call more specialized algorithms (e.g., for weak automata) when appropriate, and will deal with more than just Rabinlike automata.
twa_graph_ptr spot::remove_fin  (  const const_twa_graph_ptr &  aut  ) 
#include <spot/twaalgos/remfin.hh>
Rewrite an automaton without Fin or f acceptance.
This algorithm dispatches between many strategies. It has dedicated algorithms for weak automata, automata with Rabinlike acceptance, automata with Streettlike acceptance, and some generic code that will work on any kind of acceptance condition.
In Spot "f" acceptance is not considered Finless, because it can be seen as a case of generalized coBüchi with 0 sets. Just like "t" corresponds generalized Büchi with 0 sets.)
twa_graph_ptr spot::separate_sets_here  (  const twa_graph_ptr &  aut  ) 
#include <spot/twaalgos/sepsets.hh>
Separate the Fin and Inf sets used by an automaton.
This makes sure that the numbers used a Fin and Inf are disjoints.
twa_graph_ptr spot::simplify_acceptance  (  const_twa_graph_ptr  aut  ) 
#include <spot/twaalgos/cleanacc.hh>
Simplify an acceptance condition.
Does everything cleanup_acceptance() does, but additionally: merge identical sets, detect whether two sets i and j are complementary to apply the following reductions:
Fin(i) & Inf(j) = Fin(i)
Fin(i) & Fin(j) = f
Fin(i) & Inf(i) = f
Fin(i)  Inf(j) = Inf(j)
Inf(i)  Inf(j) = t
Fin(i)  Inf(i) = t
And also merge terms like Inf(i)Inf(j)
or Fin(i)&Fin(j)
provided at least i or j is used uniquely in the formula. (for instance if i is unique, Inf(i)Inf(j)
is rewritten as Inf(i)
, and i
is added on all transitions where j
is present in the automaton.)simplify_acceptance_here() works in place, simplify_acceptance() returns a new automaton that has been simplified.
twa_graph_ptr spot::simplify_acceptance_here  (  twa_graph_ptr  aut  ) 
#include <spot/twaalgos/cleanacc.hh>
Simplify an acceptance condition.
Does everything cleanup_acceptance() does, but additionally: merge identical sets, detect whether two sets i and j are complementary to apply the following reductions:
Fin(i) & Inf(j) = Fin(i)
Fin(i) & Fin(j) = f
Fin(i) & Inf(i) = f
Fin(i)  Inf(j) = Inf(j)
Inf(i)  Inf(j) = t
Fin(i)  Inf(i) = t
And also merge terms like Inf(i)Inf(j)
or Fin(i)&Fin(j)
provided at least i or j is used uniquely in the formula. (for instance if i is unique, Inf(i)Inf(j)
is rewritten as Inf(i)
, and i
is added on all transitions where j
is present in the automaton.)simplify_acceptance_here() works in place, simplify_acceptance() returns a new automaton that has been simplified.
spot::SPOT_DEPRECATED  (  "use to_parity() and spot::acc_cond::is_rabin_like() instead"  )  const & 
#include <spot/twaalgos/toparity.hh>
Turn a Rabinlike or Streettlike automaton into a parity automaton based on the index appearence record (IAR)
Returns nullptr if the input automaton is neither Rabinlike nor Streettlike, and calls spot::iar() otherwise.
spot::SPOT_DEPRECATED  (  "use to_parity() instead"  )  const & 
#include <spot/twaalgos/toparity.hh>
Turn a Rabinlike or Streettlike automaton into a parity automaton based on the index appearence record (IAR)
This is an implementation of [36] . If the input automaton has n states and k pairs, the output automaton has at most k!*n states and 2k+1 colors. If the input automaton is deterministic, the output automaton is deterministic as well, which is the intended use case for this function. If the input automaton is nondeterministic, the result is still correct, but way larger than an equivalent Büchi automaton.
If the input automaton is Rabinlike (resp. Streettlike), the output automaton has max odd (resp. min even) acceptance condition.
Throws an std::runtime_error if the input is neither Rabinlike nor Streetlike.
It is better to use to_parity() instead, as it will use better strategies when possible, and has additional optimizations.
twa_graph_ptr spot::streett_to_generalized_buchi  (  const const_twa_graph_ptr &  in  ) 
#include <spot/twaalgos/totgba.hh>
Convert Streett acceptance into generalized Büchi acceptance.
twa_graph_ptr spot::streett_to_generalized_buchi_maybe  (  const const_twa_graph_ptr &  in  ) 
#include <spot/twaalgos/totgba.hh>
Convert Streett acceptance into generalized Büchi.
This version only works SPOT_STREET_CONF_MIN is set to a number of pairs less than the number of pairs used by in. The default is 3. It returns nullptr of that condition is not met, or if the input automaton does not have Streettlike acceptance.
twa_graph_ptr spot::to_generalized_buchi  (  const const_twa_graph_ptr &  aut  ) 
#include <spot/twaalgos/totgba.hh>
Take an automaton with any acceptance condition and return an equivalent Generalized Büchi automaton.
This dispatch between many algorithms. If the input has Streett (or Streettlike) acceptance, spot::streett_to_generalized_buchi() is called right away and produces a TGBA. Otherwise, it calls spot::remove_in() which returns a TBA.
twa_graph_ptr spot::to_generalized_rabin  (  const const_twa_graph_ptr &  aut, 
bool  share_inf = false 

) 
#include <spot/twaalgos/totgba.hh>
Take an automaton with any acceptance condition and return an equivalent Generalized Rabin automaton.
This works by putting the acceptance condition in disjunctive normal form, and then merging all the Fin(x1)&Fin(x2)&...&Fin(xn) that may occur in clauses into a single Fin(X).
The acceptanceset numbers used by Inf may appear in multiple clauses if share_inf is set.
twa_graph_ptr spot::to_generalized_streett  (  const const_twa_graph_ptr &  aut, 
bool  share_fin = false 

) 
#include <spot/twaalgos/totgba.hh>
Take an automaton with any acceptance condition and return an equivalent Generalized Streett automaton.
This works by putting the acceptance condition in cunjunctive normal form, and then merging all the Inf(x1)Inf(x2)...Inf(xn) that may occur in clauses into a single Inf(X).
The acceptanceset numbers used by Fin may appear in multiple clauses if share_fin is set.
twa_graph_ptr spot::to_parity  (  const const_twa_graph_ptr &  aut, 
const to_parity_options  options = to_parity_options() 

) 
#include <spot/twaalgos/toparity.hh>
Take an automaton with any acceptance condition and return an equivalent parity automaton.
If the input is already a parity automaton of any kind, it is returned unchanged. Otherwise a new parity automaton with max odd or max even condition is created.
This procedure combines many strategies in an attempt to produce the smallest possible parity automaton. Some of the strategies include CAR (color acceptance record), IAR (index appearance record), partial degenerazation, conversion from Rabin to Büchi when possible, etc.
The options argument can be used to selectively disable some of the optimizations.
twa_graph_ptr spot::to_parity_old  (  const const_twa_graph_ptr &  aut, 
bool  pretty_print = false 

) 
#include <spot/twaalgos/toparity.hh>
Take an automaton with any acceptance condition and return an equivalent parity automaton.
The parity condition of the returned automaton is max even.
This implements a straightforward adaptation of the LAR (latest appearance record) to automata with transitionbased marks. We call this adaptation the CAR (color apperance record), as it tracks colors (i.e., acceptance sets) instead of states.
It is better to use to_parity() instead, as it will use better strategies when possible, and has additional optimizations.
twa_graph_ptr spot::zielonka_tree_transform  (  const const_twa_graph_ptr &  aut  ) 
#include <spot/twaalgos/zlktree.hh>
Paritize an automaton using Zielonka tree.
This corresponds to the application of Section 3 of [8]
The resulting automaton has a parity acceptance that is either "min odd" or "min even", depending on the original acceptance. It may uses up to n+1 colors if the input automaton has n colors. Finally, it is colored, i.e., each output transition has exactly one color.