Run valgrind in test cases.
* src/tgbatest/defs.in (VALGRIND, run): Define. * src/tgbatest/bddprod.test, src/tgbatest/dupexp.test, src/tgbatest/emptchk.test, src/tgbatest/emptchke.test, src/tgbatest/explicit.test, src/tgbatest/explpro2.test, src/tgbatest/explpro3.test, src/tgbatest/explprod.test, src/tgbatest/ltl2tgba.test, src/tgbatest/ltlprod.test, src/tgbatest/mixprod.test, src/tgbatest/readsave.test, src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Use run().
This commit is contained in:
Alexandre Duret-Lutz
parent
7aecf4ad09
commit
92cc5f9b9f
16 changed files with 112 additions and 81 deletions
12
ChangeLog
12
ChangeLog
|
|
@ -1,3 +1,15 @@
|
|||
2004-01-08 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||
|
||||
Run valgrind in test cases.
|
||||
* src/tgbatest/defs.in (VALGRIND, run): Define.
|
||||
* src/tgbatest/bddprod.test, src/tgbatest/dupexp.test,
|
||||
src/tgbatest/emptchk.test, src/tgbatest/emptchke.test,
|
||||
src/tgbatest/explicit.test, src/tgbatest/explpro2.test,
|
||||
src/tgbatest/explpro3.test, src/tgbatest/explprod.test,
|
||||
src/tgbatest/ltl2tgba.test, src/tgbatest/ltlprod.test,
|
||||
src/tgbatest/mixprod.test, src/tgbatest/readsave.test,
|
||||
src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Use run().
|
||||
|
||||
2004-01-06 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||
|
||||
* iface/gspn/eesrg.cc (format_state): Do not rewrite \n's,
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -28,11 +28,11 @@ set -e
|
|||
# We don't check the output, but just running these might be enough to
|
||||
# trigger assertions.
|
||||
|
||||
./bddprod a b
|
||||
./bddprod a a
|
||||
./bddprod 'a U b' 'X f'
|
||||
./bddprod 'X a' 'X a'
|
||||
./bddprod 'X a' 'a U b'
|
||||
./bddprod 'a & b & c' 'b & d & c'
|
||||
./bddprod 'a | b | (c U (d & (g U (h ^ i))))' 'h ^ i'
|
||||
./bddprod 'Xa & (b U !a) & (b U !a)' '(b U !a) & f'
|
||||
run 0 ./bddprod a b
|
||||
run 0 ./bddprod a a
|
||||
run 0 ./bddprod 'a U b' 'X f'
|
||||
run 0 ./bddprod 'X a' 'X a'
|
||||
run 0 ./bddprod 'X a' 'a U b'
|
||||
run 0 ./bddprod 'a & b & c' 'b & d & c'
|
||||
run 0 ./bddprod 'a | b | (c U (d & (g U (h ^ i))))' 'h ^ i'
|
||||
run 0 ./bddprod 'Xa & (b U !a) & (b U !a)' '(b U !a) & f'
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
# -*- shell-script -*-
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -49,6 +49,25 @@ DOT='@DOT@'
|
|||
top_builddir='@top_builddir@'
|
||||
LBTT="@LBTT@"
|
||||
LBTT_TRANSLATE="@LBTT_TRANSLATE@"
|
||||
VALGRIND='@VALGRIND@'
|
||||
|
||||
run()
|
||||
{
|
||||
expected_exitcode=$1
|
||||
shift
|
||||
exitcode=0
|
||||
if test -n "$VALGRIND"; then
|
||||
exec 6>valgrind.err
|
||||
GLIBCPP_FORCE_NEW=1 \
|
||||
$VALGRIND --leak-check=yes --logfile-fd=6 -q "$@" || exitcode=$?
|
||||
cat valgrind.err 1>&2
|
||||
test -z "`sed 1q valgrind.err`" || exit 50
|
||||
rm -f valgrind.err
|
||||
else
|
||||
"$@" || exitcode $?
|
||||
fi
|
||||
test $exitcode = $expected_exitcode || exit 1
|
||||
}
|
||||
|
||||
# Turn on shell traces when VERBOSE=x.
|
||||
if test "x$VERBOSE" = xx; then
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -25,27 +25,27 @@
|
|||
|
||||
set -e
|
||||
|
||||
run()
|
||||
dorun()
|
||||
{
|
||||
./ltl2tgba -f -s "$1" >output1
|
||||
./ltl2tgba -f -S "$1" >output2
|
||||
run 0 ./ltl2tgba -f -s "$1" >output1
|
||||
run 0 ./ltl2tgba -f -S "$1" >output2
|
||||
test `wc -l <output1` = `wc -l <output2`
|
||||
|
||||
./ltl2tgba -s "$1" >output1
|
||||
./ltl2tgba -S "$1" >output2
|
||||
run 0 ./ltl2tgba -s "$1" >output1
|
||||
run 0 ./ltl2tgba -S "$1" >output2
|
||||
test `wc -l <output1` = `wc -l <output2`
|
||||
}
|
||||
|
||||
run 'a'
|
||||
run 'a U b'
|
||||
run 'X a'
|
||||
run 'a & b & c'
|
||||
run 'a | b | (c U (d & (g U (h ^ i))))'
|
||||
run 'Xa & (b U !a) & (b U !a)'
|
||||
run 'Fa & Xb & GFc & Gd'
|
||||
run 'Fa & Xa & GFc & Gc'
|
||||
run 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
|
||||
run '!((FF a) <=> (F x))'
|
||||
run '!((FF a) <=> (F a))'
|
||||
run 'Xa && (!a U b) && !b && X!b'
|
||||
run '(a U !b) && Gb'
|
||||
dorun 'a'
|
||||
dorun 'a U b'
|
||||
dorun 'X a'
|
||||
dorun 'a & b & c'
|
||||
dorun 'a | b | (c U (d & (g U (h ^ i))))'
|
||||
dorun 'Xa & (b U !a) & (b U !a)'
|
||||
dorun 'Fa & Xb & GFc & Gd'
|
||||
dorun 'Fa & Xa & GFc & Gc'
|
||||
dorun 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
|
||||
dorun '!((FF a) <=> (F x))'
|
||||
dorun '!((FF a) <=> (F a))'
|
||||
dorun 'Xa && (!a U b) && !b && X!b'
|
||||
dorun '(a U !b) && Gb'
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -27,22 +27,22 @@ set -e
|
|||
|
||||
expect_ce()
|
||||
{
|
||||
./ltl2tgba -e "$1"
|
||||
./ltl2tgba -e -D "$1"
|
||||
./ltl2tgba -e -f "$1"
|
||||
./ltl2tgba -e -f -D "$1"
|
||||
./ltl2tgba -m "$1"
|
||||
./ltl2tgba -m -f "$1"
|
||||
run 0 ./ltl2tgba -e "$1"
|
||||
run 0 ./ltl2tgba -e -D "$1"
|
||||
run 0 ./ltl2tgba -e -f "$1"
|
||||
run 0 ./ltl2tgba -e -f -D "$1"
|
||||
run 0 ./ltl2tgba -m "$1"
|
||||
run 0 ./ltl2tgba -m -f "$1"
|
||||
}
|
||||
|
||||
expect_no()
|
||||
{
|
||||
./ltl2tgba -E "$1"
|
||||
./ltl2tgba -E -D "$1"
|
||||
./ltl2tgba -E -f "$1"
|
||||
./ltl2tgba -E -f -D "$1"
|
||||
./ltl2tgba -M "$1"
|
||||
./ltl2tgba -M -f "$1"
|
||||
run 0 ./ltl2tgba -E "$1"
|
||||
run 0 ./ltl2tgba -E -D "$1"
|
||||
run 0 ./ltl2tgba -E -f "$1"
|
||||
run 0 ./ltl2tgba -E -f -D "$1"
|
||||
run 0 ./ltl2tgba -M "$1"
|
||||
run 0 ./ltl2tgba -M -f "$1"
|
||||
}
|
||||
|
||||
expect_ce 'a'
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -32,5 +32,5 @@ s1, "s2", "a & !b", c d;
|
|||
"state 3", s1,,;
|
||||
EOF
|
||||
|
||||
./ltl2tgba -e -X input
|
||||
./ltl2tgba -m -X input
|
||||
run 0 ./ltl2tgba -e -X input
|
||||
run 0 ./ltl2tgba -m -X input
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -25,7 +25,7 @@
|
|||
|
||||
set -e
|
||||
|
||||
./explicit > stdout
|
||||
run 0 ./explicit > stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph G {
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -43,7 +43,7 @@ acc = "p1" "p2" "p3";
|
|||
"s1 * s1", "s3 * s3", "(a & !b)", "p2" "p3";
|
||||
EOF
|
||||
|
||||
./explprod input1 input2 > stdout
|
||||
run 0 ./explprod input1 input2 > stdout
|
||||
|
||||
# Sort out some possible inversions in the output.
|
||||
# (The order is not guaranteed by SPOT.)
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -43,11 +43,11 @@ acc = "p2" "p3";
|
|||
"s1 * s1", "s3 * s3", "(a & !b)", "p3";
|
||||
EOF
|
||||
|
||||
./explprod input1 input2 > stdout
|
||||
run 0 ./explprod input1 input2 > stdout
|
||||
|
||||
# Sort out some possible inversions in the output.
|
||||
# (The order is not guaranteed by SPOT.)
|
||||
sed 's/"p3" "p2"/"p2" "p3"/g;s/(!b & a)/(a \& !b)/g' stdout > tmp_ && mv tmp_ stdout
|
||||
sed 's/"p3" "p2"/"p2" "p3"/g;s/(!b & a)/(a \& !b)/g;s/(b & !a)/(!a \& b)/g' stdout > tmp_ && mv tmp_ stdout
|
||||
|
||||
cat stdout
|
||||
diff stdout expected
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -46,7 +46,7 @@ acc = "p1" "p2" "p3";
|
|||
"s2 * s2", "s3 * s1", "(a & c)", "p1" "p3";
|
||||
EOF
|
||||
|
||||
./explprod input1 input2 > stdout
|
||||
run 0 ./explprod input1 input2 > stdout
|
||||
# Sort out some possible inversions in the output.
|
||||
# (The order is not guaranteed by SPOT.)
|
||||
perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g;s/\(c & a\)/(a & c)/g;s/\(b & a\)/(a & b)/g' \
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -28,12 +28,12 @@ set -e
|
|||
# We don't check the output, but just running these might be enough to
|
||||
# trigger assertions.
|
||||
|
||||
./ltl2tgba a
|
||||
./ltl2tgba 'a U b'
|
||||
./ltl2tgba 'X a'
|
||||
./ltl2tgba 'a & b & c'
|
||||
./ltl2tgba 'a | b | (c U (d & (g U (h ^ i))))'
|
||||
./ltl2tgba 'Xa & (b U !a) & (b U !a)'
|
||||
./ltl2tgba 'Fa & Xb & GFc & Gd'
|
||||
./ltl2tgba 'Fa & Xa & GFc & Gc'
|
||||
./ltl2tgba 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
|
||||
run 0 ./ltl2tgba a
|
||||
run 0 ./ltl2tgba 'a U b'
|
||||
run 0 ./ltl2tgba 'X a'
|
||||
run 0 ./ltl2tgba 'a & b & c'
|
||||
run 0 ./ltl2tgba 'a | b | (c U (d & (g U (h ^ i))))'
|
||||
run 0 ./ltl2tgba 'Xa & (b U !a) & (b U !a)'
|
||||
run 0 ./ltl2tgba 'Fa & Xb & GFc & Gd'
|
||||
run 0 ./ltl2tgba 'Fa & Xa & GFc & Gc'
|
||||
run 0 ./ltl2tgba 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -28,11 +28,11 @@ set -e
|
|||
# We don't check the output, but just running these might be enough to
|
||||
# trigger assertions.
|
||||
|
||||
./ltlprod a b
|
||||
./ltlprod a a
|
||||
./ltlprod 'a U b' 'X f'
|
||||
./ltlprod 'X a' 'X a'
|
||||
./ltlprod 'X a' 'a U b'
|
||||
./ltlprod 'a & b & c' 'b & d & c'
|
||||
./ltlprod 'a | b | (c U (d & (g U (h ^ i))))' 'h ^ i'
|
||||
./ltlprod 'Xa & (b U !a) & (b U !a)' '(b U !a) & f'
|
||||
run 0 ./ltlprod a b
|
||||
run 0 ./ltlprod a a
|
||||
run 0 ./ltlprod 'a U b' 'X f'
|
||||
run 0 ./ltlprod 'X a' 'X a'
|
||||
run 0 ./ltlprod 'X a' 'a U b'
|
||||
run 0 ./ltlprod 'a & b & c' 'b & d & c'
|
||||
run 0 ./ltlprod 'a | b | (c U (d & (g U (h ^ i))))' 'h ^ i'
|
||||
run 0 ./ltlprod 'Xa & (b U !a) & (b U !a)' '(b U !a) & f'
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -36,11 +36,11 @@ s2, s1, "!a",;
|
|||
s2, s3, "c",;
|
||||
EOF
|
||||
|
||||
./mixprod 'F(a U b) & Xa' input1 >stdout
|
||||
run 0 ./mixprod 'F(a U b) & Xa' input1 >stdout
|
||||
cat stdout
|
||||
|
||||
# Make sure we can read the produced output
|
||||
|
||||
./mixprod 'G!a' stdout
|
||||
run 0 ./mixprod 'G!a' stdout
|
||||
|
||||
rm input1 stdout
|
||||
|
|
|
|||
|
|
@ -48,7 +48,7 @@ sed 's/"d" "c"/"c" "d"/g;s/!b & a/a \& !b/g' stdout > tmp_ && mv tmp_ stdout
|
|||
diff stdout expected
|
||||
|
||||
mv stdout input
|
||||
./readsave input > stdout
|
||||
run 0 ./readsave input > stdout
|
||||
|
||||
# Sort out some possible inversions in the output.
|
||||
# (The order is not guaranteed by SPOT.)
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -32,7 +32,7 @@ s1, "s2", "a & !b", c d;
|
|||
"state 3", s1,,;
|
||||
EOF
|
||||
|
||||
./tgbaread input > stdout
|
||||
run 0 ./tgbaread input > stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph G {
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -57,7 +57,7 @@ acc = "p1" "p2" "p3" "p4";
|
|||
"s2 * s2 * s3", "s3 * s1 * s2", "(a & c)", "p3" "p4";
|
||||
EOF
|
||||
|
||||
./tripprod input1 input2 input3 > stdout
|
||||
run 0 ./tripprod input1 input2 input3 > stdout
|
||||
|
||||
# Sort out some possible inversions in the output.
|
||||
# (The order is not guaranteed by SPOT.)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue