oaut.org 30.2 KB
Newer Older
1
# -*- coding: utf-8 -*-
2
#+TITLE: Common output options for automata
3
4
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

Spot supports different output syntaxes for automata.  This page
documents the options, common to all tools where it makes sense, that
are used to specify how to output of automata.

* Common output options

All tools that can output automata implement the following options:

#+BEGIN_SRC sh :results verbatim :exports results
ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
#+begin_example
  -8, --utf8                 enable UTF-8 characters in output (ignored with
                             --lbtt or --spin)
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
      --dot[=a|b|c|f(FONT)|h|n|N|r|R|s|t|v]
                             GraphViz's format (default).  Add letters for (a)
                             acceptance display, (b) acceptance sets as
                             bullets,(c) circular nodes, (f(FONT)) use FONT,
                             (h) horizontal layout, (v) vertical layout, (n)
                             with name, (N) without name, (r) rainbow colors
                             for acceptance set, (R) color acceptance set by
                             Inf/Fin, (s) with SCCs, (t) force transition-based
                             acceptance.
  -H, --hoaf[=i|s|t|m|l]     Output the automaton in HOA format.  Add letters
                             to select (i) use implicit labels for complete
                             deterministic automata, (s) prefer state-based
                             acceptance when possible [default], (t) force
                             transition-based acceptance, (m) mix state and
                             transition-based acceptance, (l) single-line
                             output
37
      --lbtt[=t]             LBTT's format (add =t to force transition-based
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
38
                             acceptance even on Büchi automata)
39
      --name=FORMAT          set the name of the output automaton
40
41
42
  -o, --output=FORMAT        send output to a file named FORMAT instead of
                             standard output.  The first automaton sent to a
                             file truncates it unless FORMAT starts with '>>'.
43
  -q, --quiet                suppress all normal output
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
44
45
46
  -s, --spin[=6|c]           Spin neverclaim (implies --ba).  Add letters to
                             select (6) Spin's 6.2.4 style, (c) comments on
                             states
47
48
49
50
51
      --stats=FORMAT         output statistics about the automaton
#+end_example

The main three output formats (that can also been used as input to
some of the tools) are [[http://adl.github.io/hoaf/][HOAF]] (activated by =-H= or =--hoaf=), [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]]
52
(activated by =--lbtt=), or Spin [[http://spinroot.com/spin/Man/never.html][never claims]] (activated by =-s= or
53
54
55
56
57
=--spin=).  These three formats also support *streaming*, i.e., you
can concatenate multiple automata (and even mix these three formats in
the same stream), and the tools will be able to read and process them
in sequence.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
58
59
60
The other possible outputs are [[http://www.graphviz.org/][GraphViz]] output (=--dot=), various
statistics (=--stats=), or nothing at all (=--quiet=).  It may seem
strange to ask a tool to not output anything, but it makes sense when
61
only the exit status matters (for instance using [[file:autfilt.org][=autfilt=]] to check
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
62
whether an input automaton has some property) or for timing purposes.
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80

* HOAF output

The [[http://adl.github.io/hoaf/][HOAF]] output should be the preferred format to use if you want to
pass automata between different tools.  This format can be requested
using the =-H= option.

Here is an example where [[file:ltl2tgba.org][=ltl2tgba=]] is used to construct two automata:
one for =a U b= and one for =(Ga -> Gb) W c=.

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -H 'a U b' '(Ga -> Gb) W c'
#+END_SRC
#+RESULTS:
#+begin_example
HOA: v1
name: "a U b"
States: 2
81
Start: 1
82
83
84
85
86
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
87
88
89
90
91
State: 0 {0}
[t] 0
State: 1
[1] 0
[0&!1] 1
92
93
94
95
--END--
HOA: v1
name: "(Gb | F!a) W c"
States: 5
96
Start: 1
97
98
99
100
101
102
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
103
104
105
106
[0] 0 {0}
State: 1
[0&1&!2] 0
[!1&!2] 1 {0}
107
108
109
[1&!2] 2
[2] 3
State: 2
110
[!1&!2] 1 {0}
111
112
113
114
115
116
117
118
119
120
121
[1&!2] 2
[!1&2] 3
[1&2] 4
State: 3
[t] 3 {0}
State: 4
[!1] 3
[1] 4
--END--
#+end_example

122
The above output contains two automata, named after the formulas they
123
124
125
126
represent.  Here is a picture of these two automata:

#+NAME: hoafex
#+BEGIN_SRC sh :results verbatim :exports none
127
ltl2tgba --dot=.cn '(Ga -> Gb) W c' 'a U b' | dot | gvpack |
128
129
130
131
132
perl -pe 's/\\\n//g;s/\\/\\\\/g;s/graph G/graph cluster/g'
#+END_SRC
#+RESULTS: hoafex
#+begin_example
digraph root {
133
134
	graph [bb="0,0,427,231.07",
		fontname=Lato,
135
136
137
138
		labelloc=t,
		lheight=0.21,
		rankdir=LR
	];
139
140
141
142
143
	node [fillcolor="#ffffa0",
		fontname=Lato,
		label="\\N",
		shape=circle,
		style=filled
144
	];
145
	edge [fontname=Lato];
146
147
	subgraph cluster {
		graph [bb="",
148
149
			fontname=Lato,
			label=<(Gb | F!a) W c>,
150
151
			labelloc=t,
			lheight=0.21,
152
153
			lp="197.5,196.66",
			lwidth=1.19,
154
155
			rankdir=LR
		];
156
157
158
		node [fillcolor="#ffffa0",
			fontname=Lato,
			height="",
159
160
161
			label="\\N",
			pos="",
			shape=circle,
162
			style=filled,
163
164
			width=""
		];
165
166
		edge [fontname=Lato,
			label="",
167
168
169
170
171
			lp="",
			pos=""
		];
		I		 [height=0.013889,
			label="",
172
			pos="1,49.168",
173
174
175
176
			style=invis,
			width=0.013889];
		1		 [height=0.5,
			label=1,
177
			pos="56,49.168",
178
179
			width=0.5];
		I -> 1		 [pos="e,37.942,49.324 1.1549,49.324 2.6725,49.324 15.097,49.324 27.628,49.324"];
180
		1 -> 1		 [label=<!a &amp; !c<br/><font color="#5DA5DA">⓿</font>>,
181
			lp="56,100.32",
182
			pos="e,62.379,66.362 49.621,66.362 48.319,76.182 50.445,85.324 56,85.324 59.472,85.324 61.604,81.753 62.398,76.677"];
183
184
		0		 [height=0.5,
			label=0,
185
			pos="190,121.17",
186
			width=0.5];
187
188
189
		1 -> 0		 [label=<a &amp; b &amp; !c>,
			lp="123,113.83",
			pos="e,172.99,115.19 70.127,60.572 76.491,65.727 84.391,71.704 92,76.324 115.21,90.42 143.57,103.1 163.61,111.38"];
190
191
		2		 [height=0.5,
			label=2,
192
			pos="190,34.168",
193
			width=0.5];
194
195
196
		1 -> 2		 [label=<a &amp; !c>,
			lp="123,64.824",
			pos="e,175.09,44.492 73.8,53.268 93.402,57.17 126.62,61.596 154,54.324 158.19,53.213 162.39,51.47 166.37,49.467"];
197
198
		3		 [height=0.5,
			label=3,
199
			pos="377,34.168",
200
			width=0.5];
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
		1 -> 3		 [label=<c>,
			lp="242,9.8246",
			pos="e,361.03,25.984 66.027,34.327 72.161,25.632 81.127,15.423 92,10.325 114.02,0 277.48,0.3418 312,7.3246 325.76,10.108 340.24,15.943 351.94,21.478"];
		0 -> 0		 [label=<b<br/><font color="#5DA5DA">⓿</font>>,
			lp="190,172.33",
			pos="e,198.98,137.24 181.02,137.24 178.68,147.48 181.67,157.33 190,157.33 195.47,157.33 198.63,153.08 199.5,147.28"];
		2 -> 1		 [label=<!a &amp; !c<br/><font color="#5DA5DA">⓿</font>>,
			lp="123,35.324",
			pos="e,68.596,36.186 173.36,26.591 167.44,24.066 160.55,21.587 154,20.324 126.94,15.113 117.92,10.98 92,20.324 86.432,22.331 81.123,25.651 76.398,29.343"];
		2 -> 2		 [label=<a &amp; !c>,
			lp="190,77.824",
			pos="e,198.98,50.24 181.02,50.24 178.68,60.475 181.67,70.324 190,70.324 195.47,70.324 198.63,66.083 199.5,60.274"];
		2 -> 3		 [label=<!a &amp; c>,
			lp="294,105.83",
			pos="e,365.94,48.712 203.15,46.686 218.52,61.348 246.56,84.98 276,94.324 291.25,99.165 297.12,100.21 312,94.324 331.12,86.764 347.87,70.495 359.43,56.803"];
216
217
		4		 [height=0.5,
			label=4,
218
			pos="294,34.168",
219
			width=0.5];
220
221
222
223
224
225
226
227
228
229
230
231
		2 -> 4		 [label=<a &amp; c>,
			lp="242,41.824",
			pos="e,275.95,34.324 208.3,34.324 224.08,34.324 247.64,34.324 265.91,34.324"];
		3 -> 3		 [label=<1<br/><font color="#5DA5DA">⓿</font>>,
			lp="377,85.324",
			pos="e,384.03,50.989 369.97,50.989 368.41,60.949 370.75,70.324 377,70.324 381,70.324 383.4,66.477 384.2,61.093"];
		4 -> 3		 [label=<!a>,
			lp="335.5,41.824",
			pos="e,358.85,34.324 312.18,34.324 322.81,34.324 336.69,34.324 348.8,34.324"];
		4 -> 4		 [label=<a>,
			lp="294,77.824",
			pos="e,301.03,50.989 286.97,50.989 285.41,60.949 287.75,70.324 294,70.324 298,70.324 300.4,66.477 301.2,61.093"];
232
233
234
	}
	subgraph cluster_gv1 {
		graph [bb="",
235
236
			fontname=Lato,
			label=<a U b>,
237
238
			labelloc=t,
			lheight=0.21,
239
240
			lp="81.5,88.5",
			lwidth=0.47,
241
242
			rankdir=LR
		];
243
244
245
		node [fillcolor="#ffffa0",
			fontname=Lato,
			height="",
246
247
248
249
			label="\\N",
			peripheries="",
			pos="",
			shape=circle,
250
			style=filled,
251
252
			width=""
		];
253
254
		edge [fontname=Lato,
			label="",
255
256
257
258
259
			lp="",
			pos=""
		];
		I_gv1		 [height=0.013889,
			label="",
260
			pos="261,156.17",
261
262
263
264
			style=invis,
			width=0.013889];
		"1_gv1"		 [height=0.5,
			label=1,
265
			pos="316,156.17",
266
			width=0.5];
267
268
269
270
		I_gv1 -> "1_gv1"		 [pos="e,297.94,156.17 261.15,156.17 262.67,156.17 275.1,156.17 287.63,156.17"];
		"1_gv1" -> "1_gv1"		 [label=<a &amp; !b>,
			lp="316,199.67",
			pos="e,322.38,173.21 309.62,173.21 308.32,183.03 310.44,192.17 316,192.17 319.47,192.17 321.6,188.6 322.4,183.52"];
271
272
273
		"0_gv1"		 [height=0.72222,
			label=0,
			peripheries=2,
274
			pos="401,156.17",
275
			width=0.72222];
276
277
278
		"1_gv1" -> "0_gv1"		 [label=<b>,
			lp="356.5,163.67",
			pos="e,379,156.17 334.2,156.17 344.16,156.17 357,156.17 368.7,156.17"];
279
		"0_gv1" -> "0_gv1"		 [label=1,
280
281
			lp="401,203.67",
			pos="e,409.01,176.75 392.99,176.75 391.89,187.01 394.55,196.17 401,196.17 405.13,196.17 407.71,192.41 408.74,187.01"];
282
283
284
285
286
287
288
289
290
291
292
	}
}
#+end_example

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

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
293
The [[http://adl.github.io/hoaf/][HOA format]] supports both state and transition-based acceptance.
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
Although Spot works only with transition-based acceptance, its output
routines default to state-based acceptance whenever possible (this is
the case in the first of these two automata) and use transition-based
acceptance otherwise.  You can change this behavior using =-Hs= (or
=--hoaf=s=), =-Ht=, or =-Hm=.  Option =s= corresponds to the default
to use state-based acceptance whenever possible.  Option =t= forces
transition-based acceptance.  For instance compare this output to the
previous one:

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -Ht 'a U b'
#+END_SRC
#+RESULTS:
#+begin_example
HOA: v1
name: "a U b"
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[1] 1
[0&!1] 0
State: 1
[t] 1 {0}
--END--
#+end_example

Option =m= uses mixed acceptance, i.e, some states might use
state-based acceptance while other will not:

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -Hm '(Ga -> Gb) W c'
#+END_SRC
#+RESULTS:
#+begin_example
HOA: v1
name: "(Gb | F!a) W c"
States: 5
336
Start: 1
337
338
339
340
341
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels
--BODY--
342
343
344
345
346
State: 0 {0}
[0] 0
State: 1
[0&1&!2] 0
[!1&!2] 1 {0}
347
348
349
[1&!2] 2
[2] 3
State: 2
350
[!1&!2] 1 {0}
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
[1&!2] 2
[!1&2] 3
[1&2] 4
State: 3 {0}
[t] 3
State: 4
[!1] 3
[1] 4
--END--
#+end_example


It is also possible to output each automaton on a single line, in case
the result should be used with line-based tools or embedded into a CSV
file...  Here is an example using both transition-based acceptance,
and single-line output:

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -Htl 'a U b' '(Ga -> Gb) W c'
#+END_SRC
#+RESULTS:
372
373
: HOA: v1 name: "a U b" States: 2 Start: 1 AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0 [t] 0 {0} State: 1 [1] 0 [0&!1] 1 --END--
: HOA: v1 name: "(Gb | F!a) W c" States: 5 Start: 1 AP: 3 "b" "a" "c" acc-name: Buchi Acceptance: 1 Inf(0) properties: trans-labels explicit-labels trans-acc --BODY-- State: 0 [0] 0 {0} State: 1 [0&1&!2] 0 [!1&!2] 1 {0} [1&!2] 2 [2] 3 State: 2 [!1&!2] 1 {0} [1&!2] 2 [!1&2] 3 [1&2] 4 State: 3 [t] 3 {0} State: 4 [!1] 3 [1] 4 --END--
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
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440

* LBTT output

The [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]] output has two flavors: state-based (which is used to output
Büchi automata or monitors) or transition-based (for TGBA).

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba --ba --lbtt 'p0 U p1'
#+END_SRC
#+RESULTS:
: 2 1
: 0 1 -1
: 1 p1
: 0 & p0 ! p1
: -1
: 1 0 0 -1
: 1 t
: -1

If you want to request transition-based output even for Büchi automata,
use =--lbtt=t=.

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba --ba --lbtt=t 'p0 U p1'
#+END_SRC

#+RESULTS:
: 2 1t
: 0 1
: 1 -1 p1
: 0 -1 & p0 ! p1
: -1
: 1 0
: 1 0 -1 t
: -1

Note that the [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]] output generalizes the format output by [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][LBT]] with
support for transition-based acceptance.  Both formats however are
restricted to atomic propositions of the form =p0=, =p1=, etc...  In
case other atomic propositions are used, Spot output them in double
quotes.  This other extension of the format is also supported by
[[http://www.ltl2dstar.de/][ltl2dstar]].

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba --ba --lbtt 'a U b'
#+END_SRC

#+RESULTS:
: 2 1
: 0 1 -1
: 1 "b"
: 0 & "a" ! "b"
: -1
: 1 0 0 -1
: 1 t
: -1

* Spin output

Spin [[http://spinroot.com/spin/Man/never.html][never claims]] can be requested using =-s= or =--spin=.  They can only
represent Büchi automata, so these options imply =--ba=.

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -s 'a U b'
#+END_SRC

#+RESULTS:
441
: never { /* a U b */
442
443
444
445
446
447
448
449
450
: T0_init:
:   if
:   :: ((b)) -> goto accept_all
:   :: ((a) && (!(b))) -> goto T0_init
:   fi;
: accept_all:
:   skip
: }

451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
Recent versions of Spin (starting with Spin 6.2.4) output never claims
in a slightly different style that can be requested using either
=-s6= or =--spin=6=:

#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba -s6 'a U b'
#+END_SRC

#+RESULTS:
: never { /* a U b */
: T0_init:
:   do
:   :: atomic { ((b)) -> assert(!((b))) }
:   :: ((a) && (!(b))) -> goto T0_init
:   od;
: accept_all:
:   skip
: }

(Note that while Spot is able to read never claims that follow any of
these two styles, it is not capable of interpreting an arbitrary piece
of Promela syntax.)

474
475
476
477
478
* Dot output

The =--dot= option (which usually is the default) causes automata to be
output in GraphViz's format.

479
#+BEGIN_SRC sh :results verbatim :exports code
480
481
482
ltl2tgba '(Ga -> Gb) W c'
#+END_SRC

483
484
485
486
#+BEGIN_SRC sh :results verbatim :exports result
SPOT_DOTEXTRA= ltl2tgba '(Ga -> Gb) W c' --dot=
#+END_SRC

487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
#+RESULTS:
#+begin_example
digraph G {
  rankdir=LR
  I [label="", style=invis, width=0]
  I -> 1
  0 [label="0"]
  0 -> 0 [label="b\n{0}"]
  1 [label="1"]
  1 -> 0 [label="a & b & !c"]
  1 -> 1 [label="!a & !c\n{0}"]
  1 -> 2 [label="a & !c"]
  1 -> 3 [label="c"]
  2 [label="2"]
  2 -> 1 [label="!a & !c\n{0}"]
  2 -> 2 [label="a & !c"]
  2 -> 3 [label="!a & c"]
  2 -> 4 [label="a & c"]
  3 [label="3"]
  3 -> 3 [label="1\n{0}"]
  4 [label="4"]
  4 -> 3 [label="!a"]
  4 -> 4 [label="a"]
}
#+end_example

This output should be processed with =dot= to be converted into a
picture.  For instance use =dot -Tpng= or =dot -Tpdf=.

#+NAME: oaut-dot1
#+BEGIN_SRC sh :results verbatim :exports none
518
SPOT_DOTEXTRA= ltl2tgba '(Ga -> Gb) W c' --dot= | sed 's/\\/\\\\/'
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
#+END_SRC

#+RESULTS: oaut-dot1
#+begin_example
digraph G {
  rankdir=LR
  I [label="", style=invis, width=0]
  I -> 1
  0 [label="0"]
  0 -> 0 [label="b\\n{0}"]
  1 [label="1"]
  1 -> 0 [label="a & b & !c"]
  1 -> 1 [label="!a & !c\\n{0}"]
  1 -> 2 [label="a & !c"]
  1 -> 3 [label="c"]
  2 [label="2"]
  2 -> 1 [label="!a & !c\\n{0}"]
  2 -> 2 [label="a & !c"]
  2 -> 3 [label="!a & c"]
  2 -> 4 [label="a & c"]
  3 [label="3"]
  3 -> 3 [label="1\\n{0}"]
  4 [label="4"]
  4 -> 3 [label="!a"]
  4 -> 4 [label="a"]
}
#+end_example

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

#+RESULTS:
[[file:oaut-dot1.png]]

This output can be customized by passing optional characters to the
=--dot= option.  For instance =v= requests a vertical layout (instead
of the default horizontal layout), =c= requests circle states, =s=
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
557
558
causes strongly-connected components to be displayed, =n= causes the
name (see below) of the automaton to be displayed, and =a= causes the
559
560
561
562
563
acceptance condition to be shown as well.  Option =b= causes sets to
be ouput as bullets (e.g., ⓿ instead of ={0}=); option =r= (for
rainbow) causes sets to be displayed in different colors, while option
=R= also uses colors, but it chooses them depending on whether a set
is used with Fin-acceptance, Inf-acceptance, or both.  Finally option
564
=f(FONT)= is used to select a fontname: it is often necessary when =b=
565
566
is used to ensure the characters ⓿, ❶, etc. are all selected from the
same font.
567
568

#+BEGIN_SRC sh :results verbatim :exports code
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
569
ltl2tgba --dot=vcsna '(Ga -> Gb) W c'
570
571
572
573
#+END_SRC
#+RESULTS:
#+begin_example
digraph G {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
574
  label="(Gb | F!a) W c\nInf(0)"
575
576
  labelloc="t"
  node [shape="circle"]
577
  node[style=filled, fillcolor="#ffffa0"]
578
579
580
  I [label="", style=invis, height=0]
  I -> 1
  subgraph cluster_0 {
581
  color=green
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
582
  label=""
583
584
585
  0 [label="0"]
  }
  subgraph cluster_1 {
586
  color=green
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
587
  label=""
588
589
590
  3 [label="3"]
  }
  subgraph cluster_2 {
591
  color=red
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
592
  label=""
593
594
595
  4 [label="4"]
  }
  subgraph cluster_3 {
596
  color=green
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
597
  label=""
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
  1 [label="1"]
  2 [label="2"]
  }
  0 -> 0 [label="b\n{0}"]
  1 -> 0 [label="a & b & !c"]
  1 -> 1 [label="!a & !c\n{0}"]
  1 -> 2 [label="a & !c"]
  1 -> 3 [label="c"]
  2 -> 1 [label="!a & !c\n{0}"]
  2 -> 2 [label="a & !c"]
  2 -> 3 [label="!a & c"]
  2 -> 4 [label="a & c"]
  3 -> 3 [label="1\n{0}"]
  4 -> 3 [label="!a"]
  4 -> 4 [label="a"]
}
#+end_example

#+NAME: oaut-dot2
#+BEGIN_SRC sh :results verbatim :exports none
618
SPOT_DOTEXTRA= ltl2tgba --dot=vcsna '(Ga -> Gb) W c' | sed 's/\\/\\\\/'
619
620
621
622
623
#+END_SRC

#+RESULTS: oaut-dot2
#+begin_example
digraph G {
624
  label="(Gb | F!a) W c\\nInf(0)"
625
626
  labelloc="t"
  node [shape="circle"]
627
  I [label="", style=invis, height=0]
628
629
  I -> 1
  subgraph cluster_0 {
630
631
  color=green
  label=""
632
  0 [label="0"]
633
  }
634
  subgraph cluster_1 {
635
636
  color=green
  label=""
637
  3 [label="3"]
638
  }
639
  subgraph cluster_2 {
640
641
642
643
  color=red
  label=""
  4 [label="4"]
  }
644
  subgraph cluster_3 {
645
646
647
  color=green
  label=""
  1 [label="1"]
648
  2 [label="2"]
649
  }
650
651
652
653
654
655
656
657
658
659
660
661
  0 -> 0 [label="b\\n{0}"]
  1 -> 0 [label="a & b & !c"]
  1 -> 1 [label="!a & !c\\n{0}"]
  1 -> 2 [label="a & !c"]
  1 -> 3 [label="c"]
  2 -> 1 [label="!a & !c\\n{0}"]
  2 -> 2 [label="a & !c"]
  2 -> 3 [label="!a & c"]
  2 -> 4 [label="a & c"]
  3 -> 3 [label="1\\n{0}"]
  4 -> 3 [label="!a"]
  4 -> 4 [label="a"]
662
663
664
665
666
667
668
669
670
671
}
#+end_example

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

#+RESULTS:
[[file:oaut-dot2.png]]

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
672
673
674
675
The acceptance condition is displayed in the same way as in the [[http://adl.github.io/hoaf/][HOA
format]]. Here =Inf(0)= means that runs are accepting if and only if
they visit some the transitions in the set #0 infinitely often.

676
677
678
679
680
681
682
683
684
685
686
The strongly connected components are displayed using the following colors:
- *green* components contain an accepting cycle
- *red* components contain no accepting cycle
- *orange* components may or may not contain an accepting cycle.  Such an indecision occur only when using =Fin= acceptance primitive, deciding that would require a better algorithm than what the output routine is using.
- *black* components are trivial (i.e., they contain no cycle)
- *gray* components are useless (i.e., they are non-accepting, and are only followed by non-accepting components)

Here is an example involving all colors:

#+NAME: oaut-dot3
#+BEGIN_SRC sh :results verbatim :exports none
687
SPOT_DOTEXTRA= autfilt --dot=cas <<EOF | sed 's/\\/\\\\/'
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
HOA: v1
States: 10
Start: 1
AP: 2 "a" "b"
acc-name: generalized-Buchi 2
Acceptance: 3 Inf(0)&Inf(1)&Fin(2)
--BODY--
State: 0 {2}
[0&1] 0 {0 1}
[!0&!1] 0
[0] 5
State: 1
[1] 4
[0&!1] 3
State: 4
[!1] 4 {1 2}
[1] 2
State: 2
[0] 0
[1] 7
State: 3
[0&1] 1 {1 0}
State: 5
[t] 6 {1}
State: 6
[t] 5
State: 7
[!0&1] 7 {0 2}
[0&1] 7 {0 1}
[t] 8
State: 8
[!0&1] 8 {0 2}
[0&1] 9 {0 1}
State: 9
[!0&1] 8 {0 1}
[0&1] 9 {0 2}
--END--
EOF
#+END_SRC

#+RESULTS: oaut-dot3
#+begin_example
digraph G {
  rankdir=LR
  label="Fin(2) & (Inf(0)&Inf(1))"
  labelloc="t"
  node [shape="circle"]
  I [label="", style=invis, width=0]
  I -> 1
  subgraph cluster_0 {
  color=grey
  label=""
  5 [label="5"]
  6 [label="6"]
  }
  subgraph cluster_1 {
  color=orange
  label=""
  0 [label="0"]
  }
  subgraph cluster_2 {
  color=orange
  label=""
  8 [label="8"]
  9 [label="9"]
  }
  subgraph cluster_3 {
  color=green
  label=""
  7 [label="7"]
  }
  subgraph cluster_4 {
  color=black
  label=""
  2 [label="2"]
  }
  subgraph cluster_5 {
  color=red
  label=""
  4 [label="4"]
  }
  subgraph cluster_6 {
  color=green
  label=""
  1 [label="1"]
  3 [label="3"]
  }
  0 -> 0 [label="a & b\\n{0,1,2}"]
  0 -> 0 [label="!a & !b\\n{2}"]
  0 -> 5 [label="a\\n{2}"]
  1 -> 4 [label="b"]
  1 -> 3 [label="a & !b"]
  2 -> 0 [label="a"]
  2 -> 7 [label="b"]
  3 -> 1 [label="a & b\\n{0,1}"]
  4 -> 4 [label="!b\\n{1,2}"]
  4 -> 2 [label="b"]
  5 -> 6 [label="1\\n{1}"]
  6 -> 5 [label="1"]
  7 -> 7 [label="!a & b\\n{0,2}"]
  7 -> 7 [label="a & b\\n{0,1}"]
  7 -> 8 [label="1"]
  8 -> 8 [label="!a & b\\n{0,2}"]
  8 -> 9 [label="a & b\\n{0,1}"]
  9 -> 8 [label="!a & b\\n{0,1}"]
  9 -> 9 [label="a & b\\n{0,2}"]
}
#+end_example

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

#+RESULTS:
[[file:oaut-dot3.png]]

804
<<default-dot>>
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824

The dot output can also be customized via two environment variables:
- =SPOT_DOTDEFAULT= contains default arguments for the =--dot= option
  (for when it is used implicitly, or used as just =--dot= without
  argument).  For instance after =export SPOT_DOTDEFAULT=vcsn=, using
  =--dot= is equivalent to =--dot=vcsn=.  However using =--dot=xyz=
  (for any value of =xyz=, even empty) will ignore the
  =SPOT_DOTDEFAULT= variable.  If the argument of =--dot= contains
  a dot character, then this dot is replaced by the contents of
  =SPOT_DOTDEFAULT=.  So ~--dot=.a~ would be equivalent to =--dot=vcsna=
  with our example definition of =SPOT_DOTDEFAULT=.
- =SPOT_DOTEXTRA= may contains an arbitrary string that will be emitted
  in the dot output before the first state.  This can be used to modify
  any attribute.  For instance (except for this page, where we had
  do demonstrate the various options of =--dot=, and a few pages where
  we show the =--dot= output verbatim) all the automata displayed in
  this documentation are generated with the following environment
  variables set:

#+BEGIN_SRC sh :results verbatim :exports code
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
825
export SPOT_DOTDEFAULT='Brf(Lato)'
826
export SPOT_DOTEXTRA='node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]'
827
#+END_SRC
828

829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
* Statistics

The =--stats= option takes format string parameter to specify what and
how statistics should be output.

Most tool support a common set of statistics about the output
automaton (like =%s= for the number of states, =%t= for transitions,
=%e= for edges, etc.)  Additional statistics might be available
depending on what the tool does (for instance [[file:autfilt.org][=autfilt=]] also has =%S=,
=%T=, and =%E= to display the same statistics about the input
automaton).  All the available statistics are displayed when a tool is
run with =--help=.

For instance here are the statistics available in [[file:randaut.org][=randaut=]]:

#+BEGIN_SRC sh :results verbatim :exports results
randaut --help | sed -n '/ sequences:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
#+begin_example
  %%                         a single %
  %a                         number of acceptance sets
  %c                         number of SCCs
  %d                         1 if the output is deterministic, 0 otherwise
  %e                         number of edges
  %F                         seed number
  %L                         automaton number
  %m                         name of the automaton
  %n                         number of nondeterministic states in output
  %p                         1 if the output is complete, 0 otherwise
  %r                         processing time (excluding parsing) in seconds
  %s                         number of states
  %t                         number of transitions
  %w                         one word accepted by the output automaton
#+end_example

In most tools =%F= and =%L= are the input filename and line number,
but as this makes no sense in =randaut=, these two sequences emit
numbers related to the generation of automata.

For instance let's generate 100 random automata with 10 states and
density 0.2, and just count the number of edges in each automaton. Then
use =R= to summarize the distribution of these values:

#+BEGIN_SRC sh :results verbatim :exports both
randaut -d 0.2 -S 10 -n 1000 a --stats %e > size.csv
R --slave -e "summary(read.csv('size.csv', header=FALSE, col.names='edges'))"
#+END_SRC

#+RESULTS:
:      edges
:  Min.   :17.00
:  1st Qu.:25.00
:  Median :28.00
:  Mean   :27.96
:  3rd Qu.:30.00
:  Max.   :42.00


For $S=10$ states and density $D=0.2$ the expected degree of each
state $1+(S-1)D = 1+9\times 0.2 = 2.8$ so the expected number of edges
should be 10 times that.


* Naming automata

Automata can be given names.  This name can be output in GraphViz
output when =--dot=n= is given, and is also part of the HOA format (as
activated by =-H=).

By default, =ltl2tgba= will use the input format as name.  Other tools
have no default name.  This name can be changed using the =--name= option,
that takes a format string similar to the one of =--stats=.

903
#+NAME: oaut-name
904
905
906
907
908
909
910
911
912
913
#+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba --name='TGBA for %f' --dot=n 'a U b'
#+END_SRC

#+RESULTS: oaut-name
#+begin_example
digraph G {
  rankdir=LR
  label="TGBA for a U b"
  labelloc="t"
914
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
  I [label="", style=invis, width=0]
  I -> 1
  0 [label="0", peripheries=2]
  0 -> 0 [label="1"]
  1 [label="1"]
  1 -> 0 [label="b"]
  1 -> 1 [label="a & !b"]
}
#+end_example

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

#+RESULTS:
[[file:oaut-name.png]]

If you have an automaton saved in the HOA format, you can extract its
name using =autfilt --stats=%M input.hoa=. The =%M= escape sequence is
replaced by the name of the input automaton.

Here is a pipeline of commands that generates five LTL formulas
$\varphi$ such that both $\varphi$ and $\lnot\varphi$ are translated
into a 3-state TGBA by [[file:ltl2tgba.org][=ltl2tgba=]].  It starts by generating an
infinite stream of random LTL formulas using =a= and =b= as atomic
propositions, then it converts these formulas as TGBA (in the HOA
format, therefore carrying the formula as name), filtering only the
TGBA with 3 states and outputting =!(%M)= (that is the negation of the
associated formula), translating the resulting formulas as TGBA, again
retaining only the names (i.e. formulas) of the automata with 3
states, and finally restricting the output to the first 5 matches
using =autfilt -n5=.

#+BEGIN_SRC sh :results verbatim :exports both
randltl -n -1 a b |
ltl2tgba -H -F- |
autfilt --states=3 --stats='!(%M)' |
ltl2tgba -H -F- |
autfilt --states=3 --stats=%M -n5
#+END_SRC

#+RESULTS:
: G(F!a & XF(a | G!b))
: GFb | G(!b & FG!b)
: !a & F((a | b) & (!a | !b))
: !a | (b R a)
: !b & X(!b U a)

963
Note that the above result can also be obtained without using
964
=autfilt= and automata names.  We can use the fact that =ltl2tgba
965
966
--stats= can output the automaton size, and that =ltl2tgba= is also
capable of [[file:csv.org][reading from a CSV file]] (=-F-/2= instructs =ltl2tgba= to
967
read the standard input as if it was a CSV file, and to process its
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
second column):

#+BEGIN_SRC sh :results verbatim :exports both
randltl -n -1 a b |                 # generate a stream of random LTL formulas
ltl2tgba -F- --stats='%s,!(%f)' |   # for each formula output "states,negated formula"
grep '^3,' |                        # keep only formulas with 3 states
ltl2tgba -F-/2 --stats='%s,%f' |    # for each negated formula output "states,formula"
grep '^3,' |                        # keep only negated formulas with 3 states
head -n5 | cut -d, -f2              # return the five first formulas
#+END_SRC

#+RESULTS:
: G(F!a & XF(a | G!b))
: GFb | G(!b & FG!b)
: !a & F((!a | !b) & (a | b))
: !a | (b R a)
: !b & X(!b U a)



988
989
990
991
992
993
994
#  LocalWords:  num toc html syntaxes ltl tgba sed utf UTF lbtt SCCs
#  LocalWords:  GraphViz's hoaf HOA LBTT's neverclaim ba SPOT's Gb cn
#  LocalWords:  GraphViz autfilt acc Buchi hoafex gvpack perl pe bb
#  LocalWords:  labelloc rankdir subgraph lp pos invis gv png cmdline
#  LocalWords:  Tpng txt Hs Hm CSV Htl LBT dstar init goto fi Tpdf XF
#  LocalWords:  oaut vcsn randaut nondeterministic filename csv hoa
#  LocalWords:  varphi lnot GFb FG
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
* Naming output

By default, all output is sent to standard output, so you can either
redirect it to a file, or pipe it to another program.
You can also use the =--output= (a.k.a. =-o=) option to specify a
filename where automata should be written.  The advantage over
a shell redirection, is that you may build a name using the same
escape sequences as used by =--stats= and =--name=.

For instance =%d= is replaced by 0 or 1 depending on whether the
automaton is deterministic.  We can generate 20 random automata, and
output them in two files depending on their determinism:

#+BEGIN_SRC sh :results verbatim :exports both
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1009
randaut -n 20 -S2 -d1 1 -H -o out-det%d.hoa
1010
1011
1012
1013
1014
autfilt -c out-det0.hoa    # Count of non-deterministic automata
autfilt -c out-det1.hoa    # Count of deterministic automata
#+END_SRC

#+RESULTS:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1015
1016
: 14
: 6
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026

If you use this feature, beware that the output filename
is only truncated by the first file that is output to it: so
if no automaton generate some filename, the existing file
will be left untouched.  For instance we we run the above
commands, again, but forcing [[file:randaut.org][=randaut=]] to output 20
deterministic automata, it may look like we produced more
than 20 automata:

#+BEGIN_SRC sh :results verbatim :exports both
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1027
randaut -D -n 20 -S2 -d1 1 -H -o out-det%d.hoa
1028
1029
1030
1031
1032
autfilt -c out-det0.hoa    # Count of non-deterministic automata
autfilt -c out-det1.hoa    # Count of deterministic automata
#+END_SRC

#+RESULTS:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1033
: 14
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
: 20

This is because the =out-det0.hoa= file hasn't changed from the
previous execution, while =out-det1.hoa= has been overwritten.

In the case where you want to append to a file instead of overwriting
it, prefix the output filename with =>>= as in

: randaut -D -n 20 -S2 1 -H -o '>>out-det%d.hoa'

(You need the quotes so that the shell does not interpret '>>'.)