# -*- coding: utf-8 -*- #+TITLE: =randaut= #+DESCRIPTION: Spot command-line tool for generating random ω-automata. #+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=] 0 -> 3 [label=] 0 -> 4 [label=] 1 [label=<1>] 1 -> 7 [label=] 1 -> 0 [label=] 1 -> 6 [label=] 2 [label=<2>] 2 -> 4 [label=] 2 -> 0 [label=] 2 -> 5 [label=] 2 -> 9 [label=] 3 [label=<3>] 3 -> 2 [label=] 3 -> 9 [label=] 3 -> 3 [label=] 4 [label=<4>] 4 -> 0 [label=] 4 -> 7 [label=] 5 [label=<5>] 5 -> 3 [label=] 5 -> 1 [label=] 5 -> 7 [label=] 5 -> 9 [label=] 5 -> 5 [label=] 6 [label=<6>] 6 -> 8 [label=] 6 -> 5 [label=] 6 -> 2 [label=] 7 [label=<7>] 7 -> 8 [label=] 7 -> 9 [label=] 7 -> 0 [label=] 7 -> 1 [label=] 7 -> 4 [label=] 8 [label=<8>] 8 -> 1 [label=] 8 -> 3 [label=] 9 [label=<9>] 9 -> 1 [label=] 9 -> 3 [label=] } #+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=] 1 [label=<1>] 1 -> 1 [label=] 2 [label=<2>] 2 -> 1 [label=] } #+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=] 0 -> 0 [label=] 0 -> 1 [label=] 1 [label=<1>] 1 -> 1 [label=] 1 -> 2 [label=] 1 -> 0 [label=] 2 [label=<2>] 2 -> 1 [label=] 2 -> 0 [label=] 2 -> 2 [label=] } #+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=] 0 -> 0 [label=❷>] 1 [label="1"] 1 -> 1 [label=⓿❶>] 1 -> 2 [label=❶>] 2 [label="2"] 2 -> 1 [label=⓿>] 2 -> 0 [label=⓿>] 2 -> 2 [label=⓿>] } #+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=] 0 -> 2 [label=] 1 [label="1", peripheries=2] 1 -> 1 [label=] 1 -> 0 [label=] 2 [label="2", peripheries=2] 2 -> 0 [label=] 2 -> 2 [label=] 2 -> 1 [label=] } #+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(⓿) | Inf(❶)) & (Fin(❷) | Inf(❸))> 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=] 0 -> 1 [label=] 0 -> 3 [label=] 1 [label=<1>] 1 -> 5 [label=] 2 [label=<2
⓿❷>] 2 -> 1 [label=] 2 -> 2 [label=] 2 -> 4 [label=] 3 [label=<3>] 3 -> 2 [label=] 3 -> 3 [label=] 4 [label=<4>] 4 -> 0 [label=] 4 -> 5 [label=] 5 [label=<5
❶❷>] 5 -> 1 [label=] 5 -> 2 [label=] 5 -> 3 [label=] } #+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=⓿) | (Fin(❶) & (Inf(❷) | Fin(❸)))> 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=] 0 -> 8 [label=] 0 -> 0 [label=] 0 -> 6 [label=] 1 [label=<1
❸>] 1 -> 5 [label=] 1 -> 9 [label=] 2 [label=<2
❷>] 2 -> 4 [label=] 2 -> 5 [label=] 3 [label=<3
⓿>] 3 -> 6 [label=] 3 -> 1 [label=] 4 [label=<4
⓿>] 4 -> 6 [label=] 4 -> 1 [label=] 5 [label=<5
⓿>] 5 -> 0 [label=] 5 -> 8 [label=] 5 -> 7 [label=] 6 [label=<6
⓿>] 6 -> 2 [label=] 6 -> 3 [label=] 7 [label=<7
❷>] 7 -> 3 [label=] 7 -> 1 [label=] 8 [label=<8
⓿>] 8 -> 3 [label=] 8 -> 4 [label=] 8 -> 2 [label=] 8 -> 0 [label=] 9 [label=<9
❶>] 9 -> 0 [label=] 9 -> 6 [label=] } #+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=] 0 -> 2 [label=] 1 [label="1"] 1 -> 2 [label=❶>] 1 -> 0 [label=⓿>] 2 [label="2"] 2 -> 2 [label=⓿>] 2 -> 0 [label=❶>] 2 -> 1 [label=⓿>] } #+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.