Hi back,
Sorry for the late answer.
On 24/06/15 18:25, Alexandre Duret-Lutz wrote:
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 do use this library (not the binary), to load divine models to run my tests.
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.
Oops, I had missed those. Thanks for the pointers.