21#include <spot/misc/common.hh>
22#include <spot/twa/fwd.hh>
23#include <spot/twaalgos/powerset.hh>
56 twa_graph_ptr product(
const const_twa_graph_ptr& left,
57 const const_twa_graph_ptr& right,
87 twa_graph_ptr product(
const const_twa_graph_ptr& left,
88 const const_twa_graph_ptr& right,
115 const const_twa_graph_ptr& right);
142 const const_twa_graph_ptr& right,
144 unsigned right_state);
163 const const_twa_graph_ptr& right);
184 const const_twa_graph_ptr& right);
203 const const_twa_graph_ptr& right_susp);
224 const const_twa_graph_ptr& right_susp);
Helper object to specify when an algorithm should abort its construction.
Definition: powerset.hh:44
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:26
std::vector< std::pair< unsigned, unsigned > > product_states
Automata constructed by product() contain a property named "product-states" with this type.
Definition: product.hh:31