# -*- coding: utf-8 -*-
#+TITLE: =randaut=
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html

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.

#+NAME: randaut1
#+BEGIN_SRC sh :results verbatim :exports code
randaut a b --dot
#+END_SRC
#+RESULTS: randaut1
#+begin_example
digraph G {
  rankdir=LR
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label=<0>]
  0 -> 8 [label=<!a &amp; !b>]
  0 -> 3 [label=<!a &amp; !b>]
  0 -> 4 [label=<!a &amp; !b>]
  1 [label=<1>]
  1 -> 7 [label=<a &amp; b>]
  1 -> 0 [label=<a &amp; b>]
  1 -> 6 [label=<a &amp; !b>]
  2 [label=<2>]
  2 -> 4 [label=<!a &amp; !b>]
  2 -> 0 [label=<a &amp; !b>]
  2 -> 5 [label=<a &amp; !b>]
  2 -> 9 [label=<!a &amp; b>]
  3 [label=<3>]
  3 -> 2 [label=<a &amp; b>]
  3 -> 9 [label=<a &amp; !b>]
  3 -> 3 [label=<a &amp; !b>]
  4 [label=<4>]
  4 -> 0 [label=<!a &amp; !b>]
  4 -> 7 [label=<!a &amp; b>]
  5 [label=<5>]
  5 -> 3 [label=<a &amp; !b>]
  5 -> 1 [label=<!a &amp; b>]
  5 -> 7 [label=<!a &amp; !b>]
  5 -> 9 [label=<!a &amp; b>]
  5 -> 5 [label=<!a &amp; !b>]
  6 [label=<6>]
  6 -> 8 [label=<a &amp; b>]
  6 -> 5 [label=<a &amp; !b>]
  6 -> 2 [label=<a &amp; !b>]
  7 [label=<7>]
  7 -> 8 [label=<!a &amp; !b>]
  7 -> 9 [label=<a &amp; b>]
  7 -> 0 [label=<!a &amp; b>]
  7 -> 1 [label=<!a &amp; !b>]
  7 -> 4 [label=<a &amp; b>]
  8 [label=<8>]
  8 -> 1 [label=<a &amp; b>]
  8 -> 3 [label=<!a &amp; b>]
  9 [label=<9>]
  9 -> 1 [label=<!a &amp; b>]
  9 -> 3 [label=<a &amp; !b>]
}
#+end_example

#+BEGIN_SRC dot :file randaut1.png :cmdline -Tpng :var txt=randaut1 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:randaut1.png]]

As for [[file:randltl.org][=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.

#+NAME: randaut2
#+BEGIN_SRC sh :results verbatim :exports code
randaut -Q3 -e0 2 --dot
#+END_SRC

#+RESULTS: randaut2
#+begin_example
digraph G {
  rankdir=LR
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label=<0>]
  0 -> 2 [label=<!p0 &amp; !p1>]
  1 [label=<1>]
  1 -> 1 [label=<!p0 &amp; !p1>]
  2 [label=<2>]
  2 -> 1 [label=<!p0 &amp; !p1>]
}
#+end_example

#+BEGIN_SRC dot :file randaut2.png :cmdline -Tpng :var txt=randaut2 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:randaut2.png]]

#+NAME: randaut3
#+BEGIN_SRC sh :results verbatim :exports code
randaut -Q3 -e1 2 --dot
#+END_SRC

#+RESULTS: randaut3
#+begin_example
digraph G {
  rankdir=LR
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label=<0>]
  0 -> 2 [label=<!p0 &amp; !p1>]
  0 -> 0 [label=<!p0 &amp; !p1>]
  0 -> 1 [label=<!p0 &amp; !p1>]
  1 [label=<1>]
  1 -> 1 [label=<p0 &amp; p1>]
  1 -> 2 [label=<p0 &amp; !p1>]
  1 -> 0 [label=<p0 &amp; !p1>]
  2 [label=<2>]
  2 -> 1 [label=<!p0 &amp; !p1>]
  2 -> 0 [label=<p0 &amp; !p1>]
  2 -> 2 [label=<p0 &amp; !p1>]
}
#+end_example

#+BEGIN_SRC dot :file randaut3.png :cmdline -Tpng :var txt=randaut3 :exports results
$txt
#+END_SRC

#+RESULTS:
[[file: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:
#+BEGIN_SRC sh :results verbatim :exports results
randaut --help | sed -n '/^ \(ACCEPTANCE\|RANGE\)/,/^$/p'
#+END_SRC

#+RESULTS:
#+begin_example
 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.

#+end_example

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


#+NAME: randaut4
#+BEGIN_SRC sh :results verbatim :exports code
randaut -Q3 -e0.5 -A3 -a0.5 2 --dot
#+END_SRC

#+RESULTS: randaut4
#+begin_example
digraph G {
  rankdir=LR
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
  0 -> 1 [label=<!p0 &amp; !p1>]
  0 -> 0 [label=<!p0 &amp; !p1<br/><font color="#FAA43A">❷</font>>]
  1 [label="1"]
  1 -> 1 [label=<!p0 &amp; p1<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
  1 -> 2 [label=<!p0 &amp; p1<br/><font color="#F17CB0">❶</font>>]
  2 [label="2"]
  2 -> 1 [label=<!p0 &amp; p1<br/><font color="#5DA5DA">⓿</font>>]
  2 -> 0 [label=<p0 &amp; p1<br/><font color="#5DA5DA">⓿</font>>]
  2 -> 2 [label=<!p0 &amp; p1<br/><font color="#5DA5DA">⓿</font>>]
}
#+end_example

#+BEGIN_SRC dot :file randaut4.png :cmdline -Tpng :var txt=randaut4 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:randaut4.png]]


#+NAME: randaut5
#+BEGIN_SRC sh :results verbatim :exports code
randaut -Q3 -e0.4 -B -a0.7 2 --dot
#+END_SRC

#+RESULTS: randaut5
#+begin_example
digraph G {
  rankdir=LR
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
  0 -> 1 [label=<!p0 &amp; !p1>]
  0 -> 2 [label=<!p0 &amp; !p1>]
  1 [label="1", peripheries=2]
  1 -> 1 [label=<!p0 &amp; !p1>]
  1 -> 0 [label=<p0 &amp; p1>]
  2 [label="2", peripheries=2]
  2 -> 0 [label=<p0 &amp; p1>]
  2 -> 2 [label=<p0 &amp; !p1>]
  2 -> 1 [label=<!p0 &amp; !p1>]
}
#+end_example

#+BEGIN_SRC dot :file randaut5.png :cmdline -Tpng :var txt=randaut5 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file:randaut5.png]]

#+NAME: randaut5b
#+BEGIN_SRC sh :results verbatim :exports code
randaut -Q6 -e0.4 -S -a.2 -A 'Streett 1..3' 2 --dot=.a
#+END_SRC

#+RESULTS: randaut5b
#+begin_example
digraph G {
  rankdir=LR
  label=<(Fin(<font color="#5DA5DA">⓿</font>) | Inf(<font color="#F17CB0">❶</font>)) &amp; (Fin(<font color="#FAA43A">❷</font>) | Inf(<font color="#B276B2">❸</font>))>
  labelloc="t"
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label=<0>]
  0 -> 2 [label=<!p0 &amp; !p1>]
  0 -> 1 [label=<!p0 &amp; !p1>]
  0 -> 3 [label=<!p0 &amp; !p1>]
  1 [label=<1>]
  1 -> 5 [label=<!p0 &amp; p1>]
  2 [label=<2<br/><font color="#5DA5DA">⓿</font><font color="#FAA43A">❷</font>>]
  2 -> 1 [label=<!p0 &amp; p1>]
  2 -> 2 [label=<!p0 &amp; !p1>]
  2 -> 4 [label=<p0 &amp; p1>]
  3 [label=<3>]
  3 -> 2 [label=<!p0 &amp; !p1>]
  3 -> 3 [label=<!p0 &amp; p1>]
  4 [label=<4>]
  4 -> 0 [label=<!p0 &amp; !p1>]
  4 -> 5 [label=<!p0 &amp; p1>]
  5 [label=<5<br/><font color="#F17CB0">❶</font><font color="#FAA43A">❷</font>>]
  5 -> 1 [label=<p0 &amp; p1>]
  5 -> 2 [label=<!p0 &amp; !p1>]
  5 -> 3 [label=<p0 &amp; p1>]
}
#+end_example

#+BEGIN_SRC dot :file randaut5b.png :cmdline -Tpng :var txt=randaut5b :exports results
$txt
#+END_SRC
#+RESULTS:
[[file: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.

#+NAME: randaut5c
#+BEGIN_SRC sh :results verbatim :exports code
randaut -Q10 -S --colored -A 'parity rand rand 3..4' 2 --dot=.a
#+END_SRC

#+RESULTS: randaut5c
#+begin_example
digraph G {
  rankdir=LR
  label=<Inf(<font color="#5DA5DA">⓿</font>) | (Fin(<font color="#F17CB0">❶</font>) &amp; (Inf(<font color="#FAA43A">❷</font>) | Fin(<font color="#B276B2">❸</font>)))>
  labelloc="t"
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label=<0<br/><font color="#F17CB0">❶</font>>]
  0 -> 2 [label=<!p0 &amp; !p1>]
  0 -> 8 [label=<!p0 &amp; !p1>]
  0 -> 0 [label=<p0 &amp; !p1>]
  0 -> 6 [label=<!p0 &amp; p1>]
  1 [label=<1<br/><font color="#B276B2">❸</font>>]
  1 -> 5 [label=<!p0 &amp; !p1>]
  1 -> 9 [label=<!p0 &amp; p1>]
  2 [label=<2<br/><font color="#FAA43A">❷</font>>]
  2 -> 4 [label=<p0 &amp; p1>]
  2 -> 5 [label=<!p0 &amp; !p1>]
  3 [label=<3<br/><font color="#5DA5DA">⓿</font>>]
  3 -> 6 [label=<p0 &amp; !p1>]
  3 -> 1 [label=<!p0 &amp; p1>]
  4 [label=<4<br/><font color="#5DA5DA">⓿</font>>]
  4 -> 6 [label=<!p0 &amp; !p1>]
  4 -> 1 [label=<p0 &amp; p1>]
  5 [label=<5<br/><font color="#5DA5DA">⓿</font>>]
  5 -> 0 [label=<!p0 &amp; !p1>]
  5 -> 8 [label=<p0 &amp; !p1>]
  5 -> 7 [label=<!p0 &amp; !p1>]
  6 [label=<6<br/><font color="#5DA5DA">⓿</font>>]
  6 -> 2 [label=<!p0 &amp; !p1>]
  6 -> 3 [label=<!p0 &amp; !p1>]
  7 [label=<7<br/><font color="#FAA43A">❷</font>>]
  7 -> 3 [label=<!p0 &amp; p1>]
  7 -> 1 [label=<!p0 &amp; p1>]
  8 [label=<8<br/><font color="#5DA5DA">⓿</font>>]
  8 -> 3 [label=<!p0 &amp; p1>]
  8 -> 4 [label=<p0 &amp; !p1>]
  8 -> 2 [label=<p0 &amp; !p1>]
  8 -> 0 [label=<!p0 &amp; p1>]
  9 [label=<9<br/><font color="#F17CB0">❶</font>>]
  9 -> 0 [label=<p0 &amp; p1>]
  9 -> 6 [label=<p0 &amp; !p1>]
}
#+end_example

#+BEGIN_SRC dot :file randaut5c.png :cmdline -Tpng :var txt=randaut5c :exports results
$txt
#+END_SRC
#+RESULTS:
[[file: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.

#+NAME: randaut6
#+BEGIN_SRC sh :results verbatim :exports code
randaut -D -Q3 -e0.6 -A2 -a0.5 2 --dot
#+END_SRC

#+RESULTS: randaut6
#+begin_example
digraph G {
  rankdir=LR
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
  0 -> 1 [label=<p0>]
  0 -> 2 [label=<!p0>]
  1 [label="1"]
  1 -> 2 [label=<p0<br/><font color="#F17CB0">❶</font>>]
  1 -> 0 [label=<!p0<br/><font color="#5DA5DA">⓿</font>>]
  2 [label="2"]
  2 -> 2 [label=<!p0 &amp; p1<br/><font color="#5DA5DA">⓿</font>>]
  2 -> 0 [label=<!p0 &amp; !p1<br/><font color="#F17CB0">❶</font>>]
  2 -> 1 [label=<p0<br/><font color="#5DA5DA">⓿</font>>]
}
#+end_example

#+BEGIN_SRC dot :file randaut6.png :cmdline -Tpng :var txt=randaut6 :exports results
$txt
#+END_SRC
#+RESULTS:
[[file: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 [[file:oaut.org][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.
