29 Jun
2015
29 Jun
'15
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.