diff --git a/ChangeLog b/ChangeLog
index 22de19bce..c51fdb5e1 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,15 @@
+2005-04-15  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* bench/ltl2tgba/Makefile.am, bench/ltl2tgba/README,
+	bench/ltl2tgba/algorithms, bench/ltl2tgba/big,
+	bench/ltl2tgba/defs.in, bench/ltl2tgba/formulae.ltl,
+	bench/ltl2tgba/known, bench/ltl2tgba/parseout.pl,
+	bench/ltl2tgba/small: New files.
+	* src/tgbatest/ltl2baw.pl: Move ...
+	* bench/ltl2tgba/ltl2baw.in: ... here.
+	* src/tgbatest/Makefile.am: Adjust.
+	* configure.ac: Adjust.
+
 2005-04-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/tgbatest/ltl2tgba.cc (main): Delete the reduced automaton
diff --git a/bench/ltl2tgba/.cvsignore b/bench/ltl2tgba/.cvsignore
new file mode 100644
index 000000000..56a141e28
--- /dev/null
+++ b/bench/ltl2tgba/.cvsignore
@@ -0,0 +1,7 @@
+Makefile.in
+Makefile
+*.cfg
+*.txt
+*.log
+defs
+ltl2baw.pl
diff --git a/bench/ltl2tgba/Makefile.am b/bench/ltl2tgba/Makefile.am
new file mode 100644
index 000000000..d1aaefb74
--- /dev/null
+++ b/bench/ltl2tgba/Makefile.am
@@ -0,0 +1,11 @@
+EXTRA_DIST = \
+  algorithms \
+  big \
+  formulae.ltl \
+  known \
+  parseout.pl \
+  small
+CLEAN_FILES = \
+  big.cfg big.log big.txt \
+  small.cfg small.log small.txt \
+  known.cfg known.log known.txt
diff --git a/bench/ltl2tgba/README b/bench/ltl2tgba/README
new file mode 100644
index 000000000..9d672ac42
--- /dev/null
+++ b/bench/ltl2tgba/README
@@ -0,0 +1,94 @@
+This directory contains benchmark scripts for LTL-to-Büchi translators.
+They are all based on lbtt.
+
+==========
+ CONTENTS
+==========
+
+* algorithms
+
+  The lbtt configuration of all the algorithms.  More about these below.
+
+* small
+* big
+* known
+
+  Run lbtt on, respectively:
+    small formulae (size 10, 4 propositions)
+    big formulae (size 12..15, 8 propositions)
+    known formulae (96 formulae from formulae.ltl)
+
+  Each script generates 3 files:
+    xxxx.cfg: the configuration file for lbtt
+    xxxx.log: the log of lbtt's execution (also output when the script runs)
+    xxxx.txt: the sumary of the test (also output at the end of the script)
+
+* ltl2baw.in
+* ltl2baw.pl
+
+  ltl2baw.pl is generated from ltl2baw.in by configure.  This perl
+  script converts the intermediate generalized automata computed by
+  ltl2ba into a form usable by lbtt.
+
+* formulae.ltl
+
+  A list of LTL formulae used by the `known' check.
+  See ../emptchk/README for the sources.
+
+* parseout.pl
+
+  This scripts is used to create *.txt files from *.log files.
+
+
+====================
+ ALGORITHMS & TOOLS
+====================
+
+The page http://spot.lip6.fr/wiki/LtlTranslationBenchmark explains
+all the keys used and the different tools involved in the benchmark.
+
+Spot's configure script checks for the tools needed in the
+benchmark, and the script in this directory should omit the tools
+that are not available.
+
+
+=======================
+ Reading the summaries
+=======================
+
+The files small.txt, big.txt, and known.txt contain a summary of the
+results.  Each algorithm is described as two lines formated as
+follows.
+
+   18: FM, gen, +symb_merge, -exprop, LTLopt
+            494 /    975 /  100 /      4.25       98798 /   3935920   (100)
+
+The first line presents the name of the algorithm ("FM, gen,
++symb_merge, -exprop, LTLopt") and its number for lbtt (18).
+The number is useless.  See http://spot.lip6.fr/wiki/LtlTranslationBenchmark
+for the naming conventions.
+
+The second line display 7 values:
+  1. the total number of states of all generated automata (494)
+  2. the total number of transitions of all generated automata (975)
+  3. the total number of acceptance conditions of all generated automata (100)
+  4. the cumulated translation time in seconds (4.25)
+  5. the total number of states in the synchronized products (98798)
+  6. the total number of transitions in the synchronized products (3935920)
+  7. the number of translated automata (100)
+
+Notes:
+
+  * Small translation times are not accurate because most of the translators
+    are run through scripts that translate their input from and their ouput to
+    the format understood by lbtt.  For fast translators, most of the time
+    is spent through these wrappers.  (For instance Spot's ltl2tgba is
+    run through lbtt-translate, and depending on how Spot has been configured
+    w.r.t. to dynamic libraries, ltl2tgba itself is often a shell script that
+    run the real binary with the locally built libraries.)
+
+  * Some tools will appear to have translated fewer automata than the
+    others.  This normally indicates bugs in the translator.  In that
+    case it is harder to compare the results.  (Normalizing the other
+    values accordingly may not be fair: maybe the translator precisely
+    failed to translate the largest automata.)
diff --git a/bench/ltl2tgba/algorithms b/bench/ltl2tgba/algorithms
new file mode 100644
index 000000000..b6727683a
--- /dev/null
+++ b/bench/ltl2tgba/algorithms
@@ -0,0 +1,282 @@
+cat >"$conffile" <<EOF
+Algorithm
+{
+   Name = "LaCIM, degen"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -t -D -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "LaCIM, gen"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -t -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "LaCIM, degen, +pre"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -t -D -r4 -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "LaCIM, gen, +pre"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -t -r4 -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, degen, +symb_merge, +exprop, LTLopt"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$srcdir/ltl2baw.pl --spot=\"-f -t -x -D\" -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, degen, +symb_merge, +exprop, +pre"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -r4 -f -t -x -D -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, degen, +symb_merge, +exprop, +pre, +post"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -r4 -R1q -R1t -R3 -f -t -x -D -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, degen, +symb_merge, +exprop, +pre, +post, +flapprox"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -r4 -R1q -R1t -R3 -L -f -t -x -D -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, degen, +symb_merge, +exprop, +pre, +post, +flapprox, +post_branch"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -r4 -R1q -R1t -R3 -L -f -t -x -D -p -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, degen, +symb_merge, +exprop, +post_branch, LTLopt"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$srcdir/ltl2baw.pl --spot=\"-f -x -p -t -D\" -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, degen, +symb_merge, +exprop, +flapprox, LTLopt"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$srcdir/ltl2baw.pl --spot=\"-f -x -t -L -D\" -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, degen, +symb_merge, +exprop, +post_branch, +flapprox, LTLopt"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$srcdir/ltl2baw.pl --spot=\"-f -x -p -t -L -D\" -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, gen, -symb_merge, -exprop"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -F -f -y -t'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, gen, -symb_merge, +exprop"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -F -f -y -x -t'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, gen, +symb_merge, -exprop"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -F -f -t'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, gen, +symb_merge, +exprop"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -F -f -x -t'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, gen, -symb_merge, -exprop, LTLopt"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot './ltl2baw.pl --spot=\"-f -y -t\" -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, gen, -symb_merge, +exprop, LTLopt"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot './ltl2baw.pl --spot=\"-f -y -x -t\" -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, gen, +symb_merge, -exprop, LTLopt"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot './ltl2baw.pl --spot=\"-f -t\" -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, gen, +symb_merge, +exprop, LTLopt"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot './ltl2baw.pl --spot=\"-f -x -t\" -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, gen, +symb_merge, +exprop, +post_branch, LTLopt"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot './ltl2baw.pl --spot=\"-f -x -p -t\" -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, gen, +symb_merge, +exprop, +flapprox, LTLopt"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot './ltl2baw.pl --spot=\"-f -x -L -t\" -F'"
+   Enabled = yes
+}
+
+
+Algorithm
+{
+   Name = "FM, gen, +symb_merge, +exprop, +post_branch, +flapprox, LTLopt"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot './ltl2baw.pl --spot=\"-f -x -p -L -t\" -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, gen, +symb_merge, +exprop, +pre"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -r4 -f -t -x -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, gen, +symb_merge, +exprop, +pre, +post"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -r4 -R1q -R1t -R3 -f -t -x -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, gen, +symb_merge, +exprop, +pre, +post, +flapprox"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -r4 -R1q -R1t -R3 -L -f -t -x -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "FM, gen, +symb_merge, +exprop, +pre, +post, +flapprox, +post_branch"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -r4 -R1q -R1t -R3 -L -f -t -x  -p -F'"
+   Enabled = yes
+}
+
+
+Algorithm
+{
+   Name = "Spin"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spin $SPIN"
+   Enabled = $HAVE_SPIN
+}
+
+Algorithm
+{
+   Name = "LBT"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--lbt $LBT"
+   Enabled = $HAVE_LBT
+}
+
+Algorithm
+{
+   Name = "LTL2BA, degen"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spin $LTL2BA"
+   Enabled = $HAVE_LTL2BA
+}
+
+Algorithm
+{
+   Name = "LTL2BA, gen (unfair)"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot './ltl2baw.pl -F'"
+   Enabled = $HAVE_LTL2BA
+}
+
+Algorithm
+{
+   Name = "Wring (Wring RewRule+BoolOpt+AutSempl)"
+   Path = "$WRING2LBTT"
+   Parameters = "--5"
+   Enabled = $HAVE_WRING2LBTT
+}
+
+Algorithm
+{
+   Name = "Wring (Wring RewRule+BoolOpt+AutSempl), degen"
+   Path = "$WRING2LBTT"
+   Parameters = "-d --5"
+   Enabled = $HAVE_WRING2LBTT
+}
+
+Algorithm
+{
+   Name = "Modella -o1 -g -e -r12"
+   Path = "$MODELLA"
+   Parameters = "-o1 -g -e -r12"
+   Enabled = $HAVE_MODELLA
+}
+
+Algorithm
+{
+   Name = "NBA"
+   Path = "$LTL2NBA"
+   Enabled = $HAVE_LTL2NBA
+}
+EOF
diff --git a/bench/ltl2tgba/big b/bench/ltl2tgba/big
new file mode 100644
index 000000000..945f14259
--- /dev/null
+++ b/bench/ltl2tgba/big
@@ -0,0 +1,78 @@
+#!/bin/sh
+# -*- shell-script -*-
+# Copyright (C) 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# et Marie Curie.
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+. ./defs
+
+conffile=big.cfg
+logfile=big.log
+sumfile=big.txt
+
+. "$srcdir/algorithms"
+
+cat >>"$conffile" <<EOF
+GlobalOptions
+{
+   Rounds = 100
+   Interactive = Never
+#   Verbosity = 5
+#   ComparisonCheck = no
+   ConsistencyCheck = no
+#   IntersectionCheck = no
+}
+
+StateSpaceOptions
+{
+   Size = 200
+   Propositions = 8
+}
+
+FormulaOptions
+{
+  Size = 15...20
+  Propositions = 8
+
+  AbbreviatedOperators = No
+  GenerateMode = Normal
+  OutputMode = NNF
+  PropositionPriority = 50
+
+  TruePriority = 1
+  FalsePriority = 1
+
+  AndPriority = 10
+  OrPriority = 10
+  XorPriority = 0
+  EquivalencePriority = 0
+
+  BeforePriority = 0
+  StrongReleasePriority = 0
+  WeakUntilPriority = 0
+
+  UntilPriority = 30
+  DefaultOperatorPriority = 15
+}
+
+EOF
+
+"$LBTT" --configfile="$conffile" | tee "$logfile"
+"$srcdir"/parseout.pl "$logfile" | tee "$sumfile"
diff --git a/bench/ltl2tgba/defs.in b/bench/ltl2tgba/defs.in
new file mode 100644
index 000000000..5c1451892
--- /dev/null
+++ b/bench/ltl2tgba/defs.in
@@ -0,0 +1,54 @@
+# -*- shell-script -*-
+# Copyright (C) 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# et Marie Curie.
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+# Ensure we are running from the right directory.
+test -f ./defs || {
+   echo "defs: not found in current directory" 1>&2
+   exit 1
+}
+
+srcdir='@srcdir@'
+
+# Ensure $srcdir is set correctly.
+test -f "$srcdir/defs.in" || {
+   echo "$srcdir/defs.in not found, check \$srcdir" 1>&2
+   exit 1
+}
+
+LBT='@LBT@'
+LBTT='@LBTT@'
+LBTT_TRANSLATE="@LBTT_TRANSLATE@"
+LTL2BA='@LTL2BA@'
+LTL2NBA='@LTL2NBA@'
+LTL2TGBA='@top_builddir@/src/tgbatest/ltl2tgba@EXEEXT@'
+MODELLA='@MODELLA@'
+SPIN='@SPIN@'
+WRING2LBTT='@WRING2LBTT@'
+
+for var in LBT LTL2BA LTL2NBA MODELLA SPIN WRING2LBTT
+do
+  if eval 'test -z "$'$var'"'; then
+    eval HAVE_$var=no
+  else
+    eval HAVE_$var=yes
+  fi
+done
diff --git a/bench/ltl2tgba/formulae.ltl b/bench/ltl2tgba/formulae.ltl
new file mode 100644
index 000000000..59af12813
--- /dev/null
+++ b/bench/ltl2tgba/formulae.ltl
@@ -0,0 +1,94 @@
+U p0 p1
+U p0 U p1 p2
+V ! p0 V ! p1 ! p2
+| U t V f ! p0 V f U t p1
+U U t p0 V f p1
+U V f p0 p1
+& & U t U t p0 V f ! p0 & U t p0 V f V f ! p0
+& V f U t p0 U t V f ! p1
+& & V f U t p0 U t V f ! p1 & V f U t p1 U t V f ! p0
+V p0 | p0 p1
+| U X p0 X p1 X V ! p0 ! p1
+| U X p0 p1 X V ! p0 | ! p0 ! p1
+& V f | ! p0 U t p1 | U X p0 p1 X V ! p0 | ! p0 ! p1
+& V f | ! p0 U t p1 | U X p0 X p1 X V ! p0 ! p1
+V f | ! p0 U t p1
+U t & p0 X U ! p1 ! p2
+& U t V f ! p0 V f U t ! p1
+V f & U t p0 U t p1
+& U t p0 U t ! p0
+V & X p1 p2 X U V U p3 p0 p2 V p3 p2
+| | & V f | p1 V f U t p0 V f | p2 V f U t ! p0 V f p1 V f p2
+| | & V f | p1 U t V f p0 V f | p2 U t V f ! p0 V f p1 V f p2
+& & | U t & ! p1 U t V f ! p0 U t & ! p2 U t V f p0 U t p1 U t p2
+& & | U t & ! p1 V f U t ! p0 U t & ! p2 V f U t p0 U t p1 U t p2
+& V f | p1 X V f p0 V f | p2 X V f ! p0
+V f | p1 & X p0 X ! p0
+| U p0 p0 U p1 p0
+U p0 & p1 V f p2
+U p0 & p1 X U p2 p3
+U p0 & p1 X & p2 U t & p3 X U t & p4 X U t & p5 X U t p6
+U t & p0 X V f p1
+U t & p0 X & p1 X U t p2
+U t & p0 X U p1 p2
+| U t V f p0 U t V f p1
+V f | ! p0 U p1 p2
+U t & p0 X U t & p1 X U t & p2 X U t p3
+& & & & V f U t p0 V f U t p1 V f U t p2 V f U t p3 V f U t p4
+| | U p0 U p1 p2 U p1 U p2 p0 U p2 U p0 p1
+V f | ! p0 U p1 | V f p2 V f p3
+[](!p0)
+<>p1 -> (!p0 U p1)
+[](p2 -> [](!p0))
+[]((p2 & !p1 & <>p1) -> (!p0 U p1))
+[](p2 & !p1 -> (!p0 U (p1 | []!p0)))
+<>(p0)
+!p1 U ((p0 & !p1) | []!p1)
+[](!p2) | <>(p2 & <>p0)
+[](p2 & !p1 -> (!p1 U ((p0 & !p1) | []!p1)))
+[](p2 & !p1 -> (!p1 U (p0 & !p1)))
+<>p1 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1)))))))))
+[]((p2 & <>p1) -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1))))))))))
+[](p2 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U (p1 | []!p0)) | []p0)))))))))
+[](p0)
+<>p1 -> (p0 U p1)
+[](p2 -> [](p0))
+[]((p2 & !p1 & <>p1) -> (p0 U p1))
+[](p2 & !p1 -> (p0 U (p1 | [] p0)))
+!p0 U (p3 | []!p0)
+<>p1 -> (!p0 U (p3 | p1))
+[]!p2 | <>(p2 & (!p0 U (p3 | []!p0)))
+[]((p2 & !p1 & <>p1) -> (!p0 U (p3 | p1)))
+[](p2 & !p1 -> (!p0 U ((p3 | p1) | []!p0)))
+[](p0 -> <>p3)
+<>p1 -> (p0 -> (!p1 U (p3 & !p1))) U p1
+[](p2 -> [](p0 -> <>p3))
+[]((p2 & !p1 & <>p1) -> (p0 -> (!p1 U (p3 & !p1))) U p1)
+[](p2 & !p1 -> ((p0 -> (!p1 U (p3 & !p1))) U (p1 | [](p0 -> (!p1 U (p3 & !p1))))))
+<>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))
+<>p1 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))
+([]!p2) | (!p2 U (p2 & <>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))))
+[]((p2 & <>p1) -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4)))))
+[](p2 -> (<>p0 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))))
+(<>(p3 & X<>p4)) -> ((!p3) U p0)
+<>p1 -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0))
+([]!p2) | ((!p2) U (p2 & ((<>(p3 & X<>p4)) -> ((!p3) U p0))))
+[]((p2 & <>p1) -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0)))
+[](p2 -> (!(p3 & (!p1) & X(!p1 U (p4 & !p1))) U (p1 | p0) | [](!(p3 & X<>p4))))
+[] (p3 & X<> p4 -> X(<>(p4 & <> p0)))
+<>p1 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1
+[] (p2 -> [] (p3 & X<> p4 -> X(!p4 U (p4 & <> p0))))
+[] ((p2 & <>p1) -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1)
+[] (p2 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U (p1 | [] (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0)))))
+[] (p0 -> <>(p3 & X<>p4))
+<>p1 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1
+[] (p2 -> [] (p0 -> (p3 & X<> p4)))
+[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1)
+[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U (p1 | [] (p0 -> (p3 & X<> p4))))
+[] (p0 -> <>(p3 & !p5 & X(!p5 U p4)))
+<>p1 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1
+[] (p2 -> [] (p0 -> (p3 & !p5 & X(!p5 U p4))))
+[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1)
+[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U (p1 | [] (p0 -> (p3 & !p5 & X(!p5 U p4)))))
+!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0)
+<>p2 -> (!p2 U (p2 & (!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0))))
diff --git a/bench/ltl2tgba/known b/bench/ltl2tgba/known
new file mode 100644
index 000000000..7c2b872a4
--- /dev/null
+++ b/bench/ltl2tgba/known
@@ -0,0 +1,63 @@
+#!/bin/sh
+# -*- shell-script -*-
+# Copyright (C) 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# et Marie Curie.
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+. ./defs
+
+conffile=known.cfg
+logfile=known.log
+sumfile=known.txt
+ltlfile=formulae.ltl
+
+. "$srcdir/algorithms"
+
+cat >>"$conffile" <<EOF
+GlobalOptions
+{
+   Rounds = 100
+   Interactive = Never
+#   Verbosity = 5
+#   ComparisonCheck = no
+   ConsistencyCheck = no
+#   IntersectionCheck = no
+}
+
+StateSpaceOptions
+{
+   Size = 200
+   Propositions = 6
+}
+
+FormulaOptions
+{
+  Size = 10
+  Propositions = 4
+
+  AbbreviatedOperators = No
+  GenerateMode = Normal
+  OutputMode = NNF
+  DefaultOperatorPriority = 10
+}
+EOF
+
+"$LBTT" --configfile="$conffile" --formulafile="$ltlfile" | tee "$logfile"
+"$srcdir"/parseout.pl "$logfile" | tee "$sumfile"
diff --git a/src/tgbatest/ltl2baw.pl b/bench/ltl2tgba/ltl2baw.in
old mode 100755
new mode 100644
similarity index 93%
rename from src/tgbatest/ltl2baw.pl
rename to bench/ltl2tgba/ltl2baw.in
index ae2d4be98..a59e85720
--- a/src/tgbatest/ltl2baw.pl
+++ b/bench/ltl2tgba/ltl2baw.in
@@ -1,5 +1,6 @@
-#!/usr/bin/perl -w
-# Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+#!/usr/bin/env @PERL@
+
+# Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -20,6 +21,7 @@
 # Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
 # 02111-1307, USA.
 
+use warnings;
 
 # Usage:
 # ------
@@ -77,18 +79,18 @@ my $output_formula = 0;
 
 if ($arg =~ '^--ltl2ba=(.*)$')
   {
-    open(LTL2TGBA, "| ./ltl2tgba $1 -X -");
+    open(LTL2TGBA, "| @top_builddir@/src/tgbatest/ltl2tgba $1 -X -");
     shift;
   }
 elsif ($arg =~ '--spot=(.*)$')
   {
     $output_formula = 1;
-    open(LTL2TGBA, "| ./ltl2tgba $1 -F -");
+    open(LTL2TGBA, "| @top_builddir@/src/tgbatest/ltl2tgba $1 -F -");
     shift;
   }
 else
   {
-    open(LTL2TGBA, "| ./ltl2tgba -t -X -");
+    open(LTL2TGBA, "| @top_builddir@/src/tgbatest/ltl2tgba -t -X -");
   }
 
 END {
@@ -97,7 +99,7 @@ END {
 }
 
 my @args = dquote @ARGV;
-open(LTL2BA, "ltl2ba -d @args |") || die "failed to run ltl2ba";
+open(LTL2BA, "@LTL2BA@ -d @args |") || die "failed to run ltl2ba";
 
 my $state = PROLOGUE;
 
diff --git a/bench/ltl2tgba/parseout.pl b/bench/ltl2tgba/parseout.pl
new file mode 100755
index 000000000..ab55c5878
--- /dev/null
+++ b/bench/ltl2tgba/parseout.pl
@@ -0,0 +1,69 @@
+#!/usr/bin/env perl
+
+# Copyright (C) 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# et Marie Curie.
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+use warnings;
+
+my $line = 0;
+my $tool = 0;
+my ($a, $b, $acc, $time);
+
+format STDOUT2 =
+||<:>@>>||@<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<||<)>@>>>>>||<)>@>>>>>||<)>@>>>||<)>@#####.##||<)>@>>>>>>>>||<)>@>>>>>>>>||<)>@>>||
+$num, $tool, $a, $b, $acc, $time, $2, $3, $1
+.
+
+format STDOUT =
+@>>: @<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<
+$num, $tool
+       @>>>>> / @>>>>> / @>>> / @#####.##   @>>>>>>>> / @>>>>>>>>   (@>>)
+$a, $b, $acc, $time, $2, $3, $1
+.
+
+$~ = STDOUT2 if (exists $ENV{'WIKI'});
+
+my %impl;
+
+while (<>)
+{
+    if (/^\s{4}(\d+):\s`(.+)'\s*(?:\(disabled\))?\s*$/)
+    {
+	$impl{$1} = $2 unless exists $impl{$1};
+    }
+    if (/Pos\. formulae \|\s*([^|]*?)\s*\|\s*([^|]*?)\s*\|$/)
+    {
+        $acc = $1;
+	$time = $2;
+    }
+    next unless /Pos\. formulae \|\s*(.*?)\s*\|\s*(.*?)\s*\|\s*(.*?)\s*\|/;
+    if ($line % 2)
+    {
+	$num = $line >> 1;
+        $tool = $impl{$num};
+	write;
+    }
+    else
+    {
+	($a, $b) = ($2, $3);
+    }
+    ++$line;
+}
diff --git a/bench/ltl2tgba/small b/bench/ltl2tgba/small
new file mode 100644
index 000000000..09d5bed1b
--- /dev/null
+++ b/bench/ltl2tgba/small
@@ -0,0 +1,78 @@
+#!/bin/sh
+# -*- shell-script -*-
+# Copyright (C) 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# et Marie Curie.
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+. ./defs
+
+conffile=small.cfg
+logfile=small.log
+sumfile=small.txt
+
+. "$srcdir/algorithms"
+
+cat >>"$conffile" <<EOF
+GlobalOptions
+{
+   Rounds = 100
+   Interactive = Never
+#   Verbosity = 5
+#   ComparisonCheck = no
+   ConsistencyCheck = no
+#   IntersectionCheck = no
+}
+
+StateSpaceOptions
+{
+   Size = 200
+   Propositions = 4
+}
+
+FormulaOptions
+{
+  Size = 10
+  Propositions = 4
+
+  AbbreviatedOperators = No
+  GenerateMode = Normal
+  OutputMode = NNF
+  PropositionPriority = 50
+
+  TruePriority = 1
+  FalsePriority = 1
+
+  AndPriority = 10
+  OrPriority = 10
+  XorPriority = 0
+  EquivalencePriority = 0
+
+  BeforePriority = 0
+  StrongReleasePriority = 0
+  WeakUntilPriority = 0
+
+  UntilPriority = 30
+  DefaultOperatorPriority = 15
+}
+
+EOF
+
+"$LBTT" --configfile="$conffile" | tee "$logfile"
+"$srcdir"/parseout.pl "$logfile" | tee "$sumfile"
diff --git a/configure.ac b/configure.ac
index 14e04f818..1b46680b5 100644
--- a/configure.ac
+++ b/configure.ac
@@ -57,14 +57,22 @@ adl_NDEBUG
 
 AM_CONDITIONAL([NEVER], [false])
 AC_CHECK_PROG([DOT], [dot], [dot])
+AC_CHECK_PROG([LBT], [lbt], [lbt])
+AC_CHECK_PROG([LTL2BA], [ltl2ba], [ltl2ba])
+AC_CHECK_PROG([MODELLA], [modella], [modella])
+AC_CHECK_PROG([LTL2NBA], [script4lbtt.py], [script4lbtt.py])
 AC_CHECK_PROG([PERL], [perl], [perl])
+AC_CHECK_PROG([SPIN], [spin], [spin])
 AC_CHECK_PROG([VALGRIND], [valgrind], [valgrind])
+AC_CHECK_PROG([WRING2LBTT], [wring2lbtt], [wring2lbtt])
 
 AC_CONFIG_FILES([
   Makefile
   bench/Makefile
   bench/emptchk/Makefile
   bench/emptchk/defs
+  bench/ltl2tgba/Makefile
+  bench/ltl2tgba/defs
   doc/Doxyfile
   doc/Makefile
   iface/Makefile
@@ -95,5 +103,7 @@ AC_CONFIG_FILES([
   wrap/python/cgi/Makefile
   wrap/python/tests/Makefile
 ])
+AC_CONFIG_FILES([bench/ltl2tgba/ltl2baw.pl:bench/ltl2tgba/ltl2baw.in],
+	        [chmod +x bench/ltl2tgba/ltl2baw.pl])
 AC_CONFIG_FILES([wrap/python/tests/run], [chmod +x wrap/python/tests/run])
 AC_OUTPUT
diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am
index 1855568eb..6d81d3496 100644
--- a/src/tgbatest/Makefile.am
+++ b/src/tgbatest/Makefile.am
@@ -86,7 +86,7 @@ TESTS = \
   emptchkr.test \
   spotlbtt.test
 
-EXTRA_DIST = $(TESTS) ltl2baw.pl
+EXTRA_DIST = $(TESTS)
 
 CLEANFILES = \
   blue_counter \