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