22 #include <spot/misc/bitvect.hh>
23 #include <spot/twa/fwd.hh>
56 typedef std::vector<struct nca_st_info*> vect_nca_info;
70 SPOT_API twa_graph_ptr
72 bool named_states =
false,
73 vect_nca_info* nca_info =
nullptr);
84 SPOT_API twa_graph_ptr
86 bool named_states =
false,
87 vect_nca_info* nca_info =
nullptr);
97 SPOT_API twa_graph_ptr
98 to_nca(const_twa_graph_ptr aut,
bool named_states =
false);
108 SPOT_API twa_graph_ptr
109 nsa_to_dca(const_twa_graph_ptr aut,
bool named_states =
false);
119 SPOT_API twa_graph_ptr
120 dnf_to_dca(const_twa_graph_ptr aut,
bool named_states =
false);
131 SPOT_API twa_graph_ptr
132 to_dca(const_twa_graph_ptr aut,
bool named_states =
false);
A bit vector.
Definition: bitvect.hh:52
Definition: automata.hh:27
twa_graph_ptr dnf_to_dca(const_twa_graph_ptr aut, bool named_states=false)
Converts an aut. with acceptance in DNF to a det. co-Büchi aut.
twa_graph_ptr dnf_to_nca(const_twa_graph_ptr aut, bool named_states=false, vect_nca_info *nca_info=nullptr)
Converts an aut. with acceptance in DNF to a nondet. co-Büchi aut.
twa_graph_ptr to_dca(const_twa_graph_ptr aut, bool named_states=false)
Converts any ω-automata to deterministic co-buchi.
twa_graph_ptr to_nca(const_twa_graph_ptr aut, bool named_states=false)
Converts any ω-automata to non-deterministic co-buchi.
twa_graph_ptr nsa_to_dca(const_twa_graph_ptr aut, bool named_states=false)
Converts a nondet Streett-like aut. to a det. co-Büchi aut.
twa_graph_ptr nsa_to_nca(const_twa_graph_ptr aut, bool named_states=false, vect_nca_info *nca_info=nullptr)
Converts a nondet Streett-like aut. to a nondet. co-Büchi aut.
Definition: cobuchi.hh:38