spot/doc/org/randaut.org

randaut

• States and density
• Acceptance condition
• Determinism
• Output formats
• Generating a stream of automata

The randaut tool generates random (connected) automata.

By default, it will generate a random automaton with 10 states, no acceptance sets, and using a set of atomic propositions you have to supply.

randaut a b

As for randltl, you can supply a number of atomic propositions instead of giving a list of atomic propositions.

States and density

The numbers of states can be controlled using the -S option. This option will accept a range as argument, so for instance -S3..6 will generate an automaton with 3 to 6 states.

The number of edges can be controlled using the -d (or --density) option. The argument should be a number between 0 and 1. In an automaton with $S$ states and density $d$, the degree of each state will follow a normal distribution with mean $1+(S-1)d$ and variance $(S-1)d(1-d)$.

In particular -d0 will cause all states to have 1 successors, and -d1 will cause all states to be interconnected.

randaut -S3 -d0 2

randaut -S3 -d1 2

Acceptance condition

The generation of the acceptance sets abn is controlled with the following three parameters:

• -A ACCEPTANCE (or --acceptance=ACCEPTANCE) controls both the acceptance condition, and the number of associated acceptance sets. The ACCEPTANCE argument is documented in --help as follows:

 RANGE may have one of the following forms: 'INT', 'INT..INT', or '..INT'.
 In the latter case, the missing number is assumed to be 1.

 ACCEPTANCE may be either a RANGE (in which case generalized Büchi is
 assumed), or an arbitrary acceptance formula such as 'Fin(0)|Inf(1)&Fin(2)' in
 the same syntax as in the HOA format, or one of the following patterns:
   none
   all
   Buchi
   co-Buchi
   generalized-Buchi RANGE
   generalized-co-Buchi RANGE
   Rabin RANGE
   Streett RANGE
   generalized-Rabin INT RANGE RANGE ... RANGE
   parity (min|max|rand) (odd|even|rand) RANGE
   random RANGE
   random RANGE PROBABILITY
 The random acceptance condition uses each set only once, unless a probability
 (to reuse the set again every time it is used) is given.

When a range of the form $i..j$ is used, the actual value is taken as randomly between $i$ and $j$ (included).

• -a (or --acc-probability) controls the probability that any transition belong to a given acceptance set.
• --state-acc requests that the automaton use state-based acceptance. In this case, -a is the probability that a state belong to the acceptance set. (Because Spot only deals with transition-based acceptance internally, this options force all transitions leaving a state to belong to the same acceptance sets. But if the output format allows state-acceptance, it will be used.)

In addition, -B (or --ba) is a shorthand for -A1 --state-acc, ans -s (or --spin) implies -B.

randaut -S3 -d0.5 -A3 -a0.5 2

randaut -S3 -d0.4 -B -a0.7 2

randaut -S6 -d0.4 --state-acc -a.2 -A 'Streett 1..3' 2 --dot=.a

Determinism

The output can only contain a single edge between two given states. By default, the label of this edge is a random assignment of all atomic propositions. Two edges leaving the same state may therefore have the same label.

If the -D (or --deterministic) option is supplied, the labels are generated differently: once the degree $m$ of a state has been decided, the algorithm will compute a set of $m$ disjoint Boolean formulas over the given atomic propositions, such that the sum of all these formulas is $\top$. The resulting automaton is therefore deterministic and complete.

randaut -D -S3 -d0.6 -A2 -a0.5 2

Note that in a deterministic automaton with $a$ atomic propositions, it is not possible to have states with more than $2^a$ successors. If the combination of -d and -S allows the situation where a state can have more than $2^a$ successors, the degree will be clipped to $2^a$. When working with random deterministic automata over $a$ atomic propositions, we suggest you always request more than $2^a$ states.

Output formats

The output format can be controlled using the common output options like --hoaf, --dot=, --lbtt, and --spin. Note that --spin automatically implies --ba.

Generating a stream of automata

Use option -n to specify a number of automata to build. A negative value will cause an infinite number of automata to be produced. This generation of multiple automata is probably useful only with --hoaf, when piped to another tool that can read this format and process automata in batches.