spot
2.9.3
|
Enumerations | |
enum | spot::gen::aut_pattern_id { AUT_BEGIN = 256, spot::gen::AUT_KS_NCA = AUT_BEGIN, spot::gen::AUT_L_NBA, spot::gen::AUT_L_DSA, spot::gen::AUT_M_NBA, AUT_END } |
Identifiers for automaton patterns. More... | |
Functions | |
twa_graph_ptr | spot::gen::aut_pattern (aut_pattern_id pattern, int n, spot::bdd_dict_ptr dict=make_bdd_dict()) |
generate an automaton from a known pattern More... | |
const char * | spot::gen::aut_pattern_name (aut_pattern_id pattern) |
convert an aut_pattern_it value into a name More... | |
#include <spot/gen/automata.hh>
Identifiers for automaton patterns.
Enumerator | |
---|---|
AUT_KS_NCA | A family of co-Büchi automata. Builds a co-Büchi automaton of size 2n+1 that is good-for-games and that has no equivalent deterministic co-Büchi automaton with less than 2^n / (2n+1) states. [24] Only defined for n>0. |
AUT_L_NBA | Hard-to-complement non-deterministic Büchi automata. Build a non-deterministic Büchi automaton with 3n+1 states and whose complementary language requires an automaton with at least n! states if Streett acceptance is used. Only defined for n>0. The automaton constructed corresponds to the right part of Fig.1 of [30] , except that only state q_1 is initial. (The fact that states q_2, q_3, ..., and q_n are not initial as in the paper does not change the recognized language.) |
AUT_L_DSA | DSA hard to convert to DRA. Build a deterministic Streett automaton 4n states, and n acceptance pairs, such that an equivalent deterministic Rabin automaton would require at least n! states. Only defined for 1<n<=16 because Spot does not support more than 32 acceptance pairs. This automaton corresponds to the right part of Fig.2 of [30] . |
AUT_M_NBA | An NBA with (n+1) states whose complement needs ≥n! states. This automaton is usually attributed to Max Michel (1988), who described it in some unpublished document. Other descriptions of this automaton can be found in a number of papers [49] . Our implementation uses $ (n+1)$ atomic propositions to encode the $n+1$ letters used in the original alphabet. |
twa_graph_ptr spot::gen::aut_pattern | ( | aut_pattern_id | pattern, |
int | n, | ||
spot::bdd_dict_ptr | dict = make_bdd_dict() |
||
) |
#include <spot/gen/automata.hh>
generate an automaton from a known pattern
The pattern is specified using one value from the aut_pattern_id enum. See the man page of the genaut
binary for a description of those patterns, and bibliographic references.
In case you want to combine this automaton with other automata, pass the bdd_dict to use to make sure that all share the same.
const char* spot::gen::aut_pattern_name | ( | aut_pattern_id | pattern | ) |
#include <spot/gen/automata.hh>
convert an aut_pattern_it value into a name
The returned name is suitable to be used as an option key for the genaut binary.