From 66bd8f34dbb31d47617dbc7a9f8cffb615d959cc Mon Sep 17 00:00:00 2001 From: Etienne Renault Date: Thu, 23 Apr 2015 10:08:45 +0200 Subject: [PATCH] Merge kripketest, graphtest and ltltest into tests * README, configure.ac, iface/ltsmin/Makefile.am, src/tests/defs.in, src/tests/.gitignore, src/tests/Makefile.am, src/Makefile.am: update references. * src/kripketest/.gitignore, src/kripketest/Makefile.am, src/kripketest/defs.in, src/graphtest/.gitignore, src/graphtest/Makefile.am, src/graphtest/defs.in, src/ltltest/.cvsignore, src/ltltest/.gitignore, src/ltltest/Makefile.am, src/ltltest/defs.in:: remove files. * src/kripketest/bad_parsing.test, src/kripketest/kripke.test, src/kripketest/origin, src/kripketest/parse_print_test.cc, src/ltltest/bare.test, src/ltltest/consterm.cc, src/ltltest/consterm.test, src/tests/defs.in, src/ltltest/equals.test, src/ltltest/equalsf.cc, src/ltltest/eventuniv.test, src/ltltest/exclusive-ltl.test, src/graphtest/graph.cc, src/graphtest/graph.test, src/ltltest/isop.test, src/ltltest/kind.cc, src/ltltest/kind.test, src/ltltest/latex.test, src/ltltest/lbt.test, src/ltltest/length.cc, src/ltltest/length.test, src/ltltest/lenient.test, src/ltltest/ltlcrossgrind.test, src/ltltest/ltlfilt.test, src/ltltest/ltlgrind.test, src/ltltest/ltlrel.cc, src/ltltest/ltlrel.test, src/ltltest/lunabbrev.test, src/ltltest/nenoform.test, src/graphtest/ngraph.cc, src/graphtest/ngraph.test, src/ltltest/parse.test, src/ltltest/parseerr.test, src/ltltest/rand.test, src/ltltest/readltl.cc, src/ltltest/reduc.cc, src/ltltest/reduc.test, src/ltltest/reduc0.test, src/ltltest/reduccmp.test, src/ltltest/reducpsl.test, src/ltltest/remove_x.test, src/ltltest/stutter-ltl.test, src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test, src/graphtest/tgbagraph.test, src/ltltest/tostring.cc, src/ltltest/tostring.test, src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test, src/graphtest/twagraph.cc, src/ltltest/unabbrevwm.test,src/ltltest/utf8.test, src/ltltest/uwrm.test: rename as... * src/tests/bad_parsing.test, src/tests/kripke.test, src/tests/origin, src/tests/parse_print_test.cc, src/tests/bare.test, src/tests/consterm.cc, src/tests/consterm.test, src/tests/equals.test, src/tests/equalsf.cc, src/tests/eventuniv.test, src/tests/exclusive-ltl.test, src/tests/graph.cc, src/tests/graph.test, src/tests/isop.test, src/tests/kind.cc, src/tests/kind.test, src/tests/latex.test, src/tests/lbt.test, src/tests/length.cc, src/tests/length.test, src/tests/lenient.test, src/tests/ltlcrossgrind.test, src/tests/ltlfilt.test, src/tests/ltlgrind.test, src/tests/ltlrel.cc, src/tests/ltlrel.test, src/tests/lunabbrev.test, src/tests/nenoform.test, src/tests/ngraph.cc, src/tests/ngraph.test, src/tests/parse.test, src/tests/parseerr.test, src/tests/rand.test, src/tests/readltl.cc, src/tests/reduc.cc, src/tests/reduc.test, src/tests/reduc0.test, src/tests/reduccmp.test, src/tests/reducpsl.test, src/tests/remove_x.test, src/tests/stutter-ltl.test, src/tests/syntimpl.cc, src/tests/syntimpl.test, src/tests/tgbagraph.test, src/tests/tostring.cc, src/tests/tostring.test, src/tests/tunabbrev.test, src/tests/tunenoform.test, src/tests/twagraph.cc, src/tests/unabbrevwm.test, src/tests/utf8.test, src/tests/uwrm.test: ...these! --- README | 9 +- configure.ac | 6 - iface/ltsmin/Makefile.am | 6 +- src/Makefile.am | 2 +- src/graphtest/.gitignore | 4 - src/graphtest/Makefile.am | 36 ------ src/graphtest/defs.in | 85 ------------- src/kripketest/.gitignore | 4 - src/kripketest/Makefile.am | 41 ------ src/kripketest/defs.in | 90 -------------- src/ltltest/.cvsignore | 19 --- src/ltltest/.gitignore | 32 ----- src/ltltest/Makefile.am | 117 ------------------ src/ltltest/defs.in | 76 ------------ src/tests/.gitignore | 29 +++++ src/tests/Makefile.am | 102 ++++++++++++++- src/{kripketest => tests}/bad_parsing.test | 0 src/{ltltest => tests}/bare.test | 0 src/{ltltest => tests}/consterm.cc | 0 src/{ltltest => tests}/consterm.test | 0 src/tests/defs.in | 1 + src/{ltltest => tests}/equals.test | 0 src/{ltltest => tests}/equalsf.cc | 0 src/{ltltest => tests}/eventuniv.test | 0 src/{ltltest => tests}/exclusive-ltl.test | 0 src/{graphtest => tests}/graph.cc | 0 src/{graphtest => tests}/graph.test | 0 src/{ltltest => tests}/isop.test | 0 src/{ltltest => tests}/kind.cc | 0 src/{ltltest => tests}/kind.test | 0 src/{kripketest => tests}/kripke.test | 0 src/{ltltest => tests}/latex.test | 0 src/{ltltest => tests}/lbt.test | 0 src/{ltltest => tests}/length.cc | 0 src/{ltltest => tests}/length.test | 0 src/{ltltest => tests}/lenient.test | 0 src/{ltltest => tests}/ltlcrossgrind.test | 0 src/{ltltest => tests}/ltlfilt.test | 0 src/{ltltest => tests}/ltlgrind.test | 0 src/{ltltest => tests}/ltlrel.cc | 0 src/{ltltest => tests}/ltlrel.test | 0 src/{ltltest => tests}/lunabbrev.test | 0 src/{ltltest => tests}/nenoform.test | 0 src/{graphtest => tests}/ngraph.cc | 0 src/{graphtest => tests}/ngraph.test | 0 src/{kripketest => tests}/origin | 0 src/{ltltest => tests}/parse.test | 0 src/{kripketest => tests}/parse_print_test.cc | 0 src/{ltltest => tests}/parseerr.test | 0 src/{ltltest => tests}/rand.test | 0 src/{ltltest => tests}/readltl.cc | 0 src/{ltltest => tests}/reduc.cc | 0 src/{ltltest => tests}/reduc.test | 0 src/{ltltest => tests}/reduc0.test | 0 src/{ltltest => tests}/reduccmp.test | 0 src/{ltltest => tests}/reducpsl.test | 0 src/{ltltest => tests}/remove_x.test | 0 src/{ltltest => tests}/stutter-ltl.test | 0 src/{ltltest => tests}/syntimpl.cc | 0 src/{ltltest => tests}/syntimpl.test | 0 src/{graphtest => tests}/tgbagraph.test | 0 src/{ltltest => tests}/tostring.cc | 0 src/{ltltest => tests}/tostring.test | 0 src/{ltltest => tests}/tunabbrev.test | 0 src/{ltltest => tests}/tunenoform.test | 0 src/{graphtest => tests}/twagraph.cc | 0 src/{ltltest => tests}/unabbrevwm.test | 0 src/{ltltest => tests}/utf8.test | 0 src/{ltltest => tests}/uwrm.test | 0 69 files changed, 137 insertions(+), 522 deletions(-) delete mode 100644 src/graphtest/.gitignore delete mode 100644 src/graphtest/Makefile.am delete mode 100644 src/graphtest/defs.in delete mode 100644 src/kripketest/.gitignore delete mode 100644 src/kripketest/Makefile.am delete mode 100644 src/kripketest/defs.in delete mode 100644 src/ltltest/.cvsignore delete mode 100644 src/ltltest/.gitignore delete mode 100644 src/ltltest/Makefile.am delete mode 100644 src/ltltest/defs.in rename src/{kripketest => tests}/bad_parsing.test (100%) rename src/{ltltest => tests}/bare.test (100%) rename src/{ltltest => tests}/consterm.cc (100%) rename src/{ltltest => tests}/consterm.test (100%) rename src/{ltltest => tests}/equals.test (100%) rename src/{ltltest => tests}/equalsf.cc (100%) rename src/{ltltest => tests}/eventuniv.test (100%) rename src/{ltltest => tests}/exclusive-ltl.test (100%) rename src/{graphtest => tests}/graph.cc (100%) rename src/{graphtest => tests}/graph.test (100%) rename src/{ltltest => tests}/isop.test (100%) rename src/{ltltest => tests}/kind.cc (100%) rename src/{ltltest => tests}/kind.test (100%) rename src/{kripketest => tests}/kripke.test (100%) rename src/{ltltest => tests}/latex.test (100%) rename src/{ltltest => tests}/lbt.test (100%) rename src/{ltltest => tests}/length.cc (100%) rename src/{ltltest => tests}/length.test (100%) rename src/{ltltest => tests}/lenient.test (100%) rename src/{ltltest => tests}/ltlcrossgrind.test (100%) rename src/{ltltest => tests}/ltlfilt.test (100%) rename src/{ltltest => tests}/ltlgrind.test (100%) rename src/{ltltest => tests}/ltlrel.cc (100%) rename src/{ltltest => tests}/ltlrel.test (100%) rename src/{ltltest => tests}/lunabbrev.test (100%) rename src/{ltltest => tests}/nenoform.test (100%) rename src/{graphtest => tests}/ngraph.cc (100%) rename src/{graphtest => tests}/ngraph.test (100%) rename src/{kripketest => tests}/origin (100%) rename src/{ltltest => tests}/parse.test (100%) rename src/{kripketest => tests}/parse_print_test.cc (100%) rename src/{ltltest => tests}/parseerr.test (100%) rename src/{ltltest => tests}/rand.test (100%) rename src/{ltltest => tests}/readltl.cc (100%) rename src/{ltltest => tests}/reduc.cc (100%) rename src/{ltltest => tests}/reduc.test (100%) rename src/{ltltest => tests}/reduc0.test (100%) rename src/{ltltest => tests}/reduccmp.test (100%) rename src/{ltltest => tests}/reducpsl.test (100%) rename src/{ltltest => tests}/remove_x.test (100%) rename src/{ltltest => tests}/stutter-ltl.test (100%) rename src/{ltltest => tests}/syntimpl.cc (100%) rename src/{ltltest => tests}/syntimpl.test (100%) rename src/{graphtest => tests}/tgbagraph.test (100%) rename src/{ltltest => tests}/tostring.cc (100%) rename src/{ltltest => tests}/tostring.test (100%) rename src/{ltltest => tests}/tunabbrev.test (100%) rename src/{ltltest => tests}/tunenoform.test (100%) rename src/{graphtest => tests}/twagraph.cc (100%) rename src/{ltltest => tests}/unabbrevwm.test (100%) rename src/{ltltest => tests}/utf8.test (100%) rename src/{ltltest => tests}/uwrm.test (100%) diff --git a/README b/README index 2bfc77aae..7cc2f194d 100644 --- a/README +++ b/README @@ -139,21 +139,18 @@ src/ Sources for libspot. man/ Man pages for the above tools. dstarparse/ Parser for the output of ltl2dstar. graph/ Graph representations. - graphtest/ Graph representations. hoaparse/ Parser for HOA automata and Spin's never claims. kripke/ Kripke Structure interface. kripkeparse/ Parser for explicit Kripke. - kripketest/ Tests for kripke explicit. ltlast/ LTL abstract syntax tree (including nodes for ELTL). ltlenv/ LTL environments. ltlparse/ Parser for LTL formulae. ltlvisit/ Visitors of LTL formulae. - ltltest/ Tests for ltlast/, ltlenv/, ltlparse/, and ltlvisit/. misc/ Miscellaneous support files. priv/ Private algorithms, used internally but not exported. ta/ TA objects and cousins (TGTA). taalgos/ Algorithms on TA/TGTA. - tests/ Tests for twa/, twaalgos/, ta/ and taalgos/. + tests/ Tests for the whole library. twa/ TωA objects and cousins (Transition-based ω-Automata). twaalgos/ Algorithms on TωA. gtec/ Couvreur's Emptiness-Check. @@ -202,10 +199,10 @@ End: LocalWords: Python's BuDDy LBTT LTL Büchi lbtt gspn DIR GreatSPN Soheib Yann LocalWords: Baarir Thierry Mieg CVS Università di Torino devel src libspot ac - LocalWords: ltlast ltlenv ltlparse ltlvisit ltltest misc tgba TGBA tgbaalgos + LocalWords: ltlast ltlenv ltlparse ltlvisit misc tgba TGBA tgbaalgos LocalWords: gtec Tarjan doc html PDF spotref pdf cgi ELTL LocalWords: CGI ltl iface BDD Couvreur's emptchk kripke Kripke saba vm LocalWords: eltlparse eltltest SABA sabaalgos sabatest ssp ltlcouter scc SCC -LocalWords: formulae optimizations kripkeparse kripketest Automata +LocalWords: formulae optimizations kripkeparse Automata LocalWords: neverparse ltlcounter ltlclasses parallelizing automata LocalWords: wdba WDBA ajax dve DiVinE ltdl Libtool's dlopen diff --git a/configure.ac b/configure.ac index b5284a858..9b54b2ee7 100644 --- a/configure.ac +++ b/configure.ac @@ -201,17 +201,11 @@ AC_CONFIG_FILES([ src/dstarparse/Makefile src/kripke/Makefile src/graph/Makefile - src/graphtest/Makefile - src/graphtest/defs src/hoaparse/Makefile src/ltlast/Makefile src/ltlenv/Makefile src/ltlparse/Makefile src/kripkeparse/Makefile - src/kripketest/Makefile - src/kripketest/defs - src/ltltest/defs - src/ltltest/Makefile src/ltlvisit/Makefile src/Makefile src/misc/Makefile diff --git a/iface/ltsmin/Makefile.am b/iface/ltsmin/Makefile.am index 537b98052..1fcf786c1 100644 --- a/iface/ltsmin/Makefile.am +++ b/iface/ltsmin/Makefile.am @@ -41,10 +41,10 @@ check_SCRIPTS = defs TESTS = check.test finite.test finite2.test kripke.test EXTRA_DIST = $(TESTS) beem-peterson.4.dve finite.dve finite.pm -kripke.test: $(top_builddir)/src/kripketest/parse_print$(EXEEXT) +kripke.test: $(top_builddir)/src/tests/parse_print$(EXEEXT) -$(top_builddir)/src/kripketest/parse_print$(EXEEXT): - cd $(top_builddir)/src/kripketest && \ +$(top_builddir)/src/tests/parse_print$(EXEEXT): + cd $(top_builddir)/src/tests && \ $(MAKE) $(AM_MAKEFLAGS) parse_print$(EXEEXT) distclean-local: diff --git a/src/Makefile.am b/src/Makefile.am index f2bf0cf3d..efb0babbf 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -27,7 +27,7 @@ AUTOMAKE_OPTIONS = subdir-objects # libspot.la needed by the tests) SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse graph twa \ twaalgos ta taalgos kripke kripkeparse dstarparse hoaparse \ - . bin ltltest graphtest tests kripketest sanity + . bin tests sanity lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = diff --git a/src/graphtest/.gitignore b/src/graphtest/.gitignore deleted file mode 100644 index 5ad8c3fb2..000000000 --- a/src/graphtest/.gitignore +++ /dev/null @@ -1,4 +0,0 @@ -graph -ngraph -tgbagraph -defs diff --git a/src/graphtest/Makefile.am b/src/graphtest/Makefile.am deleted file mode 100644 index 1758a2a19..000000000 --- a/src/graphtest/Makefile.am +++ /dev/null @@ -1,36 +0,0 @@ -## -*- coding: utf-8 -*- -## Copyright (C) 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 . - - -AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -AM_CXXFLAGS = $(WARNING_CXXFLAGS) -LDADD = ../libspot.la - -noinst_PROGRAMS = graph ngraph tgbagraph - -graph_SOURCES = graph.cc -ngraph_SOURCES = ngraph.cc -tgbagraph_SOURCES = twagraph.cc - -TESTS = graph.test ngraph.test tgbagraph.test - -EXTRA_DIST = $(TESTS) - -distclean-local: - rm -rf $(TESTS:.test=.dir) diff --git a/src/graphtest/defs.in b/src/graphtest/defs.in deleted file mode 100644 index 5169462fe..000000000 --- a/src/graphtest/defs.in +++ /dev/null @@ -1,85 +0,0 @@ -# -*- mode: shell-script; coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2012, 2013, 2014 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 . - -# 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 -# $srcdir to point to the source directory corresponding to the build -# directory that contains $testSubDir. -case $srcdir in - [\\/$]* | ?:[\\/]* );; - *) srcdir=../$srcdir -esac - -DOT='@DOT@' -top_builddir='../@top_builddir@' -VALGRIND='@VALGRIND@' -PYTHON='@PYTHON@' - -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/src/kripketest/.gitignore b/src/kripketest/.gitignore deleted file mode 100644 index 2a1c12db2..000000000 --- a/src/kripketest/.gitignore +++ /dev/null @@ -1,4 +0,0 @@ -Makefile -Makefile.in -defs -parse_print diff --git a/src/kripketest/Makefile.am b/src/kripketest/Makefile.am deleted file mode 100644 index b384cdd87..000000000 --- a/src/kripketest/Makefile.am +++ /dev/null @@ -1,41 +0,0 @@ -## 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 . - -AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) - -kripketestdir = $(pkgincludedir)/kripketest - -kripketest_HEADERS = - - -LDADD = ../libspot.la - -check_SCRIPTS = defs - -parse_print_SOURCES = parse_print_test.cc -check_PROGRAMS = \ -parse_print - -TESTS = \ - kripke.test \ - bad_parsing.test - -EXTRA_DIST = $(TESTS) - -distclean-local: - rm -rf $(TESTS:.test=.dir) diff --git a/src/kripketest/defs.in b/src/kripketest/defs.in deleted file mode 100644 index cb272b871..000000000 --- a/src/kripketest/defs.in +++ /dev/null @@ -1,90 +0,0 @@ -# -*- 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 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 . - -# 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@' -top_srcdir='../@top_srcdir@' - -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/src/ltltest/.cvsignore b/src/ltltest/.cvsignore deleted file mode 100644 index c64a83274..000000000 --- a/src/ltltest/.cvsignore +++ /dev/null @@ -1,19 +0,0 @@ -Makefile -Makefile.in -.deps -ltl2dot -ltl2text -stdout -parser.dot -expect -defs -equals -lunabbrev -tunabbrev -nenoform -tunenoform -.libs -tostring -reduc -reduccmp -syntimpl diff --git a/src/ltltest/.gitignore b/src/ltltest/.gitignore deleted file mode 100644 index 1465d79b1..000000000 --- a/src/ltltest/.gitignore +++ /dev/null @@ -1,32 +0,0 @@ -Makefile -Makefile.in -.deps -ltl2dot -ltl2text -stdout -parser.dot -expect -defs -equals -nequals -lunabbrev -tunabbrev -nenoform -tunenoform -.libs -tostring -reduc -reduccmp -syntimpl -randltl -*.dot -reductau -reductaustr -genltl -kind -consterm -apcollect -length -reduceu -unabbrevwm -ltlrel diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am deleted file mode 100644 index 934a530c5..000000000 --- a/src/ltltest/Makefile.am +++ /dev/null @@ -1,117 +0,0 @@ -## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire -## de Recherche et Développement de l'Epita (LRDE). -## Copyright (C) 2003, 2004, 2005, 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 . - -AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -AM_CXXFLAGS = $(WARNING_CXXFLAGS) -LDADD = ../libspot.la - -check_SCRIPTS = defs -# Keep this sorted alphabetically. -check_PROGRAMS = \ - consterm \ - equals \ - kind \ - length \ - ltl2dot \ - ltl2text \ - ltlrel \ - lunabbrev \ - nequals \ - nenoform \ - reduc \ - reduccmp \ - reduceu \ - reductaustr \ - syntimpl \ - tostring \ - tunabbrev \ - tunenoform - -consterm_SOURCES = consterm.cc -equals_SOURCES = equalsf.cc -kind_SOURCES = kind.cc -length_SOURCES = length.cc -ltl2dot_SOURCES = readltl.cc -ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY -ltl2text_SOURCES = readltl.cc -ltlrel_SOURCES = ltlrel.cc -lunabbrev_SOURCES = equalsf.cc -lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DLUNABBREV -nenoform_SOURCES = equalsf.cc -nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -nequals_SOURCES = equalsf.cc -nequals_CPPFLAGS = $(AM_CPPFLAGS) -DNEGATE -reduc_SOURCES = reduc.cc -reduccmp_SOURCES = equalsf.cc -reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC -reduceu_SOURCES = equalsf.cc -reduceu_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC -DEVENT_UNIV -reductaustr_SOURCES = equalsf.cc -reductaustr_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAUSTR -syntimpl_SOURCES = syntimpl.cc -tostring_SOURCES = tostring.cc -tunabbrev_SOURCES = equalsf.cc -tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DTUNABBREV -tunenoform_SOURCES = equalsf.cc -tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DTUNABBREV - - -EXTRA_DIST = $(TESTS) - -# Ordered by strength of the test. Test basic features first. -TESTS = \ - bare.test \ - parse.test \ - parseerr.test \ - utf8.test \ - length.test \ - equals.test \ - tostring.test \ - lunabbrev.test \ - tunabbrev.test \ - nenoform.test \ - tunenoform.test \ - unabbrevwm.test \ - consterm.test \ - kind.test \ - remove_x.test \ - ltlrel.test \ - ltlgrind.test \ - ltlcrossgrind.test \ - ltlfilt.test \ - exclusive-ltl.test \ - latex.test \ - lbt.test \ - lenient.test \ - rand.test \ - isop.test \ - syntimpl.test \ - reduc.test \ - reduc0.test \ - reducpsl.test \ - reduccmp.test \ - uwrm.test \ - eventuniv.test \ - stutter-ltl.test - -distclean-local: - rm -rf $(TESTS:.test=.dir) diff --git a/src/ltltest/defs.in b/src/ltltest/defs.in deleted file mode 100644 index adb6b341e..000000000 --- a/src/ltltest/defs.in +++ /dev/null @@ -1,76 +0,0 @@ -# -*- shell-script -*- -# Copyright (C) 2009 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 . - -# 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 - -DOT='@DOT@' -VALGRIND='@VALGRIND@' -top_srcdir='../@top_srcdir@' - -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/src/tests/.gitignore b/src/tests/.gitignore index 5bd70e68d..3086f5b53 100644 --- a/src/tests/.gitignore +++ b/src/tests/.gitignore @@ -1,41 +1,70 @@ acc +apcollect bddprod bitvect blue_counter checkpsl checkta complement +consterm defs .deps *.dot eltl2tgba emptchk +defs +equals +expect expldot explicit explicit2 explicit3 explprod +graph +genltl input intvcomp intvcmp2 +kind +length .libs ltl2tgba +ltl2dot +ltl2text ltlmagic ltlprod +ltlrel +lunabbrev Makefile Makefile.in maskacc mixprod +nequals +nenoform +ngraph output1 output2 +parse_print powerset *.ps +randltl randtgba readsat readsave +reduc +reduceu +reductau +reductaustr reduccmp reductgba +stdout spotlbtt +syntimpl taatgba +tgbagraph tgbaread +tostring tripprod +tunabbrev +tunenoform +unabbrevwm diff --git a/src/tests/Makefile.am b/src/tests/Makefile.am index 285be2ef2..0349b69cf 100644 --- a/src/tests/Makefile.am +++ b/src/tests/Makefile.am @@ -36,12 +36,34 @@ check_PROGRAMS = \ complement \ checkpsl \ checkta \ + consterm \ emptchk \ + equals \ + graph \ + kind \ + length \ intvcomp \ intvcmp2 \ ltlprod \ + ltl2dot \ + ltl2text \ + ltlrel \ + lunabbrev \ + nequals \ + nenoform \ + ngraph \ + parse_print \ readsat \ - taatgba + reduc \ + reduccmp \ + reduceu \ + reductaustr \ + syntimpl \ + taatgba \ + tgbagraph \ + tostring \ + tunabbrev \ + tunenoform # Keep this sorted alphabetically. acc_SOURCES = acc.cc @@ -50,17 +72,93 @@ checkpsl_SOURCES = checkpsl.cc checkta_SOURCES = checkta.cc complement_SOURCES = complementation.cc emptchk_SOURCES = emptchk.cc +graph_SOURCES = graph.cc intvcomp_SOURCES = intvcomp.cc intvcmp2_SOURCES = intvcmp2.cc ltl2tgba_SOURCES = ltl2tgba.cc ltlprod_SOURCES = ltlprod.cc +ngraph_SOURCES = ngraph.cc +parse_print_SOURCES = parse_print_test.cc randtgba_SOURCES = randtgba.cc readsat_SOURCES = readsat.cc taatgba_SOURCES = taatgba.cc +tgbagraph_SOURCES = twagraph.cc +consterm_SOURCES = consterm.cc +equals_SOURCES = equalsf.cc +kind_SOURCES = kind.cc +length_SOURCES = length.cc +ltl2dot_SOURCES = readltl.cc +ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY +ltl2text_SOURCES = readltl.cc +ltlrel_SOURCES = ltlrel.cc +lunabbrev_SOURCES = equalsf.cc +lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DLUNABBREV +nenoform_SOURCES = equalsf.cc +nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM +nequals_SOURCES = equalsf.cc +nequals_CPPFLAGS = $(AM_CPPFLAGS) -DNEGATE +reduc_SOURCES = reduc.cc +reduccmp_SOURCES = equalsf.cc +reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC +reduceu_SOURCES = equalsf.cc +reduceu_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC -DEVENT_UNIV +reductaustr_SOURCES = equalsf.cc +reductaustr_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAUSTR +syntimpl_SOURCES = syntimpl.cc +tostring_SOURCES = tostring.cc +tunabbrev_SOURCES = equalsf.cc +tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DTUNABBREV +tunenoform_SOURCES = equalsf.cc +tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DTUNABBREV + # Keep this sorted by STRENGTH. Test basic things first, # because such failures will be easier to diagnose and fix. -TESTS = $(TESTS_twa) +TESTS = $(TESTS_ltl) $(TESTS_graph) $(TESTS_kripke) $(TESTS_twa) + +TESTS_ltl = \ + bare.test \ + parse.test \ + parseerr.test \ + utf8.test \ + length.test \ + equals.test \ + tostring.test \ + lunabbrev.test \ + tunabbrev.test \ + nenoform.test \ + tunenoform.test \ + unabbrevwm.test \ + consterm.test \ + kind.test \ + remove_x.test \ + ltlrel.test \ + ltlgrind.test \ + ltlcrossgrind.test \ + ltlfilt.test \ + exclusive-ltl.test \ + latex.test \ + lbt.test \ + lenient.test \ + rand.test \ + isop.test \ + syntimpl.test \ + reduc.test \ + reduc0.test \ + reducpsl.test \ + reduccmp.test \ + uwrm.test \ + eventuniv.test \ + stutter-ltl.test + +TESTS_graph = \ + graph.test \ + ngraph.test \ + tgbagraph.test + +TESTS_kripke = \ + kripke.test \ + bad_parsing.test TESTS_twa = \ acc.test \ diff --git a/src/kripketest/bad_parsing.test b/src/tests/bad_parsing.test similarity index 100% rename from src/kripketest/bad_parsing.test rename to src/tests/bad_parsing.test diff --git a/src/ltltest/bare.test b/src/tests/bare.test similarity index 100% rename from src/ltltest/bare.test rename to src/tests/bare.test diff --git a/src/ltltest/consterm.cc b/src/tests/consterm.cc similarity index 100% rename from src/ltltest/consterm.cc rename to src/tests/consterm.cc diff --git a/src/ltltest/consterm.test b/src/tests/consterm.test similarity index 100% rename from src/ltltest/consterm.test rename to src/tests/consterm.test diff --git a/src/tests/defs.in b/src/tests/defs.in index 5748da7e2..9e6b07ad8 100644 --- a/src/tests/defs.in +++ b/src/tests/defs.in @@ -65,6 +65,7 @@ VALGRIND='@VALGRIND@' SPIN='@SPIN@' LTL2BA='@LTL2BA@' PYTHON='@PYTHON@' +top_srcdir='../@top_srcdir@' # The test cases assume these variable are undefined unset SPOT_DOTEXTRA diff --git a/src/ltltest/equals.test b/src/tests/equals.test similarity index 100% rename from src/ltltest/equals.test rename to src/tests/equals.test diff --git a/src/ltltest/equalsf.cc b/src/tests/equalsf.cc similarity index 100% rename from src/ltltest/equalsf.cc rename to src/tests/equalsf.cc diff --git a/src/ltltest/eventuniv.test b/src/tests/eventuniv.test similarity index 100% rename from src/ltltest/eventuniv.test rename to src/tests/eventuniv.test diff --git a/src/ltltest/exclusive-ltl.test b/src/tests/exclusive-ltl.test similarity index 100% rename from src/ltltest/exclusive-ltl.test rename to src/tests/exclusive-ltl.test diff --git a/src/graphtest/graph.cc b/src/tests/graph.cc similarity index 100% rename from src/graphtest/graph.cc rename to src/tests/graph.cc diff --git a/src/graphtest/graph.test b/src/tests/graph.test similarity index 100% rename from src/graphtest/graph.test rename to src/tests/graph.test diff --git a/src/ltltest/isop.test b/src/tests/isop.test similarity index 100% rename from src/ltltest/isop.test rename to src/tests/isop.test diff --git a/src/ltltest/kind.cc b/src/tests/kind.cc similarity index 100% rename from src/ltltest/kind.cc rename to src/tests/kind.cc diff --git a/src/ltltest/kind.test b/src/tests/kind.test similarity index 100% rename from src/ltltest/kind.test rename to src/tests/kind.test diff --git a/src/kripketest/kripke.test b/src/tests/kripke.test similarity index 100% rename from src/kripketest/kripke.test rename to src/tests/kripke.test diff --git a/src/ltltest/latex.test b/src/tests/latex.test similarity index 100% rename from src/ltltest/latex.test rename to src/tests/latex.test diff --git a/src/ltltest/lbt.test b/src/tests/lbt.test similarity index 100% rename from src/ltltest/lbt.test rename to src/tests/lbt.test diff --git a/src/ltltest/length.cc b/src/tests/length.cc similarity index 100% rename from src/ltltest/length.cc rename to src/tests/length.cc diff --git a/src/ltltest/length.test b/src/tests/length.test similarity index 100% rename from src/ltltest/length.test rename to src/tests/length.test diff --git a/src/ltltest/lenient.test b/src/tests/lenient.test similarity index 100% rename from src/ltltest/lenient.test rename to src/tests/lenient.test diff --git a/src/ltltest/ltlcrossgrind.test b/src/tests/ltlcrossgrind.test similarity index 100% rename from src/ltltest/ltlcrossgrind.test rename to src/tests/ltlcrossgrind.test diff --git a/src/ltltest/ltlfilt.test b/src/tests/ltlfilt.test similarity index 100% rename from src/ltltest/ltlfilt.test rename to src/tests/ltlfilt.test diff --git a/src/ltltest/ltlgrind.test b/src/tests/ltlgrind.test similarity index 100% rename from src/ltltest/ltlgrind.test rename to src/tests/ltlgrind.test diff --git a/src/ltltest/ltlrel.cc b/src/tests/ltlrel.cc similarity index 100% rename from src/ltltest/ltlrel.cc rename to src/tests/ltlrel.cc diff --git a/src/ltltest/ltlrel.test b/src/tests/ltlrel.test similarity index 100% rename from src/ltltest/ltlrel.test rename to src/tests/ltlrel.test diff --git a/src/ltltest/lunabbrev.test b/src/tests/lunabbrev.test similarity index 100% rename from src/ltltest/lunabbrev.test rename to src/tests/lunabbrev.test diff --git a/src/ltltest/nenoform.test b/src/tests/nenoform.test similarity index 100% rename from src/ltltest/nenoform.test rename to src/tests/nenoform.test diff --git a/src/graphtest/ngraph.cc b/src/tests/ngraph.cc similarity index 100% rename from src/graphtest/ngraph.cc rename to src/tests/ngraph.cc diff --git a/src/graphtest/ngraph.test b/src/tests/ngraph.test similarity index 100% rename from src/graphtest/ngraph.test rename to src/tests/ngraph.test diff --git a/src/kripketest/origin b/src/tests/origin similarity index 100% rename from src/kripketest/origin rename to src/tests/origin diff --git a/src/ltltest/parse.test b/src/tests/parse.test similarity index 100% rename from src/ltltest/parse.test rename to src/tests/parse.test diff --git a/src/kripketest/parse_print_test.cc b/src/tests/parse_print_test.cc similarity index 100% rename from src/kripketest/parse_print_test.cc rename to src/tests/parse_print_test.cc diff --git a/src/ltltest/parseerr.test b/src/tests/parseerr.test similarity index 100% rename from src/ltltest/parseerr.test rename to src/tests/parseerr.test diff --git a/src/ltltest/rand.test b/src/tests/rand.test similarity index 100% rename from src/ltltest/rand.test rename to src/tests/rand.test diff --git a/src/ltltest/readltl.cc b/src/tests/readltl.cc similarity index 100% rename from src/ltltest/readltl.cc rename to src/tests/readltl.cc diff --git a/src/ltltest/reduc.cc b/src/tests/reduc.cc similarity index 100% rename from src/ltltest/reduc.cc rename to src/tests/reduc.cc diff --git a/src/ltltest/reduc.test b/src/tests/reduc.test similarity index 100% rename from src/ltltest/reduc.test rename to src/tests/reduc.test diff --git a/src/ltltest/reduc0.test b/src/tests/reduc0.test similarity index 100% rename from src/ltltest/reduc0.test rename to src/tests/reduc0.test diff --git a/src/ltltest/reduccmp.test b/src/tests/reduccmp.test similarity index 100% rename from src/ltltest/reduccmp.test rename to src/tests/reduccmp.test diff --git a/src/ltltest/reducpsl.test b/src/tests/reducpsl.test similarity index 100% rename from src/ltltest/reducpsl.test rename to src/tests/reducpsl.test diff --git a/src/ltltest/remove_x.test b/src/tests/remove_x.test similarity index 100% rename from src/ltltest/remove_x.test rename to src/tests/remove_x.test diff --git a/src/ltltest/stutter-ltl.test b/src/tests/stutter-ltl.test similarity index 100% rename from src/ltltest/stutter-ltl.test rename to src/tests/stutter-ltl.test diff --git a/src/ltltest/syntimpl.cc b/src/tests/syntimpl.cc similarity index 100% rename from src/ltltest/syntimpl.cc rename to src/tests/syntimpl.cc diff --git a/src/ltltest/syntimpl.test b/src/tests/syntimpl.test similarity index 100% rename from src/ltltest/syntimpl.test rename to src/tests/syntimpl.test diff --git a/src/graphtest/tgbagraph.test b/src/tests/tgbagraph.test similarity index 100% rename from src/graphtest/tgbagraph.test rename to src/tests/tgbagraph.test diff --git a/src/ltltest/tostring.cc b/src/tests/tostring.cc similarity index 100% rename from src/ltltest/tostring.cc rename to src/tests/tostring.cc diff --git a/src/ltltest/tostring.test b/src/tests/tostring.test similarity index 100% rename from src/ltltest/tostring.test rename to src/tests/tostring.test diff --git a/src/ltltest/tunabbrev.test b/src/tests/tunabbrev.test similarity index 100% rename from src/ltltest/tunabbrev.test rename to src/tests/tunabbrev.test diff --git a/src/ltltest/tunenoform.test b/src/tests/tunenoform.test similarity index 100% rename from src/ltltest/tunenoform.test rename to src/tests/tunenoform.test diff --git a/src/graphtest/twagraph.cc b/src/tests/twagraph.cc similarity index 100% rename from src/graphtest/twagraph.cc rename to src/tests/twagraph.cc diff --git a/src/ltltest/unabbrevwm.test b/src/tests/unabbrevwm.test similarity index 100% rename from src/ltltest/unabbrevwm.test rename to src/tests/unabbrevwm.test diff --git a/src/ltltest/utf8.test b/src/tests/utf8.test similarity index 100% rename from src/ltltest/utf8.test rename to src/tests/utf8.test diff --git a/src/ltltest/uwrm.test b/src/tests/uwrm.test similarity index 100% rename from src/ltltest/uwrm.test rename to src/tests/uwrm.test