- Spot - LRE

Unambiguous test on empty automata
by Ming-Hsien Tsai 20 Oct '15

20 Oct '15

Dear Spot developers, Attached is an automaton accepting an empty language. I think it is supposed to be unambiguous. But when I ran the following command, I got 0. autfilt --count --is-unambiguous empty.hoa After tracing the code, I found that the problem might be caused by get_init_state_number (called in the product function), which creates a new state if the input automaton has no state. -- Ming-Hsien

2 1

SPOT error in make check
by Christopher Ziegler 24 Aug '15

24 Aug '15

Hello Ladies and Gentlemen, I used your program (SPOT) on Ubuntu 12.4. 32bit, configured it with the two parameters --disable-python and --prefix=/home/my_username (for which I don't need any sudo priviliges to read/write. Then I did make check and the program reported the following: See src/tests/test-suite.log Please report to spot(a)lrde.epita.fr However, I ran make install afterwards, and tried the program and it seems to work. But when I tried to do the same (last week or so), I didn't use the --prefix parameter and I got an error, when I tried to start the program: it said: "error while loading shared libraries: libspot.so.0: cannot open shared object file: No such file or directory" I also include the src/tests/test-suite.log in the attachment. I hope this helps you finding a bug or something. Since the program works for me now, I just wrote you because it said "Please report to spot@..." . If you need more information (for example, which compiler I used etc.) you can write me back. Regards, Christopher Ziegler

2 2

Bug Report
by Oscar Chang 05 Aug '15

05 Aug '15

If you enter (FGa)||(FGb) and tick the option for the degeneralized buchi automaton, it still gives a generalised one.

2 1

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