- Spot - LRE

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

LTL input format in SPOT
by Jianwen Li 02 Mar '15

02 Mar '15

Dear Alexandre: I am trying to figure out whether SPOT can accept boolean assertions such as "x >1". For example, can SPOT recognize the LTL formula F (x > 1), which is accepted by Promela format? I tried it with SPOT by ./ltl2tgba -f "F (x>1)" and SPOT fails to parse it. But I really want to make sure whether I have used it correctly. Many thanks~ -- Best Regards Jianwen Li

2 1

Negation Propagation using Spot library
by Dennis Park 18 Oct '14

18 Oct '14

Hello, My name is Dennis Park and I'm a student at the University of British Columbia. I am using the Spot library in a research project I am currently working on and I wanted to ask whether the Spot library supports negation propagation. More specifically, I would like to take an ltl formula spot::ltl::formula* f and propagate all negations in f so that negations only occur before atomic propositions. Does the Spot library support such a functionality? If so, where in the documentation could I find information on it (I tried to look for something like it in the documentation but had trouble finding anything). Thank you, Dennis Park

2 1

Question sur la simplification de formules LTL
by Amélie DAVID 14 Oct '14

14 Oct '14

Bonjour, Je suis en doctorat d'informatique à l'université d'Evry et je travaille sur la logique ATL. Je viens de découvrir votre outil Spot et en particulier l'outil de simplification des formules. Je suis entrain de développer des méthodes de tableaux pour ATL, et je souhaiterais également pouvoir simplifier les formules fournies en entrée de l'outil. J'aurais donc voulu savoir s'il existait une référence dans la littérature ou une compilation de l'ensemble (ou en tout cas la majorité) de ces simplifications. J'ai beau chercher depuis un petit moment et je n'ai rien trouvé à l'exception de votre outil Spot. Merci d'avance pour l'aide que vous pourriez m'apporter concernant cette question. Bien cordialement, Amélie DAVID

2 1

I'd like to add you to my professional network on LinkedIn
by Jianwen Li 23 Sep '14

23 Sep '14

Hi, I'd like to add you to my professional network on LinkedIn. - Jianwen Accept: http://www.linkedin.com/blink?simpleRedirect=czgSdPsUcjsSdP4Zh4BKrSBQonhFtC… You received an invitation to connect. LinkedIn will use your email address to make suggestions to our members in features like People You May Know. Unsubscribe here: http://www.linkedin.com/blink?simpleRedirect=79Chj8BonhFs6l5cylBp79Ic3gBt6Z… Learn why we included this at the following link: http://www.linkedin.com/blink?simpleRedirect=e3wTd3RAimlIoSBQsC4Ct7dBtmtvpn… © 2014, LinkedIn Corporation. 2029 Stierlin Ct. Mountain View, CA 94043, USA

1 0

[LTL2TGBA] SPOT translation produces unexpected results
by Caroline Lemieux 13 Aug '14

13 Aug '14

Hello, I'm an undergraduate student at UBC working on a log analysis project under Ivan Beschastnikh <http://www.cs.ubc.ca/~bestchai/>. I'm using SPOT in the project to parse LTL strings into formulae, and now trying to use the translation to automata functionality. The situation I'm dealing with would involve passing a finite sequence of states into the automaton, and the description of the Monitor output appeared to be what I needed. However, the monitor DFA provided for the response formula G(a->Fb) was an all-accepting DFA: which didn't seem to align with the given definition of monitor. I've been searching the documentation, but can't find anything more describing why this DFA would be produced. I've also been looking for a description of acceptance condition syntax, especially for the state-based degeneralized Buchi automaton, where both edges and states are labeled as accepting. Could you direct me to any documentation on these subjects or give any insight on why the above monitor is being produced for the response pattern? (As defined by the specification pattern project here <http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml>.) Merci, Caroline Lemieux

2 1