[Spot] Enumerating accepting runs

hi,

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.

I wanted to implement some heuristics [1], but got stuck with the following: how to map edges of the accepting run to the edges of the original product?

(or: states of the accepting run to states of the product?)

thanks!:) ayrat

[1] An heuristics: - get an accepting run, - forbid one edge of that run in the original product (for example, by setting its label to bddfalse), - ask for another accepting run on the thus modified product, - restore that edge and change another edge, and so on.