Commit 435fec89 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

Merge branch 'master' into next

parents 58389bdb f30c9415
Pipeline #9745 passed with stages
in 364 minutes and 26 seconds
New in spot 2.7.4.dev (not yet released) New in spot 2.7.5.dev (not yet released)
Command-line tools: Command-line tools:
...@@ -55,11 +55,6 @@ New in spot 2.7.4.dev (not yet released) ...@@ -55,11 +55,6 @@ New in spot 2.7.4.dev (not yet released)
helpful to display automata as "graphs", e.g., when illustrating helpful to display automata as "graphs", e.g., when illustrating
algorithms that do not care about labels. 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 - A new complement() function that return automata with unspecified
acceptance condition. The output can be alternating only if the acceptance condition. The output can be alternating only if the
input was alternating. input was alternating.
...@@ -105,8 +100,27 @@ New in spot 2.7.4.dev (not yet released) ...@@ -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") F(G(a & Fb) = FGa & GFb (unless option "reduce_size_strictly")
G(F(a & Gb)) = GFa & FGb (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: 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 - The remove_ap algorithm was preserving the "terminal property" of
automata, but it is possible that a non-terminal input produces a automata, but it is possible that a non-terminal input produces a
terminal output after some propositions are removed. terminal output after some propositions are removed.
......
...@@ -23,6 +23,7 @@ Jan Strejček ...@@ -23,6 +23,7 @@ Jan Strejček
Jean-Michel Couvreur Jean-Michel Couvreur
Jean-Michel Ilié Jean-Michel Ilié
Jeroen Meijer Jeroen Meijer
Jiraphapa Jiravaraphan
Joachim Klein Joachim Klein
Juan Tzintzun Juan Tzintzun
Juraj Major Juraj Major
......
...@@ -21,7 +21,7 @@ ...@@ -21,7 +21,7 @@
# along with this program. If not, see <http://www.gnu.org/licenses/>. # along with this program. If not, see <http://www.gnu.org/licenses/>.
AC_PREREQ([2.61]) 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_AUX_DIR([tools])
AC_CONFIG_MACRO_DIR([m4]) AC_CONFIG_MACRO_DIR([m4])
AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])
......
#+OPTIONS: H:2 num:nil toc:t html-postamble:nil ^:nil #+OPTIONS: H:2 num:nil toc:t html-postamble:nil ^:nil
#+EMAIL: spot@lrde.epita.fr #+EMAIL: spot@lrde.epita.fr
#+HTML_LINK_HOME: index.html #+HTML_LINK_HOME: index.html
#+MACRO: SPOTVERSION 2.7.4 #+MACRO: SPOTVERSION 2.7.5
#+MACRO: LASTRELEASE 2.7.4 #+MACRO: LASTRELEASE 2.7.5
#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.7.4.tar.gz][=spot-2.7.4.tar.gz=]] #+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-4/NEWS][summary of the changes]] #+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-7-5/NEWS][summary of the changes]]
#+MACRO: LASTDATE 2019-04-27 #+MACRO: LASTDATE 2019-06-05
#+ATTR_HTML: :id spotlogo #+ATTR_HTML: :id spotlogo
[[file:spot2.svg]] [[file:spot2.svg]]
The DiVinE model checker [http://anna.fi.muni.cz/divine/] has a The DiVinE 2 model checker
specification language called DVE that makes it easy to model [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 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 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 The LTSmin group [https://ltsmin.utwente.nl/] patched
DiVinE and SpinJa to compile models as dynamic libraries. This dynamic DiVinE and to compile models as dynamic libraries. This dynamic
library provides a very simple C interface (no C++) and extra library provides a very simple C interface (no C++) and extra
information about state variables (name, type, possible values). We information about state variables (name, type, possible values).
use this interface so you will need to install their version of these They also distribute SpinS, a compiler for PROMELA models generating
tools to use Spot with DVE or PROMELA models. dynamic libraries with the same interface.
The source code for our interface is in spot/ltsmin/ and generate a Spot uses this interface so you will need to install their version of
separate library, libspotltsmin.so, that has to be loaded in addition 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 to libspot.so. The current directory contains some testing code based
on a toy modelchecker built upon the above interface: using it require on a toy modelchecker built upon the above interface: using it require
an installation of DiVinE or SpinS (preferably both for testing an installation of DiVinE or SpinS (preferably both for testing
...@@ -27,8 +31,8 @@ Installation of DiVinE ...@@ -27,8 +31,8 @@ Installation of DiVinE
Use the following commands to compile and install the patched version Use the following commands to compile and install the patched version
of DiVinE. of DiVinE.
git clone http://fmt.cs.utwente.nl/tools/scm/divine2.git git clone https://gitlab.lrde.epita.fr/spot/divine-ltsmin-deb
cd divine2 cd divine-ltsmin-deb
mkdir _build && cd _build mkdir _build && cd _build
cmake .. -DMURPHI=OFF -DHOARD=OFF -DGUI=OFF -DRX_PATH= -DCMAKE_INSTALL_PREFIX=$HOME/usr cmake .. -DMURPHI=OFF -DHOARD=OFF -DGUI=OFF -DRX_PATH= -DCMAKE_INSTALL_PREFIX=$HOME/usr
make make
...@@ -45,6 +49,13 @@ DiVinE 2 only compiles with the GNU std C++ library; as a consequence, ...@@ -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 you must provide the option -DCMAKE_CXX_FLAGS="-stdlib=libstdc++" to
the cmake command line. 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 After installation, you can check that compilation works by running
the following command on any DVE model. It should create a file the following command on any DVE model. It should create a file
model.dve2C (which is a dynamic library). model.dve2C (which is a dynamic library).
...@@ -56,10 +67,9 @@ Installation of SpinS ...@@ -56,10 +67,9 @@ Installation of SpinS
====================== ======================
The extended version of SpinJa is called SpinS and should be included The extended version of SpinJa is called SpinS and should be included
with LTSmin. with LTSmin. You can download LTSmin from their website
You can download LTSmin from their website: [http://ltsmin.utwente.nl/] and install it following the INSTALL
[http://fmt.cs.utwente.nl/tools/ltsmin/] and install it following the instructions.
INSTALL instructions.
To compile a promela model, simply run the following command: To compile a promela model, simply run the following command:
spins model.pm spins model.pm
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment