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 --dot

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 -Q option. This option will accept a range as argument, so for instance -Q3..6 will generate an automaton with 3 to 6 states.

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

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

randaut -Q3 -e0 2 --dot

randaut -Q3 -e1 2 --dot

Acceptance condition

The generation of the acceptance sets abn is controlled with the following four 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.
• -S (or --state-based-acceptance) 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-based acceptance, it will be used.)
• --colored requests that each transition (of state if combined with -S) in the generated automaton should belong to exactly one set (in that case -a is ignored, and -A must be used to specify an acceptance condition with at least one set).

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

randaut -Q3 -e0.5 -A3 -a0.5 2 --dot

randaut -Q3 -e0.4 -B -a0.7 2 --dot

randaut -Q6 -e0.4 -S -a.2 -A 'Streett 1..3' 2 --dot=.a

For generating random parity automata you should use the option --colored to make sure each transition (or state in the following example) belong to exactly one acceptance set. Note that you can specify a precise parity acceptance such as parity min even 3, or give randaut some freedom, as in this example.

randaut -Q10 -S --colored -A 'parity rand rand 3..4' 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 -Q3 -e0.6 -A2 -a0.5 2 --dot

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 -e and -Q 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 useful when piped to another tool that can process automata in batches.