ltsmin: fix test cases and naming.

* iface/ltsmin/kripke.test: Fix detection of divine's ltsmin option.
* iface/ltsmin/finite.test: Likewise.  Also extra the Spins test
into...
* iface/ltsmin/finite2.test: ... this new file, so that we
can test the divine and spins interfaces independently.
* iface/ltsmin/Makefile.am: Distribute finite2.test and finite.pm.
* iface/ltsmin/ltsmin.cc, iface/ltsmin/ltsmin.hh,
iface/ltsmin/modelcheck.cc: Adjust function names.

NEWS

@@ -53,6 +53,11 @@ New in spot 1.99a (not yet released)
       and transition of an automaton at random.  It can be
       used from the command-line using "autfilt --randomize".
 
+    - the interface in iface/dve2 has been renamed to iface/ltsmin
+      because it can now interface the dynamic libraries created
+      either by Divine (as patched by the LTSmin people) or by
+      Spins (the LTSmin compiler for Promela).
+
     - Spot is now compiling in C++11 mode.  The set of features we use
       requires GCC >= 4.6 or Clang >= 3.1.  These minimum versions
       are old enough that it should not be an issue to most people.

iface/ltsmin/Makefile.am

@@ -1,4 +1,4 @@
-## Copyright (C) 2011, 2013 Laboratoire de Recherche et Developpement
+## Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et Developpement
 ## de l'Epita (LRDE).
 ##
 ## This file is part of Spot, a model checking library.
@@ -37,8 +37,8 @@ modelcheck_LDADD = libspotltsmin.la
 
 check_SCRIPTS = defs
 
-TESTS = check.test finite.test kripke.test
+TESTS = check.test finite.test finite2.test kripke.test
-EXTRA_DIST = $(TESTS) beem-peterson.4.dve finite.dve
+EXTRA_DIST = $(TESTS) beem-peterson.4.dve finite.dve finite.pm
 
 kripke.test: $(top_builddir)/src/kripketest/parse_print$(EXEEXT)
 

iface/ltsmin/finite.test

@@ -1,5 +1,6 @@
 #!/bin/sh
-# Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement
+# -*- coding: utf-8 -*-
+# Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -22,18 +23,13 @@
 
 divine compile > output 2>&1
 
-if grep -i ltsmin output; then
+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
@@ -60,31 +56,3 @@ run 0 ../modelcheck -ddead -e $srcdir/finite.dve \
 # 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

iface/ltsmin/finite2.test

@@ -0,0 +1,54 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2011, 2013, 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/>.
+
+#These are the same tests as in finite.test, except with Spins' interface
+
+. ./defs
+
+# Compile the model beforehand to avoid compiler's output interference.
+if ! spins $srcdir/finite.pm; then
+  echo "spins not functionnal."
+  exit 77
+fi
+
+run 0 ../modelcheck -gm $srcdir/finite.pm '"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 '"P_0.a < 10"' > stdout2
+diff stdout stdout2
+
+run 0 ../modelcheck -dfalse -gm $srcdir/finite.pm '"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 '"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 \
+  '!(G(dead -> ("P_0.a==3" | "P_0.b==3")))'
+
+run 0 ../modelcheck -ddead -e $srcdir/finite.pm \
+  '!(G(dead -> ("P_0.a==2" | "P_0.b==3")))'
+
+run 0 ../modelcheck -gp $srcdir/finite.pm true

iface/ltsmin/kripke.test

@@ -1,6 +1,6 @@
 #! /bin/sh
-
+# -*- coding: utf-8 -*-
-# Copyright (C) 2011 Laboratoire de Recherche et Developpement
+# Copyright (C) 2011, 2014 Laboratoire de Recherche et Developpement
 # de l'Epita (LRDE)
 #
 # This file is part of Spot, a model checking library.
@@ -24,7 +24,7 @@
 
 divine compile > output 2>&1
 
-if grep -i ltsmin output; then
+if grep -i 'ltsmin ' output; then
   :
 else
   echo "divine not installed, or no ltsmin interface"

iface/ltsmin/ltsmin.cc

@@ -998,7 +998,7 @@ namespace spot
     struct stat d;
     if (stat(filename.c_str(), &d) == 0)
       if (s.st_mtime < d.st_mtime)
-	// The .prom.spins is up-to-date, no need to recompile it.
+	// The .spins or .dve2C is up-to-date, no need to recompile it.
 	return false;
 
     int res = system(command.c_str());
@@ -1014,11 +1014,9 @@ namespace spot
   }
 
   kripke_ptr
-  load_model(const std::string& file_arg, const bdd_dict_ptr& dict,
+  load_ltsmin(const std::string& file_arg, const bdd_dict_ptr& dict,
-	    const ltl::atomic_prop_set* to_observe,
+	      const ltl::atomic_prop_set* to_observe,
-	    const ltl::formula* dead,
+	      const ltl::formula* dead, int compress, bool verbose)
-	    int compress,
-	    bool verbose)
   {
     std::string file;
     if (file_arg.find_first_of("/\\") != std::string::npos)
@@ -1104,8 +1102,7 @@ namespace spot
         lt_dlsym(h, "get_state_variable_type_value");
       }
 
-    if (!(
+    if (!(d->get_initial_state
-          d->get_initial_state
 	  && d->get_successors
 	  && d->get_state_size
 	  && d->get_state_variable_name

iface/ltsmin/ltsmin.hh

@@ -17,8 +17,8 @@
 // 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
+#ifndef SPOT_IFACE_LTSMIN_LTSMIN_HH
-# define SPOT_IFACE_PROMELA_PROMELA_HH
+# define SPOT_IFACE_LTSMIN_LTSMIN_HH
 
 #include "kripke/kripke.hh"
 #include "ltlvisit/apcollect.hh"
@@ -28,12 +28,15 @@
 namespace spot
 {
 
-  // \brief Load a PROMELA model.
+  // \brief Load an ltsmin model, either from divine or promela.
   //
-  // The filename given can be either a *.prom source or a *.spins
+  // The filename given can be either a *.pm/*.pml/*.prom promela
-  // dynamic library compiled with "spins file".
+  // source or a *.spins dynamic library compiled with "spins file".
-  // When the *.prom source is supplied, the *.spins will be updated
+  // If a promela source is supplied, this function will call spins to
-  // only if it is not newer.
+  // update the *.spins library only if it is not newer.
+  //
+  // Similarly the divine models can be specified as *.dve source or
+  // *.dve or *.dve2C libraries.
   //
   // The dead parameter is used to control the behavior of the model
   // on dead states (i.e. the final states of finite sequences).
@@ -56,10 +59,10 @@ namespace spot
   //         dead states
   // \a verbose whether to output verbose messages
   SPOT_API kripke_ptr
-  load_model(const std::string& file, const bdd_dict_ptr& dict,
+  load_ltsmin(const std::string& file, const bdd_dict_ptr& dict,
-	    const ltl::atomic_prop_set* to_observe,
+	      const ltl::atomic_prop_set* to_observe,
-	    const ltl::formula* dead = ltl::constant::true_instance(),
+	      const ltl::formula* dead = ltl::constant::true_instance(),
-	    int compress = 0, bool verbose = true);
+	      int compress = 0, bool verbose = true);
 }
 
-#endif // SPOT_IFACE_PROMELA_PROMELA_HH
+#endif // SPOT_IFACE_LTSMIN_LTSMIN_HH

iface/ltsmin/modelcheck.cc

@@ -217,10 +217,10 @@ checked_main(int argc, char **argv)
 
   if (output != DotFormula)
     {
-      tm.start("loading spins");
+      tm.start("loading ltsmin model");
-      model = spot::load_model(argv[1], dict, &ap, deadf,
+      model = spot::load_ltsmin(argv[1], dict, &ap, deadf,
-                               compress_states, true);
+				compress_states, true);
-      tm.stop("loading spins");
+      tm.stop("loading ltsmin model");
 
       if (!model)
 	{