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
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. TheACCEPTANCE
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.