randaut.org 13.5 KB
Newer Older
1
# -*- coding: utf-8 -*-
2
#+TITLE: =randaut=
3
4
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
5
6
7

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

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

12
#+NAME: randaut1
13
14
15
16
17
18
#+BEGIN_SRC sh :results verbatim :exports code
randaut a b
#+END_SRC
#+RESULTS: randaut1
#+begin_example
digraph G {
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
  rankdir=LR
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
  0 -> 8 [label=<!a &amp; !b>]
  0 -> 4 [label=<!a &amp; !b>]
  1 [label="1"]
  1 -> 2 [label=<a &amp; !b>]
  1 -> 7 [label=<!a &amp; !b>]
  1 -> 4 [label=<!a &amp; b>]
  2 [label="2"]
  2 -> 2 [label=<!a &amp; !b>]
  2 -> 0 [label=<a &amp; !b>]
  2 -> 5 [label=<a &amp; !b>]
  3 [label="3"]
  3 -> 6 [label=<!a &amp; b>]
  4 [label="4"]
  4 -> 8 [label=<a &amp; !b>]
  4 -> 2 [label=<!a &amp; b>]
  4 -> 3 [label=<a &amp; b>]
  4 -> 7 [label=<!a &amp; b>]
  5 [label="5"]
  5 -> 9 [label=<!a &amp; !b>]
  5 -> 3 [label=<a &amp; !b>]
  5 -> 7 [label=<!a &amp; !b>]
  6 [label="6"]
  6 -> 7 [label=<!a &amp; !b>]
  6 -> 1 [label=<!a &amp; b>]
  7 [label="7"]
  7 -> 3 [label=<!a &amp; !b>]
  8 [label="8"]
  8 -> 8 [label=<!a &amp; b>]
  9 [label="9"]
  9 -> 0 [label=<!a &amp; b>]
  9 -> 6 [label=<!a &amp; b>]
58
59
60
61
62
63
64
65
66
67
68
69
70
71
}
#+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

72
73
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
74
75
76
77
generate an automaton with 3 to 6 states.

The number of edges can be controlled using the =-d= (or
=--density=) option.  The argument should be a number between 0 and 1.
78
79
80
In an automaton with $Q$ states and density $d$, the degree of each
state will follow a normal distribution with mean $1+(Q-1)d$ and
variance $(Q-1)d(1-d)$.
81
82
83
84

In particular =-d0= will cause all states to have 1 successors, and
=-d1= will cause all states to be interconnected.

85
#+NAME: randaut2
86
#+BEGIN_SRC sh :results verbatim :exports code
87
randaut -Q3 -d0 2
88
89
90
91
92
#+END_SRC

#+RESULTS: randaut2
#+begin_example
digraph G {
93
94
95
96
97
98
99
100
101
102
103
104
105
  rankdir=LR
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"]
  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>]
106
107
108
109
110
111
112
113
114
}
#+end_example

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

115
#+NAME: randaut3
116
#+BEGIN_SRC sh :results verbatim :exports code
117
randaut -Q3 -d1 2
118
119
120
121
122
#+END_SRC

#+RESULTS: randaut3
#+begin_example
digraph G {
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
  rankdir=LR
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"]
  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>]
142
143
144
145
146
147
148
149
150
151
152
}
#+end_example

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

#+RESULTS:
[[file:randaut3.png]]


153
* Acceptance condition
154

155
The generation of the acceptance sets abn is controlled with the following four parameters:
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190

 - =-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).
191
192
193

 - =-a= (or =--acc-probability=) controls the probability that any
   transition belong to a given acceptance set.
194
195
196
197
198
199
200
201
202
203
204
 - =-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).
205

206
In addition, =-B= (or =--ba=) is a shorthand for =-A1 -S=,
207
ans =-s= (or =--spin=) implies =-B=.
208
209
210


#+NAME: randaut4
211
#+BEGIN_SRC sh :results verbatim :exports code
212
randaut -Q3 -d0.5 -A3 -a0.5 2
213
214
215
216
217
#+END_SRC

#+RESULTS: randaut4
#+begin_example
digraph G {
218
219
220
221
222
223
224
225
226
227
228
229
  rankdir=LR
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"]
  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 -> 2 [label=<!p0 &amp; p1<br/><font color="#F17CB0">❶</font><font color="#FAA43A">❷</font>>]
230
  2 [label="2"]
231
232
  2 -> 2 [label=<!p0 &amp; !p1<br/><font color="#5DA5DA">⓿</font>>]
  2 -> 1 [label=<p0 &amp; !p1<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
233
234
235
236
237
238
239
240
241
242
243
}
#+end_example

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


#+NAME: randaut5
244
#+BEGIN_SRC sh :results verbatim :exports code
245
randaut -Q3 -d0.4 -B -a0.7 2
246
247
248
249
250
#+END_SRC

#+RESULTS: randaut5
#+begin_example
digraph G {
251
252
253
254
255
256
257
258
259
260
261
  rankdir=LR
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"]
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
  0 -> 2 [label=<!p0 &amp; !p1>]
  1 [label="1"]
  1 -> 2 [label=<!p0 &amp; p1>]
262
  2 [label="2", peripheries=2]
263
264
  2 -> 1 [label=<!p0 &amp; !p1>]
  2 -> 0 [label=<p0 &amp; !p1>]
265
266
267
268
269
270
271
272
273
}
#+end_example

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

274
275
#+NAME: randaut5b
#+BEGIN_SRC sh :results verbatim :exports code
276
randaut -Q6 -d0.4 -S -a.2 -A 'Streett 1..3' 2 --dot=.a
277
278
279
280
281
282
#+END_SRC

#+RESULTS: randaut5b
#+begin_example
digraph G {
  rankdir=LR
283
  label=<(Fin(<font color="#5DA5DA">⓿</font>) | Inf(<font color="#F17CB0">❶</font>)) &amp; (Fin(<font color="#FAA43A">❷</font>) | Inf(<font color="#B276B2">❸</font>))>
284
285
286
287
288
289
290
291
  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
292
  0 [label=<0>]
293
  0 -> 2 [label=<!p0 &amp; !p1>]
294
295
296
297
  0 -> 1 [label=<!p0 &amp; !p1>]
  0 -> 3 [label=<!p0 &amp; !p1>]
  1 [label=<1>]
  1 -> 5 [label=<!p0 &amp; p1>]
298
299
300
301
  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>]
302
  3 [label=<3>]
303
304
305
306
307
308
  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>>]
309
  5 -> 1 [label=<p0 &amp; p1>]
310
311
  5 -> 2 [label=<!p0 &amp; !p1>]
  5 -> 3 [label=<p0 &amp; p1>]
312
313
314
315
316
317
318
319
320
}
#+end_example

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

321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
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]]
388

389
390
391
392
393
394
395
396
397
398
399
400
401
402
* 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.

403
#+NAME: randaut6
404
#+BEGIN_SRC sh :results verbatim :exports code
405
randaut -D -Q3 -d0.6 -A2 -a0.5 2
406
407
408
409
410
#+END_SRC

#+RESULTS: randaut6
#+begin_example
digraph G {
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
  rankdir=LR
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"]
  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>>]
428
429
430
431
432
433
434
435
436
437
438
439
}
#+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
440
the combination of =-d= and =-Q= allows the situation where a state
441
442
443
444
445
446
447
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

448
449
450
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=.
451
452
453
454
455
456
457
458

* 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 probably useful only with =--hoaf=,
when piped to another tool that can read this format and process
automata in batches.