diff --git a/README b/README index 871aeb7ab..e4c0b71bb 100644 --- a/README +++ b/README @@ -151,7 +151,9 @@ spot/ Sources for libspot. sanity/ Sanity tests for the whole project. bin/ Command-line tools built on top of libspot. man/ Man pages for the above tools. -tests/ Tests for libspot and the binaries. +tests/ Test suite + core/ Tests for libspot and the binaries. + python/ Tests for Python bindings. doc/ Documentation for Spot. org/ Source of userdoc/ as org-mode files. tl/ Documentation of the Temporal Logic operators. @@ -167,7 +169,6 @@ bench/ Benchmarks for ... stutter/ ... stutter-invariance checking algorithms, wdba/ ... WDBA minimization (for obligation properties). python/ Python bindings for Spot and BuDDy - tests/ Tests for these bindings ajax/ LTL-to-TGBA translator with web interface, using Javascript. Third party software diff --git a/configure.ac b/configure.ac index 371507e86..bd0f02556 100644 --- a/configure.ac +++ b/configure.ac @@ -219,14 +219,13 @@ AC_CONFIG_FILES([ spot/twa/Makefile python/ajax/Makefile python/Makefile - python/tests/Makefile - tests/defs + tests/core/defs tests/Makefile tools/x-to-1 ]) AC_CONFIG_FILES([doc/org/g++wrap], [chmod +x doc/org/g++wrap]) AC_CONFIG_FILES([doc/dot], [chmod +x doc/dot]) -AC_CONFIG_FILES([python/tests/run], [chmod +x python/tests/run]) +AC_CONFIG_FILES([tests/run], [chmod +x tests/run]) AC_OUTPUT case $VERSION:$enable_devel in diff --git a/debian/python3-spot.examples b/debian/python3-spot.examples index 0b92304f2..2affe402b 100644 --- a/debian/python3-spot.examples +++ b/debian/python3-spot.examples @@ -1,2 +1,2 @@ -python/tests/*.ipynb -python/tests/*.html +tests/python/*.ipynb +tests/python/*.html diff --git a/debian/rules b/debian/rules index 5f836c334..f4e9e89e9 100755 --- a/debian/rules +++ b/debian/rules @@ -84,8 +84,8 @@ override_dh_python3: dh_python3 -p python3-spot override_dh_auto_build: dh_auto_build - $(MAKE) -C python/tests nb-html + $(MAKE) -C tests/python nb-html fix-mathjax: perl -pi -e 's|http://orgmode.org/mathjax/MathJax.js|file:///usr/share/javascript/mathjax/MathJax.js|' doc/userdoc/*.html - perl -pi -e 's|https://cdn.mathjax.org/mathjax/latest/MathJax.js|file:///usr/share/javascript/mathjax/MathJax.js|' python/tests/*.html + perl -pi -e 's|https://cdn.mathjax.org/mathjax/latest/MathJax.js|file:///usr/share/javascript/mathjax/MathJax.js|' tests/python/*.html diff --git a/doc/org/tut.org b/doc/org/tut.org index abf3a99cd..43d8da865 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -30,7 +30,7 @@ three interfaces supported by Spot: shell commands, Python, or C++. * Examples in Python only -In directory =python/tests=, the [[file:install.org][Spot tarball]] contains a small +In directory the, =python/tests= [[file:install.org][Spot tarball]] contains a small collection of IPython notebooks. As the name of the directory implies, these are part of the test suite for the Python bindings, however they can be interesting to look at if you want to see more code examples. diff --git a/python/Makefile.am b/python/Makefile.am index b34562544..9a5bc0843 100644 --- a/python/Makefile.am +++ b/python/Makefile.am @@ -20,7 +20,7 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . -SUBDIRS = . ajax tests +SUBDIRS = . ajax AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_builddir) -I$(top_srcdir) \ $(BUDDY_CPPFLAGS) -DSWIG_TYPE_TABLE=spot diff --git a/python/tests/Makefile.am b/python/tests/Makefile.am deleted file mode 100644 index 327c2f2b5..000000000 --- a/python/tests/Makefile.am +++ /dev/null @@ -1,67 +0,0 @@ -## -*- coding: utf-8 -*- -## Copyright (C) 2010, 2012, 2013, 2014, 2015 Labortatoire de -## Recherche et Développement de l'EPITA. -## Copyright (C) 2003, 2004, 2005 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 . - -EXTRA_DIST = \ - $(TESTS) \ - ltl2tgba.py \ - ipnbdoctest.py - -LOG_COMPILER = ./run -LOG_DRIVER = $(TEST_LOG_DRIVER) -# ensure run is rebuilt before the tests are run. -check_SCRIPTS = run - -TESTS = \ - acc_cond.ipynb \ - accparse.ipynb \ - accparse2.py \ - alarm.py \ - automata.ipynb \ - automata-io.ipynb \ - bddnqueen.py \ - decompose.ipynb \ - formulas.ipynb \ - implies.py \ - interdep.py \ - ltl2tgba.test \ - ltlparse.py \ - ltlsimple.py \ - minato.py \ - optionmap.py \ - parsetgba.py \ - piperead.ipynb \ - product.ipynb \ - randaut.ipynb \ - randgen.py \ - randltl.ipynb \ - relabel.py \ - remfin.py \ - satmin.py \ - setxor.py \ - testingaut.ipynb - -SUFFIXES = .ipynb .html -.ipynb.html: - $(IPYTHON) nbconvert $< --to html - -.PHONY: nb-html -nb-html: $(TESTS:.ipynb=.html) diff --git a/python/tests/ltl2tgba.test b/python/tests/ltl2tgba.test deleted file mode 100755 index 70f09a37c..000000000 --- a/python/tests/ltl2tgba.test +++ /dev/null @@ -1,50 +0,0 @@ -#!/bin/sh -# Copyright (C) 2014 Laboratoire de Recherche et -# Développement de l'EPITA. -# Copyright (C) 2003 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 . - - -set -e - -# We don't check the output, but just running these might be enough to -# trigger assertions. - -./run $srcdir/ltl2tgba.py -T a -./run $srcdir/ltl2tgba.py -T 'a U b' -./run $srcdir/ltl2tgba.py -T 'X a' -./run $srcdir/ltl2tgba.py -T 'a & b & c' -./run $srcdir/ltl2tgba.py -T 'a | b | (c U (d & (g U (h ^ i))))' -./run $srcdir/ltl2tgba.py -T 'Xa & (b U !a) & (b U !a)' -./run $srcdir/ltl2tgba.py -T 'Fa & Xb & GFc & Gd' -./run $srcdir/ltl2tgba.py -T 'Fa & Xa & GFc & Gc' -./run $srcdir/ltl2tgba.py -T 'Fc & X(a | Xb) & GF(a | Xb) & Gc' - -./run $srcdir/ltl2tgba.py -f a -./run $srcdir/ltl2tgba.py -f 'a U b' -./run $srcdir/ltl2tgba.py -f 'X a' -./run $srcdir/ltl2tgba.py -f 'a & b & c' -./run $srcdir/ltl2tgba.py -f 'a | b | (c U (d & (g U (h ^ i))))' -./run $srcdir/ltl2tgba.py -f 'Xa & (b U !a) & (b U !a)' -./run $srcdir/ltl2tgba.py -f 'Fa & Xb & GFc & Gd' -./run $srcdir/ltl2tgba.py -f 'Fa & Xa & GFc & Gc' -./run $srcdir/ltl2tgba.py -f 'Fc & X(a | Xb) & GF(a | Xb) & Gc' - -./run $srcdir/ltl2tgba.py -W -f 'Ga | Gb | Gc' -./run $srcdir/ltl2tgba.py -W -T 'Ga | Gb | Gc' diff --git a/spot/ltsmin/Makefile.am b/spot/ltsmin/Makefile.am index 1f94a63df..10374ef48 100644 --- a/spot/ltsmin/Makefile.am +++ b/spot/ltsmin/Makefile.am @@ -42,11 +42,11 @@ 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)/tests/parse_print$(EXEEXT) +kripke.test: $(top_builddir)/tests/core/parse_print$(EXEEXT) -$(top_builddir)/tests/parse_print$(EXEEXT): +$(top_builddir)/tests/core/parse_print$(EXEEXT): cd $(top_builddir)/tests && \ - $(MAKE) $(AM_MAKEFLAGS) parse_print$(EXEEXT) + $(MAKE) $(AM_MAKEFLAGS) core/parse_print$(EXEEXT) distclean-local: rm -rf $(TESTS:.test=.dir) diff --git a/spot/ltsmin/kripke.test b/spot/ltsmin/kripke.test index 1c95666b7..383778a6f 100755 --- a/spot/ltsmin/kripke.test +++ b/spot/ltsmin/kripke.test @@ -34,9 +34,9 @@ fi set -e run 0 ../modelcheck -gK $srcdir/finite.dve 'F("P.a > 5")' > output -run 0 $top_builddir/tests/parse_print output | tr -d '"' > output2 +run 0 $top_builddir/tests/core/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/tests/ikwiad -e -KPoutputP '!G("pos[1] < 3")' +$top_builddir/tests/core/ikwiad -e -KPoutputP '!G("pos[1] < 3")' diff --git a/spot/sanity/ipynb.test b/spot/sanity/ipynb.test index 39a62eff4..f5afb6f15 100755 --- a/spot/sanity/ipynb.test +++ b/spot/sanity/ipynb.test @@ -33,7 +33,7 @@ my $top_srcdir = $ENV{top_srcdir} || "../../"; my $top_srcdir_len = length($top_srcdir) + 1; my $tut = "$top_srcdir/doc/org/tut.org"; -my $dir = "$top_srcdir/python/tests"; +my $dir = "$top_srcdir/tests/python"; unless (-f $tut) { print STDERR "$tut not found"; @@ -58,10 +58,10 @@ while () } close(FD); -open(FD, "$dir/Makefile.am") or die $!; +open(FD, "$dir/../Makefile.am") or die "$!"; while () { - if (m:\s([\w-]+\.ipynb):) + if (m:python/([\w-]+\.ipynb):) { # print "$1 exist"; unless (exists $seen{$1}) diff --git a/tests/.gitignore b/tests/.gitignore index 35bf1ca83..ae88eb6a6 100644 --- a/tests/.gitignore +++ b/tests/.gitignore @@ -1,70 +1 @@ -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 -ikwiad -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 +*.dir diff --git a/tests/Makefile.am b/tests/Makefile.am index f5fb56308..82e512a0a 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -20,234 +20,282 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . +AUTOMAKE_OPTIONS = subdir-objects AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) LDADD = $(top_builddir)/spot/libspot.la # These are the most used test programs, and they are also useful # to run manually outside the test suite. Always build them. -noinst_PROGRAMS = ikwiad randtgba +noinst_PROGRAMS = core/ikwiad core/randtgba + +TEST_EXTENTIONS = .test .py .ipynb + +LOG_COMPILER = ./run +TEST_LOG_COMPILER = ./run +LOG_DRIVER = $(TEST_LOG_DRIVER) +# ensure run is rebuilt before the tests are run. +check_SCRIPTS = run core/defs -check_SCRIPTS = defs # Keep this sorted alphabetically. check_PROGRAMS = \ - acc \ - bitvect \ - complement \ - checkpsl \ - checkta \ - consterm \ - emptchk \ - equals \ - graph \ - kind \ - length \ - intvcomp \ - intvcmp2 \ - ltlprod \ - ltl2dot \ - ltl2text \ - ltlrel \ - lunabbrev \ - nequals \ - nenoform \ - ngraph \ - parse_print \ - readsat \ - reduc \ - reduccmp \ - reduceu \ - reductaustr \ - syntimpl \ - taatgba \ - tgbagraph \ - tostring \ - tunabbrev \ - tunenoform + core/acc \ + core/bitvect \ + core/complement \ + core/checkpsl \ + core/checkta \ + core/consterm \ + core/emptchk \ + core/equals \ + core/graph \ + core/kind \ + core/length \ + core/intvcomp \ + core/intvcmp2 \ + core/ltlprod \ + core/ltl2dot \ + core/ltl2text \ + core/ltlrel \ + core/lunabbrev \ + core/nequals \ + core/nenoform \ + core/ngraph \ + core/parse_print \ + core/readsat \ + core/reduc \ + core/reduccmp \ + core/reduceu \ + core/reductaustr \ + core/syntimpl \ + core/taatgba \ + core/tgbagraph \ + core/tostring \ + core/tunabbrev \ + core/tunenoform # Keep this sorted alphabetically. -acc_SOURCES = acc.cc -bitvect_SOURCES = bitvect.cc -checkpsl_SOURCES = checkpsl.cc -checkta_SOURCES = checkta.cc -complement_SOURCES = complementation.cc -emptchk_SOURCES = emptchk.cc -graph_SOURCES = graph.cc -ikwiad_SOURCES = ikwiad.cc -intvcomp_SOURCES = intvcomp.cc -intvcmp2_SOURCES = intvcmp2.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) -DUNABBREV='"^ie"' -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) -DUNABBREV='"^ieFG"' -tunenoform_SOURCES = equalsf.cc -tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DUNABBREV='"^ieFG"' +core_acc_SOURCES = core/acc.cc +core_bitvect_SOURCES = core/bitvect.cc +core_checkpsl_SOURCES = core/checkpsl.cc +core_checkta_SOURCES = core/checkta.cc +core_complement_SOURCES = core/complementation.cc +core_emptchk_SOURCES = core/emptchk.cc +core_graph_SOURCES = core/graph.cc +core_ikwiad_SOURCES = core/ikwiad.cc +core_intvcomp_SOURCES = core/intvcomp.cc +core_intvcmp2_SOURCES = core/intvcmp2.cc +core_ltlprod_SOURCES = core/ltlprod.cc +core_ngraph_SOURCES = core/ngraph.cc +core_parse_print_SOURCES = core/parse_print_test.cc +core_randtgba_SOURCES = core/randtgba.cc +core_readsat_SOURCES = core/readsat.cc +core_taatgba_SOURCES = core/taatgba.cc +core_tgbagraph_SOURCES = core/twagraph.cc +core_consterm_SOURCES = core/consterm.cc +core_equals_SOURCES = core/equalsf.cc +core_kind_SOURCES = core/kind.cc +core_length_SOURCES = core/length.cc +core_ltl2dot_SOURCES = core/readltl.cc +core_ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY +core_ltl2text_SOURCES = core/readltl.cc +core_ltlrel_SOURCES = core/ltlrel.cc +core_lunabbrev_SOURCES = core/equalsf.cc +core_lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DUNABBREV='"^ie"' +core_nenoform_SOURCES = core/equalsf.cc +core_nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM +core_nequals_SOURCES = core/equalsf.cc +core_nequals_CPPFLAGS = $(AM_CPPFLAGS) -DNEGATE +core_reduc_SOURCES = core/reduc.cc +core_reduccmp_SOURCES = core/equalsf.cc +core_reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC +core_reduceu_SOURCES = core/equalsf.cc +core_reduceu_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC -DEVENT_UNIV +core_reductaustr_SOURCES = core/equalsf.cc +core_reductaustr_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAUSTR +core_syntimpl_SOURCES = core/syntimpl.cc +core_tostring_SOURCES = core/tostring.cc +core_tunabbrev_SOURCES = core/equalsf.cc +core_tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DUNABBREV='"^ieFG"' +core_tunenoform_SOURCES = core/equalsf.cc +core_tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DUNABBREV='"^ieFG"' # Keep this sorted by STRENGTH. Test basic things first, # because such failures will be easier to diagnose and fix. -TESTS = $(TESTS_ltl) $(TESTS_graph) $(TESTS_kripke) $(TESTS_twa) +TESTS = $(TESTS_tl) $(TESTS_graph) $(TESTS_kripke) $(TESTS_twa) $(TESTS_python) -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_tl = \ + core/bare.test \ + core/parse.test \ + core/parseerr.test \ + core/utf8.test \ + core/length.test \ + core/equals.test \ + core/tostring.test \ + core/lunabbrev.test \ + core/tunabbrev.test \ + core/nenoform.test \ + core/tunenoform.test \ + core/unabbrevwm.test \ + core/consterm.test \ + core/kind.test \ + core/remove_x.test \ + core/ltlrel.test \ + core/ltlgrind.test \ + core/ltlcrossgrind.test \ + core/ltlfilt.test \ + core/exclusive-ltl.test \ + core/latex.test \ + core/lbt.test \ + core/lenient.test \ + core/rand.test \ + core/isop.test \ + core/syntimpl.test \ + core/reduc.test \ + core/reduc0.test \ + core/reducpsl.test \ + core/reduccmp.test \ + core/uwrm.test \ + core/eventuniv.test \ + core/stutter-ltl.test TESTS_graph = \ - graph.test \ - ngraph.test \ - tgbagraph.test + core/graph.test \ + core/ngraph.test \ + core/tgbagraph.test TESTS_kripke = \ - kripke.test + core/kripke.test TESTS_twa = \ - acc.test \ - acc2.test \ - intvcomp.test \ - bitvect.test \ - ltlcross3.test \ - taatgba.test \ - renault.test \ - nondet.test \ - det.test \ - neverclaimread.test \ - parseaut.test \ - optba.test \ - complete.test \ - complement.test \ - remfin.test \ - dstar.test \ - readsave.test \ - ltldo.test \ - ltldo2.test \ - maskacc.test \ - maskkeep.test \ - prodor.test \ - simdet.test \ - sim2.test \ - sim3.test \ - ltl2tgba.test \ - ltl2neverclaim.test \ - ltl2neverclaim-lbtt.test \ - ltlprod.test \ - explprod.test \ - explpro2.test \ - explpro3.test \ - explpro4.test \ - tripprod.test \ - dupexp.test \ - exclusive-tgba.test \ - remprop.test \ - degendet.test \ - degenid.test \ - degenlskip.test \ - randomize.test \ - lbttparse.test \ - scc.test \ - sccdot.test \ - sccsimpl.test \ - sepsets.test \ - dbacomp.test \ - obligation.test \ - wdba.test \ - wdba2.test \ - babiak.test \ - monitor.test \ - dra2dba.test \ - unambig.test \ - ltlcross4.test \ - ltl3dra.test \ - ltl2dstar.test \ - ltl2dstar2.test \ - ltl2dstar3.test \ - ltl2dstar4.test \ - ltl2ta.test \ - ltl2ta2.test \ - randaut.test \ - randtgba.test \ - isomorph.test \ - uniq.test \ - sbacc.test \ - stutter-tgba.test \ - strength.test \ - emptchk.test \ - emptchke.test \ - dfs.test \ - ltlcrossce.test \ - ltlcrossce2.test \ - emptchkr.test \ - ltlcounter.test \ - basimul.test \ - satmin.test \ - satmin2.test \ - spotlbtt.test \ - ltlcross.test \ - spotlbtt2.test \ - ltlcross2.test \ - complementation.test \ - randpsl.test \ - cycles.test - -EXTRA_DIST = $(TESTS) + core/acc.test \ + core/acc2.test \ + core/intvcomp.test \ + core/bitvect.test \ + core/ltlcross3.test \ + core/taatgba.test \ + core/renault.test \ + core/nondet.test \ + core/det.test \ + core/neverclaimread.test \ + core/parseaut.test \ + core/optba.test \ + core/complete.test \ + core/complement.test \ + core/remfin.test \ + core/dstar.test \ + core/readsave.test \ + core/ltldo.test \ + core/ltldo2.test \ + core/maskacc.test \ + core/maskkeep.test \ + core/prodor.test \ + core/simdet.test \ + core/sim2.test \ + core/sim3.test \ + core/ltl2tgba.test \ + core/ltl2neverclaim.test \ + core/ltl2neverclaim-lbtt.test \ + core/ltlprod.test \ + core/explprod.test \ + core/explpro2.test \ + core/explpro3.test \ + core/explpro4.test \ + core/tripprod.test \ + core/dupexp.test \ + core/exclusive-tgba.test \ + core/remprop.test \ + core/degendet.test \ + core/degenid.test \ + core/degenlskip.test \ + core/randomize.test \ + core/lbttparse.test \ + core/scc.test \ + core/sccdot.test \ + core/sccsimpl.test \ + core/sepsets.test \ + core/dbacomp.test \ + core/obligation.test \ + core/wdba.test \ + core/wdba2.test \ + core/babiak.test \ + core/monitor.test \ + core/dra2dba.test \ + core/unambig.test \ + core/ltlcross4.test \ + core/ltl3dra.test \ + core/ltl2dstar.test \ + core/ltl2dstar2.test \ + core/ltl2dstar3.test \ + core/ltl2dstar4.test \ + core/ltl2ta.test \ + core/ltl2ta2.test \ + core/randaut.test \ + core/randtgba.test \ + core/isomorph.test \ + core/uniq.test \ + core/sbacc.test \ + core/stutter-tgba.test \ + core/strength.test \ + core/emptchk.test \ + core/emptchke.test \ + core/dfs.test \ + core/ltlcrossce.test \ + core/ltlcrossce2.test \ + core/emptchkr.test \ + core/ltlcounter.test \ + core/basimul.test \ + core/satmin.test \ + core/satmin2.test \ + core/spotlbtt.test \ + core/ltlcross.test \ + core/spotlbtt2.test \ + core/ltlcross2.test \ + core/complementation.test \ + core/randpsl.test \ + core/cycles.test distclean-local: rm -rf $(TESTS:.test=.dir) + +TESTS_python = \ + python/acc_cond.ipynb \ + python/accparse.ipynb \ + python/accparse2.py \ + python/alarm.py \ + python/automata.ipynb \ + python/automata-io.ipynb \ + python/bddnqueen.py \ + python/decompose.ipynb \ + python/formulas.ipynb \ + python/implies.py \ + python/interdep.py \ + python/ltl2tgba.test \ + python/ltlparse.py \ + python/ltlsimple.py \ + python/minato.py \ + python/optionmap.py \ + python/parsetgba.py \ + python/piperead.ipynb \ + python/product.ipynb \ + python/randaut.ipynb \ + python/randgen.py \ + python/randltl.ipynb \ + python/relabel.py \ + python/remfin.py \ + python/satmin.py \ + python/setxor.py \ + python/testingaut.ipynb + +SUFFIXES = .ipynb .html +.ipynb.html: + $(IPYTHON) nbconvert $< --to html --stdout >$@ + +.PHONY: nb-html +nb-html: $(TESTS_python:.ipynb=.html) + + +EXTRA_DIST = \ + $(TESTS) \ + python/ltl2tgba.py \ + python/ipnbdoctest.py diff --git a/tests/core/.gitignore b/tests/core/.gitignore new file mode 100644 index 000000000..35bf1ca83 --- /dev/null +++ b/tests/core/.gitignore @@ -0,0 +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 +ikwiad +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/tests/acc.cc b/tests/core/acc.cc similarity index 100% rename from tests/acc.cc rename to tests/core/acc.cc diff --git a/tests/acc.test b/tests/core/acc.test similarity index 100% rename from tests/acc.test rename to tests/core/acc.test diff --git a/tests/acc2.test b/tests/core/acc2.test similarity index 88% rename from tests/acc2.test rename to tests/core/acc2.test index 42b7a008d..ba5c2ae67 100755 --- a/tests/acc2.test +++ b/tests/core/acc2.test @@ -23,10 +23,10 @@ set -e -../../bin/ltl2tgba -H 'GFa & GFb' > in +ltl2tgba -H 'GFa & GFb' > in grep 'Acceptance:' in > expected -../../bin/ltl2tgba -H 'GFa & GFb' --stats='Acceptance: %a %g' > out1 -../../bin/autfilt -H in --stats='Acceptance: %A %G' > out2 +ltl2tgba -H 'GFa & GFb' --stats='Acceptance: %a %g' > out1 +autfilt -H in --stats='Acceptance: %A %G' > out2 diff out1 expected diff out2 expected @@ -64,7 +64,7 @@ EOF while IFS=, read a b do (cat header; echo 'Acceptance:' $a; cat body) | - ../../bin/autfilt -H --dnf-acc --stats '%A %G, %a %g' + autfilt -H --dnf-acc --stats '%A %G, %a %g' done < acceptances > output diff acceptances output @@ -86,7 +86,7 @@ EOF while IFS=, read a b do (cat header; echo 'Acceptance:' $a; cat body) | - ../../bin/autfilt -H --cnf-acc --stats '%A %G, %a %g' + autfilt -H --cnf-acc --stats '%A %G, %a %g' done < acceptances > output diff acceptances output @@ -109,7 +109,7 @@ EOF while IFS=, read a b do (cat header; echo 'Acceptance:' $a; cat body) | - ../../bin/autfilt -H --complement-acc --stats '%A %G, %a %g' + autfilt -H --complement-acc --stats '%A %G, %a %g' done < acceptances > output diff acceptances output diff --git a/tests/babiak.test b/tests/core/babiak.test similarity index 98% rename from tests/babiak.test rename to tests/core/babiak.test index 5b1413f8a..95b8affae 100755 --- a/tests/babiak.test +++ b/tests/core/babiak.test @@ -41,7 +41,7 @@ EOF ltl2tgba=../ikwiad -../../bin/ltlcross %T" \ "$ltl2tgba -N -r4 -R3f %f >%N" \ "$ltl2tgba -N -r7 -R3 -x -Rm %f >%N" \ diff --git a/tests/bare.test b/tests/core/bare.test similarity index 78% rename from tests/bare.test rename to tests/core/bare.test index 2cc955f3f..719fdd663 100755 --- a/tests/bare.test +++ b/tests/core/bare.test @@ -21,13 +21,13 @@ . ./defs set -e -test "`../../bin/ltlfilt -p -f 'GFP_0.b_c'`" = "G(F(P_0.b_c))" -test "`../../bin/ltlfilt -f 'GFP_0.b_c'`" = "GFP_0.b_c" -foo=`../../bin/ltlfilt -p -f 'GF"P_0.b_c"'` +test "`ltlfilt -p -f 'GFP_0.b_c'`" = "G(F(P_0.b_c))" +test "`ltlfilt -f 'GFP_0.b_c'`" = "GFP_0.b_c" +foo=`ltlfilt -p -f 'GF"P_0.b_c"'` test "$foo" = "G(F(P_0.b_c))" -foo=`../../bin/ltlfilt -p -f '"a.b" U c.d.e'` +foo=`ltlfilt -p -f '"a.b" U c.d.e'` test "$foo" = "(a.b) U (c.d.e)" -foo=`../../bin/ltlfilt -f '"a.b" U c.d.e'` +foo=`ltlfilt -f '"a.b" U c.d.e'` test "$foo" = "a.b U c.d.e" diff --git a/tests/basimul.test b/tests/core/basimul.test similarity index 97% rename from tests/basimul.test rename to tests/core/basimul.test index 3f870a221..68c253fb6 100755 --- a/tests/basimul.test +++ b/tests/core/basimul.test @@ -22,7 +22,7 @@ set -e -ltl2tgba=../../bin/ltl2tgba +ltl2tgba=ltl2tgba # This bug was found while working on the state-based acceptance @@ -54,7 +54,7 @@ ltl2tgba=../../bin/ltl2tgba # --spin -x ba-simul=2 # --spin -x ba-simul=3 -../../bin/ltlcross --seed=0 --products=5 --json=out.json \ +ltlcross --seed=0 --products=5 --json=out.json \ -f 'X((F(Xa | b) W c) U (Xc W (a & d)))' \ -f '((<> p5 V ((p0 U p1) <-> (p5 \/ p1))) -> ((<> p4 V p2) M p2))' \ -f '!p2 & (Fp5 R (((p0 U p1) & (p5 | p1)) | (!p5 & (!p0 R !p1))))' \ diff --git a/tests/bitvect.cc b/tests/core/bitvect.cc similarity index 100% rename from tests/bitvect.cc rename to tests/core/bitvect.cc diff --git a/tests/bitvect.test b/tests/core/bitvect.test similarity index 100% rename from tests/bitvect.test rename to tests/core/bitvect.test diff --git a/tests/checkpsl.cc b/tests/core/checkpsl.cc similarity index 100% rename from tests/checkpsl.cc rename to tests/core/checkpsl.cc diff --git a/tests/checkta.cc b/tests/core/checkta.cc similarity index 100% rename from tests/checkta.cc rename to tests/core/checkta.cc diff --git a/tests/complement.test b/tests/core/complement.test similarity index 96% rename from tests/complement.test rename to tests/core/complement.test index ef968a697..92f56e7c1 100755 --- a/tests/complement.test +++ b/tests/core/complement.test @@ -22,9 +22,9 @@ set -e -autfilt=../../bin/autfilt -ltl2tgba=../../bin/ltl2tgba -randaut=../../bin/randaut +autfilt=autfilt +ltl2tgba=ltl2tgba +randaut=randaut $randaut -H -A 'random 0..4' -Q1..10 -D -n 50 0..2 >aut run 0 $autfilt --complement -H aut >/dev/null diff --git a/tests/complementation.cc b/tests/core/complementation.cc similarity index 100% rename from tests/complementation.cc rename to tests/core/complementation.cc diff --git a/tests/complementation.test b/tests/core/complementation.test similarity index 97% rename from tests/complementation.test rename to tests/core/complementation.test index 201a4d440..d8bd0e137 100755 --- a/tests/complementation.test +++ b/tests/core/complementation.test @@ -66,4 +66,4 @@ run 0 ../complement -H -a x.hoa > nx.hoa run 0 ../ikwiad -XH -e nx.hoa # however the intersection of both should not # accept any run. -run 1 ../../bin/autfilt -q nx.hoa --intersect x.hoa +run 1 autfilt -q nx.hoa --intersect x.hoa diff --git a/tests/complete.test b/tests/core/complete.test similarity index 97% rename from tests/complete.test rename to tests/core/complete.test index 777a41924..19f82465a 100755 --- a/tests/complete.test +++ b/tests/core/complete.test @@ -114,6 +114,6 @@ State: 1 --END-- EOF -run 0 ../../bin/autfilt -CH automaton >out +run 0 autfilt -CH automaton >out cat out diff out expected diff --git a/tests/consterm.cc b/tests/core/consterm.cc similarity index 100% rename from tests/consterm.cc rename to tests/core/consterm.cc diff --git a/tests/consterm.test b/tests/core/consterm.test similarity index 100% rename from tests/consterm.test rename to tests/core/consterm.test diff --git a/tests/cycles.test b/tests/core/cycles.test similarity index 100% rename from tests/cycles.test rename to tests/core/cycles.test diff --git a/tests/dbacomp.test b/tests/core/dbacomp.test similarity index 96% rename from tests/dbacomp.test rename to tests/core/dbacomp.test index e5d1b1dbc..43d59d53b 100755 --- a/tests/dbacomp.test +++ b/tests/core/dbacomp.test @@ -56,4 +56,4 @@ EOF # Check emptiness of product with complement. run 0 ../ikwiad -H -DC -C -XH input.hoa > output.hoa -run 1 ../../bin/autfilt -q input.hoa --intersect output.hoa +run 1 autfilt -q input.hoa --intersect output.hoa diff --git a/tests/defs.in b/tests/core/defs.in similarity index 89% rename from tests/defs.in rename to tests/core/defs.in index 48cca35e4..11a9fd540 100644 --- a/tests/defs.in +++ b/tests/core/defs.in @@ -58,14 +58,13 @@ case $srcdir in esac DOT='@DOT@' -top_builddir='../@top_builddir@' LBTT="@LBTT@" LBTT_TRANSLATE="@LBTT_TRANSLATE@" VALGRIND='@VALGRIND@' SPIN='@SPIN@' LTL2BA='@LTL2BA@' PYTHON='@PYTHON@' -top_srcdir='../@top_srcdir@' +top_srcdir='@abs_top_srcdir@' # The test cases assume these variable are undefined unset SPOT_DOTEXTRA @@ -83,9 +82,16 @@ run() shift exitcode=0 if test -n "$VALGRIND"; then + # Replace the command name by a full path after lookup in $PATH, so + # that valgrind will find it. + cmd=`command -v $1` + shift + test -n "$cmd" || exit 1 + set $cmd "$@" + # Run valgrind. exec 6>valgrind.err - GLIBCPP_FORCE_NEW=1 \ - ../../libtool --mode=execute \ + GLIBCXX_FORCE_NEW=1 \ + @abs_top_builddir@/libtool --mode=execute \ $VALGRIND --tool=memcheck --leak-check=yes --log-fd=6 -q "$@" || exitcode=$? cat valgrind.err 1>&2 diff --git a/tests/degendet.test b/tests/core/degendet.test similarity index 100% rename from tests/degendet.test rename to tests/core/degendet.test diff --git a/tests/degenid.test b/tests/core/degenid.test similarity index 95% rename from tests/degenid.test rename to tests/core/degenid.test index fa9271a9c..1bc11d89f 100755 --- a/tests/degenid.test +++ b/tests/core/degenid.test @@ -133,7 +133,7 @@ grep 'states: 8' out # This automaton should have a 3-state BA, but it's really # easy to obtain a 4-state BA when tweaking the degeneralization # to ignore arc entering an SCC. -test 3 = "`../../bin/ltl2tgba -B 'G(a|G(b|Fc))' --stats=%s`" +test 3 = "`ltl2tgba -B 'G(a|G(b|Fc))' --stats=%s`" # This 7-state DRA (built with @@ -220,12 +220,12 @@ Acc-Sig: 0 EOF -run 0 ../../bin/dstar2tgba in.dra -BD --stats=%s > out.stat +run 0 dstar2tgba in.dra -BD --stats=%s > out.stat test 5 = "`cat out.stat`" # Only one state should be accepting. In spot 1.2.x an initial state # in a trivial SCC was marked as accepting: this is superfluous. -../../bin/ltl2tgba -BH 'a & GFb & GFc' > out +ltl2tgba -BH 'a & GFb & GFc' > out cat out cat >expected< out1 -../../bin/ltl2tgba -B -x degen-lskip=1 'GFa & GFb' --hoa > out2 -../../bin/ltl2tgba -B -x degen-lskip=0 'GFa & GFb' --hoa > out3 -../../bin/ltl2tgba -B -x degen-lskip=1,degen-lowinit=1 'GFa & GFb' --hoa > out4 -../../bin/ltl2tgba -B -x degen-lskip=0,degen-lowinit=1 'GFa & GFb' --hoa > out5 +ltl2tgba -B 'GFa & GFb' --hoa > out1 +ltl2tgba -B -x degen-lskip=1 'GFa & GFb' --hoa > out2 +ltl2tgba -B -x degen-lskip=0 'GFa & GFb' --hoa > out3 +ltl2tgba -B -x degen-lskip=1,degen-lowinit=1 'GFa & GFb' --hoa > out4 +ltl2tgba -B -x degen-lskip=0,degen-lowinit=1 'GFa & GFb' --hoa > out5 diff out1 out2 cmp out2 out3 && exit 1 @@ -122,13 +122,13 @@ State: 2 EOF -run 0 ../../bin/autfilt -q -F out2 --isomorph expected2 -run 0 ../../bin/autfilt -q -F out3 --isomorph expected3 +run 0 autfilt -q -F out2 --isomorph expected2 +run 0 autfilt -q -F out3 --isomorph expected3 cat out4 out5 -../../bin/autfilt -q out4 --isomorph expected2 && exit 1 -../../bin/autfilt -q out5 --isomorph expected3 && exit 1 +autfilt -q out4 --isomorph expected2 && exit 1 +autfilt -q out5 --isomorph expected3 && exit 1 -../../bin/autfilt -q out4 --isomorph expected4 -../../bin/autfilt -q out5 --isomorph expected5 +autfilt -q out4 --isomorph expected4 +autfilt -q out5 --isomorph expected5 diff --git a/tests/det.test b/tests/core/det.test similarity index 92% rename from tests/det.test rename to tests/core/det.test index 37799fb87..ba4af3f17 100755 --- a/tests/det.test +++ b/tests/core/det.test @@ -21,7 +21,7 @@ . ./defs set -e -ltl2tgba=../../bin/ltl2tgba +ltl2tgba=ltl2tgba cat >formulas <<'EOF' 1,13,X((a M F((!b & !c) | (b & c))) W (G!c U b)) @@ -111,8 +111,8 @@ State: 4 {0} EOF run 0 ../ikwiad -H -DC -XH in.hoa > out.hoa -run 1 ../../bin/autfilt -q --are-isomorph in.hoa out.hoa -run 0 ../../bin/autfilt -q --are-isomorph ex.hoa out.hoa +run 1 autfilt -q --are-isomorph in.hoa out.hoa +run 0 autfilt -q --are-isomorph ex.hoa out.hoa run 0 ../ikwiad -x -DC 'GFa & XGFb' > out.tgba cat >ex.tgba < out.hoa +run 0 ltl2tgba -H '(0 R Xa) R (a xor Fa)' > out.hoa grep deterministic out.hoa && exit 1 @@ -154,7 +154,7 @@ G(!a | XXXXXXa),64 G(!a | XXXXXXXa),128 G(!a | XXXXXXXXa),256 EOF -run 0 ../../bin/ltl2tgba -D -F input/1 --stats='%f,%s' > output +run 0 ltl2tgba -D -F input/1 --stats='%f,%s' > output cat output diff input output diff --git a/tests/dfs.test b/tests/core/dfs.test similarity index 100% rename from tests/dfs.test rename to tests/core/dfs.test diff --git a/tests/dra2dba.test b/tests/core/dra2dba.test similarity index 97% rename from tests/dra2dba.test rename to tests/core/dra2dba.test index 104a21590..20b6586f5 100755 --- a/tests/dra2dba.test +++ b/tests/core/dra2dba.test @@ -329,5 +329,5 @@ Acc-Sig: +2 13 EOF -test `../../bin/dstar2tgba -D in.dra --stats="%d:%s:%e"` = "1:23:143" +test `dstar2tgba -D in.dra --stats="%d:%s:%e"` = "1:23:143" diff --git a/tests/dstar.test b/tests/core/dstar.test similarity index 93% rename from tests/dstar.test rename to tests/core/dstar.test index 7e161739a..0cfd5f2e7 100755 --- a/tests/dstar.test +++ b/tests/core/dstar.test @@ -148,8 +148,8 @@ EOF diff expected stdout # These one could be reduced to 2 5 0 0 and 3 8 1 0 -test "`../../bin/dstar2tgba -D dsa.dstar --stats '%s %t %p %d'`" = "4 8 0 0" -test "`../../bin/dstar2tgba -DC dsa.dstar --stats '%s %t %p %d'`" = "5 11 1 0" +test "`dstar2tgba -D dsa.dstar --stats '%s %t %p %d'`" = "4 8 0 0" +test "`dstar2tgba -DC dsa.dstar --stats '%s %t %p %d'`" = "5 11 1 0" @@ -212,7 +212,7 @@ State: 3 "str\n\"ing" Acc-Sig: -0 +1 3 3 3 3 State: 4 "more\"string\"" Acc-Sig: +0 +1 3 4 3 4 EOF -run 0 ../../bin/autfilt -B dra.dstar | tee stdout +run 0 autfilt -B dra.dstar | tee stdout cat >expected <expected < out +dstar2tgba --name=%F:%L -D dra.dstar --stats '%s %t %p %d %m' > out cat out diff expected out @@ -281,7 +281,7 @@ State: 0 Acc-Sig: 0 EOF -run 0 ../../bin/dstar2tgba --name=%F --dot=nt aut.dsa | tee stdout +run 0 dstar2tgba --name=%F --dot=nt aut.dsa | tee stdout cat >expected<out +run 0 ltlfilt --exclusive-ap=a,b,c --exclusive-ap=d,e formulas >out cat out diff out expected -run 0 ../../bin/ltlfilt --exclusive-ap='"a" ,b, "c" ' --exclusive-ap=' d , e' \ +run 0 ltlfilt --exclusive-ap='"a" ,b, "c" ' --exclusive-ap=' d , e' \ formulas >out cat out diff out expected -../../bin/ltlfilt --exclusive-ap='"a","b' 2>stderr && exit 1 +ltlfilt --exclusive-ap='"a","b' 2>stderr && exit 1 grep 'missing closing ."' stderr -../../bin/ltlfilt --exclusive-ap='a,,b' 2>stderr && exit 1 +ltlfilt --exclusive-ap='a,,b' 2>stderr && exit 1 grep "unexpected ',' in a,,b" stderr -../../bin/ltlfilt --exclusive-ap='"a"b' 2>stderr && exit 1 +ltlfilt --exclusive-ap='"a"b' 2>stderr && exit 1 grep "unexpected character 'b' in \"a\"b" stderr diff --git a/tests/exclusive-tgba.test b/tests/core/exclusive-tgba.test similarity index 90% rename from tests/exclusive-tgba.test rename to tests/core/exclusive-tgba.test index 8d6c87110..eb7a74263 100755 --- a/tests/exclusive-tgba.test +++ b/tests/core/exclusive-tgba.test @@ -82,12 +82,12 @@ State: 2 {0} --END-- EOF -run 0 ../../bin/autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \ +run 0 autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \ automaton >out cat out diff out expected -run 0 ../../bin/autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \ +run 0 autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \ --simplify-exclusive-ap automaton >out2 cat out2 diff out2 expected-simpl @@ -151,12 +151,12 @@ State: 2 {0} --END-- EOF -run 0 ../../bin/autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \ +run 0 autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \ automaton >out cat out diff out expected -run 0 ../../bin/autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \ +run 0 autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \ --simplify-exclusive-ap automaton >out2 cat out2 diff out2 expected-simpl diff --git a/tests/explpro2.test b/tests/core/explpro2.test similarity index 93% rename from tests/explpro2.test rename to tests/core/explpro2.test index 2d71926a2..c57826585 100755 --- a/tests/explpro2.test +++ b/tests/core/explpro2.test @@ -77,7 +77,7 @@ State: 2 --END-- EOF -run 0 ../../bin/autfilt input1 --product input2 --hoa | tee stdout -run 0 ../../bin/autfilt -F stdout --isomorph expected +run 0 autfilt input1 --product input2 --hoa | tee stdout +run 0 autfilt -F stdout --isomorph expected rm input1 input2 stdout expected diff --git a/tests/explpro3.test b/tests/core/explpro3.test similarity index 93% rename from tests/explpro3.test rename to tests/core/explpro3.test index 2c6ad241b..e682e5d3b 100755 --- a/tests/explpro3.test +++ b/tests/core/explpro3.test @@ -77,6 +77,6 @@ State: 2 --END-- EOF -run 0 ../../bin/autfilt input1 --product input2 --hoa | tee stdout -run 0 ../../bin/autfilt -F stdout --isomorph expected +run 0 autfilt input1 --product input2 --hoa | tee stdout +run 0 autfilt -F stdout --isomorph expected rm input1 input2 stdout expected diff --git a/tests/explpro4.test b/tests/core/explpro4.test similarity index 91% rename from tests/explpro4.test rename to tests/core/explpro4.test index 8852e0a71..a62444aa8 100755 --- a/tests/explpro4.test +++ b/tests/core/explpro4.test @@ -84,8 +84,8 @@ State: 0 --END-- EOF -run 0 ../../bin/autfilt input1 --product input2 --hoa | tee stdout -run 0 ../../bin/autfilt -q stdout --isomorph expected -run 1 ../../bin/autfilt -q stdout --isomorph unexpected +run 0 autfilt input1 --product input2 --hoa | tee stdout +run 0 autfilt -q stdout --isomorph expected +run 1 autfilt -q stdout --isomorph unexpected true diff --git a/tests/explprod.test b/tests/core/explprod.test similarity index 91% rename from tests/explprod.test rename to tests/core/explprod.test index 45005779d..d216784db 100755 --- a/tests/explprod.test +++ b/tests/core/explprod.test @@ -80,7 +80,7 @@ State: 3 --END-- EOF -run 0 ../../bin/autfilt input1 --product input2 --hoa | tee stdout +run 0 autfilt input1 --product input2 --hoa | tee stdout diff stdout expected cat >expected <iso$i - ../../bin/autfilt iso$i --randomize --hoa >aut$i + randaut a b --seed=$i -Q10 --hoa >iso$i + autfilt iso$i --randomize --hoa >aut$i done for i in 3 4 5; do - ../../bin/randaut a b --seed=$i -Q10 -D --hoa >iso$i - ../../bin/autfilt iso$i --randomize --hoa >aut$i + randaut a b --seed=$i -Q10 -D --hoa >iso$i + autfilt iso$i --randomize --hoa >aut$i done cat aut0 aut1 aut2 aut3 aut4 aut5 > all (for i in 0 1 2 3 4 5; do - run 0 ../../bin/autfilt all --are-isomorphic iso$i --hoa + run 0 autfilt all --are-isomorphic iso$i --hoa done) > output diff all output @@ -104,8 +104,8 @@ State: 2 [t] 2 [t] 2 --END-- EOF -run 0 ../../bin/autfilt aut1 --are-isomorphic aut2 -run 0 ../../bin/autfilt aut3 --are-isomorphic aut4 +run 0 autfilt aut1 --are-isomorphic aut2 +run 0 autfilt aut3 --are-isomorphic aut4 -run 0 ../../bin/autfilt -u aut1 aut2 aut2 aut3 -c >out +run 0 autfilt -u aut1 aut2 aut2 aut3 -c >out test 2 = "`cat out`" diff --git a/tests/isop.test b/tests/core/isop.test similarity index 93% rename from tests/isop.test rename to tests/core/isop.test index ef1e72b7c..cdd35d003 100755 --- a/tests/isop.test +++ b/tests/core/isop.test @@ -29,7 +29,7 @@ GF((a | b) & (b | d)) EOF # Make sure --boolean-to-isop works as expected... -run 0 ../../bin/ltlfilt --boolean-to-isop input > output +run 0 ltlfilt --boolean-to-isop input > output cat> expected< output +run 0 ltlfilt input > output cat> expected< b) & (b -> d) diff --git a/tests/kind.cc b/tests/core/kind.cc similarity index 100% rename from tests/kind.cc rename to tests/core/kind.cc diff --git a/tests/kind.test b/tests/core/kind.test similarity index 100% rename from tests/kind.test rename to tests/core/kind.test diff --git a/tests/kripke.test b/tests/core/kripke.test similarity index 100% rename from tests/kripke.test rename to tests/core/kripke.test diff --git a/tests/latex.test b/tests/core/latex.test similarity index 93% rename from tests/latex.test rename to tests/core/latex.test index 266177668..6e94e14d6 100755 --- a/tests/latex.test +++ b/tests/core/latex.test @@ -48,8 +48,8 @@ cat <<\EOF \begin{document} \begin{tabular}{ll} EOF -( ../../bin/ltlfilt --latex input --format='\texttt{%F:%L} & $%f$ \\'; - ../../bin/genltl --go-theta=1..3 --latex \ +( ltlfilt --latex input --format='\texttt{%F:%L} & $%f$ \\'; + genltl --go-theta=1..3 --latex \ --format='\texttt{--%F:%L} & $%f$ \\') cat <<\EOF \end{tabular} diff --git a/tests/lbt.test b/tests/core/lbt.test similarity index 97% rename from tests/lbt.test rename to tests/core/lbt.test index 15f7bfebf..4b9a30e0a 100755 --- a/tests/lbt.test +++ b/tests/core/lbt.test @@ -21,9 +21,9 @@ . ./defs set -e -ltlfilt=../../bin/ltlfilt -randltl=../../bin/randltl -genltl=../../bin/genltl +ltlfilt=ltlfilt +randltl=randltl +genltl=genltl # Some example formulas taken from Ruediger Ehlers's dbaminimizer # http://react.cs.uni-saarland.de/tools/dbaminimizer diff --git a/tests/lbttparse.test b/tests/core/lbttparse.test similarity index 83% rename from tests/lbttparse.test rename to tests/core/lbttparse.test index 90f75d66e..8bcf380fe 100755 --- a/tests/lbttparse.test +++ b/tests/core/lbttparse.test @@ -25,38 +25,38 @@ set -e for f in 'p0 U p1 U p2' 'Gp00 | Gp13 | Gp42' '{(1;1)*}[]->p1' do # Make sure Spot can read the LBTT it produces - run 0 ../../bin/ltl2tgba --lbtt "$f" > out + run 0 ltl2tgba --lbtt "$f" > out s=`wc -l < out` - if ../../bin/ltl2tgba -H "$f" | grep 'properties:.*state-acc'; then + if ltl2tgba -H "$f" | grep 'properties:.*state-acc'; then head -n 1 out | grep t && exit 1 else head -n 1 out | grep t fi - run 0 ../../bin/autfilt --lbtt out > out2 + run 0 autfilt --lbtt out > out2 s2=`wc -l < out2` test "$s" -eq "$s2" # The LBTT output use 2 lines par state, one line per transition, # and one extra line for header. - run 0 ../../bin/ltl2tgba "$f" --stats 'expr %s \* 2 + %e + 1' > size + run 0 ltl2tgba "$f" --stats 'expr %s \* 2 + %e + 1' > size l=$(eval "$(cat size)") test "$s" -eq "$l" # Make sure we output the state-based format # for BA... - run 0 ../../bin/ltl2tgba --ba --lbtt --low --any "$f" >out4 + run 0 ltl2tgba --ba --lbtt --low --any "$f" >out4 head -n 1 out4 | grep t && exit 1 s4=`wc -l < out4` test "$s" -eq "$s4" - run 0 ../../bin/autfilt --lbtt out4 > out5 - run 0 ../../bin/autfilt out4 --are-isomorphic out5 + run 0 autfilt --lbtt out4 > out5 + run 0 autfilt out4 --are-isomorphic out5 # ... unless --lbtt=t is used. - run 0 ../../bin/ltl2tgba --ba --lbtt=t --low --any "$f" >out6 + run 0 ltl2tgba --ba --lbtt=t --low --any "$f" >out6 head -n 1 out6 | grep t s6=`wc -l < out6` test "$s" -eq "$s6" - run 0 ../../bin/autfilt --lbtt out6 > out7 - run 0 ../../bin/autfilt out6 --are-isomorphic out7 + run 0 autfilt --lbtt out6 > out7 + run 0 autfilt out6 --are-isomorphic out7 done @@ -148,7 +148,7 @@ cat >input < output +run 0 autfilt --stats '%s %t %e %a' input > output cat >expected< stderr && exit 1 +autfilt -q input 2> stderr && exit 1 cat stderr diff stderr expected diff --git a/tests/length.cc b/tests/core/length.cc similarity index 100% rename from tests/length.cc rename to tests/core/length.cc diff --git a/tests/length.test b/tests/core/length.test similarity index 100% rename from tests/length.test rename to tests/core/length.test diff --git a/tests/lenient.test b/tests/core/lenient.test similarity index 98% rename from tests/lenient.test rename to tests/core/lenient.test index a39aeb9ea..2e0bdeab4 100755 --- a/tests/lenient.test +++ b/tests/core/lenient.test @@ -22,7 +22,7 @@ set -e -ltlfilt=../../bin/ltlfilt +ltlfilt=ltlfilt cat >input < GFb' -Hi > out.hoa cat >expected < %T" \ "$ltl2tgba -t -r4 -R3f %f > %T" \ "$ltl2tgba -N %f > %N" \ diff --git a/tests/ltl2ta.test b/tests/core/ltl2ta.test similarity index 100% rename from tests/ltl2ta.test rename to tests/core/ltl2ta.test diff --git a/tests/ltl2ta2.test b/tests/core/ltl2ta2.test similarity index 94% rename from tests/ltl2ta2.test rename to tests/core/ltl2ta2.test index b4fc67762..c73013efe 100755 --- a/tests/ltl2ta2.test +++ b/tests/core/ltl2ta2.test @@ -25,4 +25,4 @@ set -e # This used to trigger an assert because of BA simulation not # returning an instance of spot::sba. -run 0 ../../bin/ltl2tgta --ta 'G(F(a U b) U (c M d))' +run 0 ltl2tgta --ta 'G(F(a U b) U (c M d))' diff --git a/tests/ltl2tgba.test b/tests/core/ltl2tgba.test similarity index 86% rename from tests/ltl2tgba.test rename to tests/core/ltl2tgba.test index fa81056f2..bdb114092 100755 --- a/tests/ltl2tgba.test +++ b/tests/core/ltl2tgba.test @@ -98,7 +98,7 @@ EOF run 0 ../checkpsl check.txt # Make sure False has one acceptance set when generating Büchi automata -test 1 -eq `../../bin/ltl2tgba -B false --stats %a` +test 1 -eq `ltl2tgba -B false --stats %a` # In particular, Spot 0.9 would incorrectly reject the sequence: # (aÌ…b;aÌ…b;aÌ…bÌ…);(aÌ…b;aÌ…b;aÌ…bÌ…);(aÌ…b;aÌ…b;aÌ…bÌ…);... in 'G!{(b;1)*;a}' @@ -194,28 +194,28 @@ grep 'states: 4$' stdout # A bug in the translation of !{xxx} when xxx reduces to false caused # the following formula to be considered equivalent to anything... -../../bin/ltlfilt -f '!{[*2] && [*0..1]}' --equivalent-to 'false' && exit 1 -../../bin/ltlfilt -f '!{[*2] && [*0..1]}' --equivalent-to 'true' +ltlfilt -f '!{[*2] && [*0..1]}' --equivalent-to 'false' && exit 1 +ltlfilt -f '!{[*2] && [*0..1]}' --equivalent-to 'true' # Test some equivalences fixed in Spot 1.1.4 -../../bin/ltlfilt -f '{{a;b}[*]}' --equivalent-to 'a & Xb' -../../bin/ltlfilt -r -f '{{a;b}[*]}' --equivalent-to 'a & Xb' -../../bin/ltlfilt -f '!{{a;b}[*]}' --equivalent-to '!a | X!b' -../../bin/ltlfilt -r -f '!{{a;b}[*]}' --equivalent-to '!a | X!b' -../../bin/ltlfilt -f '{a[*];b[*]}' --equivalent-to 'a | b' -../../bin/ltlfilt -r -f '{a[*];b[*]}' --equivalent-to 'a | b' +ltlfilt -f '{{a;b}[*]}' --equivalent-to 'a & Xb' +ltlfilt -r -f '{{a;b}[*]}' --equivalent-to 'a & Xb' +ltlfilt -f '!{{a;b}[*]}' --equivalent-to '!a | X!b' +ltlfilt -r -f '!{{a;b}[*]}' --equivalent-to '!a | X!b' +ltlfilt -f '{a[*];b[*]}' --equivalent-to 'a | b' +ltlfilt -r -f '{a[*];b[*]}' --equivalent-to 'a | b' # A couple of tests for the [:*i..j] operator -../../bin/ltlfilt -q -f '{{a;b}[:*1..2];c}' \ +ltlfilt -q -f '{{a;b}[:*1..2];c}' \ --equivalent-to '(a&X(b&Xc)) | a&(X(b&a&X(b&Xc)))' -../../bin/ltlfilt -q -r -f '{{a;b}[:*1..2];c}' \ +ltlfilt -q -r -f '{{a;b}[:*1..2];c}' \ --equivalent-to '(a&X(b&Xc)) | a&(X(b&a&X(b&Xc)))' -../../bin/ltlfilt -q -f '{{a*}[:+];c}' --equivalent-to 'Xc R a' -../../bin/ltlfilt -q -r -f '{{a*}[:+];c}' --equivalent-to 'Xc R a' -../../bin/ltlfilt -q -f '{c && {b | [*0]}[:+]}' --equivalent-to 'c & b' -../../bin/ltlfilt -q -r -f '{c && {b | [*0]}[:+]}' --equivalent-to 'c & b' +ltlfilt -q -f '{{a*}[:+];c}' --equivalent-to 'Xc R a' +ltlfilt -q -r -f '{{a*}[:+];c}' --equivalent-to 'Xc R a' +ltlfilt -q -f '{c && {b | [*0]}[:+]}' --equivalent-to 'c & b' +ltlfilt -q -r -f '{c && {b | [*0]}[:+]}' --equivalent-to 'c & b' # test unknown dot options -../../bin/ltl2tgba --dot=@ a 2>stderr && exit 1 +ltl2tgba --dot=@ a 2>stderr && exit 1 grep 'ltl2tgba: unknown option.*@' stderr diff --git a/tests/ltl3dra.test b/tests/core/ltl3dra.test similarity index 95% rename from tests/ltl3dra.test rename to tests/core/ltl3dra.test index a1a8ad321..e4f7af1fa 100755 --- a/tests/ltl3dra.test +++ b/tests/core/ltl3dra.test @@ -30,7 +30,7 @@ set -e # This used to crash ltlcross because the number of # acceptance sets generated was to high. -../../bin/ltlcross '../../bin/ltl2tgba' 'ltl3dra' -f '(<>((((p0) && +ltlcross 'ltl2tgba' 'ltl3dra' -f '(<>((((p0) && (!(<>(p2)))) || ((!(p0)) && (<>(p2)))) U ((<>(((p0) && (!([](((!(p1)) && ([](p3))) || ((p1) && (!([](p3)))))))) || ((!(p0)) && ([](((!(p1)) && ([](p3))) || ((p1) && (!([](p3))))))))) && (((p0) && (!(<>(p2)))) diff --git a/tests/ltlcounter.test b/tests/core/ltlcounter.test similarity index 98% rename from tests/ltlcounter.test rename to tests/core/ltlcounter.test index 47e178616..9d08b6c66 100755 --- a/tests/ltlcounter.test +++ b/tests/core/ltlcounter.test @@ -24,7 +24,7 @@ set -e pwd -lc="../../bin/genltl" +lc="genltl" run='run 0' diff --git a/tests/ltlcross.test b/tests/core/ltlcross.test similarity index 95% rename from tests/ltlcross.test rename to tests/core/ltlcross.test index 3fcc57572..ce2564136 100755 --- a/tests/ltlcross.test +++ b/tests/core/ltlcross.test @@ -36,9 +36,9 @@ p0 xor (p0 W X!p0) p0 & (!p0 W Xp0) EOF # Random formulas -../../bin/randltl -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 +randltl -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 ) | -../../bin/ltlcross --products=2 \ +ltlcross --products=2 \ "$ltl2tgba -t -f %f > %T" \ "$ltl2tgba -t -f -y %f > %T" \ "$ltl2tgba -t -f -fu %f > %T" \ diff --git a/tests/ltlcross2.test b/tests/core/ltlcross2.test similarity index 92% rename from tests/ltlcross2.test rename to tests/core/ltlcross2.test index e4d51017b..93ccde10b 100755 --- a/tests/ltlcross2.test +++ b/tests/core/ltlcross2.test @@ -21,10 +21,10 @@ . ./defs set -e -ltl2tgba=../../bin/ltl2tgba +ltl2tgba=ltl2tgba -../../bin/randltl -P -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 --seed=314 | -../../bin/ltlcross --products=3 --timeout=60 \ +randltl -P -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 --seed=314 | +ltlcross --products=3 --timeout=60 \ "$ltl2tgba --lbtt --any --low %f > %T" \ "$ltl2tgba --lbtt --any --medium %f > %T" \ "$ltl2tgba --hoa --any --high %f > %H" \ diff --git a/tests/ltlcross3.test b/tests/core/ltlcross3.test similarity index 85% rename from tests/ltlcross3.test rename to tests/core/ltlcross3.test index 91e08c5a0..5ef75e4ed 100755 --- a/tests/ltlcross3.test +++ b/tests/core/ltlcross3.test @@ -31,21 +31,21 @@ check_csv() done) } -ltl2tgba=../../bin/ltl2tgba +ltl2tgba=ltl2tgba # Make sure ltlcross quotes formulas correctly cat >formula <<\EOF G"a'-'>'b" EOF -run 0 ../../bin/ltlcross -F formula --csv=out.csv \ +run 0 ltlcross -F formula --csv=out.csv \ "$ltl2tgba -s %f >%N" \ "$ltl2tgba --lenient -s %s >%N" -run 2 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'foo bar' 2>stderr -f a +run 2 ltlcross "$ltl2tgba -s %f >%N" 'foo bar' 2>stderr -f a grep 'ltlcross.*no input.*in.*foo bar' stderr # Make sure non-zero exit codes are reported... -run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ +run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ -f a --csv=out.csv 2>stderr grep '"exit_status"' out.csv grep '"exit_code"' out.csv @@ -54,7 +54,7 @@ test `grep '"exit code",1' out.csv | wc -l` -eq 2 check_csv out.csv # ... unless --omit-missing is supplied. -run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ +run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ -f a --csv=out.csv --omit-missing 2>stderr grep '"exit_status"' out.csv && exit 1 grep '"exit_code"' out.csv && exit 1 @@ -64,7 +64,7 @@ check_csv out.csv # Likewise for timeouts echo foo >bug -run 0 ../../bin/ltlcross 'sleep 5; false %f >%N' 'false %f >%N' \ +run 0 ltlcross 'sleep 5; false %f >%N' 'false %f >%N' \ --timeout 2 -f a --csv=out.csv \ --ignore-execution-failures \ --save-bogus=bug 2>stderr @@ -83,7 +83,7 @@ check_csv out.csv test -f bug test -s bug && exit 1 -run 0 ../../bin/ltlcross 'sleep 5; false %f >%N' \ +run 0 ltlcross 'sleep 5; false %f >%N' \ --timeout 2 --omit-missing -f a --csv=out.csv 2>stderr grep '"exit_status"' out.csv && exit 1 grep '"exit_code"' out.csv && exit 1 @@ -92,7 +92,7 @@ test `wc -l < out.csv` -eq 1 check_csv out.csv # Check with --products=5 --automata -run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ +run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ -f a --csv=out.csv --products=5 --automata 2>stderr p=`sed 's/[^,]//g;q' out.csv | wc -c` grep '"exit_status"' out.csv @@ -103,7 +103,7 @@ test `grep '"HOA:.*--BODY--.*--END--"' out.csv | wc -l` -eq 2 check_csv out.csv # ... unless --omit-missing is supplied. -run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ +run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ -f a --csv=out.csv --omit-missing --products=5 2>stderr grep '"exit_status"' out.csv && exit 1 grep '"exit_code"' out.csv && exit 1 @@ -113,7 +113,7 @@ check_csv out.csv # Check with --products=+5 -run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ +run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ -f a --csv=out.csv --products=+5 --automata 2>stderr q=`sed 's/[^,]//g;q' out.csv | wc -c` grep '"exit_status"' out.csv @@ -124,7 +124,7 @@ test `grep '"HOA:.*--BODY--.*--END--"' out.csv | wc -l` -eq 2 check_csv out.csv # ... unless --omit-missing is supplied. -run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ +run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ -f a --csv=out.csv --omit-missing --products=+5 2>stderr grep '"exit_status"' out.csv && exit 1 grep '"exit_code"' out.csv && exit 1 @@ -138,7 +138,7 @@ test $q -eq `expr $p + 12` # Check with Rabin/Streett output first="should not be erased" echo "$first" > bug.txt -run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%D' \ +run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%D' \ -f 'X a' --csv=out.csv --save-bogus='>>bug.txt' 2>stderr q=`sed 's/[^,]//g;q' out.csv | wc -c` test $q -eq `expr $p - 1` @@ -152,7 +152,7 @@ test "`head -n 1 bug.txt`" = "$first" # Support for --ABORT-- in HOA. -run 1 ../../bin/ltlcross 'echo HOA: --ABORT-- %f > %H' \ +run 1 ltlcross 'echo HOA: --ABORT-- %f > %H' \ -f a --csv=out.csv 2>stderr grep '"exit_status"' out.csv grep '"exit_code"' out.csv @@ -162,7 +162,7 @@ test 3 = `wc -l < out.csv` check_csv out.csv # The header of CSV file is not output in append mode -run 1 ../../bin/ltlcross 'echo HOA: --ABORT-- %f > %H' \ +run 1 ltlcross 'echo HOA: --ABORT-- %f > %H' \ -f a --csv='>>out.csv' 2>stderr grep '"exit_status"' out.csv grep '"exit_code"' out.csv @@ -173,7 +173,7 @@ check_csv out.csv # Diagnose empty automata, and make sure %% is correctly replaced by % -run 1 ../../bin/ltlcross ': %f >%O; echo %%>foo' -f a 2>stderr +run 1 ltlcross ': %f >%O; echo %%>foo' -f a 2>stderr test 2 = `grep -c ':.*empty input' stderr` cat foo cat >expected<formulas.txt < GFb EOF -../../bin/ltlcross -F formulas.txt \ +ltlcross -F formulas.txt \ "{ltl2tgba any} $ltl2tgba --lbtt --any %f > %T" \ "{ltl2tgba det} $ltl2tgba --lbtt --deterministic %f > %T" \ "{ltl2tgba sma} $ltl2tgba --lbtt --small %f > %T" \ diff --git a/tests/ltlcrossce.test b/tests/core/ltlcrossce.test similarity index 95% rename from tests/ltlcrossce.test rename to tests/core/ltlcrossce.test index dbb532bd6..01173fad9 100755 --- a/tests/ltlcrossce.test +++ b/tests/core/ltlcrossce.test @@ -21,7 +21,7 @@ . ./defs set -e -ltl2tgba=../../bin/ltl2tgba +ltl2tgba=ltl2tgba # The following "fake" script behaves as # version 1.5.9 of modella, when run as @@ -85,7 +85,7 @@ esac EOF chmod +x fake -run 1 ../../bin/ltlcross -f 'G(F(p0) & F(G(!p1))) | (F(G(!p0)) & G(F(p1)))' \ +run 1 ltlcross -f 'G(F(p0) & F(G(!p1))) | (F(G(!p0)) & G(F(p1)))' \ "$ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors cat errors grep 'error: P0\*N1 is nonempty' errors diff --git a/tests/ltlcrossce2.test b/tests/core/ltlcrossce2.test similarity index 97% rename from tests/ltlcrossce2.test rename to tests/core/ltlcrossce2.test index decabbd12..39c353f25 100755 --- a/tests/ltlcrossce2.test +++ b/tests/core/ltlcrossce2.test @@ -21,7 +21,7 @@ . ./defs set -e -ltl2tgba=../../bin/ltl2tgba +ltl2tgba=ltl2tgba cat >fake <<\EOF #!/bin/sh @@ -62,7 +62,7 @@ esac EOF chmod +x fake -run 1 ../../bin/ltlcross -f 'G(a <-> Fb) U c' \ +run 1 ltlcross -f 'G(a <-> Fb) U c' \ "$ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors cat errors grep 'error: P0\*N1 is nonempty' errors diff --git a/tests/ltlcrossgrind.test b/tests/core/ltlcrossgrind.test similarity index 85% rename from tests/ltlcrossgrind.test rename to tests/core/ltlcrossgrind.test index 8c9a974e4..a9f7b1eb9 100755 --- a/tests/ltlcrossgrind.test +++ b/tests/core/ltlcrossgrind.test @@ -24,13 +24,13 @@ set -e cat >fake <%N" \ -"../../bin/ltl2tgba -s -f %f >%N" --grind=bogus.grind +run 1 ltlcross -f 'p0 U p1' "./fake %f >%N" \ +"ltl2tgba -s -f %f >%N" --grind=bogus.grind echo p0 >exp diff bogus.grind exp diff --git a/tests/ltldo.test b/tests/core/ltldo.test similarity index 97% rename from tests/ltldo.test rename to tests/core/ltldo.test index d1b33b8d3..d009e21eb 100755 --- a/tests/ltldo.test +++ b/tests/core/ltldo.test @@ -21,9 +21,9 @@ . ./defs set -e -ltldo=../../bin/ltldo -ltl2tgba=../../bin/ltl2tgba -genltl=../../bin/genltl +ltldo=ltldo +ltl2tgba=ltl2tgba +genltl=genltl run 0 $ltldo -f a -f 'a&b' -t 'echo %f,%s' >output cat >expected <exp - run 0 ../../bin/ltlgrind --sort "$@" > out + run 0 ltlgrind --sort "$@" > out diff exp out } @@ -33,7 +33,7 @@ checkopt() { checkopt_noparse "$@" # The result must be parsable - ../../bin/ltlfilt out + ltlfilt out } checkopt -f 'Xp1 U (p4 | (p3 xor (p4 W p0)))' <output +run 0 autfilt --mask-acc=0 input1 -H >output diff output expect1 cat >expect2 <output +run 0 autfilt --mask-acc=1 input1 -H >output diff output expect2 cat >expect3 <output +run 0 autfilt --mask-acc=0,1,2 input1 -H >output diff output expect3 -run 0 ../../bin/autfilt --mask-acc=0 --mask-acc=1 input1 -H >output +run 0 autfilt --mask-acc=0 --mask-acc=1 input1 -H >output diff output expect3 cat >input4 <output +run 0 autfilt --mask-acc=1 input4 -H >output diff output expect4 # Errors -run 2 ../../bin/autfilt --mask-acc=a3 input1 -run 2 ../../bin/autfilt --mask-acc=3-2 input1 -run 2 ../../bin/autfilt --mask-acc=0,9999,1 input1 +run 2 autfilt --mask-acc=a3 input1 +run 2 autfilt --mask-acc=3-2 input1 +run 2 autfilt --mask-acc=0,9999,1 input1 diff --git a/tests/maskkeep.test b/tests/core/maskkeep.test similarity index 82% rename from tests/maskkeep.test rename to tests/core/maskkeep.test index 3ad825795..98dbe0719 100755 --- a/tests/maskkeep.test +++ b/tests/core/maskkeep.test @@ -59,10 +59,10 @@ State: 0 --END-- EOF -run 0 ../../bin/autfilt --keep-states=0 input1 -H >output +run 0 autfilt --keep-states=0 input1 -H >output diff output expect1 -run 0 ../../bin/autfilt --keep-states=1 input1 -H >output +run 0 autfilt --keep-states=1 input1 -H >output diff output expect1 cat >expect3 <output +run 0 autfilt --keep-states=0,1,2 input1 -H >output diff output expect3 -run 0 ../../bin/autfilt --keep-states=0,9999,1,2 input1 -H >output +run 0 autfilt --keep-states=0,9999,1,2 input1 -H >output diff output expect3 -run 0 ../../bin/autfilt --keep-states=1,2,0 input1 -H >output +run 0 autfilt --keep-states=1,2,0 input1 -H >output diff output expect4 # Errors -run 2 ../../bin/autfilt --keep-states=a3 input1 -run 2 ../../bin/autfilt --keep-states=3-2 input1 +run 2 autfilt --keep-states=a3 input1 +run 2 autfilt --keep-states=3-2 input1 diff --git a/tests/monitor.test b/tests/core/monitor.test similarity index 91% rename from tests/monitor.test rename to tests/core/monitor.test index 8a5c79cfa..d484ac598 100755 --- a/tests/monitor.test +++ b/tests/core/monitor.test @@ -31,7 +31,7 @@ expect() diff output.out output.exp } -expect ../../bin/ltl2tgba --monitor a <stdout 2>stderr && exit 1 +autfilt --name=%F --dot=nsc stdout 2>stderr && exit 1 cat >expected < f.hoa - run 0 ../../bin/ltl2tgba -s -f "$f" > f.spot + run 0 ltl2tgba -H "!($f)" > f.hoa + run 0 ltl2tgba -s -f "$f" > f.spot # Make sure there is no `!x' occurring in the # output. Because `x' is usually #define'd, we # should use `!(x)' in guards. @@ -382,7 +382,7 @@ do cp f.spot f.spin cp f.spot f.ltl2ba - sf=`../../bin/ltlfilt -sf "$f"` + sf=`ltlfilt -sf "$f"` if test -n "$SPIN"; then # Old spin versions cannot parse formulas such as ((a + b) == 42). @@ -396,7 +396,7 @@ do fi esac - run 0 ../../bin/autfilt --count -v --intersect=f.hoa \ + run 0 autfilt --count -v --intersect=f.hoa \ f.spot f.spin f.ltl2ba >out test 3 = `cat out` done out.1 +run 0 ltl2tgba -F expected.1/1 --stats='%f, %d %p' >out.1 diff out.1 expected.1 cat >expected.2<out.2 +run 0 ltl2tgba -C -F-/1 --stats='%f, %d %p' out.2 diff out.2 expected.2 # Test multi-line CSV fields. @@ -52,11 +52,11 @@ a U b, 1 1 | Fx", 0 1 EOF -run 0 ../../bin/ltl2tgba -C -Fin.2b/1 --stats='%f, %d %p' >out.2b +run 0 ltl2tgba -C -Fin.2b/1 --stats='%f, %d %p' >out.2b diff out.2b expected.2 -run 0 ../../bin/ltl2tgba FGa GFa --stats='%f %d %n %s %p' >out.3 +run 0 ltl2tgba FGa GFa --stats='%f %d %n %s %p' >out.3 cat >expected.3<out.4 +run 0 ltl2tgba -DC FGa GFa --stats='%f %d %n %s %p' >out.4 cat >expected.4< F!F!c1))' 'ltl3ba -M0' cat >input <$1.exp - ../../bin/autfilt --hoa "$@" 2>$1.err-t >$1.out && exit 1 + autfilt --hoa "$@" 2>$1.err-t >$1.out && exit 1 test $? = 2 # If autfilt is compiled statically, the '.../lt-' parse of # its name is not stripped, and the error message show the @@ -39,7 +39,7 @@ expecterr() expectok() { cat >$1.exp - ../../bin/autfilt --hoa "$@" >$1.out + autfilt --hoa "$@" >$1.out test $? = 0 cat $1.out diff $1.out $1.exp @@ -586,7 +586,7 @@ EOF # DOS-style new lines should have the same output. perl -pi -e 's/$/\r/' input -../../bin/autfilt --hoa input 2>stderr && exit 1 +autfilt --hoa input 2>stderr && exit 1 cat stderr diff stderr input.exp @@ -926,7 +926,7 @@ diff expected input.out # DOS-style new lines should have the same output. perl -pe -e 's/$/\r/' input -../../bin/autfilt --hoa input 2>stderr && exit 1 +autfilt --hoa input 2>stderr && exit 1 cat stderr diff stderr input.exp diff expected input.out @@ -1071,7 +1071,7 @@ accept_init: } EOF -../../bin/autfilt input -H >output 2>&1 && exit 1 +autfilt input -H >output 2>&1 && exit 1 cat output cat >expected <output.err grep 'foob:1.1: Cannot open file foob' output.err # Make sure we can read multiple automata from stdin -../../bin/ltl2tgba 'a U b' 'GFa' --hoa | grep -v '^name:' > input -../../bin/autfilt --hoa < input | ../../bin/autfilt --hoa > output +ltl2tgba 'a U b' 'GFa' --hoa | grep -v '^name:' > input +autfilt --hoa < input | autfilt --hoa > output diff input output @@ -1657,12 +1657,12 @@ EOF # Implicit labels -../../bin/ltl2tgba -H 'GFa & GFb & (c U d)' >out.hoa -../../bin/ltl2tgba -C -Hi 'GFa & GFb & (c U d)' >out-i.hoa -../../bin/autfilt -C -Hi out.hoa --name=%M >out-i2.hoa +ltl2tgba -H 'GFa & GFb & (c U d)' >out.hoa +ltl2tgba -C -Hi 'GFa & GFb & (c U d)' >out-i.hoa +autfilt -C -Hi out.hoa --name=%M >out-i2.hoa diff -u out-i.hoa out-i2.hoa sed 's/ stutter-invariant//;/properties:$/d' out-i3.hoa -../../bin/autfilt --trust-hoa=no -C -Hi out.hoa --name=%M >out-i2.hoa +autfilt --trust-hoa=no -C -Hi out.hoa --name=%M >out-i2.hoa diff -u out-i3.hoa out-i2.hoa @@ -2387,4 +2387,4 @@ State: 0 "$BIGLABEL" EOF # At some point, this crashed with # input buffer overflow, can't enlarge buffer because scanner uses REJECT -run 0 ../../bin/autfilt -q bigaut +run 0 autfilt -q bigaut diff --git a/tests/parseerr.test b/tests/core/parseerr.test similarity index 100% rename from tests/parseerr.test rename to tests/core/parseerr.test diff --git a/tests/prodor.test b/tests/core/prodor.test similarity index 98% rename from tests/prodor.test rename to tests/core/prodor.test index e17e508f4..bd8dbec47 100755 --- a/tests/prodor.test +++ b/tests/core/prodor.test @@ -21,8 +21,8 @@ . ./defs set -e -ltl2tgba=../../bin/ltl2tgba -autfilt=../../bin/autfilt +ltl2tgba=ltl2tgba +autfilt=autfilt $ltl2tgba -DH 'GFa' > gfa.hoa $ltl2tgba -DH 'FGb' > fgb.hoa diff --git a/tests/rand.test b/tests/core/rand.test similarity index 99% rename from tests/rand.test rename to tests/core/rand.test index c6d8a7a01..df52b4562 100755 --- a/tests/rand.test +++ b/tests/core/rand.test @@ -21,7 +21,7 @@ . ./defs set -e -randltl=../../bin/randltl +randltl=randltl run 0 $randltl -S -n 20 a b c --tree-size=10 \ --sere-priorities=and=0,andNLM=0 \ diff --git a/tests/randaut.test b/tests/core/randaut.test similarity index 98% rename from tests/randaut.test rename to tests/core/randaut.test index 2b5e3969f..d525cf535 100755 --- a/tests/randaut.test +++ b/tests/core/randaut.test @@ -22,8 +22,8 @@ set -e -randaut=../../bin/randaut -autfilt=../../bin/autfilt +randaut=randaut +autfilt=autfilt $randaut --spin -Q4 a b | ../ikwiad -H -XN - >out grep 'States: 4' out diff --git a/tests/randomize.test b/tests/core/randomize.test similarity index 98% rename from tests/randomize.test rename to tests/core/randomize.test index 6cfbc7eab..c105b2ada 100755 --- a/tests/randomize.test +++ b/tests/core/randomize.test @@ -22,8 +22,8 @@ set -e -ltl2tgba=../../bin/ltl2tgba -autfilt=../../bin/autfilt +ltl2tgba=ltl2tgba +autfilt=autfilt $ltl2tgba --hoa 'Ga | Gb | Gc | Gd' > out diff --git a/tests/randpsl.test b/tests/core/randpsl.test similarity index 81% rename from tests/randpsl.test rename to tests/core/randpsl.test index 24260ecf2..1bcf69845 100755 --- a/tests/randpsl.test +++ b/tests/core/randpsl.test @@ -25,10 +25,10 @@ set -e # Generate 50 random unique PSL formula that do not simplify to LTL # formulae, and that have a size of at lease 12. -../../bin/randltl -n -1 --tree-size 30 --seed 12 --psl a b c | -../../bin/ltlfilt -r --size-min 12 --unique | -../../bin/ltlfilt -v --ltl -n 50 | tee formulas | -../../bin/ltlcross '../ikwiad -R3 -t %f >%T' '../ikwiad -x -R3 -t %f >%T' \ +randltl -n -1 --tree-size 30 --seed 12 --psl a b c | +ltlfilt -r --size-min 12 --unique | +ltlfilt -v --ltl -n 50 | tee formulas | +ltlcross '../ikwiad -R3 -t %f >%T' '../ikwiad -x -R3 -t %f >%T' \ -F - -f '{{(p1)}[*]:{(p3) && {{!(p1)} xor {!(p3)}}}}' test `wc -l < formulas` = 50 diff --git a/tests/randtgba.cc b/tests/core/randtgba.cc similarity index 100% rename from tests/randtgba.cc rename to tests/core/randtgba.cc diff --git a/tests/randtgba.test b/tests/core/randtgba.test similarity index 96% rename from tests/randtgba.test rename to tests/core/randtgba.test index 2f0e3187b..6ba012cc9 100755 --- a/tests/randtgba.test +++ b/tests/core/randtgba.test @@ -25,7 +25,7 @@ set -e for n in 10 20 30 40 50 60 70 80 90 100 200 500 1000; do # Make sure graphs generated by randaut have successors for each # of their $n nodes. - ../../bin/randaut -Q$n 3 -Hl | + randaut -Q$n 3 -Hl | sed 's/.*--BODY--//;s/State:/\n&/g;s/--END--//' > out grep -q 'State: [0-9][0-9]* .*$' out grep -q 'State: [0-9]* *$' out && exit 1 diff --git a/tests/readltl.cc b/tests/core/readltl.cc similarity index 100% rename from tests/readltl.cc rename to tests/core/readltl.cc diff --git a/tests/readsat.cc b/tests/core/readsat.cc similarity index 100% rename from tests/readsat.cc rename to tests/core/readsat.cc diff --git a/tests/readsat.test b/tests/core/readsat.test similarity index 100% rename from tests/readsat.test rename to tests/core/readsat.test diff --git a/tests/readsave.test b/tests/core/readsave.test similarity index 97% rename from tests/readsave.test rename to tests/core/readsave.test index 4fba986e6..19815f204 100755 --- a/tests/readsave.test +++ b/tests/core/readsave.test @@ -26,9 +26,9 @@ set -e -autfilt=../../bin/autfilt -ltl2tgba=../../bin/ltl2tgba -randltl=../../bin/randltl +autfilt=autfilt +ltl2tgba=ltl2tgba +randltl=randltl cat >input <<\EOF HOA: v1 @@ -92,16 +92,16 @@ State: 1 --END-- EOF -run 0 ../../bin/autfilt --merge-transitions --hoa input > stdout +run 0 autfilt --merge-transitions --hoa input > stdout cat stdout -run 0 ../../bin/autfilt -F stdout --isomorph expected +run 0 autfilt -F stdout --isomorph expected # Likewise, with a randomly generated TGBA. -run 0 ../../bin/randaut -Q 20 a b -d 0.2 -a 0.2 -A 2 --hoa | tee input +run 0 randaut -Q 20 a b -d 0.2 -a 0.2 -A 2 --hoa | tee input # the first read-write can renumber the states run 0 $autfilt --hoa --merge-transitions input > stdout -run 0 ../../bin/autfilt -F input --isomorph stdout +run 0 autfilt -F input --isomorph stdout # But this second output should be the same as the first run 0 $autfilt --hoa stdout > stdout2 diff --git a/tests/reduc.cc b/tests/core/reduc.cc similarity index 100% rename from tests/reduc.cc rename to tests/core/reduc.cc diff --git a/tests/reduc.test b/tests/core/reduc.test similarity index 98% rename from tests/reduc.test rename to tests/core/reduc.test index d84e964cb..1ace7c3c6 100755 --- a/tests/reduc.test +++ b/tests/core/reduc.test @@ -27,7 +27,7 @@ set -e -randltl=../../bin/randltl +randltl=randltl FILE=formulae : > $FILE diff --git a/tests/reduc0.test b/tests/core/reduc0.test similarity index 100% rename from tests/reduc0.test rename to tests/core/reduc0.test diff --git a/tests/reduccmp.test b/tests/core/reduccmp.test similarity index 100% rename from tests/reduccmp.test rename to tests/core/reduccmp.test diff --git a/tests/reducpsl.test b/tests/core/reducpsl.test similarity index 98% rename from tests/reducpsl.test rename to tests/core/reducpsl.test index 1f841068f..ca2e7d243 100755 --- a/tests/reducpsl.test +++ b/tests/core/reducpsl.test @@ -24,7 +24,7 @@ set -e -randltl=../../bin/randltl +randltl=randltl FILE=formulae : > $FILE diff --git a/tests/remfin.test b/tests/core/remfin.test similarity index 99% rename from tests/remfin.test rename to tests/core/remfin.test index 98e33b84e..0b27f7dde 100755 --- a/tests/remfin.test +++ b/tests/core/remfin.test @@ -23,7 +23,7 @@ set -e -autfilt=../../bin/autfilt +autfilt=autfilt cat >test1 < out +run 0 ltlfilt --remove-x -f 'F(!a & Xa & Xb)' > out grep -v X out -run 0 ../../bin/ltlfilt -q --stutter-invariant -F 'out' +run 0 ltlfilt -q --stutter-invariant -F 'out' -run 1 ../../bin/ltlfilt -q --stutter-invariant -f 'F(!a & Xb)' -run 0 ../../bin/ltlfilt --remove-x -f 'F(!a & Xb)' > out +run 1 ltlfilt -q --stutter-invariant -f 'F(!a & Xb)' +run 0 ltlfilt --remove-x -f 'F(!a & Xb)' > out grep -v X out # The output is stutter invariant, even if the input wasn't. -run 0 ../../bin/ltlfilt -q --stutter-invariant -F 'out' +run 0 ltlfilt -q --stutter-invariant -F 'out' # Ensure remove_x does not depend on clang or gcc recursive calls echo 'F(a & ((a & (a U (!a & b)) & ((!b U !a) | (b U !a))) |'\ ' (!a & (!a U (a & !a & b)) & ((!b U a) | (b U a))) | (b & (b U (!a & b & !b))'\ ' & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b)) & ((!a U b) | (a U b)))'\ ' | (!a & b & (G!a | Ga) & (G!b | Gb))))' > expected -run 0 ../../bin/ltlfilt --remove-x -f 'F(a & X(!a & b))' > 'out' +run 0 ltlfilt --remove-x -f 'F(a & X(!a & b))' > 'out' diff expected out diff --git a/tests/remprop.test b/tests/core/remprop.test similarity index 89% rename from tests/remprop.test rename to tests/core/remprop.test index bf07fe053..d8a21dedc 100755 --- a/tests/remprop.test +++ b/tests/core/remprop.test @@ -68,7 +68,7 @@ State: 3 --END-- EOF -run 0 ../../bin/autfilt -H --remove-ap=a,b automaton >out +run 0 autfilt -H --remove-ap=a,b automaton >out cat out diff out expected @@ -89,9 +89,9 @@ State: 2 --END-- EOF -run 0 ../../bin/autfilt -H --remove-ap=a=1,b=0 automaton >out +run 0 autfilt -H --remove-ap=a=1,b=0 automaton >out cat out diff out expected -../../bin/autfilt -H --remove-ap=a==1 automaton 2>stderr && exit 1 +autfilt -H --remove-ap=a==1 automaton 2>stderr && exit 1 grep "autfilt: unexpected '=' at position 2 in 'a==1'" stderr diff --git a/tests/renault.test b/tests/core/renault.test similarity index 100% rename from tests/renault.test rename to tests/core/renault.test diff --git a/tests/satmin.test b/tests/core/satmin.test similarity index 97% rename from tests/satmin.test rename to tests/core/satmin.test index 1883204aa..1065a637c 100755 --- a/tests/satmin.test +++ b/tests/core/satmin.test @@ -24,8 +24,8 @@ set -e # Skip if $SATSOLVE is not installed. (${SATSOLVER-glucose} --help >/dev/null 2>&1) || exit 77 -ltl2tgba=../../bin/ltl2tgba -ltlcross=../../bin/ltlcross +ltl2tgba=ltl2tgba +ltlcross=ltlcross cat >formulas <<'EOF' XXa diff --git a/tests/satmin2.test b/tests/core/satmin2.test similarity index 97% rename from tests/satmin2.test rename to tests/core/satmin2.test index 5195cb630..3b0a158dd 100755 --- a/tests/satmin2.test +++ b/tests/core/satmin2.test @@ -24,8 +24,8 @@ set -e # Skip if $SATSOLVE is not installed. (${SATSOLVER-glucose} --help >/dev/null 2>&1) || exit 77 -autfilt=../../bin/autfilt -ltlfilt=../../bin/ltlfilt +autfilt=autfilt +ltlfilt=ltlfilt # This is a counterexample for one of the optimization idea we had for # the SAT-based minimization. @@ -62,7 +62,7 @@ diff output expected # At some point, this formula was correctly minimized, but # the output was not marked as state-based. -../../bin/ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" -H >out +ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" -H >out grep 'properties:.*state-acc' out grep 'properties:.*deterministic' out diff --git a/tests/sbacc.test b/tests/core/sbacc.test similarity index 92% rename from tests/sbacc.test rename to tests/core/sbacc.test index 4d86dd47e..172035781 100755 --- a/tests/sbacc.test +++ b/tests/core/sbacc.test @@ -22,8 +22,8 @@ set -e -ltl2tgba=../../bin/ltl2tgba -autfilt=../../bin/autfilt +ltl2tgba=ltl2tgba +autfilt=autfilt $ltl2tgba 'GFa & GFb' -H | run 0 $autfilt --sbacc -H > out.hoa @@ -123,5 +123,5 @@ State: 2 EOF diff out.hoa expected -../../bin/randltl --weak-fairness -n 20 2 | -../../bin/ltlcross "$ltl2tgba -DH %f >%O" "$ltl2tgba -H %f | $autfilt -H >%O" +randltl --weak-fairness -n 20 2 | +ltlcross "$ltl2tgba -DH %f >%O" "$ltl2tgba -H %f | $autfilt -H >%O" diff --git a/tests/scc.test b/tests/core/scc.test similarity index 92% rename from tests/scc.test rename to tests/core/scc.test index 4bbf8bf81..b464778fe 100755 --- a/tests/scc.test +++ b/tests/core/scc.test @@ -30,6 +30,6 @@ b U a,3,2,2 (!a & G(Ga | F(!a & b))) | (a & F(F!a & G(a | !b))),16,7,6 EOF -run 0 ../../bin/ltl2tgba --low --any --stats='%f,%e,%s,%c' -F formulas/1 >out +run 0 ltl2tgba --low --any --stats='%f,%e,%s,%c' -F formulas/1 >out cat out diff out formulas diff --git a/tests/sccdot.test b/tests/core/sccdot.test similarity index 96% rename from tests/sccdot.test rename to tests/core/sccdot.test index 1c817c607..919467a5d 100755 --- a/tests/sccdot.test +++ b/tests/core/sccdot.test @@ -68,7 +68,7 @@ State: 10 --END-- EOF -run 0 ../../bin/autfilt --dot=as in.hoa > out.dot +run 0 autfilt --dot=as in.hoa > out.dot # The important stuff is the color=xxx lines cat <expected @@ -150,7 +150,7 @@ EOF diff out.dot expected # While we are here, make sure scc_filter remove those grey SCCs. -../../bin/autfilt --small -x simul=0 in.hoa -H > out.hoa +autfilt --small -x simul=0 in.hoa -H > out.hoa cat >expected.hoa <output +run 0 autfilt -H --any --medium -x scc-filter=2 input >output cat >expected <output +run 0 autfilt -C -H --det --high input >output cat >expected < out +run 0 autfilt --separate-sets in -H > out diff out expected diff --git a/tests/sim2.test b/tests/core/sim2.test similarity index 100% rename from tests/sim2.test rename to tests/core/sim2.test diff --git a/tests/sim3.test b/tests/core/sim3.test similarity index 93% rename from tests/sim3.test rename to tests/core/sim3.test index 64fd6d8c1..147863a8a 100755 --- a/tests/sim3.test +++ b/tests/core/sim3.test @@ -47,9 +47,9 @@ State: 6 {0 3} --END-- EOF -test "`../../bin/autfilt --small input --stats=%S,%s`" = 7,5 +test "`autfilt --small input --stats=%S,%s`" = 7,5 -../../bin/autfilt -S --high --small input -H > out +autfilt -S --high --small input -H > out cat >expected <in < pos.hoa $ltl2tgba 'FG(a | Xa | G!a)' -H | $autfilt -H --destut > neg.hoa diff --git a/tests/syntimpl.cc b/tests/core/syntimpl.cc similarity index 100% rename from tests/syntimpl.cc rename to tests/core/syntimpl.cc diff --git a/tests/syntimpl.test b/tests/core/syntimpl.test similarity index 100% rename from tests/syntimpl.test rename to tests/core/syntimpl.test diff --git a/tests/taatgba.cc b/tests/core/taatgba.cc similarity index 100% rename from tests/taatgba.cc rename to tests/core/taatgba.cc diff --git a/tests/taatgba.test b/tests/core/taatgba.test similarity index 100% rename from tests/taatgba.test rename to tests/core/taatgba.test diff --git a/tests/tgbagraph.test b/tests/core/tgbagraph.test similarity index 100% rename from tests/tgbagraph.test rename to tests/core/tgbagraph.test diff --git a/tests/tostring.cc b/tests/core/tostring.cc similarity index 100% rename from tests/tostring.cc rename to tests/core/tostring.cc diff --git a/tests/tostring.test b/tests/core/tostring.test similarity index 100% rename from tests/tostring.test rename to tests/core/tostring.test diff --git a/tests/tripprod.test b/tests/core/tripprod.test similarity index 94% rename from tests/tripprod.test rename to tests/core/tripprod.test index 4d59ed2f1..4650eb010 100755 --- a/tests/tripprod.test +++ b/tests/core/tripprod.test @@ -105,9 +105,9 @@ State: 6 --END-- EOF -run 0 ../../bin/autfilt input1 --product input2 --product input3 --hoa | +run 0 autfilt input1 --product input2 --product input3 --hoa | tee stdout -run 0 ../../bin/autfilt -F stdout --isomorph expected +run 0 autfilt -F stdout --isomorph expected rm input1 input2 input3 stdout expected diff --git a/tests/tunabbrev.test b/tests/core/tunabbrev.test similarity index 100% rename from tests/tunabbrev.test rename to tests/core/tunabbrev.test diff --git a/tests/tunenoform.test b/tests/core/tunenoform.test similarity index 100% rename from tests/tunenoform.test rename to tests/core/tunenoform.test diff --git a/tests/twagraph.cc b/tests/core/twagraph.cc similarity index 100% rename from tests/twagraph.cc rename to tests/core/twagraph.cc diff --git a/tests/unabbrevwm.test b/tests/core/unabbrevwm.test similarity index 98% rename from tests/unabbrevwm.test rename to tests/core/unabbrevwm.test index a41b9c880..a9d266a6a 100755 --- a/tests/unabbrevwm.test +++ b/tests/core/unabbrevwm.test @@ -25,7 +25,7 @@ set -e -ltlfilt=../../bin/ltlfilt +ltlfilt=ltlfilt # Removing W,M in this formula caused a segfault at some point. run 0 $ltlfilt --remove-wm >out < output test `grep -c unambiguous output` = 0 # Check 1000 random PSL formulas -../../bin/randltl --psl -n 1000 3 | $ltl2tgba -U -F- -H | +randltl --psl -n 1000 3 | $ltl2tgba -U -F- -H | $autfilt -v --is-unamb --stats=%M && exit 1 cat >input < aut1 -../../bin/randaut a b c -Q10 --hoa > aut2 -../../bin/autfilt --randomize aut1 --hoa > rand11 -../../bin/autfilt --randomize --seed=1 aut1 --hoa > rand12 -../../bin/autfilt --randomize --seed=2 aut1 --hoa > rand13 -../../bin/autfilt --randomize aut2 --hoa > rand21 -../../bin/autfilt --randomize --seed=1 aut2 --hoa > rand22 -../../bin/autfilt --randomize --seed=2 aut2 --hoa > rand23 +randaut a b -Q5 --hoa > aut1 +randaut a b c -Q10 --hoa > aut2 +autfilt --randomize aut1 --hoa > rand11 +autfilt --randomize --seed=1 aut1 --hoa > rand12 +autfilt --randomize --seed=2 aut1 --hoa > rand13 +autfilt --randomize aut2 --hoa > rand21 +autfilt --randomize --seed=1 aut2 --hoa > rand22 +autfilt --randomize --seed=2 aut2 --hoa > rand23 cat aut1 aut2 > aut cat aut1 aut2 rand11 rand12 rand13 rand21 rand22 rand23 > all -../../bin/autfilt all --uniq --hoa > out +autfilt all --uniq --hoa > out diff aut out -run 0 ../../bin/randaut -Hl -u -n 4 -Q1 a b | LC_ALL=C sort | - ../../bin/autfilt -H | grep '&' > out +run 0 randaut -Hl -u -n 4 -Q1 a b | LC_ALL=C sort | + autfilt -H | grep '&' > out cat >expected <out 2>stderr && exit 1 +randaut -Hl -u -n 5 -Q1 a b >out 2>stderr && exit 1 test $? = 2 grep 'failed to generate a new unique automaton' stderr test 4 = `wc -l < out` diff --git a/tests/utf8.test b/tests/core/utf8.test similarity index 95% rename from tests/utf8.test rename to tests/core/utf8.test index 76ab3774c..aae837b3d 100755 --- a/tests/utf8.test +++ b/tests/core/utf8.test @@ -72,5 +72,5 @@ EOF cmp exp err -../../bin/randltl --psl -8 --seed 0 --tree-size 16 a b c -n 100 > formulae +randltl --psl -8 --seed 0 --tree-size 16 a b c -n 100 > formulae ../reduc -f -h 0 formulae diff --git a/tests/uwrm.test b/tests/core/uwrm.test similarity index 100% rename from tests/uwrm.test rename to tests/core/uwrm.test diff --git a/tests/wdba.test b/tests/core/wdba.test similarity index 100% rename from tests/wdba.test rename to tests/core/wdba.test diff --git a/tests/wdba2.test b/tests/core/wdba2.test similarity index 96% rename from tests/wdba2.test rename to tests/core/wdba2.test index a9d3230bf..82ed64823 100755 --- a/tests/wdba2.test +++ b/tests/core/wdba2.test @@ -80,5 +80,5 @@ State: 3 --END-- EOF -../../bin/autfilt --small --high -C -Hi input > output +autfilt --small --high -C -Hi input > output diff output expected diff --git a/python/tests/.gitignore b/tests/python/.gitignore similarity index 100% rename from python/tests/.gitignore rename to tests/python/.gitignore diff --git a/python/tests/acc_cond.ipynb b/tests/python/acc_cond.ipynb similarity index 100% rename from python/tests/acc_cond.ipynb rename to tests/python/acc_cond.ipynb diff --git a/python/tests/accparse.ipynb b/tests/python/accparse.ipynb similarity index 100% rename from python/tests/accparse.ipynb rename to tests/python/accparse.ipynb diff --git a/python/tests/accparse2.py b/tests/python/accparse2.py similarity index 100% rename from python/tests/accparse2.py rename to tests/python/accparse2.py diff --git a/python/tests/alarm.py b/tests/python/alarm.py similarity index 100% rename from python/tests/alarm.py rename to tests/python/alarm.py diff --git a/python/tests/automata-io.ipynb b/tests/python/automata-io.ipynb similarity index 100% rename from python/tests/automata-io.ipynb rename to tests/python/automata-io.ipynb diff --git a/python/tests/automata.ipynb b/tests/python/automata.ipynb similarity index 100% rename from python/tests/automata.ipynb rename to tests/python/automata.ipynb diff --git a/python/tests/bddnqueen.py b/tests/python/bddnqueen.py similarity index 100% rename from python/tests/bddnqueen.py rename to tests/python/bddnqueen.py diff --git a/python/tests/decompose.ipynb b/tests/python/decompose.ipynb similarity index 100% rename from python/tests/decompose.ipynb rename to tests/python/decompose.ipynb diff --git a/python/tests/formulas.ipynb b/tests/python/formulas.ipynb similarity index 100% rename from python/tests/formulas.ipynb rename to tests/python/formulas.ipynb diff --git a/python/tests/implies.py b/tests/python/implies.py similarity index 100% rename from python/tests/implies.py rename to tests/python/implies.py diff --git a/python/tests/interdep.py b/tests/python/interdep.py similarity index 100% rename from python/tests/interdep.py rename to tests/python/interdep.py diff --git a/python/tests/ipnbdoctest.py b/tests/python/ipnbdoctest.py similarity index 100% rename from python/tests/ipnbdoctest.py rename to tests/python/ipnbdoctest.py diff --git a/python/tests/ltl2tgba.py b/tests/python/ltl2tgba.py similarity index 100% rename from python/tests/ltl2tgba.py rename to tests/python/ltl2tgba.py diff --git a/tests/python/ltl2tgba.test b/tests/python/ltl2tgba.test new file mode 100755 index 000000000..a0a19096a --- /dev/null +++ b/tests/python/ltl2tgba.test @@ -0,0 +1,51 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2014 Laboratoire de Recherche et +# Développement de l'EPITA. +# Copyright (C) 2003 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 . + + +set -e + +# We don't check the output, but just running these might be enough to +# trigger assertions. + +../run $srcdir/ltl2tgba.py -T a +../run $srcdir/ltl2tgba.py -T 'a U b' +../run $srcdir/ltl2tgba.py -T 'X a' +../run $srcdir/ltl2tgba.py -T 'a & b & c' +../run $srcdir/ltl2tgba.py -T 'a | b | (c U (d & (g U (h ^ i))))' +../run $srcdir/ltl2tgba.py -T 'Xa & (b U !a) & (b U !a)' +../run $srcdir/ltl2tgba.py -T 'Fa & Xb & GFc & Gd' +../run $srcdir/ltl2tgba.py -T 'Fa & Xa & GFc & Gc' +../run $srcdir/ltl2tgba.py -T 'Fc & X(a | Xb) & GF(a | Xb) & Gc' + +../run $srcdir/ltl2tgba.py -f a +../run $srcdir/ltl2tgba.py -f 'a U b' +../run $srcdir/ltl2tgba.py -f 'X a' +../run $srcdir/ltl2tgba.py -f 'a & b & c' +../run $srcdir/ltl2tgba.py -f 'a | b | (c U (d & (g U (h ^ i))))' +../run $srcdir/ltl2tgba.py -f 'Xa & (b U !a) & (b U !a)' +../run $srcdir/ltl2tgba.py -f 'Fa & Xb & GFc & Gd' +../run $srcdir/ltl2tgba.py -f 'Fa & Xa & GFc & Gc' +../run $srcdir/ltl2tgba.py -f 'Fc & X(a | Xb) & GF(a | Xb) & Gc' + +../run $srcdir/ltl2tgba.py -W -f 'Ga | Gb | Gc' +../run $srcdir/ltl2tgba.py -W -T 'Ga | Gb | Gc' diff --git a/python/tests/ltlparse.py b/tests/python/ltlparse.py similarity index 100% rename from python/tests/ltlparse.py rename to tests/python/ltlparse.py diff --git a/python/tests/ltlsimple.py b/tests/python/ltlsimple.py similarity index 100% rename from python/tests/ltlsimple.py rename to tests/python/ltlsimple.py diff --git a/python/tests/minato.py b/tests/python/minato.py similarity index 100% rename from python/tests/minato.py rename to tests/python/minato.py diff --git a/python/tests/optionmap.py b/tests/python/optionmap.py similarity index 100% rename from python/tests/optionmap.py rename to tests/python/optionmap.py diff --git a/python/tests/parsetgba.py b/tests/python/parsetgba.py similarity index 100% rename from python/tests/parsetgba.py rename to tests/python/parsetgba.py diff --git a/python/tests/piperead.ipynb b/tests/python/piperead.ipynb similarity index 100% rename from python/tests/piperead.ipynb rename to tests/python/piperead.ipynb diff --git a/python/tests/product.ipynb b/tests/python/product.ipynb similarity index 100% rename from python/tests/product.ipynb rename to tests/python/product.ipynb diff --git a/python/tests/randaut.ipynb b/tests/python/randaut.ipynb similarity index 100% rename from python/tests/randaut.ipynb rename to tests/python/randaut.ipynb diff --git a/python/tests/randgen.py b/tests/python/randgen.py similarity index 100% rename from python/tests/randgen.py rename to tests/python/randgen.py diff --git a/python/tests/randltl.ipynb b/tests/python/randltl.ipynb similarity index 100% rename from python/tests/randltl.ipynb rename to tests/python/randltl.ipynb diff --git a/python/tests/relabel.py b/tests/python/relabel.py similarity index 100% rename from python/tests/relabel.py rename to tests/python/relabel.py diff --git a/python/tests/remfin.py b/tests/python/remfin.py similarity index 100% rename from python/tests/remfin.py rename to tests/python/remfin.py diff --git a/python/tests/satmin.py b/tests/python/satmin.py similarity index 100% rename from python/tests/satmin.py rename to tests/python/satmin.py diff --git a/python/tests/setxor.py b/tests/python/setxor.py similarity index 100% rename from python/tests/setxor.py rename to tests/python/setxor.py diff --git a/python/tests/testingaut.ipynb b/tests/python/testingaut.ipynb similarity index 100% rename from python/tests/testingaut.ipynb rename to tests/python/testingaut.ipynb diff --git a/python/tests/run.in b/tests/run.in similarity index 68% rename from python/tests/run.in rename to tests/run.in index 36990d475..23465263b 100755 --- a/python/tests/run.in +++ b/tests/run.in @@ -24,24 +24,54 @@ # Darwin needs some help in figuring out where non-installed libtool # libraries are (on this platform libtool encodes the expected final # path of dependent libraries in each library). -modpath='../.libs:@top_builddir@/spot/.libs:@top_builddir@/buddy/spot/.libs' +modpath='@abs_top_builddir@/python/.libs' +modpath=$modpath:'@top_builddir@/spot/.libs':'@top_builddir@/buddy/spot/.libs' -# .. is for the *.py files, and ../.libs for the *.so. We used to +# We need access to both the *.py files, and the *.so. We used to # rely on a module called ltihooks.py to teach the import function how # to load a Libtool library, but it started to cause issues with # Python 2.6. -pypath='..:../.libs:@srcdir@/..:@srcdir@/../.libs:$PYTHONPATH' +pypath='@abs_top_builddir@/python':'@abs_top_builddir@/python/.libs' +pypath=$pypath:'@abs_top_srcdir@/python':'@abs_top_srcdir@/python/.libs' PATH="@abs_top_builddir@/bin:$PATH" export PATH test -z "$1" && - PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath exec @PYTHON@ + PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath exec @PYTHON@ +srcdir="@srcdir@" + +case $1 in + */*) + dir=${1%/*} + dir=${dir##*/} + mkdir -p $dir + cd $dir + case $1 in + ../*) + base=../$1 + ;; + [\\/$]* | ?:[\\/]* ) + base=$1 + ;; + *) + base=${1##*/} + ;; + esac + + test $srcdir != '.' && srcdir="@abs_srcdir@/$dir" + shift + set x "$base" "$@" + shift + ;; +esac + +export srcdir case $1 in *.ipynb) PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath \ - exec $PREFIXCMD @PYTHON@ @srcdir@/ipnbdoctest.py "$@";; + exec $PREFIXCMD @PYTHON@ @abs_srcdir@/python/ipnbdoctest.py "$@";; *.py) PYTHONPATH=$pypath DYLD_LIBRARY_PATH=$modpath \ exec $PREFIXCMD @PYTHON@ "$@";;