spot  2.11.3
Functions
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
mThe 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
mThe 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
mThe 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
preminWhether 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
sisynthesis_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
mmThe mealy machine to be minimized, has to be unsplit.
output_assignmentWhether 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
mmThe mealy machine to be minimized, has to be unsplit.
output_assignmentWhether 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
mseparated 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
mseparated 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

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1