22 #include <spot/twa/twagraph.hh>
27 struct synthesis_info;
78 SPOT_API twa_graph_ptr
86 SPOT_API twa_graph_ptr
101 SPOT_API twa_graph_ptr
103 bool output_assignment =
false);
107 bool output_assignment =
false);
120 SPOT_API twa_graph_ptr
132 const_twa_graph_ptr right,
133 bool verbose =
false);
141 SPOT_API twa_graph_ptr
143 const const_twa_graph_ptr& right);
Definition: automata.hh:27
void reduce_mealy_here(twa_graph_ptr &mm, bool output_assignment=false)
reduce an (in)completely specified mealy machine Based on signature inclusion or equality....
twa_graph_ptr reduce_mealy(const const_twa_graph_ptr &mm, bool output_assignment=false)
reduce an (in)completely specified mealy machine Based on signature inclusion or equality....
bool is_split_mealy(const const_twa_graph_ptr &m)
Checks whether or not the automaton is a split mealy machine.
twa_graph_ptr minimize_mealy(const const_twa_graph_ptr &mm, int premin=-1)
Minimizes an (in)completely specified mealy machine The approach is described in.
twa_graph_ptr mealy_product(const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
Product between two mealy machines left and right.
bool 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.
bool is_mealy(const const_twa_graph_ptr &m)
Checks whether or not the automaton is a mealy machine.
bool is_separated_mealy(const const_twa_graph_ptr &m)
Checks whether or not the automaton is a separated mealy machine.
void 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 ...
twa_graph_ptr split_separated_mealy(const const_twa_graph_ptr &m)
make each transition in a separated mealy machine a 2-step transition.
bool is_input_deterministic_mealy(const const_twa_graph_ptr &m)
Checks whether or not a mealy machine is input deterministic.
void split_separated_mealy_here(const twa_graph_ptr &m)
make each transition in a separated mealy machine a 2-step transition.
twa_graph_ptr unsplit_mealy(const const_twa_graph_ptr &m)
the inverse of split_separated_mealy
Benchmarking data and options for synthesis.
Definition: synthesis.hh:81