diff --git a/ChangeLog b/ChangeLog
index 02de9e50f..2bfd8436d 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,37 @@
+2009-08-31  Alexandre Duret-Lutz  <adl@va-et-vient.net>
+
+	Use Automake 1.11's parallel-tests feature.
+
+	* configure.ac: Enable parallel-tests.
+	* src/eltltest/defs.in, src/evtgbatest/defs.in,
+	src/ltltest/defs.in, src/tgbatest/defs.in: Always output verbose
+	tests.  Make a subdirectory for each test case.
+	* src/ltltest/Makefile.am, src/eltltest/Makefile.am,
+	src/tgbatest/Makefile.am, src/evtgbatest/Makefile.am: Remove
+	CLEANFILES and clean the test subdirectories in a distclean-local
+	rule instead.
+	* src/eltltest/acc.test, src/eltltest/nfa.test,
+	src/evtgbatest/explicit.test, src/evtgbatest/ltl2evtgba.test,
+	src/evtgbatest/product.test, src/evtgbatest/readsave.test,
+	src/ltltest/equals.test, src/ltltest/lunabbrev.test,
+	src/ltltest/nenoform.test, src/ltltest/parse.test,
+	src/ltltest/parseerr.test, src/ltltest/reduc.test,
+	src/ltltest/reduccmp.test, src/ltltest/syntimpl.test,
+	src/ltltest/tostring.test, src/ltltest/tunabbrev.test,
+	src/ltltest/tunenoform.test, src/tgbatest/bddprod.test,
+	src/tgbatest/complementation.test, src/tgbatest/dfs.test,
+	src/tgbatest/dupexp.test, src/tgbatest/eltl2tgba.test,
+	src/tgbatest/emptchk.test, src/tgbatest/emptchke.test,
+	src/tgbatest/emptchkr.test, src/tgbatest/explicit.test,
+	src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
+	src/tgbatest/explpro4.test, src/tgbatest/explprod.test,
+	src/tgbatest/ltl2neverclaim.test, src/tgbatest/ltl2tgba.test,
+	src/tgbatest/ltlprod.test, src/tgbatest/mixprod.test,
+	src/tgbatest/readsave.test, src/tgbatest/reduccmp.test,
+	src/tgbatest/reductgba.test, src/tgbatest/scc.test,
+	src/tgbatest/spotlbtt.test, src/tgbatest/tgbaread.test,
+	src/tgbatest/tripprod.test: Adjust to run from a subdirectory.
+
 2009-08-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* configure.ac: Switch to Automake 1.11 and enable color-tests.
diff --git a/configure.ac b/configure.ac
index cbe4daaa4..feca4f438 100644
--- a/configure.ac
+++ b/configure.ac
@@ -23,7 +23,7 @@ AC_PREREQ([2.61])
 AC_INIT([spot], [0.4a])
 AC_CONFIG_AUX_DIR([tools])
 AC_CONFIG_MACRO_DIR([m4])
-AM_INIT_AUTOMAKE([1.11 gnits nostdinc tar-ustar color-tests])
+AM_INIT_AUTOMAKE([1.11 gnits nostdinc tar-ustar color-tests parallel-tests])
 
 # If the user didn't supplied a CFLAGS value,
 # set an empty one to prevent autoconf to stick -O2 -g here.
diff --git a/src/eltltest/Makefile.am b/src/eltltest/Makefile.am
index 7f8a53ed6..9af1d8dc8 100644
--- a/src/eltltest/Makefile.am
+++ b/src/eltltest/Makefile.am
@@ -1,4 +1,4 @@
-## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
+## Copyright (C) 2003, 2004, 2005, 2006, 2009 Laboratoire d'Informatique de
 ## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 ## Université Pierre et Marie Curie.
 ##
@@ -39,6 +39,5 @@ TESTS = \
   acc.test \
   nfa.test
 
-CLEANFILES = \
-  input \
-  prelude
+distclean-local:
+	rm -rf $(TESTS:.test=.dir)
diff --git a/src/eltltest/acc.test b/src/eltltest/acc.test
index fca12d508..9ca5e40cb 100755
--- a/src/eltltest/acc.test
+++ b/src/eltltest/acc.test
@@ -20,7 +20,7 @@ A=(
 %
 A(1,a,a|b)&X(!f)
 EOF
-run 0 ./acc input || exit 1
+run 0 ../acc input || exit 1
 
 cat >input <<EOF
 include prelude
@@ -32,7 +32,7 @@ A=(
 %
 A(1,a)
 EOF
-run 1 ./acc input || exit 1
+run 1 ../acc input || exit 1
 
 cat >input <<EOF
 X=(
@@ -50,7 +50,7 @@ R=!U(!\$0, !\$1)
 %
 a U b | a R b | F(true) | U(a,b) -> R(a,b)
 EOF
-run 0 ./acc input || exit 1
+run 0 ../acc input || exit 1
 
 cat >input <<EOF
 U=(
@@ -62,7 +62,7 @@ T=U(true,true)
 %
 T()|1
 EOF
-run 1 ./acc input || exit 1
+run 1 ../acc input || exit 1
 
 cat >input <<EOF
 A=(
@@ -70,4 +70,4 @@ A=(
 %
 1
 EOF
-run 0 ./acc input || exit 1
+run 0 ../acc input || exit 1
diff --git a/src/eltltest/defs.in b/src/eltltest/defs.in
index e9f01fef5..a233bcfd8 100644
--- a/src/eltltest/defs.in
+++ b/src/eltltest/defs.in
@@ -1,5 +1,5 @@
 # -*- shell-script -*-
-# Copyright (C) 2003, 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2006, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -26,9 +26,8 @@ test -f ./defs || {
    exit 1
 }
 
-# If srcdir is not set, then we are not running from `make check', be verbose.
+# If srcdir is not set, then we are not running from `make check'.
 if test -z "$srcdir"; then
-   test -z "$VERBOSE" && VERBOSE=x
    # compute $srcdir.
    srcdir=`echo "$0" | sed -e 's,/[^\\/]*$,,'`
    test $srcdir = $0 && srcdir=.
@@ -40,11 +39,16 @@ test -f $srcdir/defs.in || {
    exit 1
 }
 
-# User can set VERBOSE to see all output.
-test -z "$VERBOSE" && exec >/dev/null 2>&1
-
 echo "== Running test $0"
 
+me=`echo "$0" | sed -e 's,.*[\\/],,;s/\.test$//'`
+
+testSubDir=$me.dir
+chmod -R a+rwx $testSubDir > /dev/null 2>&1
+rm -rf $testSubDir > /dev/null 2>&1
+mkdir $testSubDir
+cd $testSubDir
+
 DOT='@DOT@'
 VALGRIND='@VALGRIND@'
 
@@ -67,9 +71,4 @@ run()
   test $exitcode = $expected_exitcode || exit 1
 }
 
-# Turn on shell traces when VERBOSE=x.
-if test "x$VERBOSE" = xx; then
-  set -x
-else
-  :
-fi
+set -x
diff --git a/src/eltltest/nfa.test b/src/eltltest/nfa.test
index 241c7f207..607d125e6 100755
--- a/src/eltltest/nfa.test
+++ b/src/eltltest/nfa.test
@@ -3,4 +3,4 @@
 . ./defs || exit 1
 
 set -e
-run 0 ./nfa || exit 1
+run 0 ../nfa || exit 1
diff --git a/src/evtgbatest/Makefile.am b/src/evtgbatest/Makefile.am
index aecb57847..362960a94 100644
--- a/src/evtgbatest/Makefile.am
+++ b/src/evtgbatest/Makefile.am
@@ -46,4 +46,6 @@ TESTS = \
   ltl2evtgba.test
 
 EXTRA_DIST = $(TESTS)
-CLEANFILES = input1 input2 input3 stdout expected
+
+distclean-local:
+	rm -rf $(TESTS:.test=.dir)
diff --git a/src/evtgbatest/defs.in b/src/evtgbatest/defs.in
index b809e9e3e..2179e38a7 100644
--- a/src/evtgbatest/defs.in
+++ b/src/evtgbatest/defs.in
@@ -1,5 +1,5 @@
 # -*- shell-script -*-
-# Copyright (C) 2003, 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2006, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -26,9 +26,8 @@ test -f ./defs || {
    exit 1
 }
 
-# If srcdir is not set, then we are not running from `make check', be verbose.
+# If srcdir is not set, then we are not running from `make check'.
 if test -z "$srcdir"; then
-   test -z "$VERBOSE" && VERBOSE=x
    # compute $srcdir.
    srcdir=`echo "$0" | sed -e 's,/[^\\/]*$,,'`
    test $srcdir = $0 && srcdir=.
@@ -40,11 +39,16 @@ test -f $srcdir/defs.in || {
    exit 1
 }
 
-# User can set VERBOSE to see all output.
-test -z "$VERBOSE" && exec >/dev/null 2>&1
-
 echo "== Running test $0"
 
+me=`echo "$0" | sed -e 's,.*[\\/],,;s/\.test$//'`
+
+testSubDir=$me.dir
+chmod -R a+rwx $testSubDir > /dev/null 2>&1
+rm -rf $testSubDir > /dev/null 2>&1
+mkdir $testSubDir
+cd $testSubDir
+
 DOT='@DOT@'
 top_builddir='@top_builddir@'
 LBTT="@LBTT@"
@@ -71,9 +75,4 @@ run()
   test $exitcode = $expected_exitcode || exit 1
 }
 
-# Turn on shell traces when VERBOSE=x.
-if test "x$VERBOSE" = xx; then
-  set -x
-else
-  :
-fi
+set -x
diff --git a/src/evtgbatest/explicit.test b/src/evtgbatest/explicit.test
index 7884e55c6..6b1c6db55 100755
--- a/src/evtgbatest/explicit.test
+++ b/src/evtgbatest/explicit.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2004, 2005, 2009  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
 
-run 0 ./explicit > stdout
+run 0 ../explicit > stdout
 
 cat >expected <<\EOF
 digraph G {
diff --git a/src/evtgbatest/ltl2evtgba.test b/src/evtgbatest/ltl2evtgba.test
index 847745b7a..e584da4c1 100755
--- a/src/evtgbatest/ltl2evtgba.test
+++ b/src/evtgbatest/ltl2evtgba.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -27,8 +27,8 @@ set -e
 
 check ()
 {
-  run 0 ./ltl2evtgba "$1"
-  run 0 ./ltl2evtgba -Uun1,un2,un3 "$1"
+  run 0 ../ltl2evtgba "$1"
+  run 0 ../ltl2evtgba -Uun1,un2,un3 "$1"
 }
 
 # We don't check the output, but just running these might be enough to
diff --git a/src/evtgbatest/product.test b/src/evtgbatest/product.test
index 378643894..4c38dc978 100755
--- a/src/evtgbatest/product.test
+++ b/src/evtgbatest/product.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -47,7 +47,7 @@ u1, u2, c, Acc1;
 u2, u1, b, Acc2;
 EOF
 
-run 0 ./product input1 input2 input3 >stdout
+run 0 ../product input1 input2 input3 >stdout
 
 cat >expected <<\EOF
 acc = Acc1 Acc2 Acc3;
diff --git a/src/evtgbatest/readsave.test b/src/evtgbatest/readsave.test
index a258ce9ad..563e5f7ce 100755
--- a/src/evtgbatest/readsave.test
+++ b/src/evtgbatest/readsave.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -33,7 +33,7 @@ s1, "s2", e1, c;
 "state 3", "s1",e4,;
 EOF
 
-./readsave input > stdout
+../readsave input > stdout
 
 cat >expected <<\EOF
 acc = c d;
@@ -46,7 +46,7 @@ EOF
 diff stdout expected
 
 mv stdout input
-run 0 ./readsave input > stdout
+run 0 ../readsave input > stdout
 
 diff input stdout
 
diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am
index 642001944..c47d42ae3 100644
--- a/src/ltltest/Makefile.am
+++ b/src/ltltest/Makefile.am
@@ -1,4 +1,4 @@
-## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
+## Copyright (C) 2003, 2004, 2005, 2006, 2009 Laboratoire d'Informatique de
 ## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 ## Université Pierre et Marie Curie.
 ##
@@ -83,4 +83,5 @@ TESTS = \
   reduc.test \
   reduccmp.test
 
-CLEANFILES = stdout expect parse.dot result.data formulae
+distclean-local:
+	rm -rf $(TESTS:.test=.dir)
diff --git a/src/ltltest/defs.in b/src/ltltest/defs.in
index e9f01fef5..a233bcfd8 100644
--- a/src/ltltest/defs.in
+++ b/src/ltltest/defs.in
@@ -1,5 +1,5 @@
 # -*- shell-script -*-
-# Copyright (C) 2003, 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2006, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -26,9 +26,8 @@ test -f ./defs || {
    exit 1
 }
 
-# If srcdir is not set, then we are not running from `make check', be verbose.
+# If srcdir is not set, then we are not running from `make check'.
 if test -z "$srcdir"; then
-   test -z "$VERBOSE" && VERBOSE=x
    # compute $srcdir.
    srcdir=`echo "$0" | sed -e 's,/[^\\/]*$,,'`
    test $srcdir = $0 && srcdir=.
@@ -40,11 +39,16 @@ test -f $srcdir/defs.in || {
    exit 1
 }
 
-# User can set VERBOSE to see all output.
-test -z "$VERBOSE" && exec >/dev/null 2>&1
-
 echo "== Running test $0"
 
+me=`echo "$0" | sed -e 's,.*[\\/],,;s/\.test$//'`
+
+testSubDir=$me.dir
+chmod -R a+rwx $testSubDir > /dev/null 2>&1
+rm -rf $testSubDir > /dev/null 2>&1
+mkdir $testSubDir
+cd $testSubDir
+
 DOT='@DOT@'
 VALGRIND='@VALGRIND@'
 
@@ -67,9 +71,4 @@ run()
   test $exitcode = $expected_exitcode || exit 1
 }
 
-# Turn on shell traces when VERBOSE=x.
-if test "x$VERBOSE" = xx; then
-  set -x
-else
-  :
-fi
+set -x
diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test
index 80e040b27..baac340c7 100755
--- a/src/ltltest/equals.test
+++ b/src/ltltest/equals.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -26,37 +26,37 @@
 . ./defs || exit 1
 
 # A few things which are equal
-run 0 ./equals 'a' 'a'
-run 0 ./equals '1' '1'
-run 0 ./equals '0' '0'
-run 0 ./equals 'a => b' 'a => b'
-run 0 ./equals 'G a ' ' G a'
-run 0 ./equals 'a U b' 'a U b'
-run 0 ./equals 'a & b' 'a & b'
-run 0 ./equals 'a & b' 'b & a'
-run 0 ./equals 'a & b & c' 'c & a && b'
-run 0 ./equals 'a & b & c' 'b & c & a'
-run 0 ./equals 'a && b & a' 'b & a & b'
-run 0 ./equals 'a & b' 'b & a & b'
-run 0 ./equals 'a & b' 'b & a & a'
-run 0 ./equals 'a & b & (c |(f U g)|| e)' \
-               'b & a & a & (c | e |(f U g)| e | c) & b'
-run 0 ./equals 'a & a' 'a'
+run 0 ../equals 'a' 'a'
+run 0 ../equals '1' '1'
+run 0 ../equals '0' '0'
+run 0 ../equals 'a => b' 'a => b'
+run 0 ../equals 'G a ' ' G a'
+run 0 ../equals 'a U b' 'a U b'
+run 0 ../equals 'a & b' 'a & b'
+run 0 ../equals 'a & b' 'b & a'
+run 0 ../equals 'a & b & c' 'c & a && b'
+run 0 ../equals 'a & b & c' 'b & c & a'
+run 0 ../equals 'a && b & a' 'b & a & b'
+run 0 ../equals 'a & b' 'b & a & b'
+run 0 ../equals 'a & b' 'b & a & a'
+run 0 ../equals 'a & b & (c |(f U g)|| e)' \
+                'b & a & a & (c | e |(f U g)| e | c) & b'
+run 0 ../equals 'a & a' 'a'
 
 # other formulae which are not
-run 1 ./equals 'a' 'b'
-run 1 ./equals '1' '0'
-run 1 ./equals 'a => b' 'b => a'
-run 1 ./equals 'a => b' 'a <=> b'
-run 1 ./equals 'a => b' 'a U b'
-run 1 ./equals 'a R b' 'a U b'
-run 1 ./equals 'a & b & c' 'c & a'
-run 1 ./equals 'b & c' 'c & a & b'
-run 1 ./equals 'a & b & (c |(f U g)| e)' \
-               'b & a & a & (c | e |(g U g)| e | c) & b'
+run 1 ../equals 'a' 'b'
+run 1 ../equals '1' '0'
+run 1 ../equals 'a => b' 'b => a'
+run 1 ../equals 'a => b' 'a <=> b'
+run 1 ../equals 'a => b' 'a U b'
+run 1 ../equals 'a R b' 'a U b'
+run 1 ../equals 'a & b & c' 'c & a'
+run 1 ../equals 'b & c' 'c & a & b'
+run 1 ../equals 'a & b & (c |(f U g)| e)' \
+                'b & a & a & (c | e |(g U g)| e | c) & b'
 
 # Precedence
-run 0 ./equals 'a & b ^ c | d' 'd | c ^ b & a'
+run 0 ../equals 'a & b ^ c | d' 'd | c ^ b & a'
 
 # Corner cases parsing
-run 0 ./equals 'FFG__GFF' 'F(F(G("__GFF")))'
+run 0 ../equals 'FFG__GFF' 'F(F(G("__GFF")))'
diff --git a/src/ltltest/lunabbrev.test b/src/ltltest/lunabbrev.test
index aec793646..9b231f601 100755
--- a/src/ltltest/lunabbrev.test
+++ b/src/ltltest/lunabbrev.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -28,24 +28,24 @@
 set -e
 
 # A few things that do not change
-run 0 ./lunabbrev 'a' 'a'
-run 0 ./lunabbrev '1' '1'
-run 0 ./lunabbrev '0' '0'
-run 0 ./lunabbrev 'G a ' ' G a'
-run 0 ./lunabbrev 'a U b' 'a U b'
-run 0 ./lunabbrev 'a & b' 'a & b'
-run 0 ./lunabbrev 'a & b' 'b & a'
-run 0 ./lunabbrev 'a & b & c' 'c & a & b'
-run 0 ./lunabbrev 'a & b & c' 'b & c & a'
-run 0 ./lunabbrev 'a & b & a' 'b & a & b'
-run 0 ./lunabbrev 'a & b' 'b & a & b'
-run 0 ./lunabbrev 'a & b' 'b & a & a'
-run 0 ./lunabbrev 'a & b & (c |(f U g)| e)' \
+run 0 ../lunabbrev 'a' 'a'
+run 0 ../lunabbrev '1' '1'
+run 0 ../lunabbrev '0' '0'
+run 0 ../lunabbrev 'G a ' ' G a'
+run 0 ../lunabbrev 'a U b' 'a U b'
+run 0 ../lunabbrev 'a & b' 'a & b'
+run 0 ../lunabbrev 'a & b' 'b & a'
+run 0 ../lunabbrev 'a & b & c' 'c & a & b'
+run 0 ../lunabbrev 'a & b & c' 'b & c & a'
+run 0 ../lunabbrev 'a & b & a' 'b & a & b'
+run 0 ../lunabbrev 'a & b' 'b & a & b'
+run 0 ../lunabbrev 'a & b' 'b & a & a'
+run 0 ../lunabbrev 'a & b & (c |(f U g)| e)' \
                   'b & a & a & (c | e |(f U g)| e | c) & b'
 # other formulae that do change
-run 0 ./lunabbrev 'a ^ b' '(a & !b) | (!a & b)'
-run 0 ./lunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
-run 0 ./lunabbrev 'GF a => F G(b)' '!GFa | F Gb'
-run 0 ./lunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
-run 0 ./lunabbrev '(a ^ b) | (b ^ c)' \
-                  '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
+run 0 ../lunabbrev 'a ^ b' '(a & !b) | (!a & b)'
+run 0 ../lunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
+run 0 ../lunabbrev 'GF a => F G(b)' '!GFa | F Gb'
+run 0 ../lunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
+run 0 ../lunabbrev '(a ^ b) | (b ^ c)' \
+                   '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
diff --git a/src/ltltest/nenoform.test b/src/ltltest/nenoform.test
index bfb833580..61f2c9080 100755
--- a/src/ltltest/nenoform.test
+++ b/src/ltltest/nenoform.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -28,39 +28,39 @@
 set -e
 
 # A few things that do not change
-run 0 ./nenoform 'a' 'a'
-run 0 ./nenoform '1' '1'
-run 0 ./nenoform '0' '0'
-run 0 ./nenoform '!a' '!a'
-run 0 ./nenoform 'a U b' 'a U b'
-run 0 ./nenoform 'a & b' 'a & b'
-run 0 ./nenoform 'a & b' 'b & a'
-run 0 ./nenoform 'a & !b & c' 'c & a & !b'
-run 0 ./nenoform 'a & b & c' 'b & c & a'
-run 0 ./nenoform 'Xa & b & Xa' 'b & Xa & b'
-run 0 ./nenoform 'a & b' 'b & a & b'
-run 0 ./nenoform 'a & !b' '!b & a & a'
-run 0 ./nenoform 'a & b & (Xc |(f U !g)| e)' \
-                 'b & a & a & (Xc | e |(f U !g)| e | Xc) & b'
-run 0 ./nenoform 'GFa => FGb' 'GFa => FGb'
+run 0 ../nenoform 'a' 'a'
+run 0 ../nenoform '1' '1'
+run 0 ../nenoform '0' '0'
+run 0 ../nenoform '!a' '!a'
+run 0 ../nenoform 'a U b' 'a U b'
+run 0 ../nenoform 'a & b' 'a & b'
+run 0 ../nenoform 'a & b' 'b & a'
+run 0 ../nenoform 'a & !b & c' 'c & a & !b'
+run 0 ../nenoform 'a & b & c' 'b & c & a'
+run 0 ../nenoform 'Xa & b & Xa' 'b & Xa & b'
+run 0 ../nenoform 'a & b' 'b & a & b'
+run 0 ../nenoform 'a & !b' '!b & a & a'
+run 0 ../nenoform 'a & b & (Xc |(f U !g)| e)' \
+                  'b & a & a & (Xc | e |(f U !g)| e | Xc) & b'
+run 0 ../nenoform 'GFa => FGb' 'GFa => FGb'
 
 # Basic rewritings
-run 0 ./nenoform '!!a' 'a'
-run 0 ./nenoform '!!!!!a' '!a'
-run 0 ./nenoform '!Xa' 'X!a'
-run 0 ./nenoform '!Fa' 'G!a'
-run 0 ./nenoform '!Ga' 'F!a'
-run 0 ./nenoform '!(a ^ b)' 'a <=> b'
-run 0 ./nenoform '!(a <=> b)' '(((a) ^ (b)))'
-run 0 ./nenoform '!(a => b)' 'a&!b'
-run 0 ./nenoform '!(!a => !b)' '!a&b'
-run 0 ./nenoform '!(a U b)' '!a R !b'
-run 0 ./nenoform '!(a R b)' '!a U !b'
-run 0 ./nenoform '!(!a R !b)' 'a U b'
-run 0 ./nenoform '!(a & b & c & d & b)' '!a | !b | !c | !d'
-run 0 ./nenoform '!(a | b | c | d)' '!a & !b & !c & !d'
+run 0 ../nenoform '!!a' 'a'
+run 0 ../nenoform '!!!!!a' '!a'
+run 0 ../nenoform '!Xa' 'X!a'
+run 0 ../nenoform '!Fa' 'G!a'
+run 0 ../nenoform '!Ga' 'F!a'
+run 0 ../nenoform '!(a ^ b)' 'a <=> b'
+run 0 ../nenoform '!(a <=> b)' '(((a) ^ (b)))'
+run 0 ../nenoform '!(a => b)' 'a&!b'
+run 0 ../nenoform '!(!a => !b)' '!a&b'
+run 0 ../nenoform '!(a U b)' '!a R !b'
+run 0 ../nenoform '!(a R b)' '!a U !b'
+run 0 ../nenoform '!(!a R !b)' 'a U b'
+run 0 ../nenoform '!(a & b & c & d & b)' '!a | !b | !c | !d'
+run 0 ../nenoform '!(a | b | c | d)' '!a & !b & !c & !d'
 
 # Nested rewritings
-run 0 ./nenoform '!(a U (!b U ((a & b & c) R d)))' \
-                 '!a R (b R ((!a | !b | !c) U !d))'
-run 0 ./nenoform '!(GF a => FG b)' 'GFa & GF!b'
+run 0 ../nenoform '!(a U (!b U ((a & b & c) R d)))' \
+                  '!a R (b R ((!a | !b | !c) U !d))'
+run 0 ../nenoform '!(GF a => FG b)' 'GFa & GF!b'
diff --git a/src/ltltest/parse.test b/src/ltltest/parse.test
index 4550f6448..1a36dfd2b 100755
--- a/src/ltltest/parse.test
+++ b/src/ltltest/parse.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -76,7 +76,7 @@ for f in \
   '((X(p2=0))U(X(p2=0)))+((Xp1=0)UFALSE)'
 
 do
-  if ./ltl2text "$f"; then
+  if ../ltl2text "$f"; then
     :
   else
     echo "ltl2dot failed to parse '$f'"
@@ -84,7 +84,7 @@ do
   fi
 
   if test -n "$DOT"; then
-    run 0 ./ltl2dot "$f" > parse.dot
+    run 0 ../ltl2dot "$f" > parse.dot
     if $DOT -o /dev/null parse.dot; then
       rm -f parse.dot
     else
diff --git a/src/ltltest/parseerr.test b/src/ltltest/parseerr.test
index 413eaa047..89e45131c 100755
--- a/src/ltltest/parseerr.test
+++ b/src/ltltest/parseerr.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -28,7 +28,7 @@
 
 check()
 {
-  run 1 ./ltl2text "$1" >stdout
+  run 1 ../ltl2text "$1" >stdout
   if test -n "$2"; then
     echo "$2" >expect
   else
@@ -52,21 +52,21 @@ check '+' ''
 check '/2/3/4/5 a + b /6/7/8/' ''
 
 # leading and trailing garbage are skipped
-run 0 ./equals -E 'a U b c' 'a U b'
-run 0 ./equals -E 'a &&& b' '0 && b'
+run 0 ../equals -E 'a U b c' 'a U b'
+run 0 ../equals -E 'a &&& b' '0 && b'
 # (check multop merging while we are at it)
-run 0 ./equals -E 'a & b & c & d e' 'a & b & c & d'
-run 0 ./equals -E 'a & (b | c) & d should work' 'a & (b | c) & d'
+run 0 ../equals -E 'a & b & c & d e' 'a & b & c & d'
+run 0 ../equals -E 'a & (b | c) & d should work' 'a & (b | c) & d'
 # Binop recovery
-run 0 ./equals -E 'a U' 0
-run 0 ./equals -E 'a U b V c R' 0
+run 0 ../equals -E 'a U' 0
+run 0 ../equals -E 'a U b V c R' 0
 
 # Recovery inside parentheses
-run 0 ./equals -E 'a U (b c) U e R (f g <=> h)' 'a U (0) U e R (0)'
-run 0 ./equals -E 'a U ((c) U e) R (<=> f g)' 'a U ((c) U e) R (0)'
+run 0 ../equals -E 'a U (b c) U e R (f g <=> h)' 'a U (0) U e R (0)'
+run 0 ../equals -E 'a U ((c) U e) R (<=> f g)' 'a U ((c) U e) R (0)'
 
 # Missing parentheses
-run 0 ./equals -E 'a & (a + b' 'a & (a + b)'
-run 0 ./equals -E 'a & (a + b c' 'a & (0)'
-run 0 ./equals -E 'a & (+' 'a & (0)'
-run 0 ./equals -E 'a & ('  'a & (0)'
+run 0 ../equals -E 'a & (a + b' 'a & (a + b)'
+run 0 ../equals -E 'a & (a + b c' 'a & (0)'
+run 0 ../equals -E 'a & (+' 'a & (0)'
+run 0 ../equals -E 'a & ('  'a & (0)'
diff --git a/src/ltltest/reduc.test b/src/ltltest/reduc.test
index 3b94c0e6c..cde33ea6e 100755
--- a/src/ltltest/reduc.test
+++ b/src/ltltest/reduc.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2004, 2005, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2004, 2005, 2006, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -30,8 +30,8 @@ FILE=formulae
 : > $FILE
 # for i in 10 11 12 13 14 15 16 17 18 19 20; do
 for i in 10 12 14 16 18 20; do
-  run 0 ./randltl -u -s 0   -f $i a b c -F 100 >> $FILE
-  run 0 ./randltl -u -s 100 -f $i a b c d e f -F 100 >> $FILE
+  run 0 ../randltl -u -s 0   -f $i a b c -F 100 >> $FILE
+  run 0 ../randltl -u -s 100 -f $i a b c d e f -F 100 >> $FILE
 done
 
 for opt in 0 1 2 3 7 8 9; do
@@ -39,7 +39,7 @@ for opt in 0 1 2 3 7 8 9; do
 
   cat $FILE |
   while read f; do
-    ./reduc $opt "$f" >> result.data
+    ../reduc $opt "$f" >> result.data
   done
 
   test $? = 0 || exit 1
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index a8684d108..f692b193d 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2004, 2006, 2009  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 @@
 
 . ./defs || exit 1
 
-for x in ./reduccmp ./reductaustr; do
+for x in ../reduccmp ../reductaustr; do
 
   # No reduction
   run 0 $x 'a U b' 'a U b'
diff --git a/src/ltltest/syntimpl.test b/src/ltltest/syntimpl.test
index 1cd639ef0..ad35ee0b6 100755
--- a/src/ltltest/syntimpl.test
+++ b/src/ltltest/syntimpl.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -27,67 +27,67 @@
 
 #
 #GFa && GFb && FG(!a && !b)
-run 1 ./syntimpl 0 'a' 'a | b'
-run 1 ./syntimpl 0 'F(a)' 'F(a | b)'
-run 1 ./syntimpl 0 'G(a)' 'G(a | b)'
-run 1 ./syntimpl 0 'GF(a)' 'GF(a | b)'
-run 1 ./syntimpl 0 'GF(a)' '!FG(!a && !b)'
+run 1 ../syntimpl 0 'a' 'a | b'
+run 1 ../syntimpl 0 'F(a)' 'F(a | b)'
+run 1 ../syntimpl 0 'G(a)' 'G(a | b)'
+run 1 ../syntimpl 0 'GF(a)' 'GF(a | b)'
+run 1 ../syntimpl 0 'GF(a)' '!FG(!a && !b)'
 
-run 1 ./syntimpl 0 'Xa' 'X(b U a)'
-run 1 ./syntimpl 0 'XXa' 'XX(b U a)'
+run 1 ../syntimpl 0 'Xa' 'X(b U a)'
+run 1 ../syntimpl 0 'XXa' 'XX(b U a)'
 
-run 1 ./syntimpl 0 '(e R f)' '(g U f)'
-run 1 ./syntimpl 0 '( X(a + b))' '( X((a + b)+(c)+(d)))'
-run 1 ./syntimpl 0 '( X(a + b)) U (e R f)' '( X((a + b)+(c)+(d))) U (g U f)'
+run 1 ../syntimpl 0 '(e R f)' '(g U f)'
+run 1 ../syntimpl 0 '( X(a + b))' '( X((a + b)+(c)+(d)))'
+run 1 ../syntimpl 0 '( X(a + b)) U (e R f)' '( X((a + b)+(c)+(d))) U (g U f)'
 
-run 1 ./syntimpl 0 '1' '1'
-run 1 ./syntimpl 0 '0' '0'
+run 1 ../syntimpl 0 '1' '1'
+run 1 ../syntimpl 0 '0' '0'
 
-run 1 ./syntimpl 0 'a' '1'
-run 1 ./syntimpl 0 'a' 'a'
+run 1 ../syntimpl 0 'a' '1'
+run 1 ../syntimpl 0 'a' 'a'
 
-run 1 ./syntimpl 0 'a' 'a * 1'
+run 1 ../syntimpl 0 'a' 'a * 1'
 
-run 1 ./syntimpl 0 'a * b' 'b'
-run 1 ./syntimpl 0 'a * b' 'a'
+run 1 ../syntimpl 0 'a * b' 'b'
+run 1 ../syntimpl 0 'a * b' 'a'
 
-run 1 ./syntimpl 0 'a' 'a + b'
-run 1 ./syntimpl 0 'b' 'a + b'
+run 1 ../syntimpl 0 'a' 'a + b'
+run 1 ../syntimpl 0 'b' 'a + b'
 
-run 1 ./syntimpl 0 'a + b' '1'
+run 1 ../syntimpl 0 'a + b' '1'
 
-run 1 ./syntimpl 0 'a' 'b U a'
-run 1 ./syntimpl 0 'a' 'b U 1'
-run 1 ./syntimpl 0 'a U b' '1'
+run 1 ../syntimpl 0 'a' 'b U a'
+run 1 ../syntimpl 0 'a' 'b U 1'
+run 1 ../syntimpl 0 'a U b' '1'
 
-run 1 ./syntimpl 0 'a' '1 R a'
-run 1 ./syntimpl 0 'a' 'a R 1'
-run 1 ./syntimpl 0 'a R b' 'b'
-run 1 ./syntimpl 0 'a R b' '1'
+run 1 ../syntimpl 0 'a' '1 R a'
+run 1 ../syntimpl 0 'a' 'a R 1'
+run 1 ../syntimpl 0 'a R b' 'b'
+run 1 ../syntimpl 0 'a R b' '1'
 
-run 1 ./syntimpl 0 'Xa' 'X(b U a)'
-run 1 ./syntimpl 0 'X(a R b)' 'Xb'
+run 1 ../syntimpl 0 'Xa' 'X(b U a)'
+run 1 ../syntimpl 0 'X(a R b)' 'Xb'
 
-run 1 ./syntimpl 0 'a U b' '1 U b'
-run 1 ./syntimpl 0 'a R b' '1 R b'
+run 1 ../syntimpl 0 'a U b' '1 U b'
+run 1 ../syntimpl 0 'a R b' '1 R b'
 
-run 1 ./syntimpl 0 'b * (a U b)' 'a U b'
-run 1 ./syntimpl 0 'a U b' 'c + (a U b)'
+run 1 ../syntimpl 0 'b * (a U b)' 'a U b'
+run 1 ../syntimpl 0 'a U b' 'c + (a U b)'
 
-run 0 ./syntimpl 0 'Xa' 'XX(b U a)'
-run 0 ./syntimpl 0 'XXa' 'X(b U a)'
+run 0 ../syntimpl 0 'Xa' 'XX(b U a)'
+run 0 ../syntimpl 0 'XXa' 'X(b U a)'
 
-run 0 ./syntimpl 0 '( X(a + b))' '( X(X(a + b)+(c)+(d)))'
-run 0 ./syntimpl 0 '( X(a + b)) U (e R f)' '( X(X(a + b)+(c)+(d))) U (g U f)'
+run 0 ../syntimpl 0 '( X(a + b))' '( X(X(a + b)+(c)+(d)))'
+run 0 ../syntimpl 0 '( X(a + b)) U (e R f)' '( X(X(a + b)+(c)+(d))) U (g U f)'
 
-run 0 ./syntimpl 0 'a' 'b'
-run 0 ./syntimpl 0 'a' 'b + c'
-run 0 ./syntimpl 0 'a + b' 'a'
-run 0 ./syntimpl 0 'a' 'a * c'
-run 0 ./syntimpl 0 'a * b' 'c'
-run 0 ./syntimpl 0 'a' 'a U b'
-run 0 ./syntimpl 0 'a' 'a R b'
-run 0 ./syntimpl 0 'a R b' 'a'
+run 0 ../syntimpl 0 'a' 'b'
+run 0 ../syntimpl 0 'a' 'b + c'
+run 0 ../syntimpl 0 'a + b' 'a'
+run 0 ../syntimpl 0 'a' 'a * c'
+run 0 ../syntimpl 0 'a * b' 'c'
+run 0 ../syntimpl 0 'a' 'a U b'
+run 0 ../syntimpl 0 'a' 'a R b'
+run 0 ../syntimpl 0 'a R b' 'a'
 
-run 0 ./syntimpl 0 'p2' 'p3 || G(p2 && p5)'
-run 0 ./syntimpl 0 '!(p3 || G(p2 && p5))' '!p2'
\ No newline at end of file
+run 0 ../syntimpl 0 'p2' 'p3 || G(p2 && p5)'
+run 0 ../syntimpl 0 '!(p3 || G(p2 && p5))' '!p2'
diff --git a/src/ltltest/tostring.test b/src/ltltest/tostring.test
index 453ad9c12..b3e135b44 100755
--- a/src/ltltest/tostring.test
+++ b/src/ltltest/tostring.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -27,30 +27,30 @@
 
 set -e
 
-run 0 ./tostring 'a'
-run 0 ./tostring '1'
-run 0 ./tostring '0'
-run 0 ./tostring 'a => b'
-run 0 ./tostring 'G a '
-run 0 ./tostring 'a U b'
-run 0 ./tostring 'a & b'
-run 0 ./tostring 'a & b & c'
-run 0 ./tostring 'b & a & b'
-run 0 ./tostring 'b & a & a'
-run 0 ./tostring 'a & b & (c |(f U g)| e)'
-run 0 ./tostring 'b & a & a & (c | e |(f U g)| e | c) & b'
-run 0 ./tostring 'a <=> b'
-run 0 ./tostring 'a & b & (c |(f U g)| e)'
-run 0 ./tostring 'b & a & a & (c | e |(g U g)| e | c) & b'
-run 0 ./tostring 'F"F1"&G"G"&X"X"'
-run 0 ./tostring 'GFfalse'
-run 0 ./tostring 'GFtrue'
-run 0 ./tostring 'p=0Uq=1Ut=1'
-run 0 ./tostring 'F"FALSE"'
-run 0 ./tostring 'G"TruE"'
-run 0 ./tostring 'FFALSE'
-run 0 ./tostring 'GTruE'
-run 0 ./tostring 'p=0UFXp=1'
-run 0 ./tostring 'GF"\GF"'
-run 0 ./tostring 'GF"foo bar"'
-run 0 ./tostring 'FFG__GFF'
+run 0 ../tostring 'a'
+run 0 ../tostring '1'
+run 0 ../tostring '0'
+run 0 ../tostring 'a => b'
+run 0 ../tostring 'G a '
+run 0 ../tostring 'a U b'
+run 0 ../tostring 'a & b'
+run 0 ../tostring 'a & b & c'
+run 0 ../tostring 'b & a & b'
+run 0 ../tostring 'b & a & a'
+run 0 ../tostring 'a & b & (c |(f U g)| e)'
+run 0 ../tostring 'b & a & a & (c | e |(f U g)| e | c) & b'
+run 0 ../tostring 'a <=> b'
+run 0 ../tostring 'a & b & (c |(f U g)| e)'
+run 0 ../tostring 'b & a & a & (c | e |(g U g)| e | c) & b'
+run 0 ../tostring 'F"F1"&G"G"&X"X"'
+run 0 ../tostring 'GFfalse'
+run 0 ../tostring 'GFtrue'
+run 0 ../tostring 'p=0Uq=1Ut=1'
+run 0 ../tostring 'F"FALSE"'
+run 0 ../tostring 'G"TruE"'
+run 0 ../tostring 'FFALSE'
+run 0 ../tostring 'GTruE'
+run 0 ../tostring 'p=0UFXp=1'
+run 0 ../tostring 'GF"\GF"'
+run 0 ../tostring 'GF"foo bar"'
+run 0 ../tostring 'FFG__GFF'
diff --git a/src/ltltest/tunabbrev.test b/src/ltltest/tunabbrev.test
index 57b3aa448..c329bc35c 100755
--- a/src/ltltest/tunabbrev.test
+++ b/src/ltltest/tunabbrev.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -28,30 +28,30 @@
 set -e
 
 # A few things that do not change
-run 0 ./tunabbrev 'a' 'a'
-run 0 ./tunabbrev '1' '1'
-run 0 ./tunabbrev '0' '0'
-run 0 ./tunabbrev 'a U b' 'a U b'
-run 0 ./tunabbrev 'a & b' 'a & b'
-run 0 ./tunabbrev 'a & b' 'b & a'
-run 0 ./tunabbrev 'a & b & c' 'c & a & b'
-run 0 ./tunabbrev 'a & b & c' 'b & c & a'
-run 0 ./tunabbrev 'a & b & a' 'b & a & b'
-run 0 ./tunabbrev 'a & b' 'b & a & b'
-run 0 ./tunabbrev 'a & b' 'b & a & a'
-run 0 ./tunabbrev 'a & b & (c |(f U g)| e)' \
-                  'b & a & a & (c | e |(f U g)| e | c) & b'
+run 0 ../tunabbrev 'a' 'a'
+run 0 ../tunabbrev '1' '1'
+run 0 ../tunabbrev '0' '0'
+run 0 ../tunabbrev 'a U b' 'a U b'
+run 0 ../tunabbrev 'a & b' 'a & b'
+run 0 ../tunabbrev 'a & b' 'b & a'
+run 0 ../tunabbrev 'a & b & c' 'c & a & b'
+run 0 ../tunabbrev 'a & b & c' 'b & c & a'
+run 0 ../tunabbrev 'a & b & a' 'b & a & b'
+run 0 ../tunabbrev 'a & b' 'b & a & b'
+run 0 ../tunabbrev 'a & b' 'b & a & a'
+run 0 ../tunabbrev 'a & b & (c |(f U g)| e)' \
+                   'b & a & a & (c | e |(f U g)| e | c) & b'
 
 # same as in lunabbrev.test:
-run 0 ./tunabbrev 'a ^ b' '(a & !b) | (!a & b)'
-run 0 ./tunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
-run 0 ./tunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
-run 0 ./tunabbrev '(a ^ b) | (b ^ c)' \
-                  '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
+run 0 ../tunabbrev 'a ^ b' '(a & !b) | (!a & b)'
+run 0 ../tunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
+run 0 ../tunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
+run 0 ../tunabbrev '(a ^ b) | (b ^ c)' \
+                   '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
 
 # LTL unabbreviations:
-run 0 ./tunabbrev 'G a ' 'false R a'
-run 0 ./tunabbrev 'GF a => F G(b)' \
-                  '!(false R (true U a)) | (true U (false V b))'
-run 0 ./tunabbrev 'GGGGa' 'false V (false V (false V (false V a)))'
-run 0 ./tunabbrev 'FFFfalse' 'true U ((true) U (true U (false)))'
+run 0 ../tunabbrev 'G a ' 'false R a'
+run 0 ../tunabbrev 'GF a => F G(b)' \
+                   '!(false R (true U a)) | (true U (false V b))'
+run 0 ../tunabbrev 'GGGGa' 'false V (false V (false V (false V a)))'
+run 0 ../tunabbrev 'FFFfalse' 'true U ((true) U (true U (false)))'
diff --git a/src/ltltest/tunenoform.test b/src/ltltest/tunenoform.test
index e301f24f7..411552ea3 100755
--- a/src/ltltest/tunenoform.test
+++ b/src/ltltest/tunenoform.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -27,10 +27,10 @@
 
 set -e
 
-run 0 ./tunenoform '!(a ^ b)' '(a|!b) & (!a|b)'
-run 0 ./tunenoform '!(a <=> b)' '(a|b) & (!a|!b)'
-run 0 ./tunenoform '!(a => b)' 'a&!b'
-run 0 ./tunenoform '!(!a => !b)' '!a&b'
-run 0 ./tunenoform '!Fa' 'false R !a'
-run 0 ./tunenoform '!G!a' 'true U a'
-run 0 ./tunenoform '!(GF a => FG b)' '(0 R (1 U a)) & (0 R (1 U !b))'
+run 0 ../tunenoform '!(a ^ b)' '(a|!b) & (!a|b)'
+run 0 ../tunenoform '!(a <=> b)' '(a|b) & (!a|!b)'
+run 0 ../tunenoform '!(a => b)' 'a&!b'
+run 0 ../tunenoform '!(!a => !b)' '!a&b'
+run 0 ../tunenoform '!Fa' 'false R !a'
+run 0 ../tunenoform '!G!a' 'true U a'
+run 0 ../tunenoform '!(GF a => FG b)' '(0 R (1 U a)) & (0 R (1 U !b))'
diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am
index 692bed88a..79e473f04 100644
--- a/src/tgbatest/Makefile.am
+++ b/src/tgbatest/Makefile.am
@@ -95,16 +95,5 @@ TESTS = \
 
 EXTRA_DIST = $(TESTS)
 
-CLEANFILES = \
-  blue_counter \
-  blue_last \
-  config \
-  expected \
-  input \
-  input1 \
-  input2 \
-  input3 \
-  output1 \
-  output2 \
-  red \
-  stdout
+distclean-local:
+	rm -rf $(TESTS:.test=.dir)
diff --git a/src/tgbatest/bddprod.test b/src/tgbatest/bddprod.test
index f357891a8..56fa99e78 100755
--- a/src/tgbatest/bddprod.test
+++ b/src/tgbatest/bddprod.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  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.
 
-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'
+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/complementation.test b/src/tgbatest/complementation.test
index 5b5c31444..355448e13 100755
--- a/src/tgbatest/complementation.test
+++ b/src/tgbatest/complementation.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # Copyright (C) 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
-# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
 # This file is part of Spot, a model checking library.
@@ -25,7 +25,7 @@
 set -e
 
 while read f; do
-    run 0 ./complement -f "$f"
+    run 0 ../complement -f "$f"
 done <<EOF
 GFa
 FGa
diff --git a/src/tgbatest/defs.in b/src/tgbatest/defs.in
index b809e9e3e..2179e38a7 100644
--- a/src/tgbatest/defs.in
+++ b/src/tgbatest/defs.in
@@ -1,5 +1,5 @@
 # -*- shell-script -*-
-# Copyright (C) 2003, 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2006, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -26,9 +26,8 @@ test -f ./defs || {
    exit 1
 }
 
-# If srcdir is not set, then we are not running from `make check', be verbose.
+# If srcdir is not set, then we are not running from `make check'.
 if test -z "$srcdir"; then
-   test -z "$VERBOSE" && VERBOSE=x
    # compute $srcdir.
    srcdir=`echo "$0" | sed -e 's,/[^\\/]*$,,'`
    test $srcdir = $0 && srcdir=.
@@ -40,11 +39,16 @@ test -f $srcdir/defs.in || {
    exit 1
 }
 
-# User can set VERBOSE to see all output.
-test -z "$VERBOSE" && exec >/dev/null 2>&1
-
 echo "== Running test $0"
 
+me=`echo "$0" | sed -e 's,.*[\\/],,;s/\.test$//'`
+
+testSubDir=$me.dir
+chmod -R a+rwx $testSubDir > /dev/null 2>&1
+rm -rf $testSubDir > /dev/null 2>&1
+mkdir $testSubDir
+cd $testSubDir
+
 DOT='@DOT@'
 top_builddir='@top_builddir@'
 LBTT="@LBTT@"
@@ -71,9 +75,4 @@ run()
   test $exitcode = $expected_exitcode || exit 1
 }
 
-# Turn on shell traces when VERBOSE=x.
-if test "x$VERBOSE" = xx; then
-  set -x
-else
-  :
-fi
+set -x
diff --git a/src/tgbatest/dfs.test b/src/tgbatest/dfs.test
index d76a0b522..7953b0ed4 100755
--- a/src/tgbatest/dfs.test
+++ b/src/tgbatest/dfs.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2005, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -77,8 +77,8 @@ s9, s8,,;
 s9, s9,,;
 EOF
 
-run 0 ./ltl2tgba -eSE05 -X blue_counter
-run 0 ./ltl2tgba -eTau03_opt -X blue_counter
+run 0 ../ltl2tgba -eSE05 -X blue_counter
+run 0 ../ltl2tgba -eTau03_opt -X blue_counter
 
 # s1->s2->s3->(large composant from s4 to s9)
 # ^       ||
@@ -129,8 +129,8 @@ s9, s8,,;
 s9, s9,,;
 EOF
 
-run 0 ./ltl2tgba -eSE05 -X blue_last
-run 0 ./ltl2tgba -eTau03_opt -X blue_last
+run 0 ../ltl2tgba -eSE05 -X blue_last
+run 0 ../ltl2tgba -eTau03_opt -X blue_last
 
 #  _______
 # |       |
@@ -185,7 +185,7 @@ s9, s8,,;
 s9, s9,,;
 EOF
 
-run 0 ./ltl2tgba -eSE05 -X red
-run 0 ./ltl2tgba -eTau03_opt -X red
+run 0 ../ltl2tgba -eSE05 -X red
+run 0 ../ltl2tgba -eTau03_opt -X red
 
 rm -f red blue_counter blue_last
diff --git a/src/tgbatest/dupexp.test b/src/tgbatest/dupexp.test
index 54b8389df..de5ddc576 100755
--- a/src/tgbatest/dupexp.test
+++ b/src/tgbatest/dupexp.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -27,12 +27,12 @@ set -e
 
 dorun()
 {
-  run 0 ./ltl2tgba -f -s "$1" >output1
-  run 0 ./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`
 
-  run 0 ./ltl2tgba -s "$1" >output1
-  run 0 ./ltl2tgba -S "$1" >output2
+  run 0 ../ltl2tgba -s "$1" >output1
+  run 0 ../ltl2tgba -S "$1" >output2
   test `wc -l <output1` = `wc -l <output2`
 }
 
diff --git a/src/tgbatest/eltl2tgba.test b/src/tgbatest/eltl2tgba.test
index d1d0b71e9..ddf845942 100755
--- a/src/tgbatest/eltl2tgba.test
+++ b/src/tgbatest/eltl2tgba.test
@@ -6,7 +6,7 @@ set -e
 # Check if the TGBA was corretly constructed.
 check_construct()
 {
-  run 0 ./eltl2tgba -F "$1" input
+  run 0 ../eltl2tgba -F "$1" input
 }
 
 # Check if the TGBA behaves correctly by doing an emptiness check on
@@ -14,11 +14,11 @@ check_construct()
 # translated using FM.
 check_true()
 {
-  run 0 ./ltl2tgba -e -Pinput -f "$1"
+  run 0 ../ltl2tgba -e -Pinput -f "$1"
 }
 check_false()
 {
-  run 1 ./ltl2tgba -e -Pinput -f "$1"
+  run 1 ../ltl2tgba -e -Pinput -f "$1"
 }
 
 # Create the prelude file.
diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test
index 993905c3d..270e05a0e 100755
--- a/src/tgbatest/emptchk.test
+++ b/src/tgbatest/emptchk.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004, 2005, 2008 Laboratoire d'Informatique de
+# Copyright (C) 2003, 2004, 2005, 2008, 2009 Laboratoire d'Informatique de
 # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 # Université Pierre et Marie Curie.
 #
@@ -27,8 +27,8 @@ set -e
 
 expect_ce_do()
 {
-  run 0 ./ltl2tgba "$@"
-  run 0 ./ltl2tgba -g "$@"
+  run 0 ../ltl2tgba "$@"
+  run 0 ../ltl2tgba -g "$@"
 }
 
 expect_ce()
@@ -43,42 +43,42 @@ expect_ce()
   expect_ce_do -e'Cou99(shy)' -f -D "$1"
   expect_ce_do -eCVWY90 "$1"
   expect_ce_do -eCVWY90 -f "$1"
-  run 0 ./ltl2tgba -e'CVWY90(bsh=10M)' "$1"
-  run 0 ./ltl2tgba -e'CVWY90(bsh=10M)' -f "$1"
-  run 0 ./ltl2tgba -eSE05 "$1"
-  run 0 ./ltl2tgba -eSE05 -f "$1"
-  run 0 ./ltl2tgba -e'SE05(bsh=10M)' "$1"
-  run 0 ./ltl2tgba -e'SE05(bsh=10M)' -f "$1"
-  run 0 ./ltl2tgba -eTau03_opt -f "$1"
-  run 0 ./ltl2tgba -eGV04 -f "$1"
+  run 0 ../ltl2tgba -e'CVWY90(bsh=10M)' "$1"
+  run 0 ../ltl2tgba -e'CVWY90(bsh=10M)' -f "$1"
+  run 0 ../ltl2tgba -eSE05 "$1"
+  run 0 ../ltl2tgba -eSE05 -f "$1"
+  run 0 ../ltl2tgba -e'SE05(bsh=10M)' "$1"
+  run 0 ../ltl2tgba -e'SE05(bsh=10M)' -f "$1"
+  run 0 ../ltl2tgba -eTau03_opt -f "$1"
+  run 0 ../ltl2tgba -eGV04 -f "$1"
   # Expect multiple accepting runs
-  test `./ltl2tgba -e'CVWY90(repeated)' "$1" | grep Prefix: | wc -l` -ge $2
-  test `./ltl2tgba -e'SE05(repeated)' "$1" | grep Prefix: | wc -l` -ge $2
+  test `../ltl2tgba -e'CVWY90(repeated)' "$1" | grep Prefix: | wc -l` -ge $2
+  test `../ltl2tgba -e'SE05(repeated)' "$1" | grep Prefix: | wc -l` -ge $2
 }
 
 expect_no()
 {
-  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 -E'Cou99(shy)' "$1"
-  run 0 ./ltl2tgba -E'Cou99(shy)' -D "$1"
-  run 0 ./ltl2tgba -E'Cou99(shy)' -f "$1"
-  run 0 ./ltl2tgba -E'Cou99(shy)' -f -D "$1"
-  run 0 ./ltl2tgba -ECVWY90 "$1"
-  run 0 ./ltl2tgba -ECVWY90 -f "$1"
-  run 0 ./ltl2tgba -E'CVWY90(bsh=10M)' "$1"
-  run 0 ./ltl2tgba -E'CVWY90(bsh=10M)' -f "$1"
-  run 0 ./ltl2tgba -ESE05 "$1"
-  run 0 ./ltl2tgba -ESE05 -f "$1"
-  run 0 ./ltl2tgba -E'SE05(bsh=10M)' "$1"
-  run 0 ./ltl2tgba -E'SE05(bsh=10M)' -f "$1"
-  run 0 ./ltl2tgba -ETau03_opt -f "$1"
-  run 0 ./ltl2tgba -EGV04 -f "$1"
-  test `./ltl2tgba -e'CVWY90(repeated)' "!($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 -E'Cou99(shy)' "$1"
+  run 0 ../ltl2tgba -E'Cou99(shy)' -D "$1"
+  run 0 ../ltl2tgba -E'Cou99(shy)' -f "$1"
+  run 0 ../ltl2tgba -E'Cou99(shy)' -f -D "$1"
+  run 0 ../ltl2tgba -ECVWY90 "$1"
+  run 0 ../ltl2tgba -ECVWY90 -f "$1"
+  run 0 ../ltl2tgba -E'CVWY90(bsh=10M)' "$1"
+  run 0 ../ltl2tgba -E'CVWY90(bsh=10M)' -f "$1"
+  run 0 ../ltl2tgba -ESE05 "$1"
+  run 0 ../ltl2tgba -ESE05 -f "$1"
+  run 0 ../ltl2tgba -E'SE05(bsh=10M)' "$1"
+  run 0 ../ltl2tgba -E'SE05(bsh=10M)' -f "$1"
+  run 0 ../ltl2tgba -ETau03_opt -f "$1"
+  run 0 ../ltl2tgba -EGV04 -f "$1"
+  test `../ltl2tgba -e'CVWY90(repeated)' "!($1)" |
         grep Prefix: | wc -l` -ge $2
-  test `./ltl2tgba -e'SE05(repeated)' "!($1)" |
+  test `../ltl2tgba -e'SE05(repeated)' "!($1)" |
         grep Prefix: | wc -l` -ge $2
 }
 
diff --git a/src/tgbatest/emptchke.test b/src/tgbatest/emptchke.test
index d4858a2a2..e2902ec82 100755
--- a/src/tgbatest/emptchke.test
+++ b/src/tgbatest/emptchke.test
@@ -1,7 +1,7 @@
 #!/bin/sh
-# 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.
+# Copyright (C) 2003, 2004, 2005, 2009 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.
 #
@@ -27,11 +27,11 @@ set -e
 
 expect_ce()
 {
-  run 0 ./ltl2tgba -e -X "$1"
-  run 0 ./ltl2tgba -e -D -X "$1"
-  run 0 ./ltl2tgba -e'Cou99(shy)' -X "$1"
-  run 0 ./ltl2tgba -e'Cou99(shy)' -D -X "$1"
-  run 0 ./ltl2tgba -eCVWY90 -X "$1"
+  run 0 ../ltl2tgba -e -X "$1"
+  run 0 ../ltl2tgba -e -D -X "$1"
+  run 0 ../ltl2tgba -e'Cou99(shy)' -X "$1"
+  run 0 ../ltl2tgba -e'Cou99(shy)' -D -X "$1"
+  run 0 ../ltl2tgba -eCVWY90 -X "$1"
 }
 
 cat >input <<'EOF'
diff --git a/src/tgbatest/emptchkr.test b/src/tgbatest/emptchkr.test
index 2997c50b3..0fb982622 100755
--- a/src/tgbatest/emptchkr.test
+++ b/src/tgbatest/emptchkr.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -28,24 +28,24 @@ set -e
 
 # With no acceptance condition, everyone should agree and find a run.
 # Do not spend to much time checking this.
-run 0 ./randtgba -e 10 -s 0 -r -m
+run 0 ../randtgba -e 10 -s 0 -r -m
 
 # One acceptance condition
-run 0 ./randtgba -e 100 -s   0 -r -m -a 1 0.1 -d 0.01
-run 0 ./randtgba -e 100 -s  50 -r -m -a 1 0.1 -d 0.02
-run 0 ./randtgba -e 100 -s 100 -r -m -a 1 0.1 -d 0.04
-run 0 ./randtgba -e 100 -s 150 -r -m -a 1 0.1 -d 0.08
+run 0 ../randtgba -e 100 -s   0 -r -m -a 1 0.1 -d 0.01
+run 0 ../randtgba -e 100 -s  50 -r -m -a 1 0.1 -d 0.02
+run 0 ../randtgba -e 100 -s 100 -r -m -a 1 0.1 -d 0.04
+run 0 ../randtgba -e 100 -s 150 -r -m -a 1 0.1 -d 0.08
 
 # Four acceptance conditions
-run 0 ./randtgba -e 100 -s 200 -r -m -a 4 0.1 -d 0.01
-run 0 ./randtgba -e 100 -s 250 -r -m -a 4 0.1 -d 0.02
-run 0 ./randtgba -e 100 -s 300 -r -m -a 4 0.1 -d 0.04
-run 0 ./randtgba -e 100 -s 350 -r -m -a 4 0.1 -d 0.08
-run 0 ./randtgba -e 100 -s 400 -r -m -a 4 0.2 -d 0.01
-run 0 ./randtgba -e 100 -s 450 -r -m -a 4 0.2 -d 0.02
-run 0 ./randtgba -e 100 -s 500 -r -m -a 4 0.2 -d 0.04
-run 0 ./randtgba -e 100 -s 550 -r -m -a 4 0.2 -d 0.08
+run 0 ../randtgba -e 100 -s 200 -r -m -a 4 0.1 -d 0.01
+run 0 ../randtgba -e 100 -s 250 -r -m -a 4 0.1 -d 0.02
+run 0 ../randtgba -e 100 -s 300 -r -m -a 4 0.1 -d 0.04
+run 0 ../randtgba -e 100 -s 350 -r -m -a 4 0.1 -d 0.08
+run 0 ../randtgba -e 100 -s 400 -r -m -a 4 0.2 -d 0.01
+run 0 ../randtgba -e 100 -s 450 -r -m -a 4 0.2 -d 0.02
+run 0 ../randtgba -e 100 -s 500 -r -m -a 4 0.2 -d 0.04
+run 0 ../randtgba -e 100 -s 550 -r -m -a 4 0.2 -d 0.08
 
 # Bigger automata.  With valgrind this is slow, so we do less.
-run 0 ./randtgba -e 10 -s 0 -n 500 -r -m -a 1 0.0003 -d 0.01
-run 0 ./randtgba -e 10 -s 0 -n 500 -r -m -a 4 0.0011 -D -d 0.01
+run 0 ../randtgba -e 10 -s 0 -n 500 -r -m -a 1 0.0003 -d 0.01
+run 0 ../randtgba -e 10 -s 0 -n 500 -r -m -a 4 0.0011 -D -d 0.01
diff --git a/src/tgbatest/explicit.test b/src/tgbatest/explicit.test
index 6510e43cd..95e081b8e 100755
--- a/src/tgbatest/explicit.test
+++ b/src/tgbatest/explicit.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004, 2005, 2008 Laboratoire d'Informatique de
+# Copyright (C) 2003, 2004, 2005, 2008, 2009 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
 
-run 0 ./explicit | sed 's/c & b/b \& c/' > stdout
+run 0 ../explicit | sed 's/c & b/b \& c/' > stdout
 
 cat >expected <<EOF
 digraph G {
diff --git a/src/tgbatest/explpro2.test b/src/tgbatest/explpro2.test
index f527984bb..329110d4b 100755
--- a/src/tgbatest/explpro2.test
+++ b/src/tgbatest/explpro2.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004, 2005, 2006, 2008 Laboratoire
+# Copyright (C) 2003, 2004, 2005, 2006, 2008, 2009 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 = "p2$1" "p3" "p2" "p1";
 "s1 * s1", "s3 * s3", "a & !b", "p3" "p2";
 EOF
 
-run 0 ./explprod input1 input2 |
+run 0 ../explprod input1 input2 |
   sed 's/!a & b/b \& !a/;s/!b & a/a \& !b/'> stdout
 
 cat stdout
diff --git a/src/tgbatest/explpro3.test b/src/tgbatest/explpro3.test
index de490ce45..f14a7cfbd 100755
--- a/src/tgbatest/explpro3.test
+++ b/src/tgbatest/explpro3.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  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 = "p2" "p3";
 "s1 * s1", "s3 * s3", "a & !b", "p3";
 EOF
 
-run 0 ./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.)
diff --git a/src/tgbatest/explpro4.test b/src/tgbatest/explpro4.test
index c10bcec67..72bdb7ff9 100755
--- a/src/tgbatest/explpro4.test
+++ b/src/tgbatest/explpro4.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2006, 2009  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$1" "p1";
 "s1 * s1", "s1 * s1", "!a", "p1$1";
 EOF
 
-run 0 ./explprod input1 input2 > stdout
+run 0 ../explprod input1 input2 > stdout
 cat stdout
 diff stdout expected
 rm input1 input2 stdout expected
diff --git a/src/tgbatest/explprod.test b/src/tgbatest/explprod.test
index 062ede06b..24db2115e 100755
--- a/src/tgbatest/explprod.test
+++ b/src/tgbatest/explprod.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004, 2005, 2008 Laboratoire d'Informatique de
+# Copyright (C) 2003, 2004, 2005, 2008, 2009 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 = "p3" "p2" "p1";
 "s2 * s2", "s3 * s1", "a & c", "p3" "p1";
 EOF
 
-run 0 ./explprod input1 input2 |
+run 0 ../explprod input1 input2 |
   sed 's/b & a/a \& b/;s/c & a/a \& c/' > stdout
 
 cat stdout
diff --git a/src/tgbatest/ltl2neverclaim.test b/src/tgbatest/ltl2neverclaim.test
index 0ab3766d4..2f8a054c2 100755
--- a/src/tgbatest/ltl2neverclaim.test
+++ b/src/tgbatest/ltl2neverclaim.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -28,14 +28,14 @@ set -e
 # We don't check the output, but just running these might be enough to
 # trigger assertions.
 
-run 0 ./ltl2tgba -N -x a
-run 0 ./ltl2tgba -N -x  'a U b'
-run 0 ./ltl2tgba -N -x 'X a'
-run 0 ./ltl2tgba -N -x 'a & b & c'
-run 0 ./ltl2tgba -N -x 'a | b | (c U (d & (g U (h ^ i))))'
-run 0 ./ltl2tgba -N -x 'Xa & (b U !a) & (b U !a)'
-run 0 ./ltl2tgba -N -x 'Fa & Xb & GFc & Gd'
-run 0 ./ltl2tgba -N -x 'Fa & Xa & GFc & Gc'
-run 0 ./ltl2tgba -N -x 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
-run 0 ./ltl2tgba -N -x 'a R (b R c)'
-run 0 ./ltl2tgba -N -x '(a U b) U (c U d)'
+run 0 ../ltl2tgba -N -x a
+run 0 ../ltl2tgba -N -x  'a U b'
+run 0 ../ltl2tgba -N -x 'X a'
+run 0 ../ltl2tgba -N -x 'a & b & c'
+run 0 ../ltl2tgba -N -x 'a | b | (c U (d & (g U (h ^ i))))'
+run 0 ../ltl2tgba -N -x 'Xa & (b U !a) & (b U !a)'
+run 0 ../ltl2tgba -N -x 'Fa & Xb & GFc & Gd'
+run 0 ../ltl2tgba -N -x 'Fa & Xa & GFc & Gc'
+run 0 ../ltl2tgba -N -x 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
+run 0 ../ltl2tgba -N -x 'a R (b R c)'
+run 0 ../ltl2tgba -N -x '(a U b) U (c U d)'
diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test
index c1321d2e4..400ce1a73 100755
--- a/src/tgbatest/ltl2tgba.test
+++ b/src/tgbatest/ltl2tgba.test
@@ -27,9 +27,9 @@ set -e
 
 check ()
 {
-  run 0 ./ltl2tgba "$1"
-  run 0 ./ltl2tgba -f "$1"
-  run 0 ./ltl2tgba -f -FC "$1"
+  run 0 ../ltl2tgba "$1"
+  run 0 ../ltl2tgba -f "$1"
+  run 0 ../ltl2tgba -f -FC "$1"
 }
 
 # We don't check the output, but just running these might be enough to
diff --git a/src/tgbatest/ltlprod.test b/src/tgbatest/ltlprod.test
index 16a258ca8..d2ace8127 100755
--- a/src/tgbatest/ltlprod.test
+++ b/src/tgbatest/ltlprod.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  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.
 
-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'
+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 7e3f2155d..4e55ebad0 100755
--- a/src/tgbatest/mixprod.test
+++ b/src/tgbatest/mixprod.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  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
 
-run 0 ./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
 
-run 0 ./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 71ebc597b..8f9dc1994 100755
--- a/src/tgbatest/readsave.test
+++ b/src/tgbatest/readsave.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  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
 
-./readsave input > stdout
+../readsave input > stdout
 
 cat >expected <<\EOF
 acc = "c" "d";
@@ -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
-run 0 ./readsave input > stdout
+run 0 ../readsave input > stdout
 
 # Sort out some possible inversions in the output.
 # (The order is not guaranteed by SPOT.)
@@ -60,11 +60,11 @@ rm -f input stdout expected
 
 
 # Likewise, with a randomly generated TGBA.
-run 0 ./randtgba -t 1 -n 20 -d 0.2 a b -a 2 0.1 >input
+run 0 ../randtgba -t 1 -n 20 -d 0.2 a b -a 2 0.1 >input
 sed 's/"b & a"/"a \& b"/g;s/"a1" "a0"/"a0" "a1"/g' input > tmp_ &&
   mv tmp_ input
 cat input
-run 0 ./readsave input > stdout
+run 0 ../readsave input > stdout
 sed 's/"b & a"/"a \& b"/g;s/"a1" "a0"/"a0" "a1"/g' stdout > tmp_ &&
   mv tmp_ stdout
 
diff --git a/src/tgbatest/reduccmp.test b/src/tgbatest/reduccmp.test
index faa8f9495..f1d780e98 100755
--- a/src/tgbatest/reduccmp.test
+++ b/src/tgbatest/reduccmp.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -35,8 +35,8 @@ s1, "s2", "a", c;
 "3", s2, "a",;
 EOF
 
-run 0 ./reduccmp 0 input
-run 0 ./reduccmp 0 input > stdout
+run 0 ../reduccmp 0 input
+run 0 ../reduccmp 0 input > stdout
 
 cat >expected <<EOF
 digraph G {
@@ -54,4 +54,4 @@ sed 's/!b & a/a \& !b/g' stdout > tmp_ && mv tmp_ stdout
 diff stdout expected
 
 # FIXME
-exit 0
\ No newline at end of file
+exit 0
diff --git a/src/tgbatest/reductgba.test b/src/tgbatest/reductgba.test
index cfbb18ac2..62080c5d5 100755
--- a/src/tgbatest/reductgba.test
+++ b/src/tgbatest/reductgba.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -27,8 +27,8 @@ set -e
 
 check()
 {
-  #run 0 ./reductgba "$1" "$2"
-  ./reductgba "$1" "$2"
+  #run 0 ../reductgba "$1" "$2"
+  ../reductgba "$1" "$2"
 }
 
 # We don't check the output, but just running these might be enough to
diff --git a/src/tgbatest/scc.test b/src/tgbatest/scc.test
index 8fb9f30bc..0fcda6007 100755
--- a/src/tgbatest/scc.test
+++ b/src/tgbatest/scc.test
@@ -24,7 +24,7 @@
 set -e
 
 
-run 0 ./ltl2tgba -f -k '(a U c) U b & (b U c)' >stdout
+run 0 ../ltl2tgba -f -k '(a U c) U b & (b U c)' >stdout
 cat >expected <<EOF
 transitions: 15
 states: 6
@@ -37,7 +37,7 @@ EOF
 diff stdout expected
 
 
-run 0 ./ltl2tgba -f -k '(b U a) | (GFa & XG!a)' >stdout
+run 0 ../ltl2tgba -f -k '(b U a) | (GFa & XG!a)' >stdout
 cat >expected <<EOF
 transitions: 7
 states: 4
diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test
index 01238298d..74b61c4b7 100755
--- a/src/tgbatest/spotlbtt.test
+++ b/src/tgbatest/spotlbtt.test
@@ -1,7 +1,7 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de
-# Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-# Université Pierre et Marie Curie.
+# Copyright (C) 2003, 2004, 2005, 2006, 2007, 2009 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.
 #
@@ -32,7 +32,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- LaCIM)"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -F -t'"
+   Parameters = "--spot '../ltl2tgba -F -t'"
    Enabled = yes
 }
 
@@ -40,7 +40,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- LaCIM), reduction of formula"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -r4 -F -t'"
+   Parameters = "--spot '../ltl2tgba -r4 -F -t'"
    Enabled = yes
 }
 
@@ -48,7 +48,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- LaCIM), degeneralized"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -F -t -D'"
+   Parameters = "--spot '../ltl2tgba -F -t -D'"
    Enabled = yes
 }
 
@@ -56,7 +56,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- LaCIM), fake"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -F -T'"
+   Parameters = "--spot '../ltl2tgba -F -T'"
    Enabled = no
 }
 
@@ -64,7 +64,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- LaCIM), eltl"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './eltl2tgba -L'"
+   Parameters = "--spot '../eltl2tgba -L'"
    Enabled = yes
 }
 
@@ -72,7 +72,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM)"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -F -f -t'"
+   Parameters = "--spot '../ltl2tgba -F -f -t'"
    Enabled = yes
 }
 
@@ -80,7 +80,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), basic reduction of formula"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -r1 -F -f -t'"
+   Parameters = "--spot '../ltl2tgba -r1 -F -f -t'"
    Enabled = no
 }
 
@@ -88,7 +88,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), reduction of formula using class of formula"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -r2 -F -f -t'"
+   Parameters = "--spot '../ltl2tgba -r2 -F -f -t'"
    Enabled = no
 }
 
@@ -96,7 +96,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), reduction of formula using implies relation"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -r3 -F -f -t'"
+   Parameters = "--spot '../ltl2tgba -r3 -F -f -t'"
    Enabled = no
 }
 
@@ -104,7 +104,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), reduction of formula (pre reduction)"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -r4 -F -f -t'"
+   Parameters = "--spot '../ltl2tgba -r4 -F -f -t'"
    Enabled = yes
 }
 
@@ -112,7 +112,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), reduction7 of formula (pre reduction)"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -r7 -F -f -t'"
+   Parameters = "--spot '../ltl2tgba -r7 -F -f -t'"
    Enabled = yes
 }
 
@@ -120,7 +120,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), reduction of formula in FM"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -fr4 -F -f -t'"
+   Parameters = "--spot '../ltl2tgba -fr4 -F -f -t'"
    Enabled = no
 }
 
@@ -128,7 +128,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM) reduction7 of formula in FM"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -fr7 -F -f -t'"
+   Parameters = "--spot '../ltl2tgba -fr7 -F -f -t'"
    Enabled = no
 }
 
@@ -138,7 +138,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), post reduction with direct simulation"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -R1q -R1t -F -f -t'"
+   Parameters = "--spot '../ltl2tgba -R1q -R1t -F -f -t'"
    Enabled = yes
 }
 
@@ -146,7 +146,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), post reduction with delayed simulation"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -R2q -R2t -F -f -t'"
+   Parameters = "--spot '../ltl2tgba -R2q -R2t -F -f -t'"
    Enabled = yes
 }
 
@@ -154,7 +154,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), post reduction with scc"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -R3 -F -f -t'"
+   Parameters = "--spot '../ltl2tgba -R3 -F -f -t'"
    Enabled = yes
 }
 
@@ -162,7 +162,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), pre + post reduction"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -r4 -R1q -R1t -R3 -F -f -t'"
+   Parameters = "--spot '../ltl2tgba -r4 -R1q -R1t -R3 -F -f -t'"
    Enabled = yes
 }
 
@@ -170,7 +170,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), pre + allpost reduction"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -r4 -R1q -R1t -R2q -R2t -R3 -F -f -t'"
+   Parameters = "--spot '../ltl2tgba -r4 -R1q -R1t -R2q -R2t -R3 -F -f -t'"
    Enabled = no
 }
 
@@ -178,7 +178,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), without symb_merge"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -F -f -y -t'"
+   Parameters = "--spot '../ltl2tgba -F -f -y -t'"
    Enabled = yes
 }
 
@@ -186,7 +186,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), degeneralized"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -F -f -t -D'"
+   Parameters = "--spot '../ltl2tgba -F -f -t -D'"
    Enabled = yes
 }
 
@@ -194,7 +194,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), degeneralized, via never claim"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spin './ltl2tgba -F -f -N'"
+   Parameters = "--spin '../ltl2tgba -F -f -N'"
    Enabled = yes
 }
 
@@ -202,7 +202,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM exprop)"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -F -f -x -t'"
+   Parameters = "--spot '../ltl2tgba -F -f -x -t'"
    Enabled = yes
 }
 
@@ -210,7 +210,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM exprop), without symb_merge"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -F -f -x -y -t'"
+   Parameters = "--spot '../ltl2tgba -F -f -x -y -t'"
    Enabled = yes
 }
 
@@ -218,7 +218,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM exprop), degeneralized"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -F -f -x -t -D'"
+   Parameters = "--spot '../ltl2tgba -F -f -x -t -D'"
    Enabled = yes
 }
 
@@ -226,7 +226,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM post_branch + exprop)"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -F -f -x -p -t'"
+   Parameters = "--spot '../ltl2tgba -F -f -x -p -t'"
    Enabled = yes
 }
 
@@ -234,7 +234,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM post_branch + exprop + flapprox)"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -F -f -x -p -L -t'"
+   Parameters = "--spot '../ltl2tgba -F -f -x -p -L -t'"
    Enabled = yes
 }
 
@@ -242,7 +242,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM post_branch + exprop), degeneralized"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -F -f -p -x -t -D'"
+   Parameters = "--spot '../ltl2tgba -F -f -p -x -t -D'"
    Enabled = yes
 }
 
@@ -250,7 +250,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM post_branch + exprop + flapprox), degeneralized"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -F -f -p -x -t -L -D'"
+   Parameters = "--spot '../ltl2tgba -F -f -p -x -t -L -D'"
    Enabled = yes
 }
 
diff --git a/src/tgbatest/tgbaread.test b/src/tgbatest/tgbaread.test
index 509ad29d0..4fadd69a1 100755
--- a/src/tgbatest/tgbaread.test
+++ b/src/tgbatest/tgbaread.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2003, 2004, 2009  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
 
-run 0 ./tgbaread input > stdout
+run 0 ../tgbaread input > stdout
 
 cat >expected <<EOF
 digraph G {
diff --git a/src/tgbatest/tripprod.test b/src/tgbatest/tripprod.test
index d297567e8..ba8ccd03f 100755
--- a/src/tgbatest/tripprod.test
+++ b/src/tgbatest/tripprod.test
@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2003, 2004, 2005, 2008 Laboratoire d'Informatique de
+# Copyright (C) 2003, 2004, 2005, 2008, 2009 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 = "p4" "p3" "p2" "p1";
 "s2 * s2 * s3", "s3 * s1 * s2", "a & c", "p4" "p3";
 EOF
 
-run 0 ./tripprod input1 input2 input3 |
+run 0 ../tripprod input1 input2 input3 |
   sed 's/b & a/a \& b/;s/c & a/a \& c/'> stdout
 
 cat stdout