Hard-coded families of automata.

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 , spot::gen::AUT_CYCLIST_TRACE_NBA , spot::gen::AUT_CYCLIST_PROOF_DBA , 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...

Detailed Description

Enumeration Type Documentation

aut_pattern_id

enum spot::gen::aut_pattern_id

#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. \cite kuperberg.15.icalp 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 \cite loding.99.fstts , 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 \cite loding.99.fstts .
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 \cite thomas.97.chapter . Our implementation uses $\lceil \log_2(n+1)\rceil$ atomic propositions to encode the $n+1$ letters used in the original alphabet.
AUT_CYCLIST_TRACE_NBA	An NBA with (n+2) states derived from a Cyclic test case. This familly of automata is derived from a couple of examples supplied by Reuben Rowe. The task is to check that the automaton generated with AUT_CYCLIST_TRACE_NBA for a given n contain the automaton generated with AUT_CYCLIST_PROOF_DBA for the same n.
AUT_CYCLIST_PROOF_DBA	A DBA with (n+2) states derived from a Cyclic test case. This familly of automata is derived from a couple of examples supplied by Reuben Rowe. The task is to check that the automaton generated with AUT_CYCLIST_TRACE_NBA for a given n contain the automaton generated with AUT_CYCLIST_PROOF_DBA for the same n.

Function Documentation

aut_pattern()

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.

aut_pattern_name()

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.