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.