Hi Clément, Clément TAMINES <Clement.TAMINES(a)umons.ac.be> writes: Thank you for what is, indeed, a bug report. You can find a fix here: https://gitlab.lrde.epita.fr/spot/spot/-/commit/fc92c88cdbc6382bbb1e80dbcf1… I'll include it in Spot 2.10.3. It has no influence on how the accepting run is computed, that code is generic. The reason it's not called Streett is that the HOA format has some peculiar requirements on what "Streett 4" means. It means "(Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & (Fin(4) | Inf(5)) & (Fin(6) | Inf(7))" and nothing else. http://adl.github.io/hoaf/#streett-acceptance So Spot does not recognize your condition as such. But in v2 of the HOA format, Streett 4 should change to mean "(Inf(0) | Fin(1)) & (Inf(2) | Fin(3)) & (Inf(4) | Fin(5)) & (Inf(6) | Fin(7))", so Spot will eventually have to switch and I'm afraid of that change. (We will probably need "Streett" and "Old Streett" and some conversions between those two.) In the meantime, HOA v1 did not define generalized Streett, so I'm using a definition of generalized Streett that is in line with what the future of Streett should be in HOA v2, as discussed here: https://github.com/adl/hoaf/issues/62 https://gitlab.lrde.epita.fr/spot/spot/-/issues/249