21#include <spot/misc/common.hh>
22#include <spot/twa/fwd.hh>
23#include <spot/twa/bdddict.hh>
132 SPOT_API twa_graph_ptr
134 spot::bdd_dict_ptr dict = make_bdd_dict());
aut_pattern_id
Identifiers for automaton patterns.
Definition: automata.hh:35
const char * aut_pattern_name(aut_pattern_id pattern)
convert an aut_pattern_it value into a name
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_CYCLE_ONEHOT_NBA
cycles of n letters repeated n times
Definition: automata.hh:119
@ AUT_CYCLE_LOG_NBA
cycles of n letters repeated n times
Definition: automata.hh:108
@ AUT_CYCLIST_PROOF_DBA
A DBA with (n+2) states derived from a Cyclic test case.
Definition: automata.hh:98
@ AUT_KS_NCA
A family of co-Büchi automata.
Definition: automata.hh:45
@ AUT_CYCLIST_TRACE_NBA
An NBA with (n+2) states derived from a Cyclic test case.
Definition: automata.hh:89
@ AUT_M_NBA
An NBA with (n+1) states whose complement needs ≥n! states.
Definition: automata.hh:80
@ AUT_L_NBA
Hard-to-complement non-deterministic Büchi automata.
Definition: automata.hh:57
@ AUT_L_DSA
DSA hard to convert to DRA.
Definition: automata.hh:69
Definition: automata.hh:26