spot
2.7

Modules  
Algorithms for parity acceptance  
Functions  
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) 
Remove useless acceptance sets. More...  
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 spot::tgba into an equivalent sba with only one acceptance condition. More...  
twa_graph_ptr  spot::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...  
twa_graph_ptr  spot::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...  
bool  spot::rabin_is_buchi_realizable (const const_twa_graph_ptr &aut) 
Check if is Büchirealizable. This is inspired from rabin_to_buchi_maybe()'s algorithm. The main difference is that here, no automaton is built. More...  
twa_graph_ptr  spot::rabin_to_buchi_maybe (const const_twa_graph_ptr &aut) 
Convert a Rabin automaton to 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, bool pretty_print=false) 
Take an automaton with any acceptance condition and return an equivalent parity automaton. 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::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::cleanup_acceptance  (  const_twa_graph_ptr  aut  ) 
#include <spot/twaalgos/cleanacc.hh>
Remove useless acceptance sets.
This removes from the automaton the acceptance marks that are not used in the acceptance condition. This also removes from the acceptance conditions the terms that corresponds to empty or full sets.
twa_graph_ptr spot::cleanup_acceptance_here  (  twa_graph_ptr  aut, 
bool  strip = true 

) 
#include <spot/twaalgos/cleanacc.hh>
Remove useless acceptance sets.
This removes from the automaton the acceptance marks that are not used in the acceptance condition. This 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 maximal number of acceptance sets used.
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 spot::tgba into an equivalent sba with only one acceptance condition.
This algorithms will build a new explicit automaton that has at most (N+1) times the number of states of the original automaton.
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 degeneralize_tba() variant produce a degeneralized automaton with transitionbased acceptance.
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. Note that these functions may return the original automaton asis if it is already degeneralized; in this case the "originalstates" property is not defined. Similarly, the property "degenlevels" keeps track of the degeneralization levels. To retrieve it, call aut>get_named_prop<std::vector<unsigned>>("degenlevels")
. @{
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 the paper below.
@Article{boker.2011.fossacs, author = {Udi Boker and Orna Kupferman}, title = {CoBüching Them All}, booktitle = {Foundations of Software Science and Computational Structures  14th International Conference, FOSSACS 2011} year = {2011}, pages = {184198}, url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}} }
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::iar  (  const const_twa_graph_ptr &  aut  ) 
#include <spot/twaalgos/rabin2parity.hh>
Turn a Rabinlike or Streettlike automaton into a parity automaton based on the index appearence record (IAR)
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. Details on the algorithm can be found in: https://arxiv.org/pdf/1701.05738.pdf (published at TACAS 2017)
Throws an std::runtime_error if the input is neither Rabinlike nor Streetlike.
twa_graph_ptr spot::iar_maybe  (  const const_twa_graph_ptr &  aut  ) 
#include <spot/twaalgos/rabin2parity.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.
bool spot::rabin_is_buchi_realizable  (  const const_twa_graph_ptr &  aut  ) 
#include <spot/twaalgos/remfin.hh>
Check if is Büchirealizable. This is inspired from rabin_to_buchi_maybe()'s algorithm. The main difference is that here, no automaton is built.
twa_graph_ptr spot::rabin_to_buchi_maybe  (  const const_twa_graph_ptr &  aut  ) 
#include <spot/twaalgos/remfin.hh>
Convert a Rabin automaton to 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.
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 evereything cleanup_acceptance() does, but additionally: merge identical sets, detect whether to 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
twa_graph_ptr spot::simplify_acceptance_here  (  twa_graph_ptr  aut  ) 
#include <spot/twaalgos/cleanacc.hh>
Simplify an acceptance condition.
Does evereything cleanup_acceptance() does, but additionally: merge identical sets, detect whether to 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
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, 
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.