randaut.org 9.03 KB
Newer Older
1
# -*- coding: utf-8 -*-
2
#+TITLE: =randaut=
3
#+DESCRIPTION: Spot command-line tool for generating random ω-automata.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4
#+INCLUDE: setup.org
5
#+HTML_LINK_UP: tools.html
6
#+PROPERTY: header-args:sh :results verbatim :exports code
7
8
9

The =randaut= tool generates random (connected) automata.

10
11
By default, it will generate a random automaton with 10 states, no
acceptance sets, and using a set of atomic propositions you have to
12
13
supply.

14
#+NAME: randaut1
15
#+BEGIN_SRC sh
16
randaut a b --dot
17
18
#+END_SRC

19
#+BEGIN_SRC dot :file randaut1.svg :var txt=randaut1 :exports results
20
21
22
$txt
#+END_SRC
#+RESULTS:
23
[[file:randaut1.svg]]
24
25
26
27
28
29

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

30
31
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
32
33
generate an automaton with 3 to 6 states.

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

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

43
#+NAME: randaut2
44
#+BEGIN_SRC sh
45
randaut -Q3 -e0 2 --dot
46
47
#+END_SRC

48
#+BEGIN_SRC dot :file randaut2.svg :var txt=randaut2 :exports results
49
50
51
$txt
#+END_SRC
#+RESULTS:
52
[[file:randaut2.svg]]
53

54
#+NAME: randaut3
55
#+BEGIN_SRC sh
56
randaut -Q3 -e1 2 --dot
57
58
#+END_SRC

59
#+BEGIN_SRC dot :file randaut3.svg :var txt=randaut3 :exports results
60
61
62
63
$txt
#+END_SRC

#+RESULTS:
64
[[file:randaut3.svg]]
65

66
* Acceptance condition
67

68
69
The generation of the acceptance condition and acceptance sets is
controlled with the following four parameters:
70

71
72
73
 - =-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:
74
#+BEGIN_SRC sh :exports results
75
76
77
78
79
80
81
82
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.

83
 ACCEPTANCE may be either a RANGE (in which case generalized Büchi is
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
 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

103
 When a range of the form $i..j$ is used, the actual value is taken randomly
104
 between $i$ and $j$ (included).
105
106
107

 - =-a= (or =--acc-probability=) controls the probability that any
   transition belong to a given acceptance set.
108
109
110
111
112
113
114
115
116
117
118
 - =-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).
119

120
In addition, =-B= (or =--ba=) is a shorthand for =-A1 -S=,
121
ans =-s= (or =--spin=) implies =-B=.
122
123
124


#+NAME: randaut4
125
#+BEGIN_SRC sh
126
randaut -Q3 -e0.5 -A3 -a0.5 2 --dot
127
128
#+END_SRC

129
#+BEGIN_SRC dot :file randaut4.svg :var txt=randaut4 :exports results
130
131
132
$txt
#+END_SRC
#+RESULTS:
133
[[file:randaut4.svg]]
134
135
136


#+NAME: randaut5
137
#+BEGIN_SRC sh
138
randaut -Q3 -e0.4 -B -a0.7 2 --dot
139
140
#+END_SRC

141
#+BEGIN_SRC dot :file randaut5.svg :var txt=randaut5 :exports results
142
143
144
$txt
#+END_SRC
#+RESULTS:
145
[[file:randaut5.svg]]
146

147
#+NAME: randaut5b
148
#+BEGIN_SRC sh
149
randaut -Q6 -e0.4 -S -a.2 -A 'Streett 1..3' 2 --dot
150
151
#+END_SRC

152
#+BEGIN_SRC dot :file randaut5b.svg :var txt=randaut5b :exports results
153
154
155
$txt
#+END_SRC
#+RESULTS:
156
[[file:randaut5b.svg]]
157

158
159
160
161
162
163
164
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
165
#+BEGIN_SRC sh
166
randaut -Q10 -S --colored -A 'parity rand rand 3..4' 2 --dot
167
168
#+END_SRC

169
#+BEGIN_SRC dot :file randaut5c.svg :var txt=randaut5c :exports results
170
171
172
$txt
#+END_SRC
#+RESULTS:
173
[[file:randaut5c.svg]]
174

175
176
177
178
179
180
181
182
183
184
185
186
187
188
* 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.

189
#+NAME: randaut6
190
#+BEGIN_SRC sh
191
randaut -D -Q3 -e0.6 -A2 -a0.5 2 --dot
192
193
#+END_SRC

194
#+BEGIN_SRC dot :file randaut6.svg :var txt=randaut6 :exports results
195
196
197
$txt
#+END_SRC
#+RESULTS:
198
[[file:randaut6.svg]]
199
200
201
202


Note that in a deterministic automaton with $a$ atomic propositions,
it is not possible to have states with more than $2^a$ successors.  If
203
the combination of =-e= and =-Q= allows the situation where a state
204
205
206
207
208
209
210
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

211
212
213
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=.
214

215
216
Automata are send to standard output by default, by you can use =-o=
to give a filename, or even a pattern for filenames.  For instance the
217
following generates 20 automata, but store them in different files
218
219
220
according to the acceptance condition.  The format =%g= represent the
formula for the acceptance condition and would not make a nice
filename, but =%[s]g= is a short name for that acceptance condition
221
222
223
(its is replaced by "other" if Spot does not know better).  We use
=-Hl= to output one automaton per line, so that =wc -l= will count
automata.
224

225
226
#+BEGIN_SRC sh :exports both
randaut -n20 -Q10 -A 'random 3' 2 -Hl -o 'randaut-%[s]g.hoa'
227
228
229
230
wc -l randaut-*.hoa
#+END_SRC

#+RESULTS:
231
232
233
234
235
236
237
238
:     1 randaut-Fin-less.hoa
:     4 randaut-Rabin-like.hoa
:     7 randaut-Streett-like.hoa
:     2 randaut-generalized-Buchi.hoa
:     1 randaut-generalized-Rabin.hoa
:     1 randaut-generalized-Streett.hoa
:     4 randaut-other.hoa
:    20 total
239
240
241
242
243

#+BEGIN_SRC sh :results silent :exports results
rm -f rautaut-*.hoa
#+END_SRC

244
245
246
247
* 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
248
249
generation of multiple automata is useful when piped to another tool
that can process automata in batches.
250
251
252
253
254
255
256
257
258
259
260

Here is an example were we use [[file:autfilt.org][=autfilt=]] to scan an infinite stream
(=-n -1=) of random parity automata for the first automaton (=-n 1=)
that have exactly 5 SCCs of particular natures: we want 1 trivial SCC
(i.e. an SCC with no cycle), 1 rejecting SCC (an SCC without any
accepting SCCs), 2 inherently weak SCCs (SCCs contains only rejecting
cycles) among which one should be weak (all transitions should belong
to the same sets).  This leaves us with one extra SCC that should
necessarily mix accepting and rejecting cycles.

(Note: the '=.=' argument passed to =--dot= below hides default
261
262
options discussed [[file:oaut.org::#default-dot][on another page]], while '=s=' causes SCCs to be
displayed.)
263
264

#+NAME: randaut7
265
#+BEGIN_SRC sh
266
267
randaut -n -1 --colored -A'parity min odd 4' a b |
autfilt --sccs=5 --trivial-sccs=1 --rejecting-sccs=1 \
268
        --inherently-weak-sccs=2 --weak-sccs=1 -n 1 --dot=.s
269
270
#+END_SRC

271
#+BEGIN_SRC dot :file randaut7.svg :var txt=randaut7 :exports results
272
273
274
275
$txt
#+END_SRC

#+RESULTS:
276
[[file:randaut7.svg]]
277
278
279

You should be able to find each of the expected type of SCCs in the above picture.
The green rectangles mark the three SCCs that contain some accepting cycles.
280
281
282
283

#  LocalWords:  utf randaut html args SRC svg txt randltl sed Buchi
#  LocalWords:  acc ba rankdir hoaf lbtt Hl wc rautaut SCCs SCC sccs
#  LocalWords:  A'parity