14 Jan
2022
14 Jan
'22
4:36 p.m.
Hi Clément,
Clément TAMINES <Clement.TAMINES(a)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/fc92c88cdbc6382bbb1e80dbcf1…
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