ltl2tgba.org 37.2 KB
Newer Older
1
# -*- coding: utf-8 -*-
2
#+TITLE: =ltl2tgba=
3
#+DESCRIPTION: Spot command-line tool for translating LTL into Transition-based Generalized Büchi 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 both
7

8
9
10
11
This tool translates LTL or PSL formulas into different types of
automata.

The inner algorithm produces Transition-based Generalized Büchi
12
Automata, hence the name of the tool, but =ltl2tgba= has grown and
13
14
15
16
now offers several options to adjust the type of automaton output.
Those options will be covered in more detail below, but here is
a quick summary:

17
18
- =--tgba= (the default) outputs Transition-based Generalized Büchi
  Automata
19
- =--ba= (or =-B=) outputs state-based Büchi automata
20
21
- =--monitor= (or =-M=) outputs monitors
- =--generic --deterministic= (or =-DG=) will do whatever it takes to
22
23
  produce a deterministic automaton, and may use any acceptance
  condition
24
25
- =--parity --deterministic= (or =-DP=) will produce a deterministic
  automaton with parity acceptance.
26

27
28
29
(The latter two can also be used with =--deterministic=, but that is
less frequent.)

30
31
32
33
34
* TGBA and BA

Formulas to translate may be specified using [[file:ioltl.org][common input options for
LTL/PSL formulas]].

35
#+BEGIN_SRC sh :wrap SRC hoa
36
37
ltl2tgba -f 'Fa & GFb'
#+END_SRC
38

39
#+RESULTS:
40
#+begin_SRC hoa
41
42
43
HOA: v1
name: "Fa & GFb"
States: 2
44
Start: 0
45
46
47
48
49
50
51
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
52
53
[!0] 0
[0] 1
54
State: 1
55
56
[!1] 1
[1] 1 {0}
57
--END--
58
#+end_SRC
59
60
61
62
63
64
65

Actually, because =ltl2tgba= is often used with a single formula
passed on the command line, the =-f= option can be omitted and any
command-line parameter that is not the argument of some option will be
assumed to be a formula to translate (this differs from [[file:ltlfilt.org][=ltlfilt=]],
where such parameters are assumed to be filenames).

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
66
=ltl2tgba= honors the [[file:oaut.org][common options for selecting the output format]].
67
68
69
70
71
72
The default output format, as shown above, is the [[file:hoa.org][HOA]] format, as this
can easily be piped to other tools.

To convert the automaton into a picture, or into vectorial format, use
=--dot= or =-d= to request [[http://www.graphviz.org/][GraphViz output]] and process the result with
=dot= or =dotty=.  Typically, you could get a =pdf= of this TGBA using
73
#+BEGIN_SRC sh :exports code
74
ltl2tgba "Fa & GFb" -d | dot -Tpdf > tgba.pdf
75
76
77
#+END_SRC
#+RESULTS:

78
The result would look like this (note that in this documentation
79
we use some [[file:oaut.org::#default-dot][environment variables]] to produce a more colorful
80
output by default)
81
#+NAME: dotex
82
#+BEGIN_SRC sh :exports none
83
ltl2tgba "Fa & GFb" -d
84
85
#+END_SRC

86
#+BEGIN_SRC dot :file dotex.svg :var txt=dotex :exports results
87
88
89
90
$txt
#+END_SRC

#+RESULTS:
91
[[file:dotex.svg]]
92

93
94
95
96
97
98
99
100
101
102
Characters like ⓿, ❶, etc. denotes the acceptance sets a transition
belongs to.  In this case, there is only one acceptance set, called
=0=, containing a single transition.  You may have many transitions in
the same acceptance set, and a transition may also belong to multiple
acceptance sets.  An infinite path through this automaton is accepting
iff it visit each acceptance set infinitely often.  Therefore, in the
above example, any accepted path will /necessarily/ leave the initial
state after a finite amount of steps, and then it will verify the
property =b= infinitely often.  It is also possible that an automaton
do not use any acceptance set at all, in which any run is accepting.
103
104
105
106
107

Here is a TGBA with multiple acceptance sets (we omit the call to
=dot= to render the output of =ltl2tgba= from now on):

#+NAME: dotex2
108
#+BEGIN_SRC sh :exports code
109
ltl2tgba "GFa & GFb" -d
110
111
#+END_SRC
#+RESULTS: dotex2
112
113
114
#+begin_example
digraph G {
  rankdir=LR
115
116
117
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
118
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
119
120
121
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
122
123
124
125
  0 -> 0 [label=<a &amp; b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
  0 -> 0 [label=<!a &amp; !b>]
  0 -> 0 [label=<!a &amp; b<br/><font color="#F17CB0">❶</font>>]
  0 -> 0 [label=<a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
126
127
}
#+end_example
128

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

135
The above TGBA has two acceptance sets: ⓿ and ❶.  The definition of
136
137
these acceptance sets ensures that atomic propositions =a= and =b= must
be true infinitely often.
138
139
140
141

A Büchi automaton for the previous formula can be obtained with the
=-B= option:

142
#+NAME: dotex2ba
143
#+BEGIN_SRC sh :exports code
144
ltl2tgba -B 'GFa & GFb' -d
145
146
147
148
#+END_SRC
#+RESULTS: dotex2ba
#+begin_example
digraph G {
149
  rankdir=LR
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
150
  node [shape="circle"]
151
152
153
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
154
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
155
156
  I [label="", style=invis, width=0]
  I -> 0
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
157
  0 [label="0", peripheries=2]
158
159
160
  0 -> 0 [label=<a &amp; b>]
  0 -> 1 [label=<!b>]
  0 -> 2 [label=<!a &amp; b>]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
161
  1 [label="1"]
162
163
164
  1 -> 0 [label=<a &amp; b>]
  1 -> 1 [label=<!b>]
  1 -> 2 [label=<!a &amp; b>]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
165
  2 [label="2"]
166
167
  2 -> 0 [label=<a>]
  2 -> 2 [label=<!a>]
168
169
170
}
#+end_example

171
#+BEGIN_SRC dot :file dotex2ba.svg :var txt=dotex2ba :exports results
172
173
174
$txt
#+END_SRC
#+RESULTS:
175
[[file:dotex2ba.svg]]
176

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
177
178
179
180
181
182
183
Although accepting states in the Büchi automaton are (traditionally)
pictured with double-lines, internally this automaton is still handled
as a TGBA with a single acceptance set such that the transitions
leaving the state are either all accepting, or all non-accepting.  You
can see this underlying TGBA if you pass the =--dot=t= option (the =t=
requests the use of transition-based acceptance as it is done
internally):
184

185
#+BEGIN_SRC sh :exports code
186
187
188
189
ltl2tgba --dot=t -B 'GFa & GFb'
#+END_SRC

#+NAME: dotex2ba-t
190
#+BEGIN_SRC sh :exports none
191
ltl2tgba --dot=.t -B 'GFa & GFb'
192
193
194
195
196
197
#+END_SRC

#+RESULTS: dotex2ba-t
#+begin_example
digraph G {
  rankdir=LR
198
199
200
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
201
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
202
203
204
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
205
206
207
  0 -> 0 [label=<a &amp; b<br/><font color="#5DA5DA">⓿</font>>]
  0 -> 1 [label=<!b<br/><font color="#5DA5DA">⓿</font>>]
  0 -> 2 [label=<!a &amp; b<br/><font color="#5DA5DA">⓿</font>>]
208
  1 [label="1"]
209
210
211
  1 -> 0 [label=<a &amp; b>]
  1 -> 1 [label=<!b>]
  1 -> 2 [label=<!a &amp; b>]
212
  2 [label="2"]
213
214
  2 -> 0 [label=<a>]
  2 -> 2 [label=<!a>]
215
216
217
}
#+end_example

218
#+BEGIN_SRC dot :file dotex2ba-t.svg :var txt=dotex2ba-t :exports results
219
220
221
$txt
#+END_SRC
#+RESULTS:
222
[[file:dotex2ba-t.svg]]
223

224
225
226
227
228
Using option =-S= instead of option =-B= you can obtain generalized
Büchi automata with state-based acceptance.  Here is the same formula
as above, for comparison.

#+NAME: dotex2gba
229
#+BEGIN_SRC sh :exports code
230
ltl2tgba -S 'GFa & GFb' -d
231
232
#+END_SRC

233
#+BEGIN_SRC dot :file dotex2gba.svg :var txt=dotex2gba :exports results
234
235
236
$txt
#+END_SRC
#+RESULTS:
237
[[file:dotex2gba.svg]]
238
239
240
241
242
243
244

Note that =ltl2tgba= is not very good at generating state-based
generalized Büchi automata (GBA): all it does is generating a
transition-based one internally, and then pushing acceptance sets onto
states.  On this example, the resulting GBA produced by =-S= is larger
than the BA produced by =-B=.

245
246
As already discussed on the page about [[file:oaut.org][common output options]], various
options controls the output format of =ltl2tgba=:
247

248
#+BEGIN_SRC sh :exports results
249
250
251
ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
252
253
254
#+begin_example
  -8, --utf8                 enable UTF-8 characters in output (ignored with
                             --lbtt or --spin)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
255
256
257
      --check[=PROP]         test for the additional property PROP and output
                             the result in the HOA format (implies -H).  PROP
                             may be any prefix of 'all' (default),
258
259
260
261
262
                             'unambiguous', 'stutter-invariant', or
                             'strength'.
  -d, --dot[=1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v|+INT]
                             GraphViz's format.  Add letters for (1) force
                             numbered states, (a) acceptance display, (b)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
263
                             acceptance sets as bullets, (B) bullets except for
264
                             Büchi/co-Büchi automata, (c) force circular
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
265
266
267
268
269
                             nodes, (e) force elliptic nodes, (f(FONT)) use
                             FONT, (h) horizontal layout, (v) vertical layout,
                             (n) with name, (N) without name, (o) ordered
                             transitions, (r) rainbow colors for acceptance
                             sets, (R) color acceptance sets by Inf/Fin, (s)
270
271
272
273
274
275
276
277
278
279
                             with SCCs, (t) force transition-based acceptance,
                             (+INT) add INT to all set numbers
  -H, --hoaf[=i|l|m|s|t|v]   Output the automaton in HOA format (default).  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, (k) use
                             state labels when possible, (l) single-line
                             output, (v) verbose properties
280
      --lbtt[=t]             LBTT's format (add =t to force transition-based
281
                             acceptance even on Büchi automata)
282
      --name=FORMAT          set the name of the output automaton
283
284
285
  -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 '>>'.
286
  -q, --quiet                suppress all normal output
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
287
288
289
  -s, --spin[=6|c]           Spin neverclaim (implies --ba).  Add letters to
                             select (6) Spin's 6.2.4 style, (c) comments on
                             states
290
291
      --stats=FORMAT         output statistics about the automaton
#+end_example
292

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
293
Option =-8= can be used to improve the readability of the output
294
295
296
if your system can display UTF-8 correctly.

#+NAME: dotex2ba8
297
#+BEGIN_SRC sh :exports code
298
ltl2tgba -B8 "GFa & GFb" -d
299
300
301
302
#+END_SRC
#+RESULTS: dotex2ba8
#+begin_example
digraph G {
303
  rankdir=LR
304
305
306
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
307
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
308
309
  I [label="", style=invis, width=0]
  I -> 0
310
  0 [label=<0<br/><font color="#5DA5DA">⓿</font>>]
311
312
313
  0 -> 0 [label=<a∧b>]
  0 -> 1 [label=<b̅>]
  0 -> 2 [label=<a̅∧b>]
314
  1 [label=<1>]
315
316
317
  1 -> 0 [label=<a∧b>]
  1 -> 1 [label=<b̅>]
  1 -> 2 [label=<a̅∧b>]
318
  2 [label=<2>]
319
320
  2 -> 0 [label=<a>]
  2 -> 2 [label=<a̅>]
321
322
323
}
#+end_example

324
#+BEGIN_SRC dot :file dotex2ba8.svg :var txt=dotex2ba8 :exports results
325
326
327
$txt
#+END_SRC
#+RESULTS:
328
[[file:dotex2ba8.svg]]
329
330
331
332
333
334
335
336

* Spin output

Using the =--spin= or =-s= option, =ltl2tgba= will produce a Büchi automaton
(the =-B= option is implied) as a never claim that can be fed to Spin.
=ltl2tgba -s= is therefore a drop-in replacement for =spin -f=.


337
#+BEGIN_SRC sh
338
339
340
341
342
343
344
345
ltl2tgba -s 'GFa & GFb'
#+END_SRC
#+RESULTS:
#+begin_example
never { /* G(Fa & Fb) */
accept_init:
  if
  :: ((a) && (b)) -> goto accept_init
346
347
  :: ((!(b))) -> goto T0_S2
  :: ((!(a)) && (b)) -> goto T0_S3
348
349
350
  fi;
T0_S2:
  if
351
352
353
  :: ((a) && (b)) -> goto accept_init
  :: ((!(b))) -> goto T0_S2
  :: ((!(a)) && (b)) -> goto T0_S3
354
355
356
  fi;
T0_S3:
  if
357
358
  :: ((a)) -> goto accept_init
  :: ((!(a))) -> goto T0_S3
359
360
361
362
363
364
365
366
  fi;
}
#+end_example

Since Spin 6 extended its syntax to support arbitrary atomic
propositions, you may also need put the parser in =--lenient= mode to
support these:

367
#+BEGIN_SRC sh
368
369
370
371
372
373
ltl2tgba -s --lenient '(a < b) U (process[2]@ok)'
#+END_SRC
#+RESULTS:
: never { /* "a < b" U "process[2]@ok" */
: T0_init:
:   if
374
:   :: (process[2]@ok) -> goto accept_all
375
376
377
378
379
380
381
382
383
:   :: ((a < b) && (!(process[2]@ok))) -> goto T0_init
:   fi;
: accept_all:
:   skip
: }

* Do you favor deterministic or small automata?

The translation procedure can be controled by a few switches.  A first
384
385
set of options specifies the goal of the simplification routines:
whenever possible, would you prefer a small automaton (=--small=) or a
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
386
deterministic (=--deterministic=) automaton?
387

388
#+BEGIN_SRC sh :exports results
389
ltl2tgba --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d'
390
391
#+END_SRC
#+RESULTS:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
392
393
:   -a, --any                  no preference, do not bother making it small or
:                              deterministic
394
395
396
:   -D, --deterministic        prefer deterministic automata (combine with
:                              --generic to be sure to obtain a deterministic
:                              automaton)
397
398
:       --small                prefer small automata (default)

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
399
400
401
402
The =--any= option tells the translator that it should attempt to
reduce or produce a deterministic result result: any automaton
denoting the given formula is OK.  This effectively disables
post-processings and speeds up the translation.
403

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
404
405
406
407
408
With the =-D= or =--deterministic= option, the translator will
/attempt/ to produce a deterministic automaton, even if this requires
a lot of states.  =ltl2tgba= knows how to produce the minimal
deterministic Büchi automaton for any obligation property (this
includes safety properties).
409
410
411
412
413

With the =--small= option (the default), the translator will not
produce a deterministic automaton when it knows how to build smaller
automaton.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
414
415
416
417
Note that options =--deterministic= and =--small= express
/preferences/.  They certainly do /not/ guarantee that the output will
be deterministic, or will be the smallest automaton possible.

418
419
420
421
In particular, for properties more complex than obligations, it is
possible that no deterministic TGBA exist, and even if it exists,
=ltl2tgba= might not find it: so a non-deterministic automaton can be
returned in this case.  If you absolutely want a deterministic
422
automaton, see [[#generic][the =--generic= option]] or [[#parity][the =--parity= option]].
423

424
425
426
427
An example formula where the difference between =-D= and =--small= is
flagrant is =Ga|Gb|Gc=:

#+NAME: gagbgc1
428
#+BEGIN_SRC sh :exports code
429
ltl2tgba 'Ga|Gb|Gc' -d
430
431
432
433
#+END_SRC
#+RESULTS: gagbgc1
#+begin_example
digraph G {
434
  rankdir=LR
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
435
  node [shape="circle"]
436
437
438
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
439
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
440
441
  I [label="", style=invis, width=0]
  I -> 0
442
  0 [label=<0>]
443
444
445
  0 -> 1 [label=<a>]
  0 -> 2 [label=<b>]
  0 -> 3 [label=<c>]
446
  1 [label=<1>]
447
  1 -> 1 [label=<a>]
448
  2 [label=<2>]
449
  2 -> 2 [label=<b>]
450
  3 [label=<3>]
451
  3 -> 3 [label=<c>]
452
453
454
}
#+end_example

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

461
#+NAME: gagbgc2
462
#+BEGIN_SRC sh :exports code
463
ltl2tgba -D 'Ga|Gb|Gc' -d
464
465
466
467
#+END_SRC
#+RESULTS: gagbgc2
#+begin_example
digraph G {
468
  rankdir=LR
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
469
  node [shape="circle"]
470
471
472
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
473
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
474
475
  I [label="", style=invis, width=0]
  I -> 6
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
476
  0 [label="0", peripheries=2]
477
  0 -> 0 [label=<c>]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
478
  1 [label="1", peripheries=2]
479
480
481
  1 -> 0 [label=<!b &amp; c>]
  1 -> 1 [label=<b &amp; c>]
  1 -> 2 [label=<b &amp; !c>]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
482
  2 [label="2", peripheries=2]
483
  2 -> 2 [label=<b>]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
484
  3 [label="3", peripheries=2]
485
486
487
  3 -> 2 [label=<!a &amp; b>]
  3 -> 3 [label=<a &amp; b>]
  3 -> 5 [label=<a &amp; !b>]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
488
  4 [label="4", peripheries=2]
489
490
491
  4 -> 0 [label=<!a &amp; c>]
  4 -> 4 [label=<a &amp; c>]
  4 -> 5 [label=<a &amp; !c>]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
492
  5 [label="5", peripheries=2]
493
  5 -> 5 [label=<a>]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
494
  6 [label="6", peripheries=2]
495
496
497
498
499
500
501
  6 -> 0 [label=<!a &amp; !b &amp; c>]
  6 -> 1 [label=<!a &amp; b &amp; c>]
  6 -> 2 [label=<!a &amp; b &amp; !c>]
  6 -> 3 [label=<a &amp; b &amp; !c>]
  6 -> 4 [label=<a &amp; !b &amp; c>]
  6 -> 5 [label=<a &amp; !b &amp; !c>]
  6 -> 6 [label=<a &amp; b &amp; c>]
502
503
504
}
#+end_example

505
#+BEGIN_SRC dot :file gagbgc2.svg :var txt=gagbgc2 :exports results
506
507
508
$txt
#+END_SRC
#+RESULTS:
509
[[file:gagbgc2.svg]]
510
511
512
513
514

You can augment the number of terms in the disjunction to magnify the
difference.  For N terms, the =--small= automaton has N+1 states,
while the =--deterministic= automaton needs 2^N-1 states.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
515
Add the =-C= or =--complete= option if you want to obtain a complete
516
517
518
automaton, with a sink state capturing that rejected words that would
not otherwise have a run in the output automaton.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
519
520
521
522
523
524
525
526
527
528
529
Add the =-U= or =--unambiguous= option if you want unambiguous
automata to be produced.  An automaton is unambiguous if any word is
recognized by at most one accepting run of the automaton (however a
word can be rejected by multiple runs, so unambiguous automata can be
non-deterministic).

The following example is an ambiguous Büchi automaton, because the are
two ways to accept a run that repeats continuously the configuration
$\bar ab$.

#+NAME: ambig1
530
#+BEGIN_SRC sh :exports code
531
ltl2tgba -B 'GFa -> GFb' -d
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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
557
558
#+END_SRC
#+RESULTS: ambig1
#+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 -> 1
  0 [label="0", peripheries=2]
  0 -> 0 [label=<!a>]
  1 [label="1"]
  1 -> 0 [label=<!a>]
  1 -> 1 [label=<1>]
  1 -> 2 [label=<b>]
  2 [label="2", peripheries=2]
  2 -> 2 [label=<b>]
  2 -> 3 [label=<!b>]
  3 [label="3"]
  3 -> 2 [label=<b>]
  3 -> 3 [label=<!b>]
}
#+end_example

559
#+BEGIN_SRC dot :file ambig1.svg :var txt=ambig1 :exports results
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
560
561
562
$txt
#+END_SRC
#+RESULTS:
563
[[file:ambig1.svg]]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
564
565
566
567
568

Here is an unambiguous automaton for the same formula, in which there
is only one run that recognizes this example word:

#+NAME: ambig2
569
#+BEGIN_SRC sh :exports code
570
ltl2tgba -B -U 'GFa -> GFb' -d
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
#+END_SRC

#+RESULTS: ambig2
#+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=<!a &amp; !b>]
  0 -> 2 [label=<1>]
  0 -> 3 [label=<a | b>]
  0 -> 4 [label=<!a &amp; !b>]
  1 [label="1", peripheries=2]
  1 -> 1 [label=<!a &amp; !b>]
  2 [label="2", peripheries=2]
  2 -> 2 [label=<b>]
  2 -> 5 [label=<!b>]
  3 [label="3"]
  3 -> 1 [label=<!a &amp; !b>]
  3 -> 3 [label=<a | b>]
  3 -> 4 [label=<!a &amp; !b>]
  4 [label="4"]
  4 -> 3 [label=<a | b>]
  4 -> 4 [label=<!a &amp; !b>]
  5 [label="5"]
  5 -> 2 [label=<b>]
  5 -> 5 [label=<!b>]
}
#+end_example

607
#+BEGIN_SRC dot :file ambig2.svg :var txt=ambig2 :exports results
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
608
609
610
611
$txt
#+END_SRC

#+RESULTS:
612
[[file:ambig2.svg]]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
613
614
615
616
617
618


Unlike =--small= and =--deterministic= that express preferences,
options =--complete= and =--unambiguous= do guarantee that the output
will be complete and unambiguous.

619

620
621
622
A last parameter that can be used to tune the translation is the amount
of pre- and post-processing performed.  These two steps can be adjusted
via a common set of switches:
623
#+BEGIN_SRC sh :exports results
624
ltl2tgba --help | sed -n '/Simplification level:/,/^$/p' | sed '1d;$d'
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
#+END_SRC
#+RESULTS:
:       --high                 all available optimizations (slow, default)
:       --low                  minimal optimizations (fast)
:       --medium               moderate optimizations

Pre-processings are rewritings done on the LTL formulas, usually to
reduce its size, but mainly to put it in a form that will help the
translator (for instance =F(a|b)= is easier to translate than
=F(a)|F(b)=).  At =--low= level, only simple syntactic rewritings are
performed.  At =--medium= level, additional simplifications based on
syntactic implications are performed.  At =--high= level, language
containment is used instead of syntactic implications.

Post-processings are cleanups and simplifications of the automaton
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
640
641
produced by the core translator.  The algorithms used during
post-processing are
642
643
644
645
646
647
648
649
- SCC filtering: removing useless strongly connected components,
  and useless acceptance sets.
- direct simulation: merge states based on suffix inclusion.
- iterated simulations: merge states based on suffix inclusion,
  or prefix inclusion, in a loop.
- WDBA minimization: determinize and minimize automata representing
  obligation properties.
- degeneralization: convert a TGBA into a BA
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
650
- BA simulation (again direct or iterated)
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672

The chaining of these various algorithms depends on the selected
combination of optimization level (=--low=, =--medium=, =--high=),
translation intent (=--small=, =--deterministic=) and type of
automaton desired (=--tgba=, =--ba=).

A notable configuration is =--any --low=, which will produce a TGBA as
fast as possible.  In this case, post-processing is disabled, and only
syntactic rewritings are performed.  This can be used for
satisfiability checking, although in this context even building an
automaton is overkill (you only need an accepted run).

Finally, it should be noted that the default optimization options
(=--small --high=) are usually overkill.  =--low= will produce good
automata most of the time.  Most of pattern formulas of [[file:genltl.org][=genltl=]] will
be efficiently translated in this configuration (meaning that =--small
--high= will not produce a better automaton).  If you are planning to
generate automata for large family of pattern formulas, it makes sense
to experiment with the different settings on a small version of the
pattern, and select the lowest setting that satisfies your
expectations.

673
* Deterministic automata with =--generic --deterministic=
674
675
676
677
678
   :PROPERTIES:
   :CUSTOM_ID: generic
   :END:

   The =--generic= (or =-G=) option allows =ltl2tgba= to use more
679
680
681
682
683
684
685
686
687
   complex acceptance conditions.  This is done by splitting the LTL
   formulas on Boolean connectives to recognize some subformulas that
   are either to translate with different types of acceptance
   conditions, and then combining everything back together.

   Combined with =--deterministic= (or =-D=) this allows the use of a
   determinization algorithm that produces automata with parity
   acceptance.  This is only used for subformulas for which we do not
   know a better way to get a deterministic automaton.
688
689
690
691
692

   For instance =FGa= is the typical formula for which not
   deterministic TGBA exists.

#+NAME: ltl2tgba-fga
693
#+BEGIN_SRC sh :exports code
694
ltl2tgba "FGa" -D -d
695
696
#+END_SRC

697
#+BEGIN_SRC dot :file ltl2tgba-fga.svg :var txt=ltl2tgba-fga :exports results
698
699
700
701
  $txt
#+END_SRC

#+RESULTS:
702
[[file:ltl2tgba-fga.svg]]
703

704
   But with =--generic=, =ltl2tgba= will output the following co-Büchi automaton:
705
706

#+NAME: ltl2tgba-fga-D
707
#+BEGIN_SRC sh :exports code
708
ltl2tgba "FGa" -G -D -d
709
710
#+END_SRC

711
#+BEGIN_SRC dot :file ltl2tgba-fga-D.svg :var txt=ltl2tgba-fga-D :exports results
712
713
714
715
  $txt
#+END_SRC

#+RESULTS:
716
[[file:ltl2tgba-fga-D.svg]]
717

718
719
720
721
722

If we translate =Fb|Gc= as a deterministic automaton with any
acceptance condition, we get a weak and deterministic Büchi automaton:

#+NAME: ltl2tgba-fbgc-D
723
#+BEGIN_SRC sh :exports code
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
ltl2tgba "Fb|Gc" -G -D -d
#+END_SRC

#+BEGIN_SRC dot :file ltl2tgba-fbgc-D.svg :var txt=ltl2tgba-fbgc-D :exports results
  $txt
#+END_SRC

#+RESULTS:
[[file:ltl2tgba-fbgc-D.svg]]


Finally if we translate the conjunction of these two subformulas, a
product of these two automata will be made, producing:

#+NAME: ltl2tgba-fbgcfga-D
739
#+BEGIN_SRC sh :exports code
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
ltl2tgba "(Fb|Gc)&FGa" -G -D -d
#+END_SRC

#+BEGIN_SRC dot :file ltl2tgba-fbgcfga-D.svg :var txt=ltl2tgba-fbgcfga-D :exports results
  $txt
#+END_SRC

#+RESULTS:
[[file:ltl2tgba-fbgcfga-D.svg]]

Disabling the splitting of the original formula LTL formulas can be
done using option =-x ltl-split=0=.  In that case the formula
=(Fb|Gc)&FGa= will be translated into a single TGBA, and because this
TGBA is non-deterministic, it will then be determinized into an
automaton with parity acceptance:

#+NAME: ltl2tgba-fbgcfga-nosplit-D
757
#+BEGIN_SRC sh :exports code
758
759
760
761
762
763
764
765
ltl2tgba "(Fb|Gc)&FGa" -G -D -xltl-split=0 -d
#+END_SRC
#+BEGIN_SRC dot :file ltl2tgba-fbgcfga-nosplit-D.svg :var txt=ltl2tgba-fbgcfga-nosplit-D :exports results
  $txt
#+END_SRC

#+RESULTS:
[[file:ltl2tgba-fbgcfga-nosplit-D.svg]]
766

767
768
769

The [[./man/spot-x.7.html][=spot-x=]](7) man page lists a few =-x= options (=det-scc=,
=det-simul=, =det-stutter=) of the determinization algorithm that are
770
enabled by default, but that you may want to disable for experimental
771
772
773
774
775
purpose.

For instance the following deterministic automaton

#+NAME: ltl2tgba-det1
776
#+BEGIN_SRC sh :exports code
777
ltl2tgba "F(a W FGb)" -G -D -d
778
779
#+END_SRC

780
#+BEGIN_SRC dot :file ltl2tgba-det1.svg :var txt=ltl2tgba-det1 :exports results
781
782
783
784
  $txt
#+END_SRC

#+RESULTS:
785
[[file:ltl2tgba-det1.svg]]
786
787
788
789

would be larger if SCC-based optimizations were disabled:

#+NAME: ltl2tgba-det2
790
#+BEGIN_SRC sh :exports code
791
ltl2tgba "F(a W FGb)" -xdet-scc=0 -G -D -d
792
793
#+END_SRC

794
#+BEGIN_SRC dot :file ltl2tgba-det2.svg :var txt=ltl2tgba-det2 :exports results
795
796
797
798
  $txt
#+END_SRC

#+RESULTS:
799
[[file:ltl2tgba-det2.svg]]
800

801
* Deterministic automata with =--parity --deterministic=
802
803
804
   :PROPERTIES:
   :CUSTOM_ID: parity
   :END:
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834

Using the =--parity= (or upper-case =-P=) option will force the
acceptance condition to be of a parity type.  This has to be
understood in the sense of the HOA format, where:
- multiple parity types are defined (=min odd n=, =min even n=, =max
  odd n=, and =max even n= where =n= is the number of acceptance
  sets), and
- the parity acceptance is only a type of acceptance condition, i.e.,
  a formula expressed in terms of acceptance sets, and does not have
  additional constraints on these sets.  In particular it is not
  necessary the case that each transition or state belongs to exactly
  one acceptance set (this is the "colored" property, see below).

Under these assumptions, Büchi acceptance is just one kind of parity
(in HOA =Buchi= is equivalent to =parity max even 1= or =parity min
even 1=), Rabin with one pair is also a parity acceptance (=Rabin 1=
is equivalent to =parity min odd 2=), and Streett with one pair as
well (=Streett 1= is equivalent to =parity max odd 2=).

In the current implementation, using =ltl2tgba --parity= (without
=--deterministic=) will always produce a Büchi automaton, and when
=--deterministic= (or =-D=) is added, it will produce an deterministic
automaton with Büchi acceptance (=parity min even 1=) or with =parity
min odd n= acceptance, because the latter is the type of parity
acceptance that our determinization procedure outputs.

For instance, =FGa= gets translated into an automaton with =Rabin 1=
acceptance (another name for =parity min odd 2=):

#+NAME: ltl2tgba-dp1
835
#+BEGIN_SRC sh :exports code
836
ltl2tgba "FGa" -D -P -d
837
838
839
840
841
842
843
844
845
846
847
848
849
#+END_SRC

#+BEGIN_SRC dot :file ltl2tgba-dp1.svg :var txt=ltl2tgba-dp1 :exports results
  $txt
#+END_SRC

#+RESULTS:
[[file:ltl2tgba-dp1.svg]]

And =GFa & GFb= gets translated into a =Büchi= automaton (another name
for =parity min even 1=):

#+NAME: ltl2tgba-dp2
850
#+BEGIN_SRC sh :exports code
851
ltl2tgba "GFa & GFb" -D -P -d
852
853
854
855
856
857
858
859
860
861
862
863
864
#+END_SRC

#+BEGIN_SRC dot :file ltl2tgba-dp2.svg :var txt=ltl2tgba-dp2 :exports results
  $txt
#+END_SRC

#+RESULTS:
[[file:ltl2tgba-dp2.svg]]

If we really want to use the same style of parity acceptance for all outputs,
we can specify it as an argument to the =--parity= option.  For instance

#+NAME: ltl2tgba-dp3
865
#+BEGIN_SRC sh :exports code
866
ltl2tgba "GFa & GFb" -D -P'min odd' -d
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
#+END_SRC

#+BEGIN_SRC dot :file ltl2tgba-dp3.svg :var txt=ltl2tgba-dp3 :exports results
  $txt
#+END_SRC

#+RESULTS:
[[file:ltl2tgba-dp3.svg]]


The =--colored-parity= (or lower-case =-p=) option works similarly to
=--parity=, but additionally requests that the automaton be colored.
I.e., each transition (or state if state-based acceptance is
requested) should belong to exactly one acceptance set.

#+NAME: ltl2tgba-dp4
883
#+BEGIN_SRC sh :exports code
884
ltl2tgba "GFa & GFb" -D -p -d
885
886
887
888
889
890
891
892
893
894
#+END_SRC

#+BEGIN_SRC dot :file ltl2tgba-dp4.svg :var txt=ltl2tgba-dp4 :exports results
  $txt
#+END_SRC

#+RESULTS:
[[file:ltl2tgba-dp4.svg]]

#+NAME: ltl2tgba-dp5
895
#+BEGIN_SRC sh :exports code
896
ltl2tgba "GFa & GFb" -D -p'min odd' -d
897
898
899
900
901
902
903
904
905
906
907
908
909
#+END_SRC

#+BEGIN_SRC dot :file ltl2tgba-dp5.svg :var txt=ltl2tgba-dp5 :exports results
  $txt
#+END_SRC

#+RESULTS:
[[file:ltl2tgba-dp5.svg]]

Note that all these options can be combined with state-based
acceptance if needed:

#+NAME: ltl2tgba-dp6
910
#+BEGIN_SRC sh :exports code
911
ltl2tgba "GFa & GFb" -D -S -p'max even' -d
912
913
914
915
916
917
918
919
920
#+END_SRC

#+BEGIN_SRC dot :file ltl2tgba-dp6.svg :var txt=ltl2tgba-dp6 :exports results
  $txt
#+END_SRC

#+RESULTS:
[[file:ltl2tgba-dp6.svg]]

921
922
923
* Translating multiple formulas for statistics

If multiple formulas are given to =ltl2tgba=, the corresponding
924
925
926
927
automata will be output one after the other.  The default output
format HOA is designed to allow streaming automata this way to build
processing pipelines, but Spot's automaton parser can also read a
stream of automata in other formats.
928

929
930
Another situation where passing many formulas to =ltl2tgba= is useful
is in combination with the =--stats=FORMAT= option.  This option will
931
932
933
934
935
output statistics about the translated automata instead of the
automata themselves.  The =FORMAT= string should indicate which
statistics should be output, and how they should be output using the
following sequence of characters (other characters are output as-is):

936
#+BEGIN_SRC sh :exports results
937
ltl2tgba --help | sed -n '/ sequences:/,/^$/p' | sed '1d;$d'
938
939
#+END_SRC
#+RESULTS:
940
#+begin_example
941
942
943
944
  %<                         the part of the line before the formula if it
                             comes from a column extracted from a CSV file
  %>                         the part of the line after the formula if it comes
                             from a column extracted from a CSV file
945
946
  %%                         a single %
  %a                         number of acceptance sets
947
948
949
950
951
952
  %c, %[LETTERS]c            number of SCCs; you may filter the SCCs to count
                             using the following LETTERS, possibly
                             concatenated: (a) accepting, (r) rejecting, (c)
                             complete, (v) trivial, (t) terminal, (w) weak,
                             (iw) inherently weak. Use uppercase letters to
                             negate them.
953
  %d                         1 if the output is deterministic, 0 otherwise
954
  %e                         number of reachable edges
955
  %f                         the formula, in Spot's syntax
956
  %F                         name of the input file
957
958
959
960
961
962
963
964
965
966
967
968
  %g, %[LETTERS]g            acceptance condition (in HOA syntax); add brackets
                             to print an acceptance name instead and LETTERS to
                             tweak the format: (0) no parameters, (a)
                             accentuated, (b) abbreviated, (d) style used in
                             dot output, (g) no generalized parameter, (l)
                             recognize Street-like and Rabin-like, (m) no main
                             parameter, (p) no parity parameter, (o) name
                             unknown acceptance as 'other', (s) shorthand for
                             'lo0'.
  %h                         the automaton in HOA format on a single line (use
                             %[opt]h to specify additional options as in
                             --hoa=opt)
969
970
971
972
  %L                         location in the input file
  %m                         name of the automaton
  %n                         number of nondeterministic states in output
  %p                         1 if the output is complete, 0 otherwise
973
974
975
976
977
978
979
980
  %r                         wall-clock time elapsed in seconds (excluding
                             parsing)
  %R, %[LETTERS]R            CPU time (excluding parsing), in seconds; Add
                             LETTERS to restrict to(u) user time, (s) system
                             time, (p) parent process, or (c) children
                             processes.
  %s                         number of reachable states
  %t                         number of reachable transitions
981
  %w                         one word accepted by the output automaton
982
983
984
985
986
987
988
989
  %x, %[LETTERS]x            number of atomic propositions declared in the
                             automaton;  add LETTERS to list atomic
                             propositions with (n) no quoting, (s) occasional
                             double-quotes with C-style escape, (d)
                             double-quotes with C-style escape, (c)
                             double-quotes with CSV-style escape, (p) between
                             parentheses, any extra non-alphanumeric character
                             will be used to separate propositions
990
#+end_example
991
992
993
994

For instance we can study the size of the automata generated for the
right-nested =U= formulas as follows:

995
#+BEGIN_SRC sh
996
genltl --u-right=1..8 | ltl2tgba --stats '%s states and %e edges for "%f"'
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
#+END_SRC
#+RESULTS:
: 2 states and 2 edges for "p1"
: 2 states and 3 edges for "p1 U p2"
: 3 states and 6 edges for "p1 U (p2 U p3)"
: 4 states and 10 edges for "p1 U (p2 U (p3 U p4))"
: 5 states and 15 edges for "p1 U (p2 U (p3 U (p4 U p5)))"
: 6 states and 21 edges for "p1 U (p2 U (p3 U (p4 U (p5 U p6))))"
: 7 states and 28 edges for "p1 U (p2 U (p3 U (p4 U (p5 U (p6 U p7)))))"
: 8 states and 36 edges for "p1 U (p2 U (p3 U (p4 U (p5 U (p6 U (p7 U p8))))))"

1008
1009
Note that because no formula have been passed as argument to
=ltl2tgba=, it defaulted to reading them from standard input.  Such a
1010
behavior can be requested explicitly with =-F -= if needed (e.g., to
1011
1012
read from standard input in addition to processing other formula
supplied with =-f=).
1013
1014
1015
1016
1017
1018

When computing the size of an automaton, we distinguish /transitions/
and /edges/.  An edge between two states is labeled by a Boolean
formula and may in fact represent several transitions labeled by
compatible Boolean assignment.

1019
1020
1021
For instance if the atomic propositions are =x= and =y=, an edge
labeled by the formula =!x= actually represents two transitions
labeled respectively with =!x&y= and =!x&!y=.
1022
1023
1024
1025
1026

Two automata with the same structures (states and edges) but differing
labels, may have a different count of transitions, e.g., if one has
more restricted labels.

1027
1028
1029
[[file:csv.org][More examples of how to use =--stats= to create CSV
files are on a separate page]].

1030
* Building Monitors
1031
1032
1033
   :PROPERTIES:
   :CUSTOM_ID: monitors
   :END:
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044

In addition to TGBA and BA, =ltl2tgba= can output /monitor/ using the
=-M= option.  These are finite automata that accept all prefixes of a
formula.  The idea is that you can use these automata to monitor a
system as it is running, and report a violation as soon as no
compatible outgoing transition exist.

=ltl2tgba -M= may output non-deterministic monitors while =ltl2tgba
-MD= (short for =--monitor --deterministic=) will output the minimal
deterministic monitor for the given formula.

1045
#+NAME: monitor1
1046
#+BEGIN_SRC sh :exports code
1047
ltl2tgba -M '(Xa & Fb) | Gc' -d
1048
1049
1050
1051
1052
#+END_SRC

#+RESULTS: monitor1
#+begin_example
digraph G {
1053
  rankdir=LR
1054
  node [shape="circle"]
1055
1056
1057
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
1058
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
1059
1060
  I [label="", style=invis, width=0]
  I -> 0
1061
  0 [label=<0>]
1062
1063
  0 -> 1 [label=<1>]
  0 -> 3 [label=<c>]
1064
  1 [label=<1>]
1065
  1 -> 2 [label=<a>]
1066
  2 [label=<2>]
1067
  2 -> 2 [label=<1>]
1068
  3 [label=<3>]
1069
  3 -> 3 [label=<c>]
1070
1071
1072
}
#+end_example

1073
#+BEGIN_SRC dot :file monitor1.svg :var txt=monitor1 :exports results
1074
1075
1076
1077
$txt
#+END_SRC

#+RESULTS:
1078
[[file:monitor1.svg]]
1079

1080
#+NAME: monitor2
1081
#+BEGIN_SRC sh :exports code
1082
ltl2tgba -MD '(Xa & Fb) | Gc' -d
1083
1084
#+END_SRC

1085
#+BEGIN_SRC dot :file monitor2.svg :var txt=monitor2 :exports results
1086
1087
1088
1089
$txt
#+END_SRC

#+RESULTS:
1090
[[file:monitor2.svg]]
1091
1092
1093

Because they accept all finite executions that could be extended to
match the formula, monitor cannot be used to check for eventualities
1094
1095
such as =F(a)=: indeed, any finite execution can be extended to match
=F(a)=.
1096

1097
1098
For more discussion and examples about monitor, see also our [[file:tut11.org][separate
page showing how to build them in Python and C++]].
1099
1100
1101

Because Monitors accept every recognized run (in other words, they
only reject words that are not recognized), it makes little sense to
1102
use option =-C= to request /complete/ monitors.  If you combine =-C=
1103
1104
1105
1106
1107
with =-M=, the result will output as a Büchi automaton if (and only
if) a sink state had to be added.  For instance, here is the
"complete" version of the previous monitor.

#+NAME: monitor3
1108
#+BEGIN_SRC sh :exports code
1109
1110
1111
ltl2tgba -C -M -D '(Xa & Fb) | Gc' -d
#+END_SRC

1112
#+BEGIN_SRC dot :file monitor3.svg :var txt=monitor3 :exports results
1113
1114
1115
1116
$txt
#+END_SRC

#+RESULTS:
1117
[[file:monitor3.svg]]
1118
1119
1120
1121




1122
1123
1124
1125
1126
1127
#  LocalWords:  ltl tgba num toc PSL Büchi automata SRC GFb invis Acc
#  LocalWords:  ltlfilt filenames GraphViz vectorial pdf Tpdf dotex
#  LocalWords:  sed png cmdline Tpng txt iff GFa ba utf UTF lbtt Fb
#  LocalWords:  GraphViz's LBTT's neverclaim SPOT's init goto fi Gb
#  LocalWords:  controled Gc gagbgc disjunction pre rewritings SCC Xa
#  LocalWords:  WDBA determinize degeneralization satisfiability SCCs
1128
1129
1130
1131
1132
#  LocalWords:  genltl nondeterministic eval setenv concat getenv DG
#  LocalWords:  setq html args acc Buchi rankdir fontname Lato svg br
#  LocalWords:  fillcolor ffffa vee arrowsize gba hoaf processings dp
#  LocalWords:  ambig FGa fga fbgc fbgcfga determinized nosplit xltl
#  LocalWords:  det scc simul FGb xdet P'min p'min p'max CSV iw