spot 2.12.2
|
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... | |
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.
m | The automaton to be verified |
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.
m | The automaton to be verified |
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.
m | The automaton to be verified |
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
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.
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 [48].
premin | Whether to use reduce_mealy as a preprocessing:
|
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 [48].
si | synthesis_info structure used to store data for benchmarking and indicates which premin level to use |
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 [48] for details.
mm | The mealy machine to be minimized, has to be unsplit. |
output_assignment | Whether or not to use output assignment |
mm
.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 [48] for details.
mm | The mealy machine to be minimized, has to be unsplit. |
output_assignment | Whether or not to use output assignment |
mm
.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):
Minimizes the given machine m inplace, the parameter split_out specifies if the result should be split.
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):
Minimizes the given machine m inplace, the parameter split_out specifies if the result should be split.
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 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)
m | separated mealy machine to be split |
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 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)
m | separated mealy machine to be split |
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.