Hi Ulrich On Thu, Jun 25, 2015 at 3:41 PM, Ulrich Kühne <ulrichk@informatik.uni-bremen.de> wrote:

I have implemented a simple LTL model checker in c++ using SPOT. For a failing property, I can get a counterexample using the method accepting_run() on the emptiness_check_result. Now I am interested in all accepting runs,

A few of the emptiness checks, like CVW90 or SE05 (prefer this one) can be called multiple times: once the emptinesscheck::check() method has returned a first counterexample, you can call it again and it will continue the DFS from where it stopped. This won't enumerate *all* accepting runs (since you may have an infinite number of them), but it should at least give a set of runs that (together) covers all accepting cycles. These two emptiness checks are restricted to Büchi acceptance, so that could be a problem if you have generalized Büchi as input.

or, more precisely in all the states that are part of the prefix of some accepting run.

I don't think you can easily do that with the emptiness_check interface. If your automaton is not too big, you could use scc_map (or scc_info in version 1.99.1) to construct a map of all the SCCs. Then you can construct the set of SCCs that are accepting or that can lead to an accepting SCC, and from this gather all the states. This is essentially what the function scc_filter_states() has to do in order to remove all states that cannot contribute to an accepting run (but usually scc_filter_states() is run only to simplify the property automaton, not on the whole product). -- Alexandre Duret-Lutz