Functions
bool	spot::is_mealy (const const_twa_graph_ptr &m)
	Checks whether the automaton is a mealy machine. More...

bool	spot::is_separated_mealy (const const_twa_graph_ptr &m)
	Checks whether the automaton is a separated mealy machine. More...

bool	spot::is_split_mealy (const const_twa_graph_ptr &m)
	Checks whether or not the automaton is a split mealy machine. More...

twa_graph_ptr	spot::unsplit_mealy (const const_twa_graph_ptr &m)
	The inverse of split_separated_mealy. More...

twa_graph_ptr	spot::reduce_mealy (const const_twa_graph_ptr &mm, bool output_assignment=true)
	Reduce an (in)completely specified mealy machine. More...

void	spot::reduce_mealy_here (twa_graph_ptr &mm, bool output_assignment=true)
	Reduce an (in)completely specified mealy machine in place. More...

twa_graph_ptr	spot::minimize_mealy (const const_twa_graph_ptr &mm, int premin=-1)
	Minimizes an (in)completely specified mealy machine. More...

twa_graph_ptr	spot::minimize_mealy (const const_twa_graph_ptr &mm, synthesis_info &si)
	Minimizes an (in)completely specified mealy machine. More...

bool	spot::is_split_mealy_specialization (const_twa_graph_ptr left, const_twa_graph_ptr right, bool verbose=false)
	Test if the split mealy machine right is a specialization of the split mealy machine left. More...

twa_graph_ptr	spot::mealy_product (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
	Product between two mealy machines left and right. More...

twa_graph_ptr	spot::terminating_mealy_to_buchi (const const_twa_graph_ptr &mealy, const std::string &signal_name)
	Convert a terminating Mealy machine to a Büchi automaton. More...

twa_graph_ptr	spot::split_separated_mealy (const const_twa_graph_ptr &m)
	Split a separated mealy machine. More...

void	spot::split_separated_mealy_here (const twa_graph_ptr &m)
	Split a separated mealy machine. More...

void	spot::simplify_mealy_here (twa_graph_ptr &m, int minimize_lvl, bool split_out)
	Convenience function to call minimize_mealy or reduce_mealy. Uses the same convention as ltlsynt for minimize_lvl (or the field `minimize_lvl` of si): More...

void	spot::simplify_mealy_here (twa_graph_ptr &m, synthesis_info &si, bool split_out)
	Convenience function to call minimize_mealy or reduce_mealy. Uses the same convention as ltlsynt for minimize_lvl (or the field `minimize_lvl` of si): More...

Detailed Description

Function Documentation

◆ is_mealy()

bool spot::is_mealy ( const const_twa_graph_ptr & m )

#include <spot/twaalgos/mealy_machine.hh>

Checks whether the automaton is a mealy machine.

A mealy machine is an automaton with the named property "synthesis-outputs" and that has a "true" as acceptance condition.

Parameters

m	The automaton to be verified

See also: is_separated_mealy; is_split_mealy; is_input_deterministic_mealy

◆ is_separated_mealy()

bool spot::is_separated_mealy ( const const_twa_graph_ptr & m )

#include <spot/twaalgos/mealy_machine.hh>

Checks whether the automaton is a separated mealy machine.

A separated mealy machine is a mealy machine with all transitions having the form (in)&(out) where in and out are BDDs over the input and output propositions.

Parameters

m	The automaton to be verified

See also: is_mealy; is_split_mealy

◆ is_split_mealy()

bool spot::is_split_mealy ( const const_twa_graph_ptr & m )

#include <spot/twaalgos/mealy_machine.hh>

Checks whether or not the automaton is a split mealy machine.

A split mealy machine is a mealy machine that has been converted into a game. It should have the named property "state-player", moreover the game should be alternating between the two players. Transitions leaving states owned by player 0 (the environment) should use only input propositions, while transitions leaving states owned by player 1 (the controller) should use only output propositions.

Parameters

m	The automaton to be verified

See also: is_mealy; is_separated_mealy

◆ is_split_mealy_specialization()

bool spot::is_split_mealy_specialization	(	const_twa_graph_ptr	left,
		const_twa_graph_ptr	right,
		bool	verbose = `false`
	)

#include <spot/twaalgos/mealy_machine.hh>

Test if the split mealy machine right is a specialization of the split mealy machine left.

That is, all input sequences valid for left must be applicable for right and the induced sequence of output signals of right must imply the ones of left

◆ mealy_product()

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

#include <spot/twaalgos/mealy_machine.hh>

Product between two mealy machines left and right.

Precondition: The machines have to be both either split or unsplit, input complete and compatible. All of this is checked by assertion.

Returns: A mealy machine representing the shared behaviour, with the same type (mealy/separated/split) as the input machines

◆ minimize_mealy() [1/2]

twa_graph_ptr spot::minimize_mealy	(	const const_twa_graph_ptr &	mm,
		int	premin = `-1`
	)

#include <spot/twaalgos/mealy_machine.hh>

Minimizes an (in)completely specified mealy machine.

The approach is described in [renkin.22.forte].

Parameters

mm	The mealy machine to be minimized.
premin	Whether to use reduce_mealy as a preprocessing: -1: Do not use; 0: Use without output assignment; 1: Use with output assignment.

Returns: A split mealy machines which is a minimal specialization of the original machine.

Note: Enabling premin will remove finite traces.

See also: is_split_mealy_specialization

◆ minimize_mealy() [2/2]

twa_graph_ptr spot::minimize_mealy	(	const const_twa_graph_ptr &	mm,
		synthesis_info &	si
	)

#include <spot/twaalgos/mealy_machine.hh>

Minimizes an (in)completely specified mealy machine.

The approach is described in [renkin.22.forte].

Parameters

mm	The mealy machine to be minimized.
si	synthesis_info structure used to store data for benchmarking and indicates which premin level to use

Returns: A split mealy machines which is a minimal specialization of the original machine.

Note: Enabling premin will remove finite traces.; If si.opt contains an option "satlogcsv" detailed results will be stored in this file. If it contains "satlogdimacs" all sat problems will be stored.

See also: is_split_mealy_specialization

◆ reduce_mealy()

twa_graph_ptr spot::reduce_mealy	(	const const_twa_graph_ptr &	mm,
		bool	output_assignment = `true`
	)

#include <spot/twaalgos/mealy_machine.hh>

Reduce an (in)completely specified mealy machine.

This is a bisimulation based reduction, that optionally uses inclusion between signatures to force some output when there is a choice in order to favor more reductions. Only infinite traces are considered. See [renkin.22.forte] for details.

Parameters

mm	The mealy machine to be minimized, has to be unsplit.
output_assignment	Whether or not to use output assignment

Returns: A specialization of mm.

Note: If mm is separated, the returned machine is separated as well.

◆ reduce_mealy_here()

void spot::reduce_mealy_here	(	twa_graph_ptr &	mm,
		bool	output_assignment = `true`
	)

#include <spot/twaalgos/mealy_machine.hh>

Reduce an (in)completely specified mealy machine in place.

This is a bisimulation based reduction, that optionally uses inclusion between signatures to force some output when there is a choice in order to favor more reductions. Only infinite traces are considered. See [renkin.22.forte] for details.

Parameters

mm	The mealy machine to be minimized in place, has to be unsplit.
output_assignment	Whether or not to use output assignment

Note: If mm is separated, the resulting machine is separated as well.

◆ simplify_mealy_here() [1/2]

void spot::simplify_mealy_here	(	twa_graph_ptr &	m,
		int	minimize_lvl,
		bool	split_out
	)

#include <spot/twaalgos/mealy_machine.hh>

Convenience function to call minimize_mealy or reduce_mealy. Uses the same convention as ltlsynt for minimize_lvl (or the field minimize_lvl of si):

0: no reduction
1: bisimulation based reduction
2: bisimulation with output assignment
3: SAT minimization
4: 1 then 3
5: 2 then 3

Minimizes the given machine m inplace, the parameter split_out specifies if the result should be split.

◆ simplify_mealy_here() [2/2]

void spot::simplify_mealy_here	(	twa_graph_ptr &	m,
		synthesis_info &	si,
		bool	split_out
	)

#include <spot/twaalgos/mealy_machine.hh>

Convenience function to call minimize_mealy or reduce_mealy. Uses the same convention as ltlsynt for minimize_lvl (or the field minimize_lvl of si):

0: no reduction
1: bisimulation based reduction
2: bisimulation with output assignment
3: SAT minimization
4: 1 then 3
5: 2 then 3

Minimizes the given machine m inplace, the parameter split_out specifies if the result should be split.

◆ split_separated_mealy()

twa_graph_ptr spot::split_separated_mealy ( const const_twa_graph_ptr & m )

#include <spot/twaalgos/mealy_machine.hh>

Split a separated mealy machine.

In a separated mealy machine, every transition has a label of the form (in)&(out). This function will turn each transition into a pair of consecutive transitions labeled by in and out, and turn the mealy machine into a game (what we call a split mealy machine)

Parameters

m	separated mealy machine to be split

See also: is_split_mealy

◆ split_separated_mealy_here()

void spot::split_separated_mealy_here ( const twa_graph_ptr & m )

#include <spot/twaalgos/mealy_machine.hh>

Split a separated mealy machine.

In a separated mealy machine, every transition has a label of the form (in)&(out). This function will turn each transition into a pair of consecutive transitions labeled by in and out, and turn the mealy machine into a game (what we call a split mealy machine)

Parameters

m	separated mealy machine to be split

See also: is_split_mealy

◆ terminating_mealy_to_buchi()

twa_graph_ptr spot::terminating_mealy_to_buchi	(	const const_twa_graph_ptr &	mealy,
		const std::string &	signal_name
	)

#include <spot/twaalgos/mealy_machine.hh>

Convert a terminating Mealy machine to a Büchi automaton.

In a terminating Mealy machine, termination is indicated by self-loops on every state. This function converts such a machine to a Büchi automaton where an explicit output signal (named signal_name) is added: it is true on all non-terminating transitions, and becomes false on the self-loop of an added accepting sink state.

The resulting automaton has one more state than the input (the accepting sink). All transitions from the sink to itself carry !signal_name and are marked with Büchi acceptance, so an accepting run corresponds to a terminating execution of the Mealy machine.

Parameters

mealy	the terminating Mealy machine
signal_name	the name of the terminating signal to add

Returns: a Büchi automaton with explicit termination signal

◆ unsplit_mealy()

twa_graph_ptr spot::unsplit_mealy ( const const_twa_graph_ptr & m )

#include <spot/twaalgos/mealy_machine.hh>

The inverse of split_separated_mealy.

Take a split mealy machine m, and build a separated mealy machine.

See also: split_separated_mealy; is_split_mealy; is_separated_mealy

Functions

Detailed Description

Function Documentation

◆ is_mealy()

◆ is_separated_mealy()

◆ is_split_mealy()

◆ is_split_mealy_specialization()

◆ mealy_product()

◆ minimize_mealy() [1/2]

◆ minimize_mealy() [2/2]

◆ reduce_mealy()

◆ reduce_mealy_here()

◆ simplify_mealy_here() [1/2]

◆ simplify_mealy_here() [2/2]

◆ split_separated_mealy()

◆ split_separated_mealy_here()

◆ terminating_mealy_to_buchi()

◆ unsplit_mealy()