22 #include <spot/misc/common.hh> 23 #include <spot/twa/fwd.hh> 31 typedef std::vector<std::pair<unsigned, unsigned>> product_states;
49 twa_graph_ptr
product(
const const_twa_graph_ptr& left,
50 const const_twa_graph_ptr& right);
72 twa_graph_ptr
product(
const const_twa_graph_ptr& left,
73 const const_twa_graph_ptr& right,
75 unsigned right_state);
93 twa_graph_ptr
product_or(
const const_twa_graph_ptr& left,
94 const const_twa_graph_ptr& right);
116 twa_graph_ptr
product_or(
const const_twa_graph_ptr& left,
117 const const_twa_graph_ptr& right,
119 unsigned right_state);
138 twa_graph_ptr
product_susp(
const const_twa_graph_ptr& left,
139 const const_twa_graph_ptr& right_susp);
160 const const_twa_graph_ptr& right_susp);
Definition: automata.hh:26
twa_graph_ptr product(const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state)
Intersect two automata using a synchronous product.
twa_graph_ptr product_susp(const const_twa_graph_ptr &left, const const_twa_graph_ptr &right_susp)
Build the product of an automaton with a suspendable automaton.
twa_graph_ptr product_or_susp(const const_twa_graph_ptr &left, const const_twa_graph_ptr &right_susp)
Build the "or" product of an automaton with a suspendable automaton.
twa_graph_ptr product_or(const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state)
Sum two automata using a synchronous product.