10 Mar
2017
10 Mar
'17
10:45 a.m.
On Thu, Mar 9, 2017 at 6:58 PM, Alexandre Duret-Lutz <adl(a)lrde.epita.fr> wrote:
Some of the NDFS-based emptiness checks (like SE05)
support having their
check() method called several times and they will restart from where
they stopped, possibly returning more accepting runs. But I'm not sure we
even have a test for this.
I'll try to see if I can demonstrate this in Python and get back to you.
The following seems to report only non-overlapping cycles:
import spot
aut = spot.translate("G(p0 | (p0 R Xp0) | XF(!p0 & p1))", 'BA')
# Note: SE05 should only be used with Büchi acceptance.
ec = spot.make_emptiness_check_instantiator('SE05')[0].instantiate(aut)
while True:
res = ec.check()
if not res:
break
print(res.accepting_run())
--
Alexandre Duret-Lutz