Hi Ayrat,
On Thu, Mar 9, 2017 at 4:17 PM, Ayrat Khalimov ayrat.khalimov@gmail.com wrote:
Is there a way to get more than one accepting run of the product automaton? Ideally would be to have all simple accepting runs, but some cheap heuristics would also do.
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.
how to map edges of the accepting run to the edges of the original product?
Do you mean this:
prod = spot.product(left, right) run = prod.accepting_run(prod) left_run = run.project(left)
or equivalently:
left_run = left.intersecting_run(right)
?
Reading you again, I'm not sure if the question is about a product or any automaton. 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 of equality if the run has been projected as above).
PS: also I think currently none of the emptiness checks look at the label of edges they assume that all labels are different from bddfalse. This might be a flaw. Or we should at least document it. If you are altering left or right in a product, this is OK, because product() will not create bddfalse transitions, but if you are running the emptiness check directly on an automaton with bddfalse-labeled transition, that will fail (I think).