alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgbatest/Makefile.am (EXTRA_DIST): Distribute the files

Browse source 
from tba_samples_from_spin.
* src/tgbatest/tba_samples_from_spin.test: Get these example files
from $srcdir, for the sake of VPATH builds.
(light_run): Remove, not needed.
This commit is contained in:
Alexandre Duret-Lutz 2004-11-17 17:42:19 +00:00
parent 2a3d638a50
commit a1262a30fb
3 changed files with 63 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,5 +1,11 @@
2004-11-17 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbatest/Makefile.am (EXTRA_DIST): Distribute the files
from tba_samples_from_spin.
* src/tgbatest/tba_samples_from_spin.test: Get these example files
from $srcdir, for the sake of VPATH builds.
(light_run): Remove, not needed.
* src/misc/bareword.hh, src/misc/bddalloc.hh, src/misc/bddlt.hh,
src/misc/escape.hh, src/misc/freelist.hh, src/misc/hash.hh,
src/misc/hashfunc.hh, src/misc/minato.hh, src/misc/modgray.hh,
@ -17,7 +23,7 @@
* src/tgbaalgos/Makefile.am: Add it.
* src/tgbatest/ltl2tgba.cc: Add tau03 new emptiness check.
* src/tgbatest/randtgba.cc: Add tau03 new emptiness check.
* src/tgbatest/emptchkr: Fix a comment.
* src/tgbatest/emptchkr.test: Fix a comment.
* src/tgbatest/tba_samples_from_spin/explicit1_1.tba,
src/tgbatest/tba_samples_from_spin/explicit1_2.tba,
src/tgbatest/tba_samples_from_spin/explicit1_3.tba,

22
src/tgbatest/Makefile.am
View file

@ -87,7 +87,27 @@ TESTS = \
tba_samples_from_spin.test \
spotlbtt.test
EXTRA_DIST = $(TESTS) ltl2baw.pl
EXTRA_DIST = $(TESTS) ltl2baw.pl $(TBA_SAMPLES_FROM_SPIN)
TBA_SAMPLES_FROM_SPIN = \
tba_samples_from_spin/explicit1_1.tba \
tba_samples_from_spin/explicit1_2.tba \
tba_samples_from_spin/explicit1_3.tba \
tba_samples_from_spin/explicit1_4.tba \
tba_samples_from_spin/explicit1_5.tba \
tba_samples_from_spin/explicit1_6.tba \
tba_samples_from_spin/explicit1_7.tba \
tba_samples_from_spin/explicit1_8.tba \
tba_samples_from_spin/explicit1_9.tba \
tba_samples_from_spin/explicit2_1.tba \
tba_samples_from_spin/explicit2_2.tba \
tba_samples_from_spin/explicit2_3.tba \
tba_samples_from_spin/explicit2_4.tba \
tba_samples_from_spin/explicit2_5.tba \
tba_samples_from_spin/explicit2_6.tba \
tba_samples_from_spin/explicit2_7.tba \
tba_samples_from_spin/explicit2_8.tba \
tba_samples_from_spin/explicit2_9.tba
CLEANFILES = \
blue_counter \

77
src/tgbatest/tba_samples_from_spin.test
View file

@ -1,5 +1,5 @@
#!/bin/sh
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie.
#
@ -22,55 +22,48 @@
. ./defs
light_run()
{
expected_exitcode=$1
shift
exitcode=0
"$@" || exitcode=$?
test $exitcode = $expected_exitcode || exit 1
}
set -e
expect_ce()
{
light_run 0 ./ltl2tgba -X -e "$1"
light_run 0 ./ltl2tgba -X -ecouvreur99_shy "$1"
light_run 0 ./ltl2tgba -X -emagic_search "$1"
light_run 0 ./ltl2tgba -X -ebsh_magic_search "$1"
light_run 0 ./ltl2tgba -X -ese05_search "$1"
light_run 0 ./ltl2tgba -X -ebsh_se05_search "$1"
light_run 0 ./ltl2tgba -X -etau03_search "$1"
./ltl2tgba -X -e "$1"
./ltl2tgba -X -ecouvreur99_shy "$1"
./ltl2tgba -X -emagic_search "$1"
./ltl2tgba -X -ebsh_magic_search "$1"
./ltl2tgba -X -ese05_search "$1"
./ltl2tgba -X -ebsh_se05_search "$1"
./ltl2tgba -X -etau03_search "$1"
}
expect_no()
{
light_run 0 ./ltl2tgba -X -E "$1"
light_run 0 ./ltl2tgba -X -Ecouvreur99_shy "$1"
light_run 0 ./ltl2tgba -X -Emagic_search "$1"
light_run 0 ./ltl2tgba -X -Ebsh_magic_search "$1"
light_run 0 ./ltl2tgba -X -Ese05_search "$1"
light_run 0 ./ltl2tgba -X -Ebsh_se05_search "$1"
light_run 0 ./ltl2tgba -X -Etau03_search "$1"
./ltl2tgba -X -E "$1"
./ltl2tgba -X -Ecouvreur99_shy "$1"
./ltl2tgba -X -Emagic_search "$1"
./ltl2tgba -X -Ebsh_magic_search "$1"
./ltl2tgba -X -Ese05_search "$1"
./ltl2tgba -X -Ebsh_se05_search "$1"
./ltl2tgba -X -Etau03_search "$1"
}
expect_no tba_samples_from_spin/explicit1_1.tba
expect_ce tba_samples_from_spin/explicit1_2.tba
expect_no tba_samples_from_spin/explicit1_3.tba
expect_no tba_samples_from_spin/explicit1_4.tba
expect_ce tba_samples_from_spin/explicit1_5.tba
expect_no tba_samples_from_spin/explicit1_6.tba
expect_no tba_samples_from_spin/explicit1_7.tba
expect_ce tba_samples_from_spin/explicit1_8.tba
expect_ce tba_samples_from_spin/explicit1_9.tba
dir=$srcdir/tba_samples_from_spin
expect_ce tba_samples_from_spin/explicit2_1.tba
expect_ce tba_samples_from_spin/explicit2_2.tba
expect_no tba_samples_from_spin/explicit2_3.tba
expect_no tba_samples_from_spin/explicit2_4.tba
expect_ce tba_samples_from_spin/explicit2_5.tba
expect_no tba_samples_from_spin/explicit2_6.tba
expect_ce tba_samples_from_spin/explicit2_7.tba
expect_ce tba_samples_from_spin/explicit2_8.tba
expect_no tba_samples_from_spin/explicit2_9.tba
expect_no "$dir/explicit1_1.tba"
expect_ce "$dir/explicit1_2.tba"
expect_no "$dir/explicit1_3.tba"
expect_no "$dir/explicit1_4.tba"
expect_ce "$dir/explicit1_5.tba"
expect_no "$dir/explicit1_6.tba"
expect_no "$dir/explicit1_7.tba"
expect_ce "$dir/explicit1_8.tba"
expect_ce "$dir/explicit1_9.tba"
expect_ce "$dir/explicit2_1.tba"
expect_ce "$dir/explicit2_2.tba"
expect_no "$dir/explicit2_3.tba"
expect_no "$dir/explicit2_4.tba"
expect_ce "$dir/explicit2_5.tba"
expect_no "$dir/explicit2_6.tba"
expect_ce "$dir/explicit2_7.tba"
expect_ce "$dir/explicit2_8.tba"
expect_no "$dir/explicit2_9.tba"