22 #include <spot/misc/common.hh>
23 #include <spot/twa/fwd.hh>
24 #include <spot/twa/bdddict.hh>
112 SPOT_API twa_graph_ptr
114 spot::bdd_dict_ptr dict = make_bdd_dict());
const char * aut_pattern_name(aut_pattern_id pattern)
convert an aut_pattern_it value into a name
aut_pattern_id
Identifiers for automaton patterns.
Definition: automata.hh:36
twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n, spot::bdd_dict_ptr dict=make_bdd_dict())
generate an automaton from a known pattern
@ AUT_CYCLIST_PROOF_DBA
A DBA with (n+2) states derived from a Cyclic test case.
Definition: automata.hh:99
@ AUT_KS_NCA
A family of co-Büchi automata.
Definition: automata.hh:46
@ AUT_CYCLIST_TRACE_NBA
An NBA with (n+2) states derived from a Cyclic test case.
Definition: automata.hh:90
@ AUT_M_NBA
An NBA with (n+1) states whose complement needs ≥n! states.
Definition: automata.hh:81
@ AUT_L_NBA
Hard-to-complement non-deterministic Büchi automata.
Definition: automata.hh:58
@ AUT_L_DSA
DSA hard to convert to DRA.
Definition: automata.hh:70
Definition: automata.hh:27