-----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
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.22 (GNU/Linux)
iQEcBAEBAgAGBQJVjAUTAAoJEM0dHSf/6N1YGtEH/R5szUBeK0WfWKCULAiv3Q2P
MKD+AaEsZM0g6ujWLNRzVUnh5DA5WmlzmbFTPPDKEKNtaPO6sKv7ydLfsfh2GWJX
I+tsM7Uzf94hTIuwY9uTAdtSpQIWGflhr3Q6ncV77KEYgaHGFPB0Zg2BaUYtgVZ+
zgglBCowJHoEbj13tX9LlPOLGyzD95TZ8LCG1CBtLwtoy1h/x4jFjB4vEIlXGeyw
q2uEUjF9oz9thA4x/NW8X39s9E/UIi62wZb2nuLK+a8QO5FX3cJQWe4PBZ7fl42m
L8kNEeLEvZ5sH7eznkk/XiHtf/fdB+85DDq/dB8lF335lgt2ES66rvxXk6TRFRM=
=d4aZ
-----END PGP SIGNATURE-----