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

6
This tool converts automata into transition-based generalized Büchi
7
8
9
10
automata, a.k.a., TGBA.  It can also produce Büchi automata on request
(=-B=).  It's usage is almost similar to [[file:ltl2tgba.org][=ltl2tgba=]] except that
instead of supplying a formula to translate, you should specify a
filename containing the automaton to convert.
11
12

In earlier version (before Spot 1.99.4) =dstar2tgba= was only able to
13
14
15
16
17
18
19
20
read automata written in [[http://www.ltl2dstar.de/docs/ltl2dstar.html][the format output by =ltl2dstar=]].  However
nowadays it can read automata in any of the supported formats ([[file:hoa.org][HOA]],
LBTT's format, ltl2dstar's format, and never claims).  Also
=dstar2tgba= used to be the only tool being able to read ltl2dstar's
format, but today this format can also be read by any of the tool that
read automata.  So in practice, running =dstar2tgba some files...=
produces the same result as running =autfilt --tgba --high --small
some files...=.
21
22
23
24
25
26
27
28
29
30


* Two quick examples

Here are some brief examples before we discuss the behavior of
=dstar2tgba= in more detail.

** From Rabin to Büchi

The following command instructs =ltl2dstar= to:
31
1. run =ltl2tgba -Ds= to build a Büchi automaton for =(a U b) & GFb=, and then
32
33
34
35
36
2. convert that Büchi automaton into a deterministic Rabin automaton
   (DRA) stored in =fagfb=.
Additionally we use =ltlfilt= to convert our formula to the
prefix format used by =ltl2dstar=.

37
#+BEGIN_SRC sh :results silent :exports both
38
ltlfilt -f '(a U b) & GFb' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - fagfb
39
40
41
#+END_SRC

By looking at the file =fagfb= you can see the =ltl2dsar= actually
42
produced a 4-state DRA:
43
44
45
46
47
48
49
50

#+BEGIN_SRC sh :results verbatim :exports both
cat fagfb
#+END_SRC
#+RESULTS:
#+begin_example
DRA v2 explicit
Comment: "Safra[NBA=3]"
51
States: 4
52
Acceptance-Pairs: 1
53
Start: 2
54
55
56
57
AP: 2 "a" "b"
---
State: 0
Acc-Sig: +0
58
59
3
3
60
61
62
0
0
State: 1
63
64
65
Acc-Sig: -0
1
1
66
67
68
69
1
1
State: 2
Acc-Sig:
70
1
71
72
73
2
0
0
74
75
76
77
78
79
State: 3
Acc-Sig:
3
3
0
0
80
81
#+end_example

82
83
Let's display this automaton with =autfilt=:
#+NAME: fagfb
84
#+BEGIN_SRC sh :results verbatim :exports code
85
autfilt fagfb --dot=.a
86
#+END_SRC
87

88
#+RESULTS: fagfb
89
90
#+begin_example
digraph G {
91
  rankdir=LR
92
93
94
95
96
97
98
  label=<Fin(<font color="#5DA5DA">⓿</font>) &amp; Inf(<font color="#F17CB0">❶</font>)>
  labelloc="t"
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
99
  I [label="", style=invis, width=0]
100
101
102
103
104
105
106
107
108
109
110
111
112
  I -> 2
  0 [label=<0<br/><font color="#F17CB0">❶</font>>]
  0 -> 0 [label=<b>]
  0 -> 3 [label=<!b>]
  1 [label=<1<br/><font color="#5DA5DA">⓿</font>>]
  1 -> 1 [label=<1>]
  2 [label=<2>]
  2 -> 0 [label=<b>]
  2 -> 1 [label=<!a &amp; !b>]
  2 -> 2 [label=<a &amp; !b>]
  3 [label=<3>]
  3 -> 0 [label=<b>]
  3 -> 3 [label=<!b>]
113
114
115
}
#+end_example

116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
#+BEGIN_SRC dot :file fagfb.png :cmdline -Tpng :var txt=fagfb :exports results
$txt
#+END_SRC

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

We used =--dot=a= to display Spot's representation of the acceptance
condition (which uses the same convention as in the [[file:hoa.org][HOA format]]).  The
extra dot is because we use some [[file:oaut.org][environment variables]] to produce a
more colorful output by default in these pages.

=dstar2tgba= can now be used to convert this DRA into a TGBA, a BA, or
a Monitor, using the same options as [[file:ltl2tgba.org][=ltl2tgba=]].

For instance here is the conversion to a Büchi automaton (=-B=):
132
133

#+NAME: fagfb2ba
134
#+BEGIN_SRC sh :results verbatim :exports code
135
dstar2tgba -B fagfb -d
136
137
138
139
#+END_SRC
#+RESULTS: fagfb2ba
#+begin_example
digraph G {
140
  rankdir=LR
141
  node [shape="circle"]
142
143
144
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
145
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
146
  I [label="", style=invis, width=0]
147
  I -> 1
148
  0 [label="0", peripheries=2]
149
150
  0 -> 0 [label=<b>]
  0 -> 2 [label=<!b>]
151
152
153
154
  1 [label="1"]
  1 -> 0 [label=<b>]
  1 -> 1 [label=<a &amp; !b>]
  2 [label="2"]
155
156
  2 -> 0 [label=<b>]
  2 -> 2 [label=<!b>]
157
158
159
160
161
162
163
164
165
}
#+end_example

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

166
167
168
169
170

Note that by default the output is not complete.  Use =-C= if you want
a complete automaton.

But we could as well require the output as a never claim for Spin (option =-s=):
171
172
173
174
175
176
177
178
179

#+BEGIN_SRC sh :results verbatim :exports both
dstar2tgba -s fagfb
#+END_SRC
#+RESULTS:
#+begin_example
never {
T0_init:
  if
180
  :: (b) -> goto accept_S0
181
  :: ((a) && (!(b))) -> goto T0_init
182
  fi;
183
accept_S0:
184
  if
185
186
  :: (b) -> goto accept_S0
  :: (!(b)) -> goto T0_S2
187
  fi;
188
T0_S2:
189
  if
190
191
  :: (b) -> goto accept_S0
  :: (!(b)) -> goto T0_S2
192
193
194
195
196
197
198
199
200
  fi;
}
#+end_example

** Streett to TGBA
:PROPERTIES:
  :CUSTOM_ID: streett_to_tgba_example
:END:

201
Here is the translation of =GFa | GFb= to a 4-state Streett automaton:
202

203
204
#+NAME: gfafgb
#+BEGIN_SRC sh :results verbatim :exports code
205
ltlfilt -f 'GFa & GFb' -l | ltl2dstar --automata=streett --ltl2nba=spin:ltl2tgba@-Ds - gfagfb
206
autfilt --dot=.a gfagfb
207
#+END_SRC
208
209

#+RESULTS: gfafgb
210
#+begin_example
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
digraph G {
  rankdir=LR
  label=<(Fin(<font color="#5DA5DA">⓿</font>) | Inf(<font color="#F17CB0">❶</font>)) &amp; (Fin(<font color="#FAA43A">❷</font>) | Inf(<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><font color="#B276B2">❸</font>>]
  0 -> 0 [label=<a &amp; b>]
  0 -> 1 [label=<!a &amp; b>]
  0 -> 2 [label=<a &amp; !b>]
  0 -> 3 [label=<!a &amp; !b>]
  1 [label=<1<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
  1 -> 0 [label=<a &amp; b>]
  1 -> 1 [label=<!a &amp; b>]
  1 -> 2 [label=<a &amp; !b>]
  1 -> 3 [label=<!a &amp; !b>]
  2 [label=<2<br/><font color="#F17CB0">❶</font><font color="#FAA43A">❷</font>>]
  2 -> 0 [label=<a &amp; b>]
  2 -> 1 [label=<!a &amp; b>]
  2 -> 2 [label=<a &amp; !b>]
  2 -> 3 [label=<!a &amp; !b>]
  3 [label=<3<br/><font color="#5DA5DA">⓿</font><font color="#FAA43A">❷</font>>]
  3 -> 0 [label=<a &amp; b>]
  3 -> 1 [label=<!a &amp; b>]
  3 -> 2 [label=<a &amp; !b>]
  3 -> 3 [label=<!a &amp; !b>]
}
243
244
#+end_example

245
246
247
248
249
250
251
252
253
254
255
256
#+BEGIN_SRC dot :file gfafgb.png :cmdline -Tpng :var txt=gfafgb :exports results
$txt
#+END_SRC

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



And now its conversion by =dstar2tgba= to a 4-state TGBA.
We don't pass any option to =dstar2tgba= because converting to TGBA is
the default:
257

258
#+NAME: gfagfb2ba
259
#+BEGIN_SRC sh :results verbatim :exports code
260
dstar2tgba gfagfb -d
261
262
263
264
#+END_SRC
#+RESULTS: gfagfb2ba
#+begin_example
digraph G {
265
  rankdir=LR
266
  node [shape="circle"]
267
268
269
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
270
  node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
271
272
273
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
274
275
276
277
  0 -> 0 [label=<a &amp; b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
  0 -> 1 [label=<!a &amp; b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
  0 -> 2 [label=<a &amp; !b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
  0 -> 3 [label=<!a &amp; !b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
278
  1 [label="1"]
279
  1 -> 0 [label=<a &amp; b<br/><font color="#F17CB0">❶</font>>]
280
  1 -> 1 [label=<!a &amp; b<br/><font color="#F17CB0">❶</font>>]
281
282
283
284
285
286
287
288
289
290
291
292
  1 -> 2 [label=<a &amp; !b<br/><font color="#F17CB0">❶</font>>]
  1 -> 3 [label=<!a &amp; !b<br/><font color="#F17CB0">❶</font>>]
  2 [label="2"]
  2 -> 0 [label=<a &amp; b<br/><font color="#5DA5DA">⓿</font>>]
  2 -> 1 [label=<!a &amp; b<br/><font color="#5DA5DA">⓿</font>>]
  2 -> 2 [label=<a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
  2 -> 3 [label=<!a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
  3 [label="3"]
  3 -> 0 [label=<a &amp; b>]
  3 -> 1 [label=<!a &amp; b>]
  3 -> 2 [label=<a &amp; !b>]
  3 -> 3 [label=<!a &amp; !b>]
293
294
295
296
297
298
299
300
301
}
#+end_example

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

302
303
304
Obviously the resulting automaton could be simplified further, as the
minimal TGBA for this formula has a single state.  (Patches
welcome...)
305
306
307
308
309

* Details

** General behavior

310
The =dstar2tgba= tool implements a 4-step process:
311

312
  1. read the automaton
313
314
315
316
  2. convert it into TGBA
  3. postprocess the resulting TGBA (simplifying the automaton, a degeneralizing it into a BA or Monitor if requested)
  4. output the resulting automaton

317
318
319
320
BTW, the above scenario is also exactly what you get with [[file:autfilt.org][=autfilt=]] if
you run it as =autfilt --tgba --high --small=.  (This is true only
since version 1.99.4, since both tools can now read the same file
formats.)
321

322
323
324
325
326
327
328
329
330
331
332
** Controlling output

The last two steps are shared with =ltl2tgba= and use the same options.

The type of automaton to produce can be selected using the =-B= or =-M=
switches:
#+BEGIN_SRC sh :results verbatim :exports results
dstar2tgba --help | sed -n '/Output automaton type:/,/^$/p' | sed '1d;$d'
#+END_SRC

#+RESULTS:
333
:   -B, --ba                   Büchi Automaton (implies -S)
334
:   -C, --complete             output a complete automaton
335
:   -M, --monitor              Monitor (accepts all finite prefixes of the given
336
337
338
:                              property)
:   -S, --state-based-acceptance, --sbacc
:                              define the acceptance using states
339
:       --tgba                 Transition-based Generalized Büchi Automaton
340
341
:                              (default)

342
And these may be refined by a simplification goal, should the
343
344
post-processor routine had a choice to make:
#+BEGIN_SRC sh :results verbatim :exports results
345
dstar2tgba --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d'
346
347
#+END_SRC
#+RESULTS:
348
349
:   -a, --any                  no preference, do not bother making it small or
:                              deterministic
350
351
352
353
354
355
356
:   -D, --deterministic        prefer deterministic automata
:       --small                prefer small automata (default)

The effort put into post-processing can be limited with the =--low= or
=--medium= options:

#+BEGIN_SRC sh :results verbatim :exports results
357
dstar2tgba --help | sed -n '/Simplification level:/,/^$/p' | sed '1d;$d'
358
359
360
361
362
363
364
365
366
#+END_SRC
#+RESULTS:
:       --high                 all available optimizations (slow, default)
:       --low                  minimal optimizations (fast)
:       --medium               moderate optimizations

For instance using =-a --low= will skip any optional post-processing,
should you find =dstar2tgba= too slow.

367
Finally, the output format can be changed with the following
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
368
[[file:oaut.org][common ouput options]]:
369
370
371
372
#+BEGIN_SRC sh :results verbatim :exports results
dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
373
374
375
#+begin_example
  -8, --utf8                 enable UTF-8 characters in output (ignored with
                             --lbtt or --spin)
376
377
378
      --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),
379
380
381
382
383
                             '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)
384
385
386
387
388
389
390
                             acceptance sets as bullets, (B) bullets except for
                             Büchi/co-Büchi automata, (c) force circular
                             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)
391
392
393
394
395
396
397
398
399
400
                             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
401
402
403
      --lbtt[=t]             LBTT's format (add =t to force transition-based
                             acceptance even on Büchi automata)
      --name=FORMAT          set the name of the output automaton
404
405
406
407
  -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 '>>'.
  -q, --quiet                suppress all normal output
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
408
409
410
  -s, --spin[=6|c]           Spin neverclaim (implies --ba).  Add letters to
                             select (6) Spin's 6.2.4 style, (c) comments on
                             states
411
412
      --stats=FORMAT         output statistics about the automaton
#+end_example
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434

The =--stats= options can output statistics about the input and the
output automaton, so it can be useful to search for particular
pattern.

For instance here is a complex command that will

1. generate an infinite stream of random LTL formulas with [[file:randltl.org][=randltl=]],
2. use [[file:ltlfilt.org][=ltlfilt=]] to rewrite the W and M operators away (=--remove-wm=),
   simplify the formulas (=-r=), remove duplicates (=u=) as well as
   formulas that have a size less then 3 (=--size-min=3=),
3. use =head= to keep only 10 of such formula
4. loop to process each of these formula:
   - print it
   - then convert the formula into =ltl2dstar='s input format, process
     it with =ltl2dstar= (using =ltl2tgba= as the actual LTL->BA
     transltor), and process the result with =dstar2tgba= to build a
     Büchi automaton (=-B=), favoring determinism if we can (=-D=),
     and finally displaying some statistics about this conversion.

The statistics displayed in this case are: =%S=, the number of states
of the input (Rabin) automaton, =%s=, the number of states of the
435
436
output (Büchi) automaton, =%d=, whether the output automaton is
deterministic, and =%p= whether the automaton is complete.
437
438

#+BEGIN_SRC sh :results verbatim :exports both
439
randltl -n -1 --tree-size=10..14 a b c |
440
441
442
443
444
ltlfilt --remove-wm -r -u --size-min=3 |
head -n 10 |
while read f; do
  echo "$f"
  ltlfilt -l -f "$f" |
445
  ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
446
  dstar2tgba -B --stats='  DRA: %Sst.; BA: %sst.; det.? %d; complete? %p'
447
448
449
450
451
done
#+END_SRC

#+RESULTS:
#+begin_example
452
(b | Fa) R Fc
453
  DRA: 9st.; BA: 9st.; det.? 1; complete? 1
454
455
Ga U (Gc R (!a | Gc))
  DRA: 7st.; BA: 7st.; det.? 0; complete? 0
456
457
GFc
  DRA: 3st.; BA: 3st.; det.? 1; complete? 1
458
459
460
461
462
!a | (a R b)
  DRA: 3st.; BA: 2st.; det.? 1; complete? 0
Xc R (G!c R (b | G!c))
  DRA: 4st.; BA: 2st.; det.? 1; complete? 0
c & G(b | F(a & c))
463
  DRA: 4st.; BA: 3st.; det.? 1; complete? 0
464
465
466
467
468
469
470
471
XXFc
  DRA: 4st.; BA: 4st.; det.? 1; complete? 1
XFc | Gb
  DRA: 5st.; BA: 4st.; det.? 1; complete? 1
G(((!a & Gc) | (a & F!c)) U (!a | Ga))
  DRA: 6st.; BA: 5st.; det.? 1; complete? 1
a & !b
  DRA: 3st.; BA: 2st.; det.? 1; complete? 0
472
473
474
475
476
#+end_example

An important point you should be aware of when comparing these numbers
of states is that the deterministic automata produced by =ltl2dstar=
are complete, while the automata produced by =dstar2tgba=
477
478
479
480
481
(deterministic or not) are not complete by default.  This can explain
a difference of one state (the so called "sink" state).

You can instruct =dstar2tgba= to output a complete automaton using the
=--complete= option (or =-C= for short).
482

483
484
485
486
487
488
** Conversion of various acceptance conditions to TGBA and BA

Spot implements several acceptance conversion algorithms.
There is one generic cases, with some specialized variants.

*** Generic case
489

490
491
492
493
494
495
496
497
498
499
500
501
502
503
The most generic one, called =remove_fin()= in Spot, takes an
automaton with any acceptance condition, and as its name suggests, it
removes all the =Fin(x)= from the acceptance condition: the output is
an automaton whose acceptance conditions is a Boolean combination of
=Inf(x)= acceptance primitive.  (Such automata with Fin-less
acceptance can be easily tested for emptiness using SCC-based
emptiness checks.)  This algorithm works by fist converting the
acceptance conditions into disjunctive normal form, and then removing
any =Fin(x)= acceptance by adding non-deterministic jumps into clones
of the SCCs that intersect set =x=.  This is done with a few tricks
that limits the numbers of clones, and that ensure that the resulting
automaton uses /at most/ one extra acceptance sets.  This algorithm is
not readily available from =dstar2tgba=, but [[file:autfilt.org][=autfilt=]] has an option
=--remove-fin= if you need it.
504

505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
From an automaton with Fin-less acceptance, one can obtain a TGBA
without changing the transitions structure: take the Fin-less
acceptance, transform it into conjunctive normal form (CNF), and
create one new Fin-accepting set for each conjunct of the CNF.  The
combination of these two algorithms is implemented by the
=to_generalized_buchi()= function in Spot.

Finally a TGBA can easily be converted into a BA with classical
degeneralization algorithms (our version of that includes several
SCC-based optimizations described in our [[https://www.lrde.epita.fr/~adl/dl/adl/babiak.13.spin.pdf][SPIN'13 paper]]).

This generalized case is specialized for two types of acceptances that
are common (Rabin and Streett).

*** State-based Rabin to BA

For state-based Rabin automata, and dedicated conversion to BA is
used.
523
524
525
526
527
528
529
530
531

The conversion implemented is a variation of Krishnan et al.'s
"Deterministic ω-Automata vis-a-vis Deterministic Büchi Automata"
(ISAAC'94) paper.  They explain how to convert a deterministic Rabin
automaton (DRA) into a deterministic Büchi automaton (DBA) when such
an automaton exist.  The surprising result is that when a DRA is
DBA-realizable, a DBA can be obtained from the DRA without changing
its transition structure.

532
533
534
535
536
537
538
539
540
Spot implements a slight refinement to the above technique by doing it
SCC-wise: any DRA will be converted into a BA, and the determinism
will be conserved only for strongly connected components where
determinism can be conserved.  (If some SCC is not DBA-realizable, it
will be cloned into several deterministic SCC, but the jumps between
these SCCs will be nondeterministic.)

This specialized conversion is built in the =remove_fin()= procedure
described above.
541
542
543

*** Streett to TGBA

544
545
546
Streett acceptance have a specialized conversion into non-deterministic TGBA.
This improved conversion is automatically used by =to_generalized_buchi()=.

547
548
549
550
551
552
553
554
555
556
557
When a Streett automaton uses multiple acceptance pairs, we use
generalized acceptance conditions in the TGBA to limit the combinatorial
explosion.

A straightforward translation from Streett to BA, as described for
instance by [[http://www.automata.rwth-aachen.de/~loeding/diploma_loeding.pdf][Löding's diploma thesis]], will create a BA with
$|Q|\cdot(4^n-3^n+2)$ states if the input Streett automaton has $|Q|$
states and $n$ acceptance pairs.  Our translation to TGBA limits this
to $|Q|\cdot(2^n+1)$ states.

Sometimes, as in the [[#streett_to_tgba_example][example for =GFa & GFb=]] the output of this
558
559
560
conversion happens to be deterministic.  This is pure luck: Spot does
not implement any algorithm to preserve the determinism of Streett
automata.