24 Jun
2015
24 Jun
'15
4:43 p.m.
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
24 Jun
24 Jun
6:25 p.m.
Hi Maximilien,
On Wed, Jun 24, 2015 at 4:43 PM, Colange Maximilien
<maximilien.colange(a)unige.ch> wrote:
I tested the new version of Spot.
Thank you for the feedback.
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.
Do you use/need it?
I removed the library to get rid of the warning with the Debian
packages and because
I noticed that the associated binary (now called modelcheck) was not
installed (and is
not good enough to be installed IMHO). And I assumed nobody would
even notice :-)
But now I see that ltsmin.hh is still installed; so that's definitely
incoherent.
Either I should not install ltsmin.hh, or I should install
libspotltlmin.so as well (in
a separate Debian package I guess).
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.
Yes. There is some information about the internal encoding used on the page
https://spot.lrde.epita.fr/hoa.html#sec-3-2
but currently the API has to be cleaned up and documented. If you have some
idea of short acceptance-related tasks that could be used as examples on
https://spot.lrde.epita.fr/tut.html
and that would be useful to you, please let me know.
--
Alexandre Duret-Lutz
29 Jun
29 Jun
1:36 p.m.
Hi back,
Sorry for the late answer.
On 24/06/15 18:25, Alexandre Duret-Lutz wrote:
I do use this library (not the binary), to load divine models to run my
tests.
Oops, I had missed those. Thanks for the pointers.
--
Maximilien Colange
CUI Université de Genève
Battelle Bâtiment A
route de Drize 7
1227 Carouge SWITZERLAND
Tel: +41 22 379 01 73
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.
Do you
use/need it? I removed the library to get rid of the warning with
the Debian
packages and because
I noticed that the associated binary (now called modelcheck) was not
installed (and is
not good enough to be installed IMHO). And I assumed nobody would
even notice :-)
But now I see that ltsmin.hh is still installed; so that's definitely
incoherent.
Either I should not install ltsmin.hh, or I should install
libspotltlmin.so as well (in
a separate Debian package I guess).
The question is whether spot should provide a
way to load models.
IMHO, having a function in the API to load a divine/promela model is
very useful for rapid testing.
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.
Yes. There is some information about
the internal encoding used on the page
https://spot.lrde.epita.fr/hoa.html#sec-3-2
but currently the API has to be cleaned up and documented. If you have some
idea of short acceptance-related tasks that could be used as examples on
https://spot.lrde.epita.fr/tut.html
and that would be useful to you, please let me know.
3509
days inactive
3514
days old
2 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Colange Maximilien