- Spot - LRE

Creating bdds
by Miriam Blank 10 Jan '16

10 Jan '16

Hi, Can you please explain the api for creating a bdd? How can I create a bdd? How do I define it? How do I give parameter names so that I can later use it to model check a formula? What is the meaning of bdd_ithvar and bdd_nithvar and the int parameter they receive? I would be very happy if you can supply a simple example. Thank you very much and happy new year, Miriam

2 5

Parsing HOA using Python
by Marcel Walter 10 Jan '16

10 Jan '16

Hi all, I am a masters student of computer science at University of Bremen, Germany. I am working with Büchi-Automata for a study at the moment. Therefore I want to parse an HOA file representing a Büchi-Automaton using Python. It would be great to get an object in Python representing the automaton. So that I can iterate over the states and their edges, read the labels, etc. Can this be done using Spot? If so, how? It would be nice to have a code example. Thank you so much for your help! Best regards from Germany, Marcel Walter

2 2

Python documentation for spot
by Miriam Blank 17 Nov '15

17 Nov '15

Hello, Is there a full documentation of the python api for spot? All I found are the examples in wrap/python/tests. Thank you, Miriam

2 1

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