dstar2tgba.org 18.5 KB
>] 1 -> 1 [label=<1>] 2 [label=<2>] 2 -> 0 [label=] 2 -> 1 [label=] 2 -> 2 [label=] 3 [label=<3>] 3 -> 0 [label=] 3 -> 3 [label=] Alexandre Duret-Lutz committed Aug 26, 2013 114 115 116 } #+end_example Alexandre Duret-Lutz committed Nov 22, 2017 117 #+BEGIN_SRC dot :file fagfb.svg :var txt=fagfb :exports results Alexandre Duret-Lutz committed Sep 09, 2015 118 119 120 121 $txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 122 [[file:fagfb.svg]] Alexandre Duret-Lutz committed Sep 09, 2015 123 124 125 126 127 =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=): Alexandre Duret-Lutz committed Aug 26, 2013 128 129 #+NAME: fagfb2ba Alexandre Duret-Lutz committed Mar 17, 2015 130 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Jan 08, 2016 131 dstar2tgba -B fagfb -d Alexandre Duret-Lutz committed Aug 26, 2013 132 133 134 135 #+END_SRC #+RESULTS: fagfb2ba #+begin_example digraph G { Alexandre Duret-Lutz committed Jan 06, 2015 136 rankdir=LR Alexandre Duret-Lutz committed Sep 09, 2015 137 node [shape="circle"] Alexandre Duret-Lutz committed Mar 17, 2015 138 139 140 fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] Alexandre Duret-Lutz committed Mar 26, 2015 141 node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] Alexandre Duret-Lutz committed Jan 06, 2015 142 I [label="", style=invis, width=0] Alexandre Duret-Lutz committed Mar 17, 2015 143 I -> 1 Alexandre Duret-Lutz committed Sep 09, 2015 144 0 [label="0", peripheries=2] Alexandre Duret-Lutz committed Mar 17, 2015 145 146 0 -> 0 [label=] 0 -> 2 [label=] Alexandre Duret-Lutz committed Sep 09, 2015 147 148 149 150 1 [label="1"] 1 -> 0 [label=] 1 -> 1 [label=] 2 [label="2"] Alexandre Duret-Lutz committed Mar 17, 2015 151 152 2 -> 0 [label=] 2 -> 2 [label=] Alexandre Duret-Lutz committed Aug 26, 2013 153 154 155 } #+end_example Alexandre Duret-Lutz committed Nov 22, 2017 156 #+BEGIN_SRC dot :file fagfb2ba.svg :var txt=fagfb2ba :exports results Alexandre Duret-Lutz committed Aug 26, 2013 157 158 159$txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 160 [[file:fagfb2ba.svg]] Alexandre Duret-Lutz committed Aug 26, 2013 161 Alexandre Duret-Lutz committed Sep 09, 2015 162 163 164 165 166 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=): Alexandre Duret-Lutz committed Aug 26, 2013 167 168 169 170 171 172 173 174 175 #+BEGIN_SRC sh :results verbatim :exports both dstar2tgba -s fagfb #+END_SRC #+RESULTS: #+begin_example never { T0_init: if Alexandre Duret-Lutz committed Jan 08, 2016 176 :: (b) -> goto accept_S0 Alexandre Duret-Lutz committed Sep 09, 2015 177 :: ((a) && (!(b))) -> goto T0_init Alexandre Duret-Lutz committed Aug 26, 2013 178 fi; Alexandre Duret-Lutz committed Sep 09, 2015 179 accept_S0: Alexandre Duret-Lutz committed Aug 26, 2013 180 if Alexandre Duret-Lutz committed Jan 08, 2016 181 182 :: (b) -> goto accept_S0 :: (!(b)) -> goto T0_S2 Alexandre Duret-Lutz committed Aug 26, 2013 183 fi; Alexandre Duret-Lutz committed Sep 09, 2015 184 T0_S2: Alexandre Duret-Lutz committed Aug 26, 2013 185 if Alexandre Duret-Lutz committed Jan 08, 2016 186 187 :: (b) -> goto accept_S0 :: (!(b)) -> goto T0_S2 Alexandre Duret-Lutz committed Aug 26, 2013 188 189 190 191 192 193 194 195 196 fi; } #+end_example ** Streett to TGBA :PROPERTIES: :CUSTOM_ID: streett_to_tgba_example :END: Alexandre Duret-Lutz committed Sep 09, 2015 197 Here is the translation of =GFa | GFb= to a 4-state Streett automaton: Alexandre Duret-Lutz committed Aug 26, 2013 198 Alexandre Duret-Lutz committed Sep 09, 2015 199 200 #+NAME: gfafgb #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Mar 17, 2015 201 ltlfilt -f 'GFa & GFb' -l | ltl2dstar --automata=streett --ltl2nba=spin:ltl2tgba@-Ds - gfagfb Alexandre Duret-Lutz committed Mar 10, 2018 202 autfilt --dot gfagfb Alexandre Duret-Lutz committed Aug 26, 2013 203 #+END_SRC Alexandre Duret-Lutz committed Sep 09, 2015 204 Alexandre Duret-Lutz committed Nov 22, 2017 205 #+BEGIN_SRC dot :file gfafgb.svg :var txt=gfafgb :exports results Alexandre Duret-Lutz committed Sep 09, 2015 206 207 208 209 $txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 210 [[file:gfafgb.svg]] Alexandre Duret-Lutz committed Sep 09, 2015 211 212 213 214 215 216 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: Alexandre Duret-Lutz committed Aug 26, 2013 217 Alexandre Duret-Lutz committed Mar 17, 2015 218 #+NAME: gfagfb2ba Alexandre Duret-Lutz committed Aug 26, 2013 219 #+BEGIN_SRC sh :results verbatim :exports code Alexandre Duret-Lutz committed Jan 08, 2016 220 dstar2tgba gfagfb -d Alexandre Duret-Lutz committed Aug 26, 2013 221 222 223 224 #+END_SRC #+RESULTS: gfagfb2ba #+begin_example digraph G { Alexandre Duret-Lutz committed Jan 06, 2015 225 rankdir=LR Alexandre Duret-Lutz committed Sep 09, 2015 226 node [shape="circle"] Alexandre Duret-Lutz committed Mar 17, 2015 227 228 229 fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] Alexandre Duret-Lutz committed Mar 26, 2015 230 node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] Alexandre Duret-Lutz committed Jan 06, 2015 231 232 233 I [label="", style=invis, width=0] I -> 0 0 [label="0"] Alexandre Duret-Lutz committed Sep 09, 2015 234 235 236 237 0 -> 0 [label=>] 0 -> 1 [label=>] 0 -> 2 [label=>] 0 -> 3 [label=>] Alexandre Duret-Lutz committed Aug 26, 2013 238 1 [label="1"] Alexandre Duret-Lutz committed Sep 09, 2015 239 1 -> 0 [label=>] Alexandre Duret-Lutz committed Mar 17, 2015 240 1 -> 1 [label=>] Alexandre Duret-Lutz committed Sep 09, 2015 241 242 243 244 245 246 247 248 249 250 251 252 1 -> 2 [label=>] 1 -> 3 [label=>] 2 [label="2"] 2 -> 0 [label=>] 2 -> 1 [label=>] 2 -> 2 [label=>] 2 -> 3 [label=>] 3 [label="3"] 3 -> 0 [label=] 3 -> 1 [label=] 3 -> 2 [label=] 3 -> 3 [label=] Alexandre Duret-Lutz committed Aug 26, 2013 253 254 255 } #+end_example Alexandre Duret-Lutz committed Nov 22, 2017 256 #+BEGIN_SRC dot :file gfagfb2ba.svg :var txt=gfagfb2ba :exports results Alexandre Duret-Lutz committed Aug 26, 2013 257 258 259$txt #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Nov 22, 2017 260 [[file:gfagfb2ba.svg]] Alexandre Duret-Lutz committed Aug 26, 2013 261 Alexandre Duret-Lutz committed Sep 09, 2015 262 263 264 Obviously the resulting automaton could be simplified further, as the minimal TGBA for this formula has a single state. (Patches welcome...) Alexandre Duret-Lutz committed Aug 26, 2013 265 266 267 268 269 * Details ** General behavior Alexandre Duret-Lutz committed Sep 09, 2015 270 The =dstar2tgba= tool implements a 4-step process: Alexandre Duret-Lutz committed Aug 26, 2013 271 Alexandre Duret-Lutz committed Sep 09, 2015 272 1. read the automaton Alexandre Duret-Lutz committed Aug 26, 2013 273 274 275 276 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 Alexandre Duret-Lutz committed Jan 08, 2016 277 278 279 280 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.) Alexandre Duret-Lutz committed Sep 09, 2015 281 Alexandre Duret-Lutz committed Aug 26, 2013 282 283 284 285 286 287 288 289 290 291 292 ** 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: Alexandre Duret-Lutz committed Jan 08, 2016 293 : -B, --ba Büchi Automaton (implies -S) Alexandre Duret-Lutz committed Oct 26, 2015 294 : -C, --complete output a complete automaton Alexandre Duret-Lutz committed Aug 26, 2013 295 : -M, --monitor Monitor (accepts all finite prefixes of the given Alexandre Duret-Lutz committed Oct 26, 2015 296 297 298 : property) : -S, --state-based-acceptance, --sbacc : define the acceptance using states Alexandre Duret-Lutz committed Jan 08, 2016 299 : --tgba Transition-based Generalized Büchi Automaton Alexandre Duret-Lutz committed Aug 26, 2013 300 301 : (default) Alexandre Duret-Lutz committed Oct 26, 2015 302 And these may be refined by a simplification goal, should the Alexandre Duret-Lutz committed Aug 26, 2013 303 304 post-processor routine had a choice to make: #+BEGIN_SRC sh :results verbatim :exports results Alexandre Duret-Lutz committed Oct 26, 2015 305 dstar2tgba --help | sed -n '/Simplification goal:/,/^$/p' | sed '1d;$d' Alexandre Duret-Lutz committed Aug 26, 2013 306 307 #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Oct 26, 2015 308 309 : -a, --any no preference, do not bother making it small or : deterministic Alexandre Duret-Lutz committed Aug 26, 2013 310 311 312 313 314 315 316 : -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 Alexandre Duret-Lutz committed Oct 26, 2015 317 dstar2tgba --help | sed -n '/Simplification level:/,/^$/p' | sed '1d;$d' Alexandre Duret-Lutz committed Aug 26, 2013 318 319 320 321 322 323 324 325 326 #+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. Alexandre Duret-Lutz committed Jan 06, 2015 327 Finally, the output format can be changed with the following Alexandre Duret-Lutz committed Jul 17, 2015 328 [[file:oaut.org][common ouput options]]: Alexandre Duret-Lutz committed Aug 26, 2013 329 330 331 332 #+BEGIN_SRC sh :results verbatim :exports results dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: Alexandre Duret-Lutz committed Jan 06, 2015 333 334 335 #+begin_example -8, --utf8 enable UTF-8 characters in output (ignored with --lbtt or --spin) Alexandre Duret-Lutz committed Sep 09, 2015 336 337 338 --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), Alexandre Duret-Lutz committed Jan 08, 2016 339 340 341 342 343 '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 committed Sep 09, 2015 344 345 346 347 348 349 350 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) Alexandre Duret-Lutz committed Jan 08, 2016 351 352 353 354 355 356 357 358 359 360 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 Alexandre Duret-Lutz committed Jan 06, 2015 361 362 363 --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 Alexandre Duret-Lutz committed Sep 09, 2015 364 365 366 367 -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 committed Jan 31, 2015 368 369 370 -s, --spin[=6|c] Spin neverclaim (implies --ba). Add letters to select (6) Spin's 6.2.4 style, (c) comments on states Alexandre Duret-Lutz committed Jan 06, 2015 371 372 --stats=FORMAT output statistics about the automaton #+end_example Alexandre Duret-Lutz committed Aug 26, 2013 373 374 375 376 377 378 379 380 381 382 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 Alexandre Duret-Lutz committed Jul 19, 2016 383 384 385 formulas that have a size less then 3 (=--size-min=3=), and keep only the 10 first formulas (=-n 10=) 3. loop to process each of these formula: Alexandre Duret-Lutz committed Aug 26, 2013 386 387 388 389 390 391 392 393 394 - 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 Alexandre Duret-Lutz committed Sep 08, 2013 395 396 output (Büchi) automaton, =%d=, whether the output automaton is deterministic, and =%p= whether the automaton is complete. Alexandre Duret-Lutz committed Aug 26, 2013 397 398 #+BEGIN_SRC sh :results verbatim :exports both Alexandre Duret-Lutz committed Jan 06, 2015 399 randltl -n -1 --tree-size=10..14 a b c | Alexandre Duret-Lutz committed Jul 19, 2016 400 ltlfilt --remove-wm -r -u --size-min=3 -n 10 | Alexandre Duret-Lutz committed Aug 26, 2013 401 402 403 while read f; do echo "$f" ltlfilt -l -f "$f" | Alexandre Duret-Lutz committed Jul 17, 2015 404 ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - | Alexandre Duret-Lutz committed Sep 08, 2013 405 dstar2tgba -B --stats=' DRA: %Sst.; BA: %sst.; det.? %d; complete? %p' Alexandre Duret-Lutz committed Aug 26, 2013 406 407 408 409 410 done #+END_SRC #+RESULTS: #+begin_example Alexandre Duret-Lutz committed Mar 17, 2015 411 (b | Fa) R Fc Alexandre Duret-Lutz committed Sep 09, 2015 412 DRA: 9st.; BA: 9st.; det.? 1; complete? 1 Alexandre Duret-Lutz committed Mar 17, 2015 413 414 Ga U (Gc R (!a | Gc)) DRA: 7st.; BA: 7st.; det.? 0; complete? 0 Alexandre Duret-Lutz committed Jan 06, 2015 415 416 GFc DRA: 3st.; BA: 3st.; det.? 1; complete? 1 Alexandre Duret-Lutz committed Mar 17, 2015 417 418 419 420 421 !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)) Alexandre Duret-Lutz committed Sep 09, 2015 422 DRA: 4st.; BA: 3st.; det.? 1; complete? 0 Alexandre Duret-Lutz committed Mar 17, 2015 423 424 425 426 427 428 429 430 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 Alexandre Duret-Lutz committed Aug 26, 2013 431 432 433 434 435 #+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= Alexandre Duret-Lutz committed Sep 08, 2013 436 437 438 439 440 (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). Alexandre Duret-Lutz committed Aug 26, 2013 441 Alexandre Duret-Lutz committed Sep 09, 2015 442 443 444 445 446 447 ** 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 Alexandre Duret-Lutz committed Aug 26, 2013 448 Alexandre Duret-Lutz committed Sep 09, 2015 449 450 451 452 453 454 455 456 457 458 459 460 461 462 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. Alexandre Duret-Lutz committed Aug 26, 2013 463 Alexandre Duret-Lutz committed Sep 09, 2015 464 465 466 467 468 469 470 471 472 473 474 475 476 477 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). Alexandre Duret-Lutz committed Apr 02, 2019 478 *** Rabin to BA Alexandre Duret-Lutz committed Sep 09, 2015 479 Alexandre Duret-Lutz committed Apr 02, 2019 480 481 482 483 484 When the input is a Rabin automaton, a dedicated conversion to BA is used. This procedure actually works for input that is called Rabin-like, i.e., any acceptance formula that can easily be converted to Rabin by adding some extra Fin or Inf terms to the acceptance conditions and ensuring that those terms are always true. Alexandre Duret-Lutz committed Aug 26, 2013 485 486 487 488 489 490 491 492 493 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. Alexandre Duret-Lutz committed Sep 09, 2015 494 495 496 497 498 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 Alexandre Duret-Lutz committed Apr 02, 2019 499 500 these SCCs will be nondeterministic.) Our implementation also work on automata with transition-based acceptance. Alexandre Duret-Lutz committed Sep 09, 2015 501 502 503 This specialized conversion is built in the =remove_fin()= procedure described above. Alexandre Duret-Lutz committed Aug 26, 2013 504 505 506 *** Streett to TGBA Alexandre Duret-Lutz committed Sep 09, 2015 507 508 509 Streett acceptance have a specialized conversion into non-deterministic TGBA. This improved conversion is automatically used by =to_generalized_buchi()=. Alexandre Duret-Lutz committed Aug 26, 2013 510 511 512 513 514 515 516 517 518 519 520 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 Alexandre Duret-Lutz committed Mar 17, 2015 521 522 523 conversion happens to be deterministic. This is pure luck: Spot does not implement any algorithm to preserve the determinism of Streett automata.