Adding support for promela models via SpinS.

* configure.ac, iface/Makefile.am: Adjust. * iface/dve2/finite.test, iface/dve2/.gitignore, iface/dve2/Makefile.am, iface/dve2/README, iface/dve2/beem-peterson.4.dve, iface/dve2/dve2check.test, iface/dve2/defs.in, iface/dve2/finite.dve, iface/ltsmin/finite.test, iface/dve2/kripke.test, iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc: Move to iface/ltsmin. * iface/ltsmin/.gitignore, iface/ltsmin/Makefile.am, iface/ltsmin/README, iface/ltsmin/beem-peterson.4.dve, iface/ltsmin/check.test, iface/ltsmin/defs.in, iface/ltsmin/finite.dve, iface/ltsmin/finite.test, iface/ltsmin/kripke.test, iface/ltsmin/ltsmin.cc, iface/ltsmin/ltsmin.hh, iface/ltsmin/modelcheck.cc: Factorize dve2 and spins interface in iface/ltsmin/ * iface/ltsmin/elevator2.1.pm, iface/ltsmin/finite.pm: Test promela models. * README: Document iface/ltsmin/ directory.
2014-11-03 15:16:56 +01:00 · 2014-11-03 15:16:56 +01:00 · dd4b821d93
commit dd4b821d93
parent 6dd2749c25
18 changed files with 396 additions and 232 deletions
--- a/iface/ltsmin/.gitignore
+++ b/iface/ltsmin/.gitignore
@ -0,0 +1,7 @@
+*.dve2C
+*.dve.cpp
+defs
+*.dir
+*.spins
+*.c
+check
--- a/iface/ltsmin/Makefile.am
+++ b/iface/ltsmin/Makefile.am
@ -0,0 +1,50 @@
+## Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement
+## de l'Epita (LRDE).
+##
+## This file is part of Spot, a model checking library.
+##
+## Spot is free software; you can redistribute it and/or modify it
+## under the terms of the GNU General Public License as published by
+## the Free Software Foundation; either version 3 of the License, or
+## (at your option) any later version.
+##
+## Spot is distributed in the hope that it will be useful, but WITHOUT
+## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+## or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+## License for more details.
+##
+## You should have received a copy of the GNU General Public License
+## along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+AM_CPPFLAGS = -I$(top_srcdir)/src -I$(top_builddir)/src \
+              $(BUDDY_CPPFLAGS) -I$(top_srcdir)/ltdl
+AM_CXXFLAGS = $(WARNING_CXXFLAGS) -lpthread
+
+ltsmindir = $(pkgincludedir)/iface/ltsmin
+
+ltsmin_HEADERS = ltsmin.hh
+
+lib_LTLIBRARIES = libspotltsmin.la
+libspotltsmin_la_LIBADD = \
+  $(top_builddir)/src/libspot.la \
+  $(top_builddir)/ltdl/libltdlc.la
+libspotltsmin_la_SOURCES = ltsmin.cc
+
+noinst_PROGRAMS = modelcheck
+
+modelcheck_SOURCES = modelcheck.cc
+modelcheck_LDADD = libspotltsmin.la
+
+check_SCRIPTS = defs
+
+TESTS = check.test finite.test kripke.test
+EXTRA_DIST = $(TESTS) beem-peterson.4.dve finite.dve
+
+kripke.test: $(top_builddir)/src/kripketest/parse_print$(EXEEXT)
+
+$(top_builddir)/src/kripketest/parse_print$(EXEEXT):
+	cd $(top_builddir)/src/kripketest && \
+	$(MAKE) $(AM_MAKEFLAGS) parse_print$(EXEEXT)
+
+distclean-local:
+	rm -rf $(TESTS:.test=.dir)
--- a/iface/ltsmin/README
+++ b/iface/ltsmin/README
@ -0,0 +1,198 @@
+This directory contains an interface that presents DiVinE and PROMELA
+models as kripke* objects for Spot.
+
+The DiVinE model checker [http://anna.fi.muni.cz/divine/] has a
+specification language called DVE that makes it easy to model
+processes synchonizing through channels
+[http://anna.fi.muni.cz/divine/language.html].
+
+A lot of models can be found in the BEEM database at
+http://anna.fi.muni.cz/models/
+
+The LTSmin people [http://fmt.cs.utwente.nl/tools/ltsmin/] patched
+DiVinE and SpinJa 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.
+
+
+
+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
+  mkdir _build && cd _build
+  cmake .. -DMURPHI=OFF -DHOARD=OFF -DGUI=OFF -DRX_PATH= -DCMAKE_INSTALL_PREFIX=$HOME/usr
+  make
+  make install
+
+The CMAKE_INSTALL_PREFIX variable is the equivalent of the --prefix
+option of configure scripts.  If you decide to install in $HOME/usr
+like I do, make sure that $HOME/usr/bin is in your PATH.  If you omit
+the CMAKE_INSTALL_PREFIX setting, it will default to /usr/local.
+
+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).
+
+  divine compile --ltsmin model.dve
+
+
+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.
+
+To compile a promela model, simply run the following command:
+  spins model.pm
+
+It should create a dynamic library called model.pm.spins in the
+current directory.
+
+
+Usage with Spot
+===============
+
+  The function load_dve2() defined in dve2.hh in this directory will
+  accept either a model or its compiled version as file argument.  In
+  the former case, it will call "divine compile --ltsmin model.dve" or
+  "spins model.pm" depending on the file extension, only if a compiled
+  model with the corresponding file extension (.dve2C or .spins) does
+  not exist or is older.  Then it will load the compiled model
+  dynamically.
+
+  load_dve2() also requires a set of atomic propositions that should
+  be observed in the model.  These are usually the atomic propositions
+  that occur in the formula to verify, but it might be a larger set.
+
+  There are two kinds of atomic propositions, those that refer to the
+  state of a process, and those that compare the value of a variable.
+  Let's have some example on an excerpt of the beem-peterson.4.dve
+  model included in this directory:
+
+    byte pos[4];
+    byte step[4];
+
+    process P_0 {
+    byte j=0, k=0;
+    state NCS, CS, wait ,q2,q3;
+    init NCS;
+    trans
+     NCS -> wait { effect j = 1; },
+     wait -> q2  { guard j < 4; effect pos[0] = j;},
+     q2 -> q3 { effect step[j-1] = 0, k = 0; },
+     q3 -> q3 { guard k < 4 && (k == 0 || pos[k] < j); effect k = k+1;},
+     q3 -> wait { guard step[j-1] != 0 || k == 4; effect j = j+1;},
+     wait -> CS { guard j == 4; },
+     CS -> NCS { effect pos[0] = 0;};
+    }
+
+  The following atomic propositions could be used in LTL formula:
+
+    P_0.CS          Process P_0 is in state CS.
+    "pos[3] < 3"    Global variable pos[3] is less than 3.
+    "P_0.j >= 2"    Process P_0's variable j is greater or equal to 2.
+    P_0.j           This is equivalent to "P_0.j != 0".
+
+  Comparison operators available are "<", ">", ">=", "<=", "==", and
+  "!=".  The left operand should always be a variable and the right
+  operand should always be a number, so you cannot write something
+  like "P_0.j <= P_0.i".
+
+  Because the LTL parser knows nothing about the details of the
+  languages we interface with, every atomic proposition that cannot be
+  expressed using only alphanumeric characters (plus `_' and `.')
+  should be enclosed in double quote.
+
+  Caveat: "P_0.j >= 2" and " P_0.j>=2" (watch the spaces!) are
+  considered to be two distinct atomic propositions with the same
+  semantics.
+
+
+Examples
+========
+
+  Using the dve2check program built into this directory, we can verify
+  that the critical section is accessed infinitely often by some
+  processes using:
+
+    % ./dve2check beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
+    2239039 unique states visited
+    0 strongly connected components in search stack
+    11449204 transitions explored
+    1024245 items max in DFS search stack
+    no accepting run found
+
+  Process P_0 can starve, waiting to enter in critical section:
+
+     % ./dve2check beem-peterson.4.dve '!G(P_0.wait -> F P_0.CS)'
+     2190 unique states visited
+     34 strongly connected components in search stack
+     4896 transitions explored
+     83 items max in DFS search stack
+     an accepting run exists (use -C to print it)
+
+   Variable pos[1] is not always < 3 (this formula makes no sense, it
+   is just to demonstrate the use of double quote).
+
+     % ./dve2check beem-peterson.4.dve '!G("pos[1] < 3")'
+     130 unique states visited
+     61 strongly connected components in search stack
+     132 transitions explored
+     130 items max in DFS search stack
+     an accepting run exists (use -C to print it)
+
+
+Two state-compression techniques have been implemented as experiments.
+Prefer the -Z option if your model use only non-negative value less
+than 2^28, it is way faster than -z (which will work for all values).
+
+Activating state compression will often reduce runtime.  Compare:
+
+% ./dve2check -T beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
+2239039 unique states visited
+0 strongly connected components in search stack
+11449204 transitions explored
+1024245 items max in DFS search stack
+122102 pages allocated for emptiness check
+no accepting run found
+                       |    user time   |    sys. time   |      total     |
+                  name | ticks        % | ticks        % | ticks        % |   n
+-------------------------------------------------------------------------------
+          loading dve2 |     0      0.0 |     0      0.0 |     0      0.0 |   1
+       parsing formula |     0      0.0 |     0      0.0 |     0      0.0 |   1
+   reducing A_f w/ SCC |     0      0.0 |     0      0.0 |     0      0.0 |   1
+running emptiness chec |  1222    100.0 |    18    100.0 |  1240    100.0 |   1
+   translating formula |     0      0.0 |     0      0.0 |     0      0.0 |   1
+-------------------------------------------------------------------------------
+                 TOTAL |  1222    100.0 |    18    100.0 |  1240    100.0 |
+
+% ./dve2check -T -Z beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
+2239039 unique states visited
+0 strongly connected components in search stack
+11449204 transitions explored
+1024245 items max in DFS search stack
+78580 pages allocated for emptiness check
+no accepting run found
+                       |    user time   |    sys. time   |      total     |
+                  name | ticks        % | ticks        % | ticks        % |   n
+-------------------------------------------------------------------------------
+          loading dve2 |     0      0.0 |     0      0.0 |     0      0.0 |   1
+       parsing formula |     0      0.0 |     0      0.0 |     0      0.0 |   1
+   reducing A_f w/ SCC |     0      0.0 |     0      0.0 |     0      0.0 |   1
+running emptiness chec |  1051    100.0 |    10    100.0 |  1061    100.0 |   1
+   translating formula |     0      0.0 |     0      0.0 |     0      0.0 |   1
+-------------------------------------------------------------------------------
+                 TOTAL |  1051    100.0 |    10    100.0 |  1061    100.0 |
+
+It's a 15% speedup in this case, be the improvement can be more
+important on larger models.
--- a/iface/ltsmin/beem-peterson.4.dve
+++ b/iface/ltsmin/beem-peterson.4.dve
@ -0,0 +1,63 @@
+// peterson mutual exclusion protocol for N processes
+
+// Comes from http://anna.fi.muni.cz/models/cgi/model_info.cgi?name=peterson
+// Also distributed with DiVinE (using dual GPL and BSD licences)
+
+byte pos[4];
+byte step[4];
+
+process P_0 {
+byte j=0, k=0;
+state NCS, CS, wait ,q2,q3;
+init NCS;
+trans
+ NCS -> wait { effect j = 1; },
+ wait -> q2  { guard j < 4; effect pos[0] = j;},
+ q2 -> q3 { effect step[j-1] = 0, k = 0; },
+ q3 -> q3 { guard k < 4 && (k == 0 || pos[k] < j); effect k = k+1;},
+ q3 -> wait { guard step[j-1] != 0 || k == 4; effect j = j+1;},
+ wait -> CS { guard j == 4; },
+ CS -> NCS { effect pos[0] = 0;};
+}
+process P_1 {
+byte j=0, k=0;
+state NCS, CS, wait ,q2,q3;
+init NCS;
+trans
+ NCS -> wait { effect j = 1; },
+ wait -> q2  { guard j < 4; effect pos[1] = j;},
+ q2 -> q3 { effect step[j-1] = 1, k = 0; },
+ q3 -> q3 { guard k < 4 && (k == 1 || pos[k] < j); effect k = k+1;},
+ q3 -> wait { guard step[j-1] != 1 || k == 4; effect j = j+1;},
+ wait -> CS { guard j == 4; },
+ CS -> NCS { effect pos[1] = 0;};
+}
+process P_2 {
+byte j=0, k=0;
+state NCS, CS, wait ,q2,q3;
+init NCS;
+trans
+ NCS -> wait { effect j = 1; },
+ wait -> q2  { guard j < 4; effect pos[2] = j;},
+ q2 -> q3 { effect step[j-1] = 2, k = 0; },
+ q3 -> q3 { guard k < 4 && (k == 2 || pos[k] < j); effect k = k+1;},
+ q3 -> wait { guard step[j-1] != 2 || k == 4; effect j = j+1;},
+ wait -> CS { guard j == 4; },
+ CS -> NCS { effect pos[2] = 0;};
+}
+process P_3 {
+byte j=0, k=0;
+state NCS, CS, wait ,q2,q3;
+init NCS;
+trans
+ NCS -> wait { effect j = 1; },
+ wait -> q2  { guard j < 4; effect pos[3] = j;},
+ q2 -> q3 { effect step[j-1] = 3, k = 0; },
+ q3 -> q3 { guard k < 4 && (k == 3 || pos[k] < j); effect k = k+1;},
+ q3 -> wait { guard step[j-1] != 3 || k == 4; effect j = j+1;},
+ wait -> CS { guard j == 4; },
+ CS -> NCS { effect pos[3] = 0;};
+}
+
+
+system async;
--- a/iface/ltsmin/check.test
+++ b/iface/ltsmin/check.test
@ -0,0 +1,82 @@
+#!/bin/sh
+# Copyright (C) 2011, 2012, 2014 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+
+. ./defs
+
+divine compile > output 2>&1
+
+if grep -i ltsmin output; then
+  :
+else
+  echo "divine not installed, or no ltsmin interface"
+  exit 77
+fi
+
+if ! test -x "$(which spins)"; then
+  echo "spins not installed."
+  exit 77
+fi
+
+set -e
+
+# Promela
+for opt in '' '-z'; do
+
+  run 0 ../modelcheck $opt -E $srcdir/elevator2.1.pm \
+    '!G("req[1]==1" -> (F("p==1" && "cabin_0._pc==2")))'
+  run 0 ../modelcheck $opt -e $srcdir/elevator2.1.pm \
+    'F("p==2")'
+done
+
+# dve2
+for opt in '' '-z'; do
+  # The three examples from the README.
+  # (Don't run the first one using "run 0" because it would take too much
+  # time with valgrind.).
+
+  ../modelcheck $opt -E $srcdir/beem-peterson.4.dve \
+    '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' \
+    | grep -v pages > stdout1
+  # same formula, different syntax.
+  ../modelcheck $opt -E $srcdir/beem-peterson.4.dve \
+    '!GF("P_0==CS"|"P_1 == CS"|"P_2 ==CS"|"P_3==  CS")' \
+    | grep -v pages > stdout2
+  cmp stdout1 stdout2
+  run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.dve \
+    '!G(P_0.wait -> F P_0.CS)'
+  run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")'
+done
+
+# Now check some error messages.
+run 1 ../modelcheck foo.dve "F(P_0.CS)" 2>stderr
+cat stderr
+grep 'Cannot open' stderr
+# the dve2C file was generated in the current directory
+run 1 ../modelcheck beem-peterson.4.dve2C \
+        'Xfoo | P_0.f & X"P_0.k < 2xx" | G"pos[0]"' 2>stderr
+cat stderr
+grep 'variable `foo' stderr
+grep "state \`f'.*P_0" stderr
+grep "Unexpected.*\`xx'" stderr
+grep 'Possible.*CS' stderr
+grep 'Possible.*NCS' stderr
+grep 'Possible.*q2' stderr
+grep 'Possible.*q3' stderr
+grep 'Possible.*wait' stderr
--- a/iface/ltsmin/defs.in
+++ b/iface/ltsmin/defs.in
@ -0,0 +1,89 @@
+# -*- shell-script -*-
+# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
+# Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# et Marie Curie.
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+# Ensure we are running from the right directory.
+test -f ./defs || {
+   echo "defs: not found in current directory" 1>&2
+   exit 1
+}
+
+# If srcdir is not set, then we are not running from `make check'.
+if test -z "$srcdir"; then
+   # compute $srcdir.
+   srcdir=`echo "$0" | sed -e 's,/[^\\/]*$,,'`
+   test $srcdir = $0 && srcdir=.
+fi
+
+# Ensure $srcdir is set correctly.
+test -f $srcdir/defs.in || {
+   echo "$srcdir/defs.in not found, check \$srcdir" 1>&2
+   exit 1
+}
+
+echo "== Running test $0"
+
+me=`echo "$0" | sed -e 's,.*[\\/],,;s/\.test$//'`
+
+testSubDir=$me.dir
+chmod -R a+rwx $testSubDir > /dev/null 2>&1
+rm -rf $testSubDir > /dev/null 2>&1
+mkdir $testSubDir
+cd $testSubDir
+
+# Adjust srcdir now that we are in a subdirectory.  We still want to
+# source directory corresponding to the build directory that contains
+# $testSubDir.
+case $srcdir in
+  # I
+  [\\/$]* | ?:[\\/]* );;
+  *) srcdir=../$srcdir
+esac
+
+DOT='@DOT@'
+top_builddir='../@top_builddir@'
+LBTT="@LBTT@"
+LBTT_TRANSLATE="@LBTT_TRANSLATE@"
+VALGRIND='@VALGRIND@'
+SPIN='@SPIN@'
+LTL2BA='@LTL2BA@'
+
+run()
+{
+  expected_exitcode=$1
+  shift
+  exitcode=0
+  if test -n "$VALGRIND"; then
+    exec 6>valgrind.err
+    GLIBCPP_FORCE_NEW=1 \
+    ../../../libtool --mode=execute \
+    $VALGRIND --tool=memcheck --leak-check=yes --log-fd=6 -q "$@" ||
+      exitcode=$?
+    cat valgrind.err 1>&2
+    test -z "`sed 1q valgrind.err`" || exit 50
+    rm -f valgrind.err
+  else
+    "$@" || exitcode=$?
+  fi
+  test $exitcode = $expected_exitcode || exit 1
+}
+
+set -x
--- a/iface/ltsmin/elevator2.1.pm
+++ b/iface/ltsmin/elevator2.1.pm
@ -0,0 +1,61 @@
+byte req[4];
+int t=0;
+int p=0;
+byte v=0;
+
+
+active proctype cabin() { 
+
+idle: if
+:: v>0; goto mov; 
+
+fi;
+mov: if
+:: t==p; goto open; 
+
+::  d_step {t<p;p = p-1;}  goto mov; 
+
+::  d_step {t>p;p = p+1;}  goto mov; 
+
+fi;
+open: if
+::  d_step {req[p] = 0;v = 0;}  goto idle; 
+
+fi;
+}
+
+active proctype environment() { 
+
+read: if
+::  d_step {req[0]==0;req[0] = 1;}  goto read; 
+
+::  d_step {req[1]==0;req[1] = 1;}  goto read; 
+
+::  d_step {req[2]==0;req[2] = 1;}  goto read; 
+
+::  d_step {req[3]==0;req[3] = 1;}  goto read; 
+
+fi;
+}
+
+active proctype controller() { 
+byte ldir=0;
+
+wait: if
+::  d_step {v==0;t = t+(2*ldir)-1;}  goto work; 
+
+fi;
+work: if
+::  d_step {t<0 || t==4;ldir = 1-ldir;}  goto wait; 
+
+:: t>=0 && t<4 && req[t]==1; goto done; 
+
+::  d_step {t>=0 && t<4 && req[t]==0;t = t+(2*ldir)-1;}  goto work; 
+
+fi;
+done: if
+:: v = 1; goto wait; 
+
+fi;
+}
+
--- a/iface/ltsmin/finite.dve
+++ b/iface/ltsmin/finite.dve
@ -0,0 +1,11 @@
+process P {
+ int a = 0, b = 0;
+ state x;
+ init x;
+
+ trans
+   x -> x { guard a < 3 && b < 3; effect a = a + 1; },
+   x -> x { guard a < 3 && b < 3; effect b = b + 1; };
+}
+
+system async;
--- a/iface/ltsmin/finite.pm
+++ b/iface/ltsmin/finite.pm
@ -0,0 +1,8 @@
+active proctype P() {
+int a = 0;
+int b = 0;
+x: if
+  :: d_step {a < 3 && b < 3; a = a + 1; } goto x;
+  :: d_step {a < 3 && b < 3; b = b + 1; } goto x;
+fi;
+}
--- a/iface/ltsmin/finite.test
+++ b/iface/ltsmin/finite.test
@ -0,0 +1,90 @@
+#!/bin/sh
+# Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+
+. ./defs
+
+divine compile > output 2>&1
+
+if grep -i ltsmin output; then
+  :
+else
+  echo "divine not installed, or no ltsmin interface"
+  exit 77
+fi
+
+if ! test -x "$(which spins)"; then
+  echo "spins not installed."
+  exit 77
+fi
+
+set -e
+run 0 ../modelcheck -gm $srcdir/finite.dve '"P.a < 10"' > stdout
+test `grep ' -> ' stdout | wc -l` = 25
+test `grep 'P.a=' stdout | wc -l` = 15
+
+run 0 ../modelcheck -dtrue -gm $srcdir/finite.dve '"P.a < 10"' > stdout2
+cmp stdout stdout2
+
+run 0 ../modelcheck -dfalse -gm $srcdir/finite.dve '"P.a < 10"' > stdout
+test `grep ' -> ' stdout | wc -l` = 19
+test `grep 'P.a=' stdout | wc -l` = 15
+
+# the same with compressed states
+run 0 ../modelcheck -z -dfalse -gm $srcdir/finite.dve '"P.a < 10"' > stdout
+test `grep ' -> ' stdout | wc -l` = 19
+test `grep 'P.a=' stdout | wc -l` = 15
+
+run 0 ../modelcheck -ddead -E $srcdir/finite.dve \
+  '!(G(dead -> ("P.a==3" | "P.b==3")))'
+
+run 0 ../modelcheck -ddead -e $srcdir/finite.dve \
+  '!(G(dead -> ("P.a==2" | "P.b==3")))'
+
+# This used to segfault because of a bug in
+# tgba_product::transition_annotation.
+run 0 ../modelcheck -gp $srcdir/finite.dve true
+
+# Same tests with finite.pm.
+# Compile it beforehand to avoid compiler's output interference.
+spins $srcdir/finite.pm
+run 0 ../modelcheck -gm $srcdir/finite.pm.spins '"P_0.a < 10"' > stdout
+test `grep ' -> ' stdout | wc -l` = 25
+test `grep 'P_0.a=' stdout | wc -l` = 15
+
+run 0 ../modelcheck -dtrue -gm $srcdir/finite.pm.spins '"P_0.a < 10"' > stdout2
+diff stdout stdout2
+
+run 0 ../modelcheck -dfalse -gm $srcdir/finite.pm.spins '"P_0.a < 10"' > stdout
+test `grep ' -> ' stdout | wc -l` = 19
+test `grep 'P_0.a=' stdout | wc -l` = 15
+
+# the same with compressed states
+run 0 ../modelcheck -z -dfalse -gm $srcdir/finite.pm.spins '"P_0.a < 10"' \
+> stdout
+test `grep ' -> ' stdout | wc -l` = 19
+test `grep 'P_0.a=' stdout | wc -l` = 15
+
+run 0 ../modelcheck -ddead -E $srcdir/finite.pm.spins \
+  '!(G(dead -> ("P_0.a==3" | "P_0.b==3")))'
+
+run 0 ../modelcheck -ddead -e $srcdir/finite.pm.spins \
+  '!(G(dead -> ("P_0.a==2" | "P_0.b==3")))'
+
+run 0 ../modelcheck -gp $srcdir/finite.pm.spins true
--- a/iface/ltsmin/kripke.test
+++ b/iface/ltsmin/kripke.test
@ -0,0 +1,42 @@
+#! /bin/sh
+
+# Copyright (C) 2011 Laboratoire de Recherche et Developpement
+# de l'Epita (LRDE)
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+
+
+. ./defs
+
+divine compile > output 2>&1
+
+if grep -i ltsmin output; then
+  :
+else
+  echo "divine not installed, or no ltsmin interface"
+  exit 77
+fi
+
+set -e
+
+run 0 ../modelcheck -gK ${srcdir}/finite.dve 'F("P.a > 5")' > output
+run 0 ${top_builddir}/src/kripketest/parse_print output | tr -d '"' > output2
+tr -d '"' < output >outputF
+cmp outputF output2
+
+../modelcheck -gK $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")' > outputP
+${top_builddir}/src/tgbatest/ltl2tgba -e -KPoutputP '!G("pos[1] < 3")'
--- a/iface/ltsmin/ltsmin.cc
+++ b/iface/ltsmin/ltsmin.cc
--- a/iface/ltsmin/ltsmin.hh
+++ b/iface/ltsmin/ltsmin.hh
@ -0,0 +1,65 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
+// Developpement de l'Epita (LRDE)
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#ifndef SPOT_IFACE_PROMELA_PROMELA_HH
+# define SPOT_IFACE_PROMELA_PROMELA_HH
+
+#include "kripke/kripke.hh"
+#include "ltlvisit/apcollect.hh"
+#include "ltlast/constant.hh"
+
+
+namespace spot
+{
+
+  // \brief Load a PROMELA model.
+  //
+  // The filename given can be either a *.prom source or a *.spins
+  // dynamic library compiled with "spins file".
+  // When the *.prom source is supplied, the *.spins will be updated
+  // only if it is not newer.
+  //
+  // The dead parameter is used to control the behavior of the model
+  // on dead states (i.e. the final states of finite sequences).
+  // If DEAD is "false", it means we are not
+  // interested in finite sequences of the system, and dead state
+  // will have no successor.  If DEAD is
+  // "true", we want to check finite sequences as well as infinite
+  // sequences, but do not need to distinguish them.  In that case
+  // dead state will have a loop labeled by true.  If DEAD is any
+  // other string, this is the name a property that should be true
+  // when looping on a dead state, and false otherwise.
+  //
+  // This function returns 0 on error.
+  //
+  // \a file the name of the *.prom source file or the dynamic library
+  // \a to_observe the list of atomic propositions that should be observed
+  //               in the model
+  // \a dict the BDD dictionary to use
+  // \a dead an atomic proposition or constant to use for looping on
+  //         dead states
+  // \a verbose whether to output verbose messages
+  SPOT_API kripke_ptr
+  load_model(const std::string& file, const bdd_dict_ptr& dict,
+	    const ltl::atomic_prop_set* to_observe,
+	    const ltl::formula* dead = ltl::constant::true_instance(),
+	    int compress = 0, bool verbose = true);
+}
+
+#endif // SPOT_IFACE_PROMELA_PROMELA_HH
--- a/iface/ltsmin/modelcheck.cc
+++ b/iface/ltsmin/modelcheck.cc
@ -0,0 +1,386 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
+// Developpement de l'Epita (LRDE)
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include "ltsmin.hh"
+#include "tgbaalgos/dotty.hh"
+#include "ltlenv/defaultenv.hh"
+#include "ltlast/allnodes.hh"
+#include "ltlparse/public.hh"
+#include "tgbaalgos/translate.hh"
+#include "tgbaalgos/emptiness.hh"
+#include "tgbaalgos/reducerun.hh"
+#include "tgbaalgos/postproc.hh"
+#include "tgba/tgbaproduct.hh"
+#include "misc/timer.hh"
+#include "misc/memusage.hh"
+#include <cstring>
+#include "kripke/kripkeexplicit.hh"
+#include "kripke/kripkeprint.hh"
+
+static void
+syntax(char* prog)
+{
+  // Display the supplied name unless it appears to be a libtool wrapper.
+  char* slash = strrchr(prog, '/');
+  if (slash && (strncmp(slash + 1, "lt-", 3) == 0))
+    prog = slash + 4;
+
+  std::cerr << "usage: " << prog << " [options] model formula\n\
+\n\
+Options:\n\
+  -dDEAD use DEAD as property for marking DEAD states\n\
+          (by default DEAD = true)\n\
+  -e[ALGO]  run emptiness check, expect an accepting run\n\
+  -E[ALGO]  run emptiness check, expect no accepting run\n\
+  -C     compute an accepting run (Counterexample) if it exists\n\
+  -D     favor a deterministic translation over a small transition\n\
+  -gf    output the automaton of the formula in dot format\n\
+  -gm    output the model state-space in dot format\n\
+  -gK    output the model state-space in Kripke format\n\
+  -gp    output the product state-space in dot format\n\
+  -T     time the different phases of the execution\n\
+  -z     compress states to handle larger models\n\
+  -Z     compress states (faster) assuming all values in [0 .. 2^28-1]\n\
+";
+  exit(1);
+}
+
+int
+checked_main(int argc, char **argv)
+{
+  spot::timer_map tm;
+
+  bool use_timer = false;
+
+  enum { DotFormula, DotModel, DotProduct, EmptinessCheck, Kripke }
+  output = EmptinessCheck;
+  bool accepting_run = false;
+  bool expect_counter_example = false;
+  bool deterministic = false;
+  char *dead = 0;
+  int compress_states = 0;
+
+  const char* echeck_algo = "Cou99";
+
+  int dest = 1;
+  int n = argc;
+  for (int i = 1; i < n; ++i)
+    {
+      char* opt = argv[i];
+      if (*opt == '-')
+	{
+	  switch (*++opt)
+	    {
+	    case 'C':
+	      accepting_run = true;
+	      break;
+	    case 'd':
+	      dead = opt + 1;
+	      break;
+	    case 'D':
+	      deterministic = true;
+	      break;
+	    case 'e':
+	    case 'E':
+	      {
+		echeck_algo = opt + 1;
+		if (!*echeck_algo)
+		  echeck_algo = "Cou99";
+
+		expect_counter_example = (*opt == 'e');
+		output = EmptinessCheck;
+		break;
+	      }
+	    case 'g':
+	      switch (opt[1])
+		{
+		case 'm':
+		  output = DotModel;
+		  break;
+		case 'p':
+		  output = DotProduct;
+		  break;
+		case 'f':
+		  output = DotFormula;
+		  break;
+                case 'K':
+                  output = Kripke;
+                  break;
+		default:
+		  goto error;
+		}
+	      break;
+	    case 'T':
+	      use_timer = true;
+	      break;
+	    case 'z':
+	      compress_states = 1;
+	      break;
+	    case 'Z':
+	      compress_states = 2;
+	      break;
+	    default:
+	    error:
+	      std::cerr << "Unknown option `" << argv[i] << "'." << std::endl;
+	      exit(1);
+	    }
+	  --argc;
+	}
+      else
+	{
+	  argv[dest++] = argv[i];
+	}
+    }
+
+  if (argc != 3)
+    syntax(argv[0]);
+
+  spot::ltl::default_environment& env =
+    spot::ltl::default_environment::instance();
+
+
+  spot::ltl::atomic_prop_set ap;
+  auto dict = spot::make_bdd_dict();
+  spot::const_kripke_ptr model = nullptr;
+  spot::const_tgba_ptr prop = nullptr;
+  spot::const_tgba_ptr product = nullptr;
+  spot::emptiness_check_instantiator_ptr echeck_inst = nullptr;
+  int exit_code = 0;
+  spot::postprocessor post;
+  const spot::ltl::formula* deadf = nullptr;
+  const spot::ltl::formula* f = nullptr;
+
+  if (!dead || !strcasecmp(dead, "true"))
+    {
+      deadf = spot::ltl::constant::true_instance();
+    }
+  else if (!strcasecmp(dead, "false"))
+    {
+      deadf = spot::ltl::constant::false_instance();
+    }
+  else
+    {
+      deadf = env.require(dead);
+    }
+
+  if (output == EmptinessCheck)
+    {
+      const char* err;
+      echeck_inst = spot::make_emptiness_check_instantiator(echeck_algo, &err);
+      if (!echeck_inst)
+	{
+	  std::cerr << "Failed to parse argument of -e/-E near `"
+		    << err <<  "'\n";
+	  exit_code = 1;
+	  goto safe_exit;
+	}
+    }
+
+  tm.start("parsing formula");
+  {
+    spot::ltl::parse_error_list pel;
+    f = spot::ltl::parse(argv[2], pel, env, false);
+    exit_code = spot::ltl::format_parse_errors(std::cerr, argv[2], pel);
+  }
+  tm.stop("parsing formula");
+
+  if (exit_code)
+    goto safe_exit;
+
+  tm.start("translating formula");
+  {
+    spot::translator trans(dict);
+    if (deterministic)
+      trans.set_pref(spot::postprocessor::Deterministic);
+
+    prop = trans.run(&f);
+  }
+  tm.stop("translating formula");
+
+  atomic_prop_collect(f, &ap);
+
+  if (output != DotFormula)
+    {
+      tm.start("loading spins");
+      model = spot::load_model(argv[1], dict, &ap, deadf,
+                               compress_states, true);
+      tm.stop("loading spins");
+
+      if (!model)
+	{
+	  exit_code = 1;
+	  goto safe_exit;
+	}
+
+      if (output == DotModel)
+	{
+	  tm.start("dotty output");
+	  spot::dotty_reachable(std::cout, model);
+	  tm.stop("dotty output");
+	  goto safe_exit;
+	}
+      if (output == Kripke)
+      {
+        tm.start("kripke output");
+	spot::kripke_save_reachable_renumbered(std::cout, model);
+        tm.stop("kripke output");
+        goto safe_exit;
+      }
+    }
+
+  if (output == DotFormula)
+    {
+      tm.start("dotty output");
+      spot::dotty_reachable(std::cout, prop);
+      tm.stop("dotty output");
+      goto safe_exit;
+    }
+
+  product = spot::product(model, prop);
+
+  if (output == DotProduct)
+    {
+      tm.start("dotty output");
+      spot::dotty_reachable(std::cout, product);
+      tm.stop("dotty output");
+      goto safe_exit;
+    }
+
+  assert(echeck_inst);
+
+  {
+    auto ec = echeck_inst->instantiate(product);
+    bool search_many = echeck_inst->options().get("repeated");
+    assert(ec);
+    do
+      {
+	int memused = spot::memusage();
+	tm.start("running emptiness check");
+	spot::emptiness_check_result_ptr res;
+	try
+	  {
+	    res = ec->check();
+	  }
+	catch (std::bad_alloc)
+	  {
+	    std::cerr << "Out of memory during emptiness check."
+		      << std::endl;
+	    if (!compress_states)
+	      std::cerr << "Try option -z for state compression." << std::endl;
+	    exit_code = 2;
+	    exit(exit_code);
+	  }
+	tm.stop("running emptiness check");
+	memused = spot::memusage() - memused;
+
+	ec->print_stats(std::cout);
+	std::cout << memused << " pages allocated for emptiness check"
+		  << std::endl;
+
+	if (expect_counter_example == !res &&
+	    (!expect_counter_example || ec->safe()))
+	  exit_code = 1;
+
+	if (!res)
+	  {
+	    std::cout << "no accepting run found";
+	    if (!ec->safe() && expect_counter_example)
+	      {
+		std::cout << " even if expected" << std::endl;
+		std::cout << "this may be due to the use of the bit"
+			  << " state hashing technique" << std::endl;
+		std::cout << "you can try to increase the heap size "
+			  << "or use an explicit storage"
+			  << std::endl;
+	      }
+	    std::cout << std::endl;
+	    break;
+	  }
+	else if (accepting_run)
+	  {
+
+	    spot::tgba_run_ptr run;
+	    tm.start("computing accepting run");
+	    try
+	      {
+		run = res->accepting_run();
+	      }
+	    catch (std::bad_alloc)
+	      {
+		std::cerr << "Out of memory while looking for counterexample."
+			  << std::endl;
+		exit_code = 2;
+		exit(exit_code);
+	      }
+	    tm.stop("computing accepting run");
+
+	    if (!run)
+	      {
+		std::cout << "an accepting run exists" << std::endl;
+	      }
+	    else
+	      {
+		tm.start("reducing accepting run");
+		run = spot::reduce_run(res->automaton(), run);
+		tm.stop("reducing accepting run");
+
+		tm.start("printing accepting run");
+		spot::print_tgba_run(std::cout, product, run);
+		tm.stop("printing accepting run");
+	      }
+	  }
+	else
+	  {
+	    std::cout << "an accepting run exists "
+		      << "(use -C to print it)" << std::endl;
+	  }
+      }
+    while (search_many);
+  }
+
+ safe_exit:
+  if (f)
+    f->destroy();
+
+  deadf->destroy();
+
+  if (use_timer)
+    tm.print(std::cout);
+  tm.reset_all();		// This helps valgrind.
+  return exit_code;
+}
+
+int
+main(int argc, char **argv)
+{
+  auto exit_code = checked_main(argc, argv);
+
+  // Additional checks to debug reference counts in formulas.
+  spot::ltl::atomic_prop::dump_instances(std::cerr);
+  spot::ltl::unop::dump_instances(std::cerr);
+  spot::ltl::binop::dump_instances(std::cerr);
+  spot::ltl::multop::dump_instances(std::cerr);
+  spot::ltl::bunop::dump_instances(std::cerr);
+  assert(spot::ltl::atomic_prop::instance_count() == 0);
+  assert(spot::ltl::unop::instance_count() == 0);
+  assert(spot::ltl::binop::instance_count() == 0);
+  assert(spot::ltl::multop::instance_count() == 0);
+  assert(spot::ltl::bunop::instance_count() == 0);
+  exit(exit_code);
+}