Hi Clément,

Clément TAMINES Clement.TAMINES@umons.ac.be writes:

I created an example (see attached) where, if I am not mistaken, the accepting run that is yielded does not satisfy the acceptance formula. Could you confirm that this is a problem and not a mistake

Thank you for what is, indeed, a bug report. You can find a fix here: https://gitlab.lrde.epita.fr/spot/spot/-/commit/fc92c88cdbc6382bbb1e80dbcf1e... I'll include it in Spot 2.10.3.

In addition, the acceptance formula is somehow detected as being a gen. Streett condition, can this be prevented and does it have an influence on how the emptiness check/accepting run generation is handled ?

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