22 #include <spot/misc/common.hh> 23 #include <spot/twa/fwd.hh> 31 typedef std::vector<std::pair<unsigned, unsigned>> product_states;
46 twa_graph_ptr
product(
const const_twa_graph_ptr& left,
47 const const_twa_graph_ptr& right);
66 twa_graph_ptr
product(
const const_twa_graph_ptr& left,
67 const const_twa_graph_ptr& right,
69 unsigned right_state);
84 twa_graph_ptr
product_or(
const const_twa_graph_ptr& left,
85 const const_twa_graph_ptr& right);
104 twa_graph_ptr
product_or(
const const_twa_graph_ptr& left,
105 const const_twa_graph_ptr& right,
107 unsigned right_state);
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_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.