22 #include <spot/misc/common.hh> 23 #include <spot/twa/fwd.hh> 24 #include <spot/twaalgos/powerset.hh> 32 typedef std::vector<std::pair<unsigned, unsigned>> product_states;
53 twa_graph_ptr
product(
const const_twa_graph_ptr& left,
54 const const_twa_graph_ptr& right,
55 const output_aborter* aborter =
nullptr);
80 twa_graph_ptr
product(
const const_twa_graph_ptr& left,
81 const const_twa_graph_ptr& right,
84 const output_aborter* aborter =
nullptr);
102 twa_graph_ptr
product_or(
const const_twa_graph_ptr& left,
103 const const_twa_graph_ptr& right);
125 twa_graph_ptr
product_or(
const const_twa_graph_ptr& left,
126 const const_twa_graph_ptr& right,
128 unsigned right_state);
147 twa_graph_ptr
product_susp(
const const_twa_graph_ptr& left,
148 const const_twa_graph_ptr& right_susp);
169 const const_twa_graph_ptr& right_susp);
Definition: automata.hh:26
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.
twa_graph_ptr product(const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state, const output_aborter *aborter=nullptr)
Intersect two automata using a synchronous product.