dstar2tgba.org 19.8 KB
Newer Older
1
# -*- coding: utf-8 -*-
2
#+TITLE: =dstar2tgba=
3
#+DESCRIPTION: Spot command-line tool for converting automata into Transition-based Generalized Büchi Automata.
4 5
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
6

7
This tool converts automata into transition-based generalized Büchi
8 9 10 11
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.
12 13

In earlier version (before Spot 1.99.4) =dstar2tgba= was only able to
14 15 16 17 18 19 20 21
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...=.
22 23 24 25 26 27 28 29 30 31


* 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:
32
1. run =ltl2tgba -Ds= to build a Büchi automaton for =(a U b) & GFb=, and then
33 34 35 36 37
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=.

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

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

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

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

89
#+RESULTS: fagfb
90 91
#+begin_example
digraph G {
92
  rankdir=LR
93 94 95 96 97 98 99
  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]
100
  I [label="", style=invis, width=0]
101 102 103 104 105 106 107 108 109 110 111 112 113
  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>]
114 115 116
}
#+end_example

117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132
#+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=):
133 134

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

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

167 168 169 170 171

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=):
172 173 174 175 176 177 178 179 180

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

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

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

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

#+RESULTS: gfafgb
211
#+begin_example
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 243
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>]
}
244 245
#+end_example

246 247 248 249 250 251 252 253 254 255 256 257
#+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:
258

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

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

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

* Details

** General behavior

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

313
  1. read the automaton
314 315 316 317
  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

318 319 320 321
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.)
322

323 324 325 326 327 328 329 330 331 332 333
** 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:
334
:   -B, --ba                   Büchi Automaton (implies -S)
335
:   -C, --complete             output a complete automaton
336
:   -M, --monitor              Monitor (accepts all finite prefixes of the given
337 338 339
:                              property)
:   -S, --state-based-acceptance, --sbacc
:                              define the acceptance using states
340
:       --tgba                 Transition-based Generalized Büchi Automaton
341 342
:                              (default)

343
And these may be refined by a simplification goal, should the
344 345
post-processor routine had a choice to make:
#+BEGIN_SRC sh :results verbatim :exports results
346
dstar2tgba --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d'
347 348
#+END_SRC
#+RESULTS:
349 350
:   -a, --any                  no preference, do not bother making it small or
:                              deterministic
351 352 353 354 355 356 357
:   -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
358
dstar2tgba --help | sed -n '/Simplification level:/,/^$/p' | sed '1d;$d'
359 360 361 362 363 364 365 366 367
#+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.

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

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
436 437
output (Büchi) automaton, =%d=, whether the output automaton is
deterministic, and =%p= whether the automaton is complete.
438 439

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

#+RESULTS:
#+begin_example
453
(b | Fa) R Fc
454
  DRA: 9st.; BA: 9st.; det.? 1; complete? 1
455 456
Ga U (Gc R (!a | Gc))
  DRA: 7st.; BA: 7st.; det.? 0; complete? 0
457 458
GFc
  DRA: 3st.; BA: 3st.; det.? 1; complete? 1
459 460 461 462 463
!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))
464
  DRA: 4st.; BA: 3st.; det.? 1; complete? 0
465 466 467 468 469 470 471 472
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
473 474 475 476 477
#+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=
478 479 480 481 482
(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).
483

484 485 486 487 488 489
** 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
490

491 492 493 494 495 496 497 498 499 500 501 502 503 504
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.
505

506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523
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.
524 525 526 527 528 529 530 531 532

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.

533 534 535 536 537 538 539 540 541
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.
542 543 544

*** Streett to TGBA

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

548 549 550 551 552 553 554 555 556 557 558
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
559 560 561
conversion happens to be deterministic.  This is pure luck: Spot does
not implement any algorithm to preserve the determinism of Streett
automata.