29 Jun
2015
29 Jun
'15
7:44 p.m.
Hi Ulrich
On Thu, Jun 25, 2015 at 3:41 PM, Ulrich Kühne
<ulrichk(a)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