Functions related to Mealy machines

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::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::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...
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 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 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 machine that has be 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 tyoe (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 [46].

Parameters

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 [46].

Parameters

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 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 use inclusion between signatures to force some output when there is a choice in order to favor more reductions. Only infinite traces are considered. See [46] 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

This is a bisimulation based reduction, that optionally use inclusion between signatures to force some output when there is a choice in order to favor more reductions. Only infinite traces are considered. See [46] 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.

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 transitions as a label of the form (in)&(out). This function will turn each transtion 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 transitions as a label of the form (in)&(out). This function will turn each transtion 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

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