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