UP | HOME

randaut

Table of Contents

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

randaut1.png

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

randaut2.png

randaut -Q3 -e1 2 --dot

randaut3.png

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

randaut4.png

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

randaut5.png

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

randaut5b.png

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

randaut5c.png

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

randaut6.png

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.