June 2015 - Spot

Installation of SPOT 1.99.1
by Vitus Lam 30 Jun '15

30 Jun '15

Dear Alexandre, I tried to install SPOT 1.99.1 on Fedora 21. During the execution of the "make" command, the following error returned. How can I fix the compilation issue? make[3]: Entering directory '/home/vituslam/spot-1.99.1/wrap/python' Making all in . make[4]: Entering directory '/home/vituslam/spot-1.99.1/wrap/python' /bin/sh ../../libtool --tag=CXX --mode=compile g++ -DHAVE_CONFIG_H -I. -I../.. -I/usr/include/python3.4m -I../../src -I../../src -I../../buddy/src -DSWIG_TYPE_TABLE=spot -DNDEBUG -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++11 -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -MT spot_impl_wrap.lo -MD -MP -MF .deps/spot_impl_wrap.Tpo -c -o spot_impl_wrap.lo `test -f './spot_impl_wrap.cxx' || echo './'`./spot_impl_wrap.cxx libtool: compile: g++ -DHAVE_CONFIG_H -I. -I../.. -I/usr/include/python3.4m -I../../src -I../../src -I../../buddy/src -DSWIG_TYPE_TABLE=spot -DNDEBUG -fvisibility=hidden -fvisibility-inlines-hidden -DSPOT_BUILD -std=c++11 -g -O3 -ffast-math -fstrict-aliasing -fomit-frame-pointer -MT spot_impl_wrap.lo -MD -MP -MF .deps/spot_impl_wrap.Tpo -c ./spot_impl_wrap.cxx -fPIC -DPIC -o .libs/spot_impl_wrap.o ./spot_impl_wrap.cxx:155:21: fatal error: Python.h: No such file or directory # include <Python.h> ^ compilation terminated. Makefile:1282: recipe for target 'spot_impl_wrap.lo' failed make[4]: *** [spot_impl_wrap.lo] Error 1 make[4]: Leaving directory '/home/vituslam/spot-1.99.1/wrap/python' Makefile:1349: recipe for target 'all-recursive' failed make[3]: *** [all-recursive] Error 1 make[3]: Leaving directory '/home/vituslam/spot-1.99.1/wrap/python' Makefile:1107: recipe for target 'all-recursive' failed make[2]: *** [all-recursive] Error 1 make[2]: Leaving directory '/home/vituslam/spot-1.99.1/wrap' Makefile:1186: recipe for target 'all-recursive' failed make[1]: *** [all-recursive] Error 1 make[1]: Leaving directory '/home/vituslam/spot-1.99.1' Makefile:1109: recipe for target 'all' failed make: *** [all] Error 2 Thanks in advance for your assistance. Vitus Lam

2 3

Multiple (all) accessing runs
by Ulrich Kühne 29 Jun '15

29 Jun '15

-----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-----

2 1

[Bugreport] libspotltsmin is not installed
by Colange Maximilien 29 Jun '15

29 Jun '15

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

2 2

Checkpn
by Alexandre Duret-Lutz 24 Jun '15

24 Jun '15

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

1 0

LTL operator precedence
by Molnár Vince 08 Jun '15

08 Jun '15

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

2 1