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 Rablin-like and Büchi-realizable. More...

twa_graph_ptr	spot::rabin_to_buchi_if_realizable (const const_twa_graph_ptr &aut)
	Convert a Rabin-like 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 Rabin-like 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 Rabin-like or Streett-like 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 Rabin-like or Streett-like 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 co-Bü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 Streett-like. 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...

Detailed Description

Enumeration Type Documentation

◆ acd_options

enum spot::acd_options

strong

#include <spot/twaalgos/zlktree.hh>

Options to alter the behavior of acd.

Enumerator
NONE	Build the ACD, without checking its shape.
CHECK_RABIN	Check if the ACD has Rabin shape.
CHECK_STREETT	Check if the ACD has Streett shape.
CHECK_PARITY	Check if the ACD has Parity shape.
ABORT_WRONG_SHAPE	Abort the construction of the ACD if it does not have the shape that is tested. When that happens, node_count() is set to 0.
ORDER_HEURISTIC	Order the children of a node by decreasing size of the number of states they would introduce if that child appears as the last child of an "ACD" round in the state-based version of the ACD output.

◆ zielonka_tree_options

enum spot::zielonka_tree_options

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.

Function Documentation

◆ acd_transform()

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 transition-based output (optimal in the sense of least number of duplicated states), while the acd_tansform_sbacc() variant produces state-based output from transition-based input and without any optimality claim. The order_heuristics argument, enabled by default activates the ORDER_HEURISTICS option of the ACD.

◆ acd_transform_sbacc()

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 transition-based output (optimal in the sense of least number of duplicated states), while the acd_tansform_sbacc() variant produces state-based output from transition-based input and without any optimality claim. The order_heuristics argument, enabled by default activates the ORDER_HEURISTICS option of the ACD.

◆ buchi_type_to_buchi()

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.

Parameters

aut	Automaton that we want to convert

◆ cleanup_acceptance()

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.

◆ cleanup_acceptance_here()

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.

◆ co_buchi_type_to_co_buchi()

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 co-Büchi automaton preserving structure when possible.

Return nullptr if no such automaton is found.

Parameters

aut	Automaton that we want to convert

◆ degeneralize()

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 state-based (co)Büchi automaton that has at most (N+1) times the number of states of the original automaton. degeneralize_tba() builds a transition-based (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 self-loop. 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 "original-states" named property of the produced automaton. Call aut->get_named_prop<std::vector<unsigned>>("original-states") to retrieve it. However be aware that if the input automaton already defines the "original-states" named property, it will be composed with the new one, so the "original-states" of the degeneralized automaton will refer to the same automaton as the "original-states" of the input automaton.

Note that these functions may return the original automaton as-is if it is already degeneralized; in this case the "original-states" property is not defined (or not changed).

Similarly, the property "degen-levels" keeps track of the degeneralization levels. To retrieve it, call aut->get_named_prop<std::vector<unsigned>>("degen-levels").

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.

@{

◆ dnf_to_streett()

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 Streett-like.

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 "original-states" named property of the produced automaton. Call aut->get_named_prop<std::vector<unsigned>>("original-states") to retrieve it. Additionally, the correspondence between each created state and the associated DNF clause is recorded in the "original-clauses" property (also a vector of unsigned).

◆ has_separate_sets()

bool spot::has_separate_sets ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/sepsets.hh>

Whether the Inf and Fin numbers are disjoints.

◆ parity_type_to_parity()

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.

Parameters

aut	Automaton that we want to convert

◆ partial_degeneralize() [1/2]

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 Inf-conjunction 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 "original-state" and "degen-levels" named properties are updated as for degeneralize() and degeneralize_tba().

◆ partial_degeneralize() [2/2]

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 Inf-conjunction 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 "original-state" and "degen-levels" named properties are updated as for degeneralize() and degeneralize_tba().

◆ rabin_is_buchi_realizable()

bool spot::rabin_is_buchi_realizable ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/remfin.hh>

Check if aut is Rablin-like and Büchi-realizable.

This is inspired from rabin_to_buchi_maybe()'s algorithm. The main difference is that here, no automaton is built.

If the input is non-deterministic, this algorithm may fail to detect Büchi-realizability (false-negative).

◆ rabin_to_buchi_if_realizable()

twa_graph_ptr spot::rabin_to_buchi_if_realizable ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/remfin.hh>

Convert a Rabin-like automaton into a Büchi automaton only when it can be done without changing the automaton structure.

If aut is a Rabin-like automaton that is not Büchi-realizable, 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 Rabin-like automaton or is not Büchi-realizable, return nullptr.

If the input is non-deterministic, this algorithm may fail to detect Büchi-realizability (false-negative).

◆ rabin_to_buchi_maybe()

twa_graph_ptr spot::rabin_to_buchi_maybe ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/remfin.hh>

Convert a Rabin-like automaton into a Büchi automaton, preserving determinism when possible.

Return nullptr if the input is not a Rabin (or Rabin-like) automaton.

This essentially applies the algorithm from "Deterministic ω-automata vis-a-vis Deterministic Büchi Automata", S. Krishnan, A. Puri, and R. Brayton (ISAAC'94), but SCC-wise.

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 Rabin-like automata.

◆ remove_fin()

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 Rabin-like acceptance, automata with Streett-like acceptance, and some generic code that will work on any kind of acceptance condition.

In Spot "f" acceptance is not considered Fin-less, because it can be seen as a case of generalized co-Büchi with 0 sets. Just like "t" corresponds generalized Büchi with 0 sets.)

◆ separate_sets_here()

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.

◆ simplify_acceptance()

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.

◆ simplify_acceptance_here()

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_DEPRECATED() [1/2]

spot::SPOT_DEPRECATED ( "use to_parity() and spot::acc_cond::is_rabin_like() instead" ) const &

#include <spot/twaalgos/toparity.hh>

Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence record (IAR)

Returns nullptr if the input automaton is neither Rabin-like nor Streett-like, and calls spot::iar() otherwise.

◆ SPOT_DEPRECATED() [2/2]

spot::SPOT_DEPRECATED ( "use to_parity() instead" ) const &

#include <spot/twaalgos/toparity.hh>

Turn a Rabin-like or Streett-like 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 non-deterministic, the result is still correct, but way larger than an equivalent Büchi automaton.

If the input automaton is Rabin-like (resp. Streett-like), the output automaton has max odd (resp. min even) acceptance condition.

Throws an std::runtime_error if the input is neither Rabin-like nor Street-like.

It is better to use to_parity() instead, as it will use better strategies when possible, and has additional optimizations.

◆ streett_to_generalized_buchi()

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.

◆ streett_to_generalized_buchi_maybe()

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 Streett-like acceptance.

◆ to_generalized_buchi()

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 Streett-like) acceptance, spot::streett_to_generalized_buchi() is called right away and produces a TGBA. Otherwise, it calls spot::remove_in() which returns a TBA.

◆ to_generalized_rabin()

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 acceptance-set numbers used by Inf may appear in multiple clauses if share_inf is set.

◆ to_generalized_streett()

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 acceptance-set numbers used by Fin may appear in multiple clauses if share_fin is set.

◆ to_parity()

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.

◆ to_parity_old()

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 transition-based 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.

◆ zielonka_tree_transform()

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.

Modules

Classes

Enumerations

Functions

Detailed Description

Enumeration Type Documentation

◆ acd_options

◆ zielonka_tree_options

Function Documentation

◆ acd_transform()

◆ acd_transform_sbacc()

◆ buchi_type_to_buchi()

◆ cleanup_acceptance()

◆ cleanup_acceptance_here()

◆ co_buchi_type_to_co_buchi()

◆ degeneralize()

◆ dnf_to_streett()

◆ has_separate_sets()

◆ parity_type_to_parity()

◆ partial_degeneralize() [1/2]

◆ partial_degeneralize() [2/2]

◆ rabin_is_buchi_realizable()

◆ rabin_to_buchi_if_realizable()

◆ rabin_to_buchi_maybe()

◆ remove_fin()

◆ separate_sets_here()

◆ simplify_acceptance()

◆ simplify_acceptance_here()

◆ SPOT_DEPRECATED() [1/2]

◆ SPOT_DEPRECATED() [2/2]

◆ streett_to_generalized_buchi()

◆ streett_to_generalized_buchi_maybe()

◆ to_generalized_buchi()

◆ to_generalized_rabin()

◆ to_generalized_streett()

◆ to_parity()

◆ to_parity_old()

◆ zielonka_tree_transform()