thanks!

I used the enumeration of accepting runs that you suggested. (my tool didn't perform as better as i hoped, but that is my task:)

>> Do you mean this:
>> prod = spot.product(left, right)
>> run = prod.accepting_run(prod)
>> left_run = run.project(left)
>> Anyway to map a edge from a run to its automaton,
>> you'd have to enumerate all the edges that leave the source of the said
>> edge, and locate one that have the same label, acceptance mark, and
>> destination (you might have to check label implication instead

you nailed it! I enumerated the edges of the original automaton and compared the edges
as you suggested. That worked!


thanks for your help,
Ayrat

On Fri, Mar 10, 2017 at 10:45 AM, Alexandre Duret-Lutz <adl@lrde.epita.fr> wrote:
On Thu, Mar 9, 2017 at 6:58 PM, Alexandre Duret-Lutz <adl@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