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

Typedefs
typedef std::shared_ptr< aig >	spot::aig_ptr
	Shared pointer to an aig. More...

typedef std::shared_ptr< const aig >	spot::const_aig_ptr
	Shared pointer to a const aig. More...

Functions
twa_graph_ptr	spot::split_2step (const const_twa_graph_ptr &aut, const bdd &output_bdd, bool complete_env=true, synthesis_info::splittype sp=synthesis_info::splittype::AUTO, bool moore=false)
	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, synthesis_info::splittype sp=synthesis_info::splittype::AUTO, bool moore=false)
	Like split_2step but relying on the named property 'synthesis-outputs'. More...

twa_graph_ptr	spot::split_2step (const const_twa_graph_ptr &aut, synthesis_info &gi)
	Like split_2step but allows to fine-tune the splitting via the options set in gi, always completes the environment states and relies on the named property to extract the output proposition. 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...

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

twa_graph_ptr	spot::ltl_to_game (formula f, const std::vector< std::string > &all_outs, const std::vector< std::string > *unobs=nullptr)
	Creates a game from a specification and a set of output propositions. 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, const std::string terminating_signal=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, const std::string terminating_signal=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 twa_graph_ptr &m, const char mode, const std::vector< std::string > &ins, const std::vector< std::string > &outs, const realizability_simplifier rs=nullptr, const std::string *terminating_signal=nullptr)
	Convert a mealy (like) machine into an aig relying on the transformation described by mode, with explicit AP lists. 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, const std::string *terminating_signal=nullptr)
	Convert a mealy (like) machine into an aig relying on the transformation described by mode, with explicit AP lists. More...

aig_ptr	spot::mealy_machines_to_aig (const std::vector< const_twa_graph_ptr > &m_vec, const char mode, const std::string terminating_signal=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::string terminating_signal=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< 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, const std::string *terminating_signal=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< 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, const std::string *terminating_signal=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, const std::string *terminating_signal=nullptr)
	Convert multiple mealy machines into an aig relying on the transformation described by mode. 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

Typedef Documentation

◆ aig_ptr

typedef std::shared_ptr<aig> spot::aig_ptr

#include <spot/twaalgos/aiger.hh>

Shared pointer to an aig.

◆ const_aig_ptr

typedef std::shared_ptr<const aig> spot::const_aig_ptr

#include <spot/twaalgos/aiger.hh>

Shared pointer to a const aig.

Function Documentation

◆ ltl_to_game() [1/2]

twa_graph_ptr spot::ltl_to_game	(	formula	f,
		const std::vector< std::string > &	all_outs,
		const std::vector< std::string > *	unobs = `nullptr`
	)

#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
all_outs	The names of all output propositions
unobs	When non-null, a list of additional unobservable propositions not included in all_outs.

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

◆ ltl_to_game() [2/2]

twa_graph_ptr spot::ltl_to_game	(	formula	f,
		const std::vector< std::string > &	all_outs,
		synthesis_info &	gi,
		const std::vector< std::string > *	unobs = `nullptr`
	)

#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
all_outs	The names of all output propositions
gi	synthesis_info structure
unobs	When non-null, a list of additional unobservable propositions not included in all_outs.

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,
		const std::string *	terminating_signal = `nullptr`
	)

#include <spot/twaalgos/aiger.hh>

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

Parameters

m	The mealy machine to convert.
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. Uses the named-property synthesis-output to determine input/output APs.
terminating_signal	If non-null, specifies the name of an extra output signal that is initially true and becomes false after the first self-loop (termination) of the Mealy machine.

◆ mealy_machine_to_aig() [2/4]

aig_ptr spot::mealy_machine_to_aig	(	const mealy_like &	m,
		const char *	mode,
		const std::string *	terminating_signal = `nullptr`
	)

#include <spot/twaalgos/aiger.hh>

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

Parameters

m	The mealy machine to convert.
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. Uses the named-property synthesis-output to determine input/output APs.
terminating_signal	If non-null, specifies the name of an extra output signal that is initially true and becomes false after the first self-loop (termination) of the Mealy machine.

◆ 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`,
		const std::string *	terminating_signal = `nullptr`
	)

#include <spot/twaalgos/aiger.hh>

Convert a mealy (like) machine into an aig relying on the transformation described by mode, with explicit AP lists.

Parameters

m	The mealy machine to convert.
mode	Encoding mode; see the 2-argument overload for details.
ins	Input atomic propositions; overrides the named-property synthesis-output. All propositions in ins and outs are guaranteed to appear in the aiger circuit.
outs	Output atomic propositions; see ins.
rs	When given and non-empty, specifies how unused outputs should be encoded by mapping them to some constant.
terminating_signal	If non-null, specifies the name of an extra output signal that is initially true and becomes false after the first self-loop (termination) of the Mealy machine.

◆ 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`,
		const std::string *	terminating_signal = `nullptr`
	)

#include <spot/twaalgos/aiger.hh>

Convert a mealy (like) machine into an aig relying on the transformation described by mode, with explicit AP lists.

Parameters

m	The mealy machine to convert.
mode	Encoding mode; see the 2-argument overload for details.
ins	Input atomic propositions; overrides the named-property synthesis-output. All propositions in ins and outs are guaranteed to appear in the aiger circuit.
outs	Output atomic propositions; see ins.
rs	When given and non-empty, specifies how unused outputs should be encoded by mapping them to some constant.
terminating_signal	If non-null, specifies the name of an extra output signal that is initially true and becomes false after the first self-loop (termination) of the Mealy machine.

◆ mealy_machines_to_aig() [1/5]

aig_ptr spot::mealy_machines_to_aig	(	const std::vector< const_twa_graph_ptr > &	m_vec,
		const char *	mode,
		const std::string *	terminating_signal = `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.

If terminating_signal is non-null, it specifies the name of an extra output signal that is initially true and becomes false after the first self-loop (termination) of the Mealy machine.

◆ mealy_machines_to_aig() [2/5]

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`,
		const std::string *	terminating_signal = `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.

If terminating_signal is non-null, it specifies the name of an extra output signal that is initially true and becomes false after the first self-loop (termination) of the Mealy machine.

◆ mealy_machines_to_aig() [3/5]

aig_ptr spot::mealy_machines_to_aig	(	const std::vector< mealy_like > &	m_vec,
		const char *	mode,
		const std::string *	terminating_signal = `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.

If terminating_signal is non-null, it specifies the name of an extra output signal that is initially true and becomes false after the first self-loop (termination) of the Mealy machine.

◆ mealy_machines_to_aig() [4/5]

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`,
		const std::string *	terminating_signal = `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.

If terminating_signal is non-null, it specifies the name of an extra output signal that is initially true and becomes false after the first self-loop (termination) of the Mealy machine.

◆ mealy_machines_to_aig() [5/5]

aig_ptr spot::mealy_machines_to_aig	(	const std::vector< 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`,
		const std::string *	terminating_signal = `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.

If terminating_signal is non-null, it specifies the name of an extra output signal that is initially true and becomes false after the first self-loop (termination) of the Mealy machine.

◆ 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/3]

twa_graph_ptr spot::split_2step	(	const const_twa_graph_ptr &	aut,
		bool	complete_env = `true`,
		synthesis_info::splittype	sp = `synthesis_info::splittype::AUTO`,
		bool	moore = `false`
	)

#include <spot/twaalgos/synthesis.hh>

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

◆ split_2step() [2/3]

twa_graph_ptr spot::split_2step	(	const const_twa_graph_ptr &	aut,
		const bdd &	output_bdd,
		bool	complete_env = `true`,
		synthesis_info::splittype	sp = `synthesis_info::splittype::AUTO`,
		bool	moore = `false`
	)

#include <spot/twaalgos/synthesis.hh>

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

This function is used to transform an automaton into a turn-based game in the context of LTL reactive synthesis.

Given a set of atomic propositions I, split each transition p – cond --> q cond in 2^2^(I∪O) into a set of transitions whose form depend on the synthesis semantics used. For Mealy semantics we want transitions of the form: p – i₁ --> (p,i₁) – o₁ --> q p – i₂ --> (p,i₂) – o₂ --> q ... where iᵢ∈2^2^I, oᵢ∈2^2^O, and cond = Or(iᵢ∧oᵢ, i=1..n). For Moore semantics, we want p – o₁ --> (p,o₁) – i₁ --> q p – o₂ --> (p,o₂) – i₂ --> q ...

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
sp	Defines which splitting algo to use
moore	If true, use Moore (output-first) semantics: the controller plays first

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_2step() [3/3]

twa_graph_ptr spot::split_2step	(	const const_twa_graph_ptr &	aut,
		synthesis_info &	gi
	)

#include <spot/twaalgos/synthesis.hh>

Like split_2step but allows to fine-tune the splitting via the options set in gi, always completes the environment states and relies on the named property to extract the output proposition.

◆ 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. [finkbeiner.21.nfm], [finkbeiner.21.arxiv].

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. [finkbeiner.21.nfm], [finkbeiner.21.arxiv].

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
gi	synthesis_info structure controlling the synthesis algorithm.
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

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ aig_ptr

◆ const_aig_ptr

Function Documentation

◆ ltl_to_game() [1/2]

◆ ltl_to_game() [2/2]

◆ 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/5]

◆ mealy_machines_to_aig() [2/5]

◆ mealy_machines_to_aig() [3/5]

◆ mealy_machines_to_aig() [4/5]

◆ mealy_machines_to_aig() [5/5]

◆ 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/3]

◆ split_2step() [2/3]

◆ split_2step() [3/3]

◆ split_independent_formulas() [1/2]

◆ split_independent_formulas() [2/2]

◆ try_create_direct_strategy()

◆ unsplit_2step()