diff --git a/NEWS b/NEWS index 06a736191..af4716521 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.7.4.dev (not yet released) +New in spot 2.7.5.dev (not yet released) Command-line tools: @@ -55,11 +55,6 @@ New in spot 2.7.4.dev (not yet released) helpful to display automata as "graphs", e.g., when illustrating algorithms that do not care about labels. - - print_dot will replace labels that have more 2048 characters by a - "(label too long)" string. This works around a limitation of - GraphViz that aborts when some label exceeds 16k characters, and - also helps making large automata more readable. - - A new complement() function that return automata with unspecified acceptance condition. The output can be alternating only if the input was alternating. @@ -105,8 +100,27 @@ New in spot 2.7.4.dev (not yet released) F(G(a & Fb) = FGa & GFb (unless option "reduce_size_strictly") G(F(a & Gb)) = GFa & FGb (unless option "reduce_size_strictly") +New in spot 2.7.5 (2019-06-05) + + Build: + + - Although the Python bindings in this release are still done with + Swig3.0, the code has been updated to be compatible with Swig4.0. + + Library: + + - print_dot will replace labels that have more 2048 characters by a + "(label too long)" string. This works around a limitation of + GraphViz that aborts when some label exceeds 16k characters, and + also helps making large automata more readable. + Bugs fixed: + - spot::translator was not applying Boolean sub-formula rewritting + by default unless a spot::option_map was passed. This caused some + C++ code for translating certains formulas to be noticeably slower + than the equivalent call to the ltl2tgba binary. + - The remove_ap algorithm was preserving the "terminal property" of automata, but it is possible that a non-terminal input produces a terminal output after some propositions are removed. diff --git a/THANKS b/THANKS index c2a5b2bd9..8fb1916d6 100644 --- a/THANKS +++ b/THANKS @@ -23,6 +23,7 @@ Jan Strejček Jean-Michel Couvreur Jean-Michel Ilié Jeroen Meijer +Jiraphapa Jiravaraphan Joachim Klein Juan Tzintzun Juraj Major diff --git a/configure.ac b/configure.ac index 9f06439b9..ef02dc9e2 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.7.4.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.7.5.dev], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests]) diff --git a/doc/org/setup.org b/doc/org/setup.org index 0309bd846..99ebf2ff1 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -1,11 +1,11 @@ #+OPTIONS: H:2 num:nil toc:t html-postamble:nil ^:nil #+EMAIL: spot@lrde.epita.fr #+HTML_LINK_HOME: index.html -#+MACRO: SPOTVERSION 2.7.4 -#+MACRO: LASTRELEASE 2.7.4 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.7.4.tar.gz][=spot-2.7.4.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-7-4/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2019-04-27 +#+MACRO: SPOTVERSION 2.7.5 +#+MACRO: LASTRELEASE 2.7.5 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.7.5.tar.gz][=spot-2.7.5.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-7-5/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2019-06-05 #+ATTR_HTML: :id spotlogo [[file:spot2.svg]] diff --git a/tests/ltsmin/README b/tests/ltsmin/README index cf603d264..9947a9e84 100644 --- a/tests/ltsmin/README +++ b/tests/ltsmin/README @@ -1,20 +1,24 @@ -The DiVinE model checker [http://anna.fi.muni.cz/divine/] has a -specification language called DVE that makes it easy to model +The DiVinE 2 model checker +[http://web.archive.org/web/20120723095042/http://divine.fi.muni.cz/index.html] +used to have a specification language called DVE, for modelling processes synchonizing through channels -[http://anna.fi.muni.cz/divine/language.html]. +[http://web.archive.org/web/20120723095115/http://divine.fi.muni.cz/language.html]. A lot of models can be found in the BEEM database at -http://anna.fi.muni.cz/models/ +http://paradise.fi.muni.cz/beem/ -The LTSmin group [http://fmt.cs.utwente.nl/tools/ltsmin/] patched -DiVinE and SpinJa to compile models as dynamic libraries. This dynamic +The LTSmin group [https://ltsmin.utwente.nl/] patched +DiVinE and to compile models as dynamic libraries. This dynamic library provides a very simple C interface (no C++) and extra -information about state variables (name, type, possible values). We -use this interface so you will need to install their version of these -tools to use Spot with DVE or PROMELA models. +information about state variables (name, type, possible values). +They also distribute SpinS, a compiler for PROMELA models generating +dynamic libraries with the same interface. -The source code for our interface is in spot/ltsmin/ and generate a -separate library, libspotltsmin.so, that has to be loaded in addition +Spot uses this interface so you will need to install their version of +these tools to use Spot with DVE or PROMELA models. + +The source code for our interface is in spot/ltsmin/ and generates a +separate library, libspotltsmin.so, that has to be linked in addition to libspot.so. The current directory contains some testing code based on a toy modelchecker built upon the above interface: using it require an installation of DiVinE or SpinS (preferably both for testing @@ -27,8 +31,8 @@ Installation of DiVinE Use the following commands to compile and install the patched version of DiVinE. - git clone http://fmt.cs.utwente.nl/tools/scm/divine2.git - cd divine2 + git clone https://gitlab.lrde.epita.fr/spot/divine-ltsmin-deb + cd divine-ltsmin-deb mkdir _build && cd _build cmake .. -DMURPHI=OFF -DHOARD=OFF -DGUI=OFF -DRX_PATH= -DCMAKE_INSTALL_PREFIX=$HOME/usr make @@ -45,6 +49,13 @@ DiVinE 2 only compiles with the GNU std C++ library; as a consequence, you must provide the option -DCMAKE_CXX_FLAGS="-stdlib=libstdc++" to the cmake command line. +The above git repository is our own copy of the LTSmin fork of Divine, +that we patched to generate Debian packages for amd64. If you use +our Debian repository [https://spot.lrde.epita.fr/install.html#Debian] +you can actually install this version of divine with just: + + apt-get install divine-ltsmin + After installation, you can check that compilation works by running the following command on any DVE model. It should create a file model.dve2C (which is a dynamic library). @@ -56,10 +67,9 @@ Installation of SpinS ====================== The extended version of SpinJa is called SpinS and should be included -with LTSmin. -You can download LTSmin from their website: -[http://fmt.cs.utwente.nl/tools/ltsmin/] and install it following the -INSTALL instructions. +with LTSmin. You can download LTSmin from their website +[http://ltsmin.utwente.nl/] and install it following the INSTALL +instructions. To compile a promela model, simply run the following command: spins model.pm