Modules
	Language containment checks

	TωA on-the-fly algorithms

	Input/Output of TωA

	Stutter-invariance checks and related functions

	Conversion between acceptance conditions

	Translating LTL formulas into TωA

	Algorithm patterns

	TωA simplifications

	Miscellaneous algorithms on TωA

	Emptiness-checks

	Functions related to game solving

	Functions related to Mealy machines

	Reactive Synthesis

Functions
bool	spot::delay_branching_here (const twa_graph_ptr &aut)
	Merge states to delay. More...

twa_graph_ptr	spot::tgba_determinize (const const_twa_graph_ptr &aut, bool pretty_print=false, bool use_scc=true, bool use_simulation=true, bool use_stutter=true, const output_aborter *aborter=nullptr, int trans_pruning=-1, bool want_classes=false)
	Determinize a TGBA. More...

twa_graph_ptr	spot::product (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, const output_aborter *aborter=nullptr)
	Intersect two automata using a synchronous product. More...

twa_graph_ptr	spot::product (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state, const output_aborter *aborter=nullptr)
	Intersect two automata using a synchronous product. More...

twa_graph_ptr	spot::product_or (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
	Sum two automata using a synchronous product. More...

twa_graph_ptr	spot::product_or (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state)
	Sum two automata using a synchronous product. More...

twa_graph_ptr	spot::product_xor (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
	XOR two deterministic automata using a synchronous product. More...

twa_graph_ptr	spot::product_xnor (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
	XNOR two automata using a synchronous product. More...

twa_graph_ptr	spot::product_susp (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right_susp)
	Build the product of an automaton with a suspendable automaton. More...

twa_graph_ptr	spot::product_or_susp (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right_susp)
	Build the "or" product of an automaton with a suspendable automaton. More...

twa_graph_ptr	spot::sbacc (twa_graph_ptr aut)
	Transform an automaton to use state-based acceptance. More...

twa_graph_ptr	spot::sum (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
	Sum two twa into a new twa, performing the union of the two input automata. More...

twa_graph_ptr	spot::sum (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state)
	Sum two twa into a new twa, performing the union of the two input automata. More...

twa_graph_ptr	spot::sum_and (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
	Sum two twa into a new twa, using a universal initial transition, performing the intersection of the two languages of the input automata. More...

twa_graph_ptr	spot::sum_and (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state)
	Sum two twa into a new twa, using a universal initial transition, performing the intersection of the two languages of the input automata. More...

std::vector< acc_cond::mark_t >	spot::propagate_marks_vector (const const_twa_graph_ptr &aut, const scc_info *si=nullptr)
	Propagate marks around the automaton. More...

void	spot::propagate_marks_here (twa_graph_ptr &aut, const scc_info *si=nullptr)
	Propagate marks around the automaton. More...

Detailed Description

Function Documentation

◆ delay_branching_here()

bool spot::delay_branching_here ( const twa_graph_ptr & aut )

#include <spot/twaalgos/dbranch.hh>

Merge states to delay.

In an automaton with transition-based acceptance, if a state (x) has two outgoing transitions (x,l,m,y) and (x,l,m,z) going to states (x) and (y) that have no other incoming edges, then (y) and (z) can be merged (keeping the union of their outgoing destinations).

If the input automaton uses state-based acceptance, running this function might make the acceptance transition-based, but only if two states with different acceptance are merged at some point.

Returns: true iff the automaton was modified.

◆ product() [1/2]

twa_graph_ptr spot::product	(	const const_twa_graph_ptr &	left,
		const const_twa_graph_ptr &	right,
		const output_aborter *	aborter = `nullptr`
	)

#include <spot/twaalgos/product.hh>

Intersect two automata using a synchronous product.

The resulting automaton will accept the intersection of both languages and have an acceptance condition that is the conjunction of the acceptance conditions of the two input automata.

As an optionmization, in case one of the left or right automaton is weak, the acceptance condition of the result is made simpler: it usually is the acceptance condition of the other argument, therefore avoiding the need to introduce new accepting sets. Similarly, the product of two co-Büchi automata will be a co-Büchi automaton.

The algorithm also defines a named property called "product-states" with type spot::product_states. This stores the pair of original state numbers associated to each state of the product.

If an aborter is given, the function will return nullptr whenever the resulting product would be too large.

◆ product() [2/2]

twa_graph_ptr spot::product	(	const const_twa_graph_ptr &	left,
		const const_twa_graph_ptr &	right,
		unsigned	left_state,
		unsigned	right_state,
		const output_aborter *	aborter = `nullptr`
	)

#include <spot/twaalgos/product.hh>

Intersect two automata using a synchronous product.

This variant allows changing the initial state of both automata in case you want to start the product at a different place.

The resulting automaton will accept the intersection of the languages recognized by each input automaton (with its initial state changed) and have an acceptance condition that is the conjunction of the acceptance conditions of the two input automata.

As an optionmization, in case one of the left or right automaton is weak, the acceptance condition of the result is made simpler: it usually is the acceptance condition of the other argument, therefore avoiding the need to introduce new accepting sets. Similarly, the product of two co-Büchi automata will be a co-Büchi automaton.

The algorithm also defines a named property called "product-states" with type spot::product_states. This stores the pair of original state numbers associated to each state of the product.

If an aborter is given, the function will return nullptr whenever the resulting product would be too large.

◆ product_or() [1/2]

twa_graph_ptr spot::product_or	(	const const_twa_graph_ptr &	left,
		const const_twa_graph_ptr &	right
	)

#include <spot/twaalgos/product.hh>

Sum two automata using a synchronous product.

The resulting automaton will accept the union of both languages and have an acceptance condition that is the disjunction of the acceptance conditions of the two input automata.

As an optionmization, in case one of the left or right automaton is weak, the acceptance condition of the result is made simpler: it usually is the acceptance condition of the other argument, therefore avoiding the need to introduce new accepting sets. Similarly, the product_pr of two Büchi automata will be a Büchi automaton.

The algorithm also defines a named property called "product-states" with type spot::product_states. This stores the pair of original state numbers associated to each state of the product.

◆ product_or() [2/2]

twa_graph_ptr spot::product_or	(	const const_twa_graph_ptr &	left,
		const const_twa_graph_ptr &	right,
		unsigned	left_state,
		unsigned	right_state
	)

#include <spot/twaalgos/product.hh>

Sum two automata using a synchronous product.

This variant allows changing the initial state of both automata in case you want to start the product at a different place.

The resulting automaton will accept the sum of the languages recognized by each input automaton (with its initial state changed) and have an acceptance condition that is the disjunction of the acceptance conditions of the two input automata.

As an optionmization, in case one of the left or right automaton is weak, the acceptance condition of the result is made simpler: it usually is the acceptance condition of the other argument, therefore avoiding the need to introduce new accepting sets. Similarly, the product_pr of two Büchi automata will be a Büchi automaton.

The algorithm also defines a named property called "product-states" with type spot::product_states. This stores the pair of original state numbers associated to each state of the product.

◆ product_or_susp()

twa_graph_ptr spot::product_or_susp	(	const const_twa_graph_ptr &	left,
		const const_twa_graph_ptr &	right_susp
	)

#include <spot/twaalgos/product.hh>

Build the "or" product of an automaton with a suspendable automaton.

The language of this product is the union of the languages of both input automata.

This function assumes that right_susp is a suspendable automaton, i.e., its language L satisfies L = Σ*.L. Therefore, after left has been completed (this will be done by product_or_susp) the product between the two automata need only be done with the SCCs of left that contains some rejecting cycles.

The current implementation is currently suboptimal as instead of looking for SCC with rejecting cycles, it simply loop for non-trivial SCC, (or in the case of weak automata, with non-trivial and rejecting SCCs).

◆ product_susp()

twa_graph_ptr spot::product_susp	(	const const_twa_graph_ptr &	left,
		const const_twa_graph_ptr &	right_susp
	)

#include <spot/twaalgos/product.hh>

Build the product of an automaton with a suspendable automaton.

The language of this product is the intersection of the languages of both input automata.

This function assumes that right_susp is a suspendable automaton, i.e., its language L satisfies L = Σ*.L. Therefore the product between the two automata need only be done with the accepting SCCs of left.

If left is a weak automaton, the acceptance condition of the output will be that of right_susp. Otherwise the acceptance condition is the conjunction of both acceptances.

◆ product_xnor()

twa_graph_ptr spot::product_xnor	(	const const_twa_graph_ptr &	left,
		const const_twa_graph_ptr &	right
	)

#include <spot/twaalgos/product.hh>

XNOR two automata using a synchronous product.

The two operands must be deterministic.

The resulting automaton will accept words that are either in both input languages, or not in both languages. (The XNOR gate it the logical complement of XOR. XNOR is also known as logical equivalence.) The output will have an acceptance condition that is the XNOR of the acceptance conditions of the two input automata. In case both the operands are weak, the acceptance condition of the result is made simpler.

The algorithm also defines a named property called "product-states" with type spot::product_states. This stores the pair of original state numbers associated to each state of the product.

◆ product_xor()

twa_graph_ptr spot::product_xor	(	const const_twa_graph_ptr &	left,
		const const_twa_graph_ptr &	right
	)

#include <spot/twaalgos/product.hh>

XOR two deterministic automata using a synchronous product.

The two operands must be deterministic.

The resulting automaton will accept the symmetric difference of both languages and have an acceptance condition that is the xor of the acceptance conditions of the two input automata. In case both operands are weak, the acceptance condition of the result is made simpler.

The algorithm also defines a named property called "product-states" with type spot::product_states. This stores the pair of original state numbers associated to each state of the product.

◆ propagate_marks_here()

void spot::propagate_marks_here	(	twa_graph_ptr &	aut,
		const scc_info *	si = `nullptr`
	)

#include <spot/twaalgos/degen.hh>

Propagate marks around the automaton.

For each state of the automaton, marks that are common to all input transitions will be pushed on the outgoing transitions, and marks that are common to all outgoing transitions will be pulled to the input transitions. This considers only transitions that are not self-loops and that belong to some SCC. If an scc_info has already been built, pass it as si to avoid building it again.

Two variants of the algorithm are provided. One modifies the automaton in place; the second returns a vector of marks indexed by transition numbers.

◆ propagate_marks_vector()

std::vector<acc_cond::mark_t> spot::propagate_marks_vector	(	const const_twa_graph_ptr &	aut,
		const scc_info *	si = `nullptr`
	)

#include <spot/twaalgos/degen.hh>

Propagate marks around the automaton.

For each state of the automaton, marks that are common to all input transitions will be pushed on the outgoing transitions, and marks that are common to all outgoing transitions will be pulled to the input transitions. This considers only transitions that are not self-loops and that belong to some SCC. If an scc_info has already been built, pass it as si to avoid building it again.

Two variants of the algorithm are provided. One modifies the automaton in place; the second returns a vector of marks indexed by transition numbers.

◆ sbacc()

twa_graph_ptr spot::sbacc ( twa_graph_ptr aut )

#include <spot/twaalgos/sbacc.hh>

Transform an automaton to use state-based acceptance.

This transformation is independent on the acceptance condition used. The implementation supports alternating automata.

It works by creating an automaton whose states correspond to pairs (s,colors) for each edge entering state s with colors. In other words, we are pushing colors from the edges to their outgoing states. The implementation is also able to pull colors on incoming states in cases where that helps.

When called on automata that are already known to have state-based acceptance, this function returns the input unmodified, not a copy.

Trues states (any state with an accepting self-loop labeled by true) are merged in the process.

The output will have a named property called "original-states" that is a vector indexed by the produced states, and giving the corresponding state in the input automaton. If the input automaton also had an "original-states" property, the two vectors will be composed, so the original-states[s] in the output will contains the value of `original-states[y] if state s was created from state y.

If the input has a property named "original-classes", then the above "original-state" property is replaced by an "original-classes" property such that original-classes[s] is the class of the original state of s.

◆ sum() [1/2]

twa_graph_ptr spot::sum	(	const const_twa_graph_ptr &	left,
		const const_twa_graph_ptr &	right
	)

#include <spot/twaalgos/sum.hh>

Sum two twa into a new twa, performing the union of the two input automata.

Parameters

left	Left term of the sum.
right	Right term of the sum.

Returns: A spot::twa_graph containing the sum of left and right

◆ sum() [2/2]

twa_graph_ptr spot::sum	(	const const_twa_graph_ptr &	left,
		const const_twa_graph_ptr &	right,
		unsigned	left_state,
		unsigned	right_state
	)

#include <spot/twaalgos/sum.hh>

Sum two twa into a new twa, performing the union of the two input automata.

Parameters

left	Left term of the sum.
right	Right term of the sum.
left_state	Initial state of the left term of the sum.
right_state	Initial state of the right term of the sum.

Returns: A spot::twa_graph containing the sum of left and right

◆ sum_and() [1/2]

twa_graph_ptr spot::sum_and	(	const const_twa_graph_ptr &	left,
		const const_twa_graph_ptr &	right
	)

#include <spot/twaalgos/sum.hh>

Sum two twa into a new twa, using a universal initial transition, performing the intersection of the two languages of the input automata.

Parameters

left	Left term of the sum.
right	Right term of the sum.

Returns: A spot::twa_graph containing the sum of left and right

◆ sum_and() [2/2]

twa_graph_ptr spot::sum_and	(	const const_twa_graph_ptr &	left,
		const const_twa_graph_ptr &	right,
		unsigned	left_state,
		unsigned	right_state
	)

#include <spot/twaalgos/sum.hh>

Sum two twa into a new twa, using a universal initial transition, performing the intersection of the two languages of the input automata.

Parameters

left	Left term of the sum.
right	Right term of the sum.
left_state	Initial state of the left term of the sum.
right_state	Initial state of the right term of the sum.

Returns: A spot::twa_graph containing the sum of left and right

◆ tgba_determinize()

twa_graph_ptr spot::tgba_determinize	(	const const_twa_graph_ptr &	aut,
		bool	pretty_print = `false`,
		bool	use_scc = `true`,
		bool	use_simulation = `true`,
		bool	use_stutter = `true`,
		const output_aborter *	aborter = `nullptr`,
		int	trans_pruning = `-1`,
		bool	want_classes = `false`
	)

#include <spot/twaalgos/determinize.hh>

Determinize a TGBA.

The main algorithm works only with automata using Büchi acceptance (preferably transition-based). If generalized Büchi is input, it will be automatically degeneralized first.

The output will be a deterministic automaton using parity acceptance.

This procedure is based on an algorithm by Roman Redziejowski [44] . Redziejowski's algorithm is similar to Piterman's improvement of Safra's algorithm, except it is presented on transition-based acceptance and use simpler notations. We implement three additional optimizations (they can be individually disabled) based on

knowledge about SCCs of the input automaton
knowledge about simulation relations in the input automaton
knowledge about stutter-invariance of the input automaton

The last optimization is an idea implemented in ltl2dstar [31] . In fact, ltl2dstar even has a finer version (letter-based stuttering) that is not implemented here.

Parameters

aut	the automaton to determinize
pretty_print	whether to decorate states with names showing the paths they track (this only makes sense if the input has Büchi acceptance already, otherwise the input automaton will be degeneralized and the names will refer to the states in the degeneralized automaton).
use_scc	whether to simplify the construction based on the SCCs in the input automaton.
use_simulation	whether to simplify the construction based on simulation relations between states in the original automaton.
use_stutter	whether to simplify the construction when the input automaton is known to be stutter-invariant. (The stutter-invariant flag of the input automaton is used, so it might be worth to call spot::check_stutter_invariance() first if possible.)
aborter	abort the construction if the constructed automaton would be too large. Return nullptr in this case.
trans_pruning	when use_simulation is true, trans_pruning is passed to the simulation-based reduction to limit the effect of transition pruning.
want_classes	If set, define a "original-class" named property as a vector of unsigned. If two states are associated to the same integer, it means they use the same subset of original states as support, so they recognize the same language. If the input define an "original-state" property (or else an "original-class" property), it is taken into account while computing the above support.

Modules

Functions

Detailed Description

Function Documentation

◆ delay_branching_here()

◆ product() [1/2]

◆ product() [2/2]

◆ product_or() [1/2]

◆ product_or() [2/2]

◆ product_or_susp()

◆ product_susp()

◆ product_xnor()

◆ product_xor()

◆ propagate_marks_here()

◆ propagate_marks_vector()

◆ sbacc()

◆ sum() [1/2]

◆ sum() [2/2]

◆ sum_and() [1/2]

◆ sum_and() [2/2]

◆ tgba_determinize()