22 #include <spot/misc/common.hh>
23 #include <spot/twa/fwd.hh>
24 #include <spot/twaalgos/powerset.hh>
53 twa_graph_ptr product(
const const_twa_graph_ptr& left,
54 const const_twa_graph_ptr& right,
80 twa_graph_ptr product(
const const_twa_graph_ptr& left,
81 const const_twa_graph_ptr& right,
103 const const_twa_graph_ptr& right);
126 const const_twa_graph_ptr& right,
128 unsigned right_state);
147 const const_twa_graph_ptr& right);
168 const const_twa_graph_ptr& right);
187 const const_twa_graph_ptr& right_susp);
208 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