-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
Hi,
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, or, more precisely in all the states that are part of the prefix of some accepting run. What would be the best SPOTish way to obtain these? I would be fine with the runs and find the relevant states myself.
Thanks for any suggestion.
Regards, Ulrich