randaut.org 16.3 KB
Newer Older
1
# -*- coding: utf-8 -*-
2
#+TITLE: =randaut=
3
#+DESCRIPTION: Spot command-line tool for generating random ω-automata.
4
5
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
6
7
8

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

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

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

73
#+BEGIN_SRC dot :file randaut1.svg :var txt=randaut1 :exports results
74
75
76
$txt
#+END_SRC
#+RESULTS:
77
[[file:randaut1.svg]]
78
79
80
81
82
83

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

84
85
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
86
87
generate an automaton with 3 to 6 states.

88
The number of edges can be controlled using the =-e= (or
89
=--density=) option.  The argument should be a number between 0 and 1.
90
In an automaton with $Q$ states and density $e$, the degree of each
91
state will follow a normal distribution with mean $1+(Q-1)d$ and
92
variance $(Q-1)e(1-e)$.
93

94
95
In particular =-e0= will cause all states to have 1 successors, and
=-e1= will cause all states to be interconnected.
96

97
#+NAME: randaut2
98
#+BEGIN_SRC sh :results verbatim :exports code
99
randaut -Q3 -e0 2 --dot
100
101
102
103
104
#+END_SRC

#+RESULTS: randaut2
#+begin_example
digraph G {
105
  rankdir=LR
106
  node [shape="circle"]
107
108
109
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
110
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
111
112
  I [label="", style=invis, width=0]
  I -> 0
113
  0 [label=<0>]
114
  0 -> 2 [label=<!p0 &amp; !p1>]
115
  1 [label=<1>]
116
  1 -> 1 [label=<!p0 &amp; !p1>]
117
  2 [label=<2>]
118
  2 -> 1 [label=<!p0 &amp; !p1>]
119
120
121
}
#+end_example

122
#+BEGIN_SRC dot :file randaut2.svg :var txt=randaut2 :exports results
123
124
125
$txt
#+END_SRC
#+RESULTS:
126
[[file:randaut2.svg]]
127

128
#+NAME: randaut3
129
#+BEGIN_SRC sh :results verbatim :exports code
130
randaut -Q3 -e1 2 --dot
131
132
133
134
135
#+END_SRC

#+RESULTS: randaut3
#+begin_example
digraph G {
136
  rankdir=LR
137
  node [shape="circle"]
138
139
140
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
141
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
142
143
  I [label="", style=invis, width=0]
  I -> 0
144
  0 [label=<0>]
145
146
147
  0 -> 2 [label=<!p0 &amp; !p1>]
  0 -> 0 [label=<!p0 &amp; !p1>]
  0 -> 1 [label=<!p0 &amp; !p1>]
148
  1 [label=<1>]
149
150
151
  1 -> 1 [label=<p0 &amp; p1>]
  1 -> 2 [label=<p0 &amp; !p1>]
  1 -> 0 [label=<p0 &amp; !p1>]
152
  2 [label=<2>]
153
154
155
  2 -> 1 [label=<!p0 &amp; !p1>]
  2 -> 0 [label=<p0 &amp; !p1>]
  2 -> 2 [label=<p0 &amp; !p1>]
156
157
158
}
#+end_example

159
#+BEGIN_SRC dot :file randaut3.svg :var txt=randaut3 :exports results
160
161
162
163
$txt
#+END_SRC

#+RESULTS:
164
[[file:randaut3.svg]]
165

166
* Acceptance condition
167

168
The generation of the acceptance sets abn is controlled with the following four parameters:
169
170
171
172
173
174
175
176
177
178
179
180
181

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

182
 ACCEPTANCE may be either a RANGE (in which case generalized Büchi is
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
 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).
204
205
206

 - =-a= (or =--acc-probability=) controls the probability that any
   transition belong to a given acceptance set.
207
208
209
210
211
212
213
214
215
216
217
 - =-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).
218

219
In addition, =-B= (or =--ba=) is a shorthand for =-A1 -S=,
220
ans =-s= (or =--spin=) implies =-B=.
221
222
223


#+NAME: randaut4
224
#+BEGIN_SRC sh :results verbatim :exports code
225
randaut -Q3 -e0.5 -A3 -a0.5 2 --dot
226
227
228
229
230
#+END_SRC

#+RESULTS: randaut4
#+begin_example
digraph G {
231
  rankdir=LR
232
  node [shape="circle"]
233
234
235
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
236
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
237
238
239
240
241
242
  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"]
243
244
  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>>]
245
  2 [label="2"]
246
247
248
  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>>]
249
250
251
}
#+end_example

252
#+BEGIN_SRC dot :file randaut4.svg :var txt=randaut4 :exports results
253
254
255
$txt
#+END_SRC
#+RESULTS:
256
[[file:randaut4.svg]]
257
258
259


#+NAME: randaut5
260
#+BEGIN_SRC sh :results verbatim :exports code
261
randaut -Q3 -e0.4 -B -a0.7 2 --dot
262
263
264
265
266
#+END_SRC

#+RESULTS: randaut5
#+begin_example
digraph G {
267
  rankdir=LR
268
  node [shape="circle"]
269
270
271
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
272
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
273
274
275
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
276
  0 -> 1 [label=<!p0 &amp; !p1>]
277
  0 -> 2 [label=<!p0 &amp; !p1>]
278
279
280
  1 [label="1", peripheries=2]
  1 -> 1 [label=<!p0 &amp; !p1>]
  1 -> 0 [label=<p0 &amp; p1>]
281
  2 [label="2", peripheries=2]
282
283
  2 -> 0 [label=<p0 &amp; p1>]
  2 -> 2 [label=<p0 &amp; !p1>]
284
  2 -> 1 [label=<!p0 &amp; !p1>]
285
286
287
}
#+end_example

288
#+BEGIN_SRC dot :file randaut5.svg :var txt=randaut5 :exports results
289
290
291
$txt
#+END_SRC
#+RESULTS:
292
[[file:randaut5.svg]]
293

294
295
#+NAME: randaut5b
#+BEGIN_SRC sh :results verbatim :exports code
296
randaut -Q6 -e0.4 -S -a.2 -A 'Streett 1..3' 2 --dot
297
298
299
300
301
302
#+END_SRC

#+RESULTS: randaut5b
#+begin_example
digraph G {
  rankdir=LR
303
  label=<(Fin(<font color="#5DA5DA">⓿</font>) | Inf(<font color="#F17CB0">❶</font>)) &amp; (Fin(<font color="#FAA43A">❷</font>) | Inf(<font color="#B276B2">❸</font>))>
304
305
306
307
308
309
310
311
  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
312
  0 [label=<0>]
313
  0 -> 2 [label=<!p0 &amp; !p1>]
314
315
316
317
  0 -> 1 [label=<!p0 &amp; !p1>]
  0 -> 3 [label=<!p0 &amp; !p1>]
  1 [label=<1>]
  1 -> 5 [label=<!p0 &amp; p1>]
318
319
320
321
  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>]
322
  3 [label=<3>]
323
324
325
326
327
328
  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>>]
329
  5 -> 1 [label=<p0 &amp; p1>]
330
331
  5 -> 2 [label=<!p0 &amp; !p1>]
  5 -> 3 [label=<p0 &amp; p1>]
332
333
334
}
#+end_example

335
#+BEGIN_SRC dot :file randaut5b.svg :var txt=randaut5b :exports results
336
337
338
$txt
#+END_SRC
#+RESULTS:
339
[[file:randaut5b.svg]]
340

341
342
343
344
345
346
347
348
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
349
randaut -Q10 -S --colored -A 'parity rand rand 3..4' 2 --dot
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
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
#+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

403
#+BEGIN_SRC dot :file randaut5c.svg :var txt=randaut5c :exports results
404
405
406
$txt
#+END_SRC
#+RESULTS:
407
[[file:randaut5c.svg]]
408

409
410
411
412
413
414
415
416
417
418
419
420
421
422
* 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.

423
#+NAME: randaut6
424
#+BEGIN_SRC sh :results verbatim :exports code
425
randaut -D -Q3 -e0.6 -A2 -a0.5 2 --dot
426
427
428
429
430
#+END_SRC

#+RESULTS: randaut6
#+begin_example
digraph G {
431
  rankdir=LR
432
  node [shape="circle"]
433
434
435
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
436
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
437
438
439
440
441
442
443
444
445
446
447
448
  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>>]
449
450
451
}
#+end_example

452
#+BEGIN_SRC dot :file randaut6.svg :var txt=randaut6 :exports results
453
454
455
$txt
#+END_SRC
#+RESULTS:
456
[[file:randaut6.svg]]
457
458
459
460


Note that in a deterministic automaton with $a$ atomic propositions,
it is not possible to have states with more than $2^a$ successors.  If
461
the combination of =-e= and =-Q= allows the situation where a state
462
463
464
465
466
467
468
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

469
470
471
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=.
472

473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
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
following generates 20 automatas, but store them in different files
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
(its is replaced by "other" if Spot does not know better).

#+BEGIN_SRC sh :results verbatim :exports both
randaut -n20 -Q10 -A 'random 3' 2 -o 'randaut-%[s]g.hoa'
wc -l randaut-*.hoa
#+END_SRC

#+RESULTS:
:   222 randaut-Rabin-like.hoa
:   380 randaut-Streett-like.hoa
:   100 randaut-generalized-Buchi.hoa
:   249 randaut-other.hoa
:   951 total

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

497
498
499
500
* 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
501
502
generation of multiple automata is useful when piped to another tool
that can process automata in batches.
503
504
505
506
507
508
509
510
511
512
513

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
514
515
options discussed [[file:oaut.org::#default-dot][on another page]], while '=s=' causes SCCs to be
displayed.)
516
517
518
519
520

#+NAME: randaut7
#+BEGIN_SRC sh :results verbatim :exports code
randaut -n -1 --colored -A'parity min odd 4' a b |
autfilt --sccs=5 --trivial-sccs=1 --rejecting-sccs=1 \
521
        --inherently-weak-sccs=2 --weak-sccs=1 -n 1 --dot=.s
522
523
#+END_SRC

524
#+BEGIN_SRC dot :file randaut7.svg :var txt=randaut7 :exports results
525
526
527
528
$txt
#+END_SRC

#+RESULTS:
529
[[file:randaut7.svg]]
530
531
532

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.