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);
146 twa_graph_ptr
product_xor(
const const_twa_graph_ptr& left,
147 const const_twa_graph_ptr& right);
167 twa_graph_ptr
product_xnor(
const const_twa_graph_ptr& left,
168 const const_twa_graph_ptr& right);
186 twa_graph_ptr
product_susp(
const const_twa_graph_ptr& left,
187 const const_twa_graph_ptr& right_susp);
208 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_xnor(const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
XNOR two automata using a synchronous product.
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.
twa_graph_ptr product_xor(const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
XOR two deterministic automata using a synchronous product.