-----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-----
Hi,
I tested the new version of Spot.
The libspotltsmin is marked as "noinst" in the Makefile.am, and thus
does not install when running make install.
In previous versions, libspotdve2 was installed, so I suppose it is a bug.
Side note: this new version is nice (especially the smart pointers).
Yet, the documentation for accepting conditions API is incomplete, but I
guess it is on the TODO list for the 2.0.
--
Maximilien Colange
CUI Université de Genève
Battelle Bâtiment A
route de Drize 7
1227 Carouge SWITZERLAND
Tel: +41 22 379 01 73
Hi Kerrache,
Kerrach Massipssa wrote:
> I would to ask you a question about Checkpn.
> I compiled Spot (last version) and for Checkpn I do it like this :
> ./configure --with-spot=/usr/local/
>
> And for make I get an error in main.cpp at this ligne
> spot::ltl::formula* f = spot::ltl::parse(ltl_string, pel);
> In fact I just add const to correct the error. But i get
> another error which i don't understand :
> /usr/local//include/spot/tgbaalgos/reachiter.hh:102:
> undefined reference to `spot::tgba_reachable_iterator::~tgba_reachable_iterator()'
>
> Could you help me to solve the problem ? And thank you in advance for response.
CheckPN is not working with any recent version of Spot, and not really
maintained.
The issue is tracked at
https://gitlab.lrde.epita.fr/spot/spot/issues/19
If you really need it and are unable to fix it, I think your best bet
is use older versions
of Spot :-(
--
Alexandre Duret-Lutz
Dear SPOT Developers,
I am writing to you to ask what the operator precedence is that you use for
parsing LTL formulae. As I use SPOT to translate LTL formulae to automata,
but I also need to handle expressions separately, it would be crucial to
stay compatible with your implementation. I am working on .NET, so I cannot
simply use your library as a parser and AST metamodel.
Thank you for your time!
Best regards,
Vince Molnár
