22 #include <spot/misc/common.hh>
23 #include <spot/twa/fwd.hh>
24 #include <spot/twaalgos/powerset.hh>
57 twa_graph_ptr product(
const const_twa_graph_ptr& left,
58 const const_twa_graph_ptr& right,
88 twa_graph_ptr product(
const const_twa_graph_ptr& left,
89 const const_twa_graph_ptr& right,
116 const const_twa_graph_ptr& right);
143 const const_twa_graph_ptr& right,
145 unsigned right_state);
164 const const_twa_graph_ptr& right);
185 const const_twa_graph_ptr& right);
204 const const_twa_graph_ptr& right_susp);
225 const const_twa_graph_ptr& right_susp);
Helper object to specify when an algorithm should abort its construction.
Definition: powerset.hh:48
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_xor(const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
XOR two deterministic automata using a synchronous product.
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(const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
Sum 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.
Definition: automata.hh:27
std::vector< std::pair< unsigned, unsigned > > product_states
Automata constructed by product() contain a property named "product-states" with this type.
Definition: product.hh:32