Add some tests for the DVE2 interface.

* iface/dve2/defs.in, iface/dve2/dve2check.test,
iface/dve2/beem-peterson.4.dve: New files.
* iface/dve2/Makefile.am: Add them.
* configure.ac: Generate iface/dve2/defs.

ChangeLog

@@ -1,3 +1,12 @@
+2011-03-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Add some tests for the DVE2 interface.
+
+	* iface/dve2/defs.in, iface/dve2/dve2check.test,
+	iface/dve2/beem-peterson.4.dve: New files.
+	* iface/dve2/Makefile.am: Add them.
+	* configure.ac: Generate iface/dve2/defs.
+
 2011-03-07  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Clear the timer map to help valgrind.

configure.ac

@@ -98,6 +98,7 @@ AC_CONFIG_FILES([
   bench/wdba/defs
   doc/Doxyfile
   doc/Makefile
+  iface/dve2/defs
   iface/dve2/Makefile
   iface/gspn/defs
   iface/gspn/Makefile

iface/dve2/.gitignore

@@ -1,2 +1,5 @@
 *.dve2C
+*.dve.cpp
 dve2check
+defs
+*.dir

iface/dve2/Makefile.am

@@ -35,3 +35,11 @@ noinst_PROGRAMS = dve2check
 
 dve2check_SOURCES = dve2check.cc
 dve2check_LDADD = libspotdve2.la
+
+check_SCRIPTS = defs
+
+TESTS = dve2check.test
+EXTRA_DIST = $(TESTS) beem-peterson.4.dve
+
+distclean-local:
+	rm -rf $(TESTS:.test=.dir)

iface/dve2/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;

iface/dve2/defs.in

@@ -0,0 +1,91 @@
+# -*- shell-script -*-
+# Copyright (C) 2009, 2010 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+# 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

iface/dve2/dve2check.test

@@ -0,0 +1,60 @@
+#!/bin/sh
+# Copyright (C) 2011 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+
+. ./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
+
+# The three examples from the README.
+# (Don't run the first one using "run 0" because it would take too much
+# time with valgrind.).
+
+../dve2check -e $srcdir/beem-peterson.4.dve '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)'
+run 0 ../dve2check -E $srcdir/beem-peterson.4.dve '!G(P_0.wait -> F P_0.CS)'
+run 0 ../dve2check -E $srcdir/beem-peterson.4.dve '!G("pos[1] < 3")'
+
+
+# Now check some error messages.
+run 1 ../dve2check 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 ../dve2check 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