[Spot] Multiple accepting runs for Buchi Automaton

Alexandre Duret-Lutz aduret at gmail.com
Fri Aug 10 20:26:41 CEST 2018


Hi Thakur,

There is usually an infinite number of accepting runs, so we cannot return
all of them.

Some of the NDFS-based emptiness checks, like SE05, support searching for
another accepting run after returning one.  But this simply works by
continuing the DFS, and does not pretend to return ALL runs.

See the first loop in
https://gitlab.lrde.epita.fr/spot/spot/blob/next/tests/python/misc-ec.py

On Aug 10, 2018 19:09, "Thakur Neupane" <thakur.neupane at aggiemail.usu.edu>
wrote:

Hello,

I am using SPOT to work with Buchi Automaton. Does SPOT supports finding
all the accepting runs instead of only one?

Sincerely,
Thakur Neupane
_______________________________________________
Spot mailing list
Spot at lrde.epita.fr
https://lists.lrde.epita.fr/listinfo/spot
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lrde.epita.fr/pipermail/spot/attachments/20180810/f38a280a/attachment-0001.html>


More information about the Spot mailing list