diff --git a/ChangeLog b/ChangeLog index 4bbdae96e..94c0b062e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2004-01-08 Alexandre Duret-Lutz + + 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 * iface/gspn/eesrg.cc (format_state): Do not rewrite \n's, diff --git a/src/tgbatest/bddprod.test b/src/tgbatest/bddprod.test index 1f24207d2..f357891a8 100755 --- a/src/tgbatest/bddprod.test +++ b/src/tgbatest/bddprod.test @@ -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' diff --git a/src/tgbatest/defs.in b/src/tgbatest/defs.in index 03c7561b1..bddc8792d 100644 --- a/src/tgbatest/defs.in +++ b/src/tgbatest/defs.in @@ -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 diff --git a/src/tgbatest/dupexp.test b/src/tgbatest/dupexp.test index 91d16d3bc..54b8389df 100755 --- a/src/tgbatest/dupexp.test +++ b/src/tgbatest/dupexp.test @@ -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 - ./ltl2tgba -S "$1" >output2 + run 0 ./ltl2tgba -s "$1" >output1 + run 0 ./ltl2tgba -S "$1" >output2 test `wc -l (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' diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test index 5057166b8..86e85f02e 100755 --- a/src/tgbatest/emptchk.test +++ b/src/tgbatest/emptchk.test @@ -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' diff --git a/src/tgbatest/emptchke.test b/src/tgbatest/emptchke.test index 5b7b669f7..62e37a2a9 100755 --- a/src/tgbatest/emptchke.test +++ b/src/tgbatest/emptchke.test @@ -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 diff --git a/src/tgbatest/explicit.test b/src/tgbatest/explicit.test index e6144f216..c64ed9848 100755 --- a/src/tgbatest/explicit.test +++ b/src/tgbatest/explicit.test @@ -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 < stdout +run 0 ./explprod input1 input2 > stdout # Sort out some possible inversions in the output. # (The order is not guaranteed by SPOT.) diff --git a/src/tgbatest/explpro3.test b/src/tgbatest/explpro3.test index 0329c843a..b2fb69645 100755 --- a/src/tgbatest/explpro3.test +++ b/src/tgbatest/explpro3.test @@ -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 diff --git a/src/tgbatest/explprod.test b/src/tgbatest/explprod.test index c2615e897..7f510dd2a 100755 --- a/src/tgbatest/explprod.test +++ b/src/tgbatest/explprod.test @@ -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' \ diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index bfdfbbcdf..26aefdf2e 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -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' diff --git a/src/tgbatest/ltlprod.test b/src/tgbatest/ltlprod.test index 7df262594..16a258ca8 100755 --- a/src/tgbatest/ltlprod.test +++ b/src/tgbatest/ltlprod.test @@ -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' diff --git a/src/tgbatest/mixprod.test b/src/tgbatest/mixprod.test index 9e72bab17..7e3f2155d 100755 --- a/src/tgbatest/mixprod.test +++ b/src/tgbatest/mixprod.test @@ -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 diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index cd0c03bfb..964f4b6c7 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -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.) diff --git a/src/tgbatest/tgbaread.test b/src/tgbatest/tgbaread.test index ee955c1eb..f3014ac9f 100755 --- a/src/tgbatest/tgbaread.test +++ b/src/tgbatest/tgbaread.test @@ -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 < stdout +run 0 ./tripprod input1 input2 input3 > stdout # Sort out some possible inversions in the output. # (The order is not guaranteed by SPOT.)