From 5318c1f96614fb3b1f2a159769727a4b41214e49 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 7 Mar 2011 11:08:12 +0100 Subject: [PATCH] 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 | 9 ++++ configure.ac | 1 + iface/dve2/.gitignore | 3 ++ iface/dve2/Makefile.am | 8 +++ iface/dve2/beem-peterson.4.dve | 63 +++++++++++++++++++++++ iface/dve2/defs.in | 91 ++++++++++++++++++++++++++++++++++ iface/dve2/dve2check.test | 60 ++++++++++++++++++++++ 7 files changed, 235 insertions(+) create mode 100644 iface/dve2/beem-peterson.4.dve create mode 100644 iface/dve2/defs.in create mode 100755 iface/dve2/dve2check.test diff --git a/ChangeLog b/ChangeLog index 14b01a07d..5dead9f99 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2011-03-07 Alexandre Duret-Lutz + + 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 Clear the timer map to help valgrind. diff --git a/configure.ac b/configure.ac index 3dccec72d..93de38638 100644 --- a/configure.ac +++ b/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 diff --git a/iface/dve2/.gitignore b/iface/dve2/.gitignore index 107d2b017..1f7c4c17b 100644 --- a/iface/dve2/.gitignore +++ b/iface/dve2/.gitignore @@ -1,2 +1,5 @@ *.dve2C +*.dve.cpp dve2check +defs +*.dir diff --git a/iface/dve2/Makefile.am b/iface/dve2/Makefile.am index 8aac97424..28c6b6155 100644 --- a/iface/dve2/Makefile.am +++ b/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) diff --git a/iface/dve2/beem-peterson.4.dve b/iface/dve2/beem-peterson.4.dve new file mode 100644 index 000000000..277e9c84e --- /dev/null +++ b/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; diff --git a/iface/dve2/defs.in b/iface/dve2/defs.in new file mode 100644 index 000000000..fccf16cd0 --- /dev/null +++ b/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 diff --git a/iface/dve2/dve2check.test b/iface/dve2/dve2check.test new file mode 100755 index 000000000..f21cbb6ce --- /dev/null +++ b/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