Classes
class	spot::aig
	A class representing AIG circuits. More...

struct	spot::synthesis_info
	Benchmarking data and options for synthesis. More...

struct	spot::mealy_like
	A struct that represents different types of mealy like objects. More...

Functions
twa_graph_ptr	spot::split_2step (const const_twa_graph_ptr &aut, const bdd &output_bdd, bool complete_env=true)
	make each transition a 2-step transition, transforming the graph into an alternating arena More...

twa_graph_ptr	spot::split_2step (const const_twa_graph_ptr &aut, bool complete_env=true)
	Like split_2step but relying on the named property 'synthesis-outputs'. More...

twa_graph_ptr	spot::unsplit_2step (const const_twa_graph_ptr &aut)
	the inverse of split_2step More...

std::ostream &	spot::operator<< (std::ostream &os, synthesis_info::algo s)
	Stream algo. More...

std::ostream &	spot::operator<< (std::ostream &os, const synthesis_info &gi)
	Stream benchmarks and options. More...

mealy_like	spot::try_create_direct_strategy (formula f, const std::vector< std::string > &output_aps, synthesis_info &gi, bool want_strategy=false)
	Creates a strategy for the formula given by calling all intermediate steps. More...

bool	spot::solve_game (twa_graph_ptr arena, synthesis_info &gi)
	Solve a game, and update synthesis_info. More...

game_relabeling_map	spot::partitioned_game_relabel_here (twa_graph_ptr &arena, bool relabel_env, bool relabel_play, bool split_env=false, bool split_play=false, unsigned max_letter=-1u, unsigned max_letter_mult=-1u)
	Tries to relabel a SPLIT game arena using fresh propositions. Can be applied to env or player depending on relabel_env and relabel_play. The arguments split_env and split_play determine whether or not env and player edges are to be split into several transitions labelled by letters not conditions. More...

void	spot::relabel_game_here (twa_graph_ptr &arena, game_relabeling_map &rel_maps)
	Undoes a relabeling done by partitioned_game_relabel_here. A dedicated function is necessary in order to remove the variables tagging env and player conditions. More...

aig_ptr	spot::mealy_machine_to_aig (const const_twa_graph_ptr &m, const char *mode)
	Convert a mealy (like) machine into an aig relying on the transformation described by mode. More...

aig_ptr	spot::mealy_machine_to_aig (const twa_graph_ptr &m, const char mode, const std::vector< std::string > &ins, const std::vector< std::string > &outs, const realizability_simplifier rs=nullptr)
	Convert a mealy (like) machine into an aig relying on the transformation described by mode. More...

aig_ptr	spot::mealy_machine_to_aig (const mealy_like &m, const char *mode)
	Convert a mealy (like) machine into an aig relying on the transformation described by mode. More...

aig_ptr	spot::mealy_machine_to_aig (mealy_like &m, const char mode, const std::vector< std::string > &ins, const std::vector< std::string > &outs, const realizability_simplifier rs=nullptr)
	Convert a mealy (like) machine into an aig relying on the transformation described by mode. More...

aig_ptr	spot::mealy_machines_to_aig (const std::vector< const_twa_graph_ptr > &m_vec, const char *mode)
	Convert multiple mealy machines into an aig relying on the transformation described by mode. More...

aig_ptr	spot::mealy_machines_to_aig (const std::vector< mealy_like > &m_vec, const char *mode)
	Convert multiple mealy machines into an aig relying on the transformation described by mode. More...

aig_ptr	spot::mealy_machines_to_aig (const std::vector< const_twa_graph_ptr > &m_vec, const char mode, const std::vector< std::string > &ins, const std::vector< std::vector< std::string > > &outs, const realizability_simplifier rs=nullptr)
	Convert multiple mealy machines into an aig relying on the transformation described by mode. More...

aig_ptr	spot::mealy_machines_to_aig (const std::vector< mealy_like > &m_vec, const char mode, const std::vector< std::string > &ins, const std::vector< std::vector< std::string > > &outs, const realizability_simplifier rs=nullptr)
	Convert multiple mealy machines into an aig relying on the transformation described by mode. More...

twa_graph_ptr	spot::ltl_to_game (const formula &f, const std::vector< std::string > &all_outs, synthesis_info &gi)
	Creates a game from a specification and a set of output propositions. More...

twa_graph_ptr	spot::ltl_to_game (const formula &f, const std::vector< std::string > &all_outs)
	Creates a game from a specification and a set of output propositions. More...

twa_graph_ptr	spot::ltl_to_game (const std::string &f, const std::vector< std::string > &all_outs, synthesis_info &gi)
	Creates a game from a specification and a set of output propositions. More...

twa_graph_ptr	spot::ltl_to_game (const std::string &f, const std::vector< std::string > &all_outs)
	Creates a game from a specification and a set of output propositions. More...

twa_graph_ptr	spot::solved_game_to_mealy (twa_graph_ptr arena, synthesis_info &gi)
	creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...

twa_graph_ptr	spot::solved_game_to_mealy (twa_graph_ptr arena)
	creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...

twa_graph_ptr	spot::solved_game_to_separated_mealy (twa_graph_ptr arena, synthesis_info &gi)
	creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...

twa_graph_ptr	spot::solved_game_to_separated_mealy (twa_graph_ptr arena)
	creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...

twa_graph_ptr	spot::solved_game_to_split_mealy (twa_graph_ptr arena, synthesis_info &gi)
	creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...

twa_graph_ptr	spot::solved_game_to_split_mealy (twa_graph_ptr arena)
	creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...

std::pair< std::vector< formula >, std::vector< std::set< formula > > >	spot::split_independent_formulas (formula f, const std::vector< std::string > &outs)
	Seeks to decompose a formula into independently synthetizable sub-parts. The conjunction of all sub-parts then satisfies the specification. More...

std::pair< std::vector< formula >, std::vector< std::set< formula > > >	spot::split_independent_formulas (const std::string &f, const std::vector< std::string > &outs)
	Seeks to decompose a formula into independently synthetizable sub-parts. The conjunction of all sub-parts then satisfies the specification. More...

Detailed Description

Function Documentation

◆ ltl_to_game() [1/4]

twa_graph_ptr spot::ltl_to_game	(	const formula &	f,
		const std::vector< std::string > &	all_outs
	)

#include <spot/twaalgos/synthesis.hh>

Creates a game from a specification and a set of output propositions.

Parameters

f	The specification given as an LTL/PSL formula, or as a string.
all_outs	The names of all output propositions
gi	synthesis_info structure

Note: All propositions in the formula that do not appear in all_outs are treated as input variables.

◆ ltl_to_game() [2/4]

twa_graph_ptr spot::ltl_to_game	(	const formula &	f,
		const std::vector< std::string > &	all_outs,
		synthesis_info &	gi
	)

#include <spot/twaalgos/synthesis.hh>

Creates a game from a specification and a set of output propositions.

Parameters

f	The specification given as an LTL/PSL formula, or as a string.
all_outs	The names of all output propositions
gi	synthesis_info structure

Note: All propositions in the formula that do not appear in all_outs are treated as input variables.

◆ ltl_to_game() [3/4]

twa_graph_ptr spot::ltl_to_game	(	const std::string &	f,
		const std::vector< std::string > &	all_outs
	)

#include <spot/twaalgos/synthesis.hh>

Creates a game from a specification and a set of output propositions.

Parameters

f	The specification given as an LTL/PSL formula, or as a string.
all_outs	The names of all output propositions
gi	synthesis_info structure

Note: All propositions in the formula that do not appear in all_outs are treated as input variables.

◆ ltl_to_game() [4/4]

twa_graph_ptr spot::ltl_to_game	(	const std::string &	f,
		const std::vector< std::string > &	all_outs,
		synthesis_info &	gi
	)

#include <spot/twaalgos/synthesis.hh>

Creates a game from a specification and a set of output propositions.

Parameters

f	The specification given as an LTL/PSL formula, or as a string.
all_outs	The names of all output propositions
gi	synthesis_info structure

Note: All propositions in the formula that do not appear in all_outs are treated as input variables.

◆ mealy_machine_to_aig() [1/4]

aig_ptr spot::mealy_machine_to_aig	(	const const_twa_graph_ptr &	m,
		const char *	mode
	)

#include <spot/twaalgos/aiger.hh>

Convert a mealy (like) machine into an aig relying on the transformation described by mode.

Parameters

mode This param has to be of the form ite|isop|both [+dc][+ud][+sub0|+sub1|+sub2] Where ite means encoded via if-then-else normal form, isop means encoded via irredundant sum-of-products, both means trying both encodings to keep the smaller one. +dc is optional and tries to take advantage of "do not care" outputs to minimize the encoding. +dual is optional and indicates that the algorithm should also try to encode the negation of each condition in case its encoding is smaller. +subN indicates that the conditions can be separated into blocks with sub0 being no separation, sub1 separation into input/latches/gates (isop only) and sub2 tries to seek common subformulas.

If ins and outs are specified, the named-property synthesis-output is ignored and all properties in ins and outs are guaranteed to appear in the aiger circuit.

If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.

◆ mealy_machine_to_aig() [2/4]

aig_ptr spot::mealy_machine_to_aig	(	const mealy_like &	m,
		const char *	mode
	)

#include <spot/twaalgos/aiger.hh>

Convert a mealy (like) machine into an aig relying on the transformation described by mode.

Parameters

mode This param has to be of the form ite|isop|both [+dc][+ud][+sub0|+sub1|+sub2] Where ite means encoded via if-then-else normal form, isop means encoded via irredundant sum-of-products, both means trying both encodings to keep the smaller one. +dc is optional and tries to take advantage of "do not care" outputs to minimize the encoding. +dual is optional and indicates that the algorithm should also try to encode the negation of each condition in case its encoding is smaller. +subN indicates that the conditions can be separated into blocks with sub0 being no separation, sub1 separation into input/latches/gates (isop only) and sub2 tries to seek common subformulas.

If ins and outs are specified, the named-property synthesis-output is ignored and all properties in ins and outs are guaranteed to appear in the aiger circuit.

If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.

◆ mealy_machine_to_aig() [3/4]

aig_ptr spot::mealy_machine_to_aig	(	const twa_graph_ptr &	m,
		const char *	mode,
		const std::vector< std::string > &	ins,
		const std::vector< std::string > &	outs,
		const realizability_simplifier *	rs = `nullptr`
	)

#include <spot/twaalgos/aiger.hh>

Convert a mealy (like) machine into an aig relying on the transformation described by mode.

Parameters

mode This param has to be of the form ite|isop|both [+dc][+ud][+sub0|+sub1|+sub2] Where ite means encoded via if-then-else normal form, isop means encoded via irredundant sum-of-products, both means trying both encodings to keep the smaller one. +dc is optional and tries to take advantage of "do not care" outputs to minimize the encoding. +dual is optional and indicates that the algorithm should also try to encode the negation of each condition in case its encoding is smaller. +subN indicates that the conditions can be separated into blocks with sub0 being no separation, sub1 separation into input/latches/gates (isop only) and sub2 tries to seek common subformulas.

If ins and outs are specified, the named-property synthesis-output is ignored and all properties in ins and outs are guaranteed to appear in the aiger circuit.

If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.

◆ mealy_machine_to_aig() [4/4]

aig_ptr spot::mealy_machine_to_aig	(	mealy_like &	m,
		const char *	mode,
		const std::vector< std::string > &	ins,
		const std::vector< std::string > &	outs,
		const realizability_simplifier *	rs = `nullptr`
	)

#include <spot/twaalgos/aiger.hh>

Convert a mealy (like) machine into an aig relying on the transformation described by mode.

Parameters

mode This param has to be of the form ite|isop|both [+dc][+ud][+sub0|+sub1|+sub2] Where ite means encoded via if-then-else normal form, isop means encoded via irredundant sum-of-products, both means trying both encodings to keep the smaller one. +dc is optional and tries to take advantage of "do not care" outputs to minimize the encoding. +dual is optional and indicates that the algorithm should also try to encode the negation of each condition in case its encoding is smaller. +subN indicates that the conditions can be separated into blocks with sub0 being no separation, sub1 separation into input/latches/gates (isop only) and sub2 tries to seek common subformulas.

If ins and outs are specified, the named-property synthesis-output is ignored and all properties in ins and outs are guaranteed to appear in the aiger circuit.

If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.

◆ mealy_machines_to_aig() [1/4]

aig_ptr spot::mealy_machines_to_aig	(	const std::vector< const_twa_graph_ptr > &	m_vec,
		const char *	mode
	)

#include <spot/twaalgos/aiger.hh>

Convert multiple mealy machines into an aig relying on the transformation described by mode.

Note: The states of each machine are represented by a block of latches not affected by the others. For this to work in a general setting, the outputs must be disjoint.

Unless ins and outs are specified, only the propositions actually used in the strategy appear in the aiger circuit. So it can happen that, for instance, propositions marked as output during the call to ltl_to_game() are absent. If ins and outs are used, all properties they list are guaranteed to appear in the aiger circuit.

If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.

◆ mealy_machines_to_aig() [2/4]

aig_ptr spot::mealy_machines_to_aig	(	const std::vector< const_twa_graph_ptr > &	m_vec,
		const char *	mode,
		const std::vector< std::string > &	ins,
		const std::vector< std::vector< std::string > > &	outs,
		const realizability_simplifier *	rs = `nullptr`
	)

#include <spot/twaalgos/aiger.hh>

Convert multiple mealy machines into an aig relying on the transformation described by mode.

Note: The states of each machine are represented by a block of latches not affected by the others. For this to work in a general setting, the outputs must be disjoint.

Unless ins and outs are specified, only the propositions actually used in the strategy appear in the aiger circuit. So it can happen that, for instance, propositions marked as output during the call to ltl_to_game() are absent. If ins and outs are used, all properties they list are guaranteed to appear in the aiger circuit.

If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.

◆ mealy_machines_to_aig() [3/4]

aig_ptr spot::mealy_machines_to_aig	(	const std::vector< mealy_like > &	m_vec,
		const char *	mode
	)

#include <spot/twaalgos/aiger.hh>

Convert multiple mealy machines into an aig relying on the transformation described by mode.

Note: The states of each machine are represented by a block of latches not affected by the others. For this to work in a general setting, the outputs must be disjoint.

Unless ins and outs are specified, only the propositions actually used in the strategy appear in the aiger circuit. So it can happen that, for instance, propositions marked as output during the call to ltl_to_game() are absent. If ins and outs are used, all properties they list are guaranteed to appear in the aiger circuit.

If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.

◆ mealy_machines_to_aig() [4/4]

aig_ptr spot::mealy_machines_to_aig	(	const std::vector< mealy_like > &	m_vec,
		const char *	mode,
		const std::vector< std::string > &	ins,
		const std::vector< std::vector< std::string > > &	outs,
		const realizability_simplifier *	rs = `nullptr`
	)

#include <spot/twaalgos/aiger.hh>

Convert multiple mealy machines into an aig relying on the transformation described by mode.

Note: The states of each machine are represented by a block of latches not affected by the others. For this to work in a general setting, the outputs must be disjoint.

Unless ins and outs are specified, only the propositions actually used in the strategy appear in the aiger circuit. So it can happen that, for instance, propositions marked as output during the call to ltl_to_game() are absent. If ins and outs are used, all properties they list are guaranteed to appear in the aiger circuit.

If rs is given and is not empty, it can be used to specify how unused output should be encoded by mapping them to some constant.

◆ operator<<() [1/2]

std::ostream & spot::operator<<	(	std::ostream &	os,
		const synthesis_info &	gi
	)

#include <spot/twaalgos/synthesis.hh>

Stream benchmarks and options.

◆ operator<<() [2/2]

std::ostream & spot::operator<<	(	std::ostream &	os,
		synthesis_info::algo	s
	)

#include <spot/twaalgos/synthesis.hh>

Stream algo.

◆ partitioned_game_relabel_here()

game_relabeling_map spot::partitioned_game_relabel_here	(	twa_graph_ptr &	arena,
		bool	relabel_env,
		bool	relabel_play,
		bool	split_env = `false`,
		bool	split_play = `false`,
		unsigned	max_letter = `-1u`,
		unsigned	max_letter_mult = `-1u`
	)

#include <spot/twaalgos/synthesis.hh>

Tries to relabel a SPLIT game arena using fresh propositions. Can be applied to env or player depending on relabel_env and relabel_play. The arguments split_env and split_play determine whether or not env and player edges are to be split into several transitions labelled by letters not conditions.

Returns: pair of relabeling_map, first is for env, second is for player. The maps are empty if no relabeling was performed

Note: Can also be applied to split mealy machine.; partitioned_relabel_here can not be used directly if there are T (true conditions)

◆ relabel_game_here()

void spot::relabel_game_here	(	twa_graph_ptr &	arena,
		game_relabeling_map &	rel_maps
	)

#include <spot/twaalgos/synthesis.hh>

Undoes a relabeling done by partitioned_game_relabel_here. A dedicated function is necessary in order to remove the variables tagging env and player conditions.

◆ solve_game()

bool spot::solve_game	(	twa_graph_ptr	arena,
		synthesis_info &	gi
	)

#include <spot/twaalgos/synthesis.hh>

Solve a game, and update synthesis_info.

This is just a wrapper around the solve_game() function with a single argument. This one measure the runtime and update gi.

◆ solved_game_to_mealy() [1/2]

twa_graph_ptr spot::solved_game_to_mealy ( twa_graph_ptr arena )

#include <spot/twaalgos/synthesis.hh>

creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations

◆ solved_game_to_mealy() [2/2]

twa_graph_ptr spot::solved_game_to_mealy	(	twa_graph_ptr	arena,
		synthesis_info &	gi
	)

#include <spot/twaalgos/synthesis.hh>

creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations

◆ solved_game_to_separated_mealy() [1/2]

twa_graph_ptr spot::solved_game_to_separated_mealy ( twa_graph_ptr arena )

#include <spot/twaalgos/synthesis.hh>

creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations

◆ solved_game_to_separated_mealy() [2/2]

twa_graph_ptr spot::solved_game_to_separated_mealy	(	twa_graph_ptr	arena,
		synthesis_info &	gi
	)

#include <spot/twaalgos/synthesis.hh>

creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations

◆ solved_game_to_split_mealy() [1/2]

twa_graph_ptr spot::solved_game_to_split_mealy ( twa_graph_ptr arena )

#include <spot/twaalgos/synthesis.hh>

creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations

◆ solved_game_to_split_mealy() [2/2]

twa_graph_ptr spot::solved_game_to_split_mealy	(	twa_graph_ptr	arena,
		synthesis_info &	gi
	)

#include <spot/twaalgos/synthesis.hh>

creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations

◆ split_2step() [1/2]

twa_graph_ptr spot::split_2step	(	const const_twa_graph_ptr &	aut,
		bool	complete_env = `true`
	)

#include <spot/twaalgos/synthesis.hh>

Like split_2step but relying on the named property 'synthesis-outputs'.

◆ split_2step() [2/2]

twa_graph_ptr spot::split_2step	(	const const_twa_graph_ptr &	aut,
		const bdd &	output_bdd,
		bool	complete_env = `true`
	)

#include <spot/twaalgos/synthesis.hh>

make each transition a 2-step transition, transforming the graph into an alternating arena

Given a set of atomic propositions I, split each transition p – cond --> q cond in 2^2^AP into a set of transitions of the form p – {a} --> (p,a) – o --> q for each a in cond ∪ 2^2^I and where o = (cond & a) ∪ 2^2^O.

By definition, the states p are deterministic, only the states of the form (p,a) may be non-deterministic. This function is used to transform an automaton into a turn-based game in the context of LTL reactive synthesis. The player of inputs (aka environment) plays first.

Parameters

aut	automaton to be transformed
output_bdd	conjunction of all output AP, all APs not present are treated as inputs
complete_env	Whether the automaton should be complete for the environment, i.e. the player of inputs

Note: This function also computes the state players; If the automaton is to be completed, sink states will be added for both env and player if necessary

◆ split_independent_formulas() [1/2]

std::pair< std::vector< formula >, std::vector< std::set< formula > > > spot::split_independent_formulas	(	const std::string &	f,
		const std::vector< std::string > &	outs
	)

#include <spot/twaalgos/synthesis.hh>

Seeks to decompose a formula into independently synthetizable sub-parts. The conjunction of all sub-parts then satisfies the specification.

The algorithm is based on work by Finkbeiner et al. [23], [24].

Parameters

f	the formula to split
outs	vector with the names of all output propositions

Returns: A vector of pairs holding a subformula and the used output propositions each.

◆ split_independent_formulas() [2/2]

std::pair< std::vector< formula >, std::vector< std::set< formula > > > spot::split_independent_formulas	(	formula	f,
		const std::vector< std::string > &	outs
	)

#include <spot/twaalgos/synthesis.hh>

Seeks to decompose a formula into independently synthetizable sub-parts. The conjunction of all sub-parts then satisfies the specification.

The algorithm is based on work by Finkbeiner et al. [23], [24].

Parameters

f	the formula to split
outs	vector with the names of all output propositions

Returns: A vector of pairs holding a subformula and the used output propositions each.

◆ try_create_direct_strategy()

mealy_like spot::try_create_direct_strategy	(	formula	f,
		const std::vector< std::string > &	output_aps,
		synthesis_info &	gi,
		bool	want_strategy = `false`
	)

#include <spot/twaalgos/synthesis.hh>

Creates a strategy for the formula given by calling all intermediate steps.

For certain formulas, we can ''bypass'' the traditional way and find directly a strategy or some other representation of a winning condition without translating the formula as such. If no such simplifications can be made, it executes the usual way.

Parameters

f	The formula to synthesize a strategy for
output_aps	A vector with the name of all output properties. All APs not named in this vector are treated as inputs
want_strategy	Set to false if we don't want to construct the strategy but only test realizability.

◆ unsplit_2step()

twa_graph_ptr spot::unsplit_2step ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/synthesis.hh>

the inverse of split_2step

Precondition: aut is an alternating arena

Postcondition: All edge conditions in the returned automaton are of the form ins&outs, with ins/outs being a condition over the input/output propositions

Note: This function relies on the named property "state-player"

Classes

Functions

Detailed Description

Function Documentation

◆ ltl_to_game() [1/4]

◆ ltl_to_game() [2/4]

◆ ltl_to_game() [3/4]

◆ ltl_to_game() [4/4]

◆ mealy_machine_to_aig() [1/4]

◆ mealy_machine_to_aig() [2/4]

◆ mealy_machine_to_aig() [3/4]

◆ mealy_machine_to_aig() [4/4]

◆ mealy_machines_to_aig() [1/4]

◆ mealy_machines_to_aig() [2/4]

◆ mealy_machines_to_aig() [3/4]

◆ mealy_machines_to_aig() [4/4]

◆ operator<<() [1/2]

◆ operator<<() [2/2]

◆ partitioned_game_relabel_here()

◆ relabel_game_here()

◆ solve_game()

◆ solved_game_to_mealy() [1/2]

◆ solved_game_to_mealy() [2/2]

◆ solved_game_to_separated_mealy() [1/2]

◆ solved_game_to_separated_mealy() [2/2]

◆ solved_game_to_split_mealy() [1/2]

◆ solved_game_to_split_mealy() [2/2]

◆ split_2step() [1/2]

◆ split_2step() [2/2]

◆ split_independent_formulas() [1/2]

◆ split_independent_formulas() [2/2]

◆ try_create_direct_strategy()

◆ unsplit_2step()