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.
Hi Maximilien,
On Wed, Jun 24, 2015 at 4:43 PM, Colange Maximilien maximilien.colange@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.
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.
-
Alexandre Duret-Lutz -
Colange Maximilien