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