From 1a823fea96256e8848fe59dfe8d6e928fe75157b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 25 Jun 2011 23:29:16 +0200
Subject: [PATCH] Revamp the ltl2tgba benchmark.

* bench/ltl2tgba/algorithms: Reduce the number of Spot configuration
tested.
* bench/ltl2tgba/Makefile.am (run, small.txt, big.txt, known.txt):
New rules.
* bench/ltl2tgba/big, bench/ltl2tgba/small, bench/ltl2tgba/known:
Add a 15min timeout to the lbtt configuration.
* bench/ltl2tgba/defs.in: Adjust variable definitions to accept
variable inderections.
* bench/ltl2tgba/parseout.pl: Add an option to output the table in
LaTeX.  Also consider all formulae, not just the positive
formulae.
* bench/ltl2tgba/README: Update.
---
 ChangeLog                  |  17 ++
 bench/ltl2tgba/Makefile.am |  10 ++
 bench/ltl2tgba/README      |  35 ++--
 bench/ltl2tgba/algorithms  | 351 +++++++------------------------------
 bench/ltl2tgba/big         |   3 +
 bench/ltl2tgba/defs.in     |  19 +-
 bench/ltl2tgba/known       |   3 +
 bench/ltl2tgba/parseout.pl |  21 ++-
 bench/ltl2tgba/small       |   3 +
 9 files changed, 145 insertions(+), 317 deletions(-)
 mode change 100644 => 100755 bench/ltl2tgba/big
 mode change 100644 => 100755 bench/ltl2tgba/known
 mode change 100644 => 100755 bench/ltl2tgba/small

diff --git a/ChangeLog b/ChangeLog
index 305e008fa..cfe4bb296 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,20 @@
+2011-06-25  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Revamp the ltl2tgba benchmark.
+
+	* bench/ltl2tgba/algorithms: Reduce the number of Spot configuration
+	tested.
+	* bench/ltl2tgba/Makefile.am (run, small.txt, big.txt, known.txt):
+	New rules.
+	* bench/ltl2tgba/big, bench/ltl2tgba/small, bench/ltl2tgba/known:
+	Add a 15min timeout to the lbtt configuration.
+	* bench/ltl2tgba/defs.in: Adjust variable definitions to accept
+	variable inderections.
+	* bench/ltl2tgba/parseout.pl: Add an option to output the table in
+	LaTeX.  Also consider all formulae, not just the positive
+	formulae.
+	* bench/ltl2tgba/README: Update.
+
 2011-06-16  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* src/ltlvisit/tostring.cc (to_spin_string_visitor): Add missing break.
diff --git a/bench/ltl2tgba/Makefile.am b/bench/ltl2tgba/Makefile.am
index d1aaefb74..6bdcee220 100644
--- a/bench/ltl2tgba/Makefile.am
+++ b/bench/ltl2tgba/Makefile.am
@@ -9,3 +9,13 @@ CLEAN_FILES = \
   big.cfg big.log big.txt \
   small.cfg small.log small.txt \
   known.cfg known.log known.txt
+
+.PHONY = run
+run: small.txt big.txt known.txt wfair.txt
+
+small.txt: $(srcdir)/small $(srcdir)/algorithms $(top_srcdir)/configure.ac
+	$(srcdir)/small
+big.txt: $(srcdir)/big $(srcdir)/algorithms $(top_srcdir)/configure.ac
+	$(srcdir)/big
+known.txt: $(srcdir)/known $(srcdir)/algorithms $(srcdir)/formulae.ltl $(top_srcdir)/configure.ac
+	$(srcdir)/known
diff --git a/bench/ltl2tgba/README b/bench/ltl2tgba/README
index e2c4b6505..3420b8bd4 100644
--- a/bench/ltl2tgba/README
+++ b/bench/ltl2tgba/README
@@ -73,7 +73,7 @@ that are not available.
 +	  fputc('\n',output);
  	}
        fprintf(output,"-1 ");
-       
+
 
        * The automata produced by Wring are translated to the syntax
          understood by lbtt using `wring2lbtt' (by the same author of
@@ -116,6 +116,11 @@ checking for wring2lbtt... wring2lbtt
         ./big
      or ./known
 
+     Alternatively running `make run' (in that directory) will run all
+     three scripts.  If you have a multicore processor, you may want
+     to run `make -j3 run' to run these three scripts in parallel.
+     None of the tested translators use more than one core.
+
   5) Wait...
 
 =======================
@@ -126,22 +131,24 @@ 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)
+    6: Spot FM (degen)
+            834 /   2419 /  188 /      2.86      166579 /   8749162   (188)
 
-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 first line presents the name of the algorithm ("Spot FM (degen)")
+and its number for lbtt (6).  The number is useless.  In this example,
+"FM (degen)" means that the Couvreur/FM algorithm is used to translate
+LTL formula into a TGBA that is then DEGENeralized.  You may want to
+look in the file `algorithms' to see which options are used for each
+name, if the naming is unclear.
 
 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)
+  1. the total number of states of all generated automata (834)
+  2. the total number of transitions of all generated automata (2419)
+  3. the total number of acceptance conditions of all generated automata (188)
+  4. the cumulated translation time in seconds (2.86)
+  5. the total number of states in the synchronized products (166579)
+  6. the total number of transitions in the synchronized products (8749162)
+  7. the number of translated formulae (188)
 
 Notes:
 
diff --git a/bench/ltl2tgba/algorithms b/bench/ltl2tgba/algorithms
index ee688d806..5fe7ba868 100644
--- a/bench/ltl2tgba/algorithms
+++ b/bench/ltl2tgba/algorithms
@@ -1,269 +1,4 @@
 cat >"$conffile" <<EOF
-Algorithm
-{
-   Name = "LaCIM, degen"
-   Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$LTL2TGBA -l -t -D -F'"
-   Enabled = yes
-}
-
-Algorithm
-{
-   Name = "LaCIM, gen"
-   Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$LTL2TGBA -l -t -F'"
-   Enabled = yes
-}
-
-Algorithm
-{
-   Name = "LaCIM, degen, +pre"
-   Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$LTL2TGBA -l -t -D -r4 -F'"
-   Enabled = yes
-}
-
-Algorithm
-{
-   Name = "LaCIM, gen, +pre"
-   Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$LTL2TGBA -l -t -r4 -F'"
-   Enabled = yes
-}
-
-Algorithm
-{
-   Name = "LACIM, eltl"
-   Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$ELTL2TGBA -LW'"
-   Enabled = yes
-}
-
-Algorithm
-{
-   Name = "LACIM, eltl, +delete_unaccepting_scc"
-   Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$ELTL2TGBA -L'"
-   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, +INpre, +post, +flapprox"
-   Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$LTL2TGBA -fr4 -R1q -R1t -R3 -L -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, +INpre, +post, +flapprox, +post_branch"
-   Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$LTL2TGBA -fr4 -R1q -R1t -R3 -L -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, +INpre, +post, +flapprox"
-   Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$LTL2TGBA -fr4 -R1q -R1t -R3 -L -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 = "FM, gen, +symb_merge, +exprop, +INpre, +post, +flapprox, +post_branch"
-   Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$LTL2TGBA -fr4 -R1q -R1t -R3 -L -t -x  -p -F'"
-   Enabled = yes
-}
-
 Algorithm
 {
    Name = "Spin"
@@ -274,39 +9,24 @@ Algorithm
 
 Algorithm
 {
-   Name = "LBT"
-   Path = "$LBTT_TRANSLATE"
-   Parameters = "--lbt $LBT"
-   Enabled = $HAVE_LBT
-}
-
-Algorithm
-{
-   Name = "LTL2BA, degen"
+   Name = "ltl2ba"
    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
+   Name = "Modella"
+   Path = "$MODELLA"
+   Parameters = "-o1 -g -e -r12"
+   Enabled = $HAVE_MODELLA
 }
 
 Algorithm
 {
-   Name = "Wring (Wring RewRule+BoolOpt+AutSempl)"
-   Path = "$WRING2LBTT"
-   Parameters = "--5"
-   Enabled = $HAVE_WRING2LBTT
-}
-
-Algorithm
-{
-   Name = "Wring (Wring RewRule+BoolOpt+AutSempl), degen"
+   Name = "Wring (RewRule+BoolOpt+AutSempl), degen"
    Path = "$WRING2LBTT"
    Parameters = "-d --5"
    Enabled = $HAVE_WRING2LBTT
@@ -314,10 +34,10 @@ Algorithm
 
 Algorithm
 {
-   Name = "Modella -o1 -g -e -r12"
-   Path = "$MODELLA"
-   Parameters = "-o1 -g -e -r12"
-   Enabled = $HAVE_MODELLA
+   Name = "Wring (RewRule+BoolOpt+AutSempl)"
+   Path = "$WRING2LBTT"
+   Parameters = "--5"
+   Enabled = $HAVE_WRING2LBTT
 }
 
 Algorithm
@@ -326,4 +46,53 @@ Algorithm
    Path = "$LTL2NBA"
    Enabled = $HAVE_LTL2NBA
 }
+
+Algorithm
+{
+   Name = "Spot FM (degen)"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spin '$LTL2TGBA -f -N -R3 -r7 -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot FM det. (degen)"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spin '$LTL2TGBA -f -N -R3 -r7 -x -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot FM WDBA (degen)"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spin '$LTL2TGBA -f -N -R3 -r7 -x -Rm -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot FM (TGBA)"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -f -t -R3f -r7 -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot FM det. (TGBA)"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -f -t -R3f -r7 -x -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot FM WDBA (TGBA)"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -f -t -R3f -r7 -x -Rm -F'"
+   Enabled = yes
+}
+
 EOF
diff --git a/bench/ltl2tgba/big b/bench/ltl2tgba/big
old mode 100644
new mode 100755
index 945f14259..54b422872
--- a/bench/ltl2tgba/big
+++ b/bench/ltl2tgba/big
@@ -1,5 +1,7 @@
 #!/bin/sh
 # -*- shell-script -*-
+# Copyright (C) 2011 Laboratoire de Recherche et Developpement de
+# l'Epita (LRDE)
 # Copyright (C) 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
@@ -38,6 +40,7 @@ GlobalOptions
 #   ComparisonCheck = no
    ConsistencyCheck = no
 #   IntersectionCheck = no
+   TranslatorTimeout = 15min
 }
 
 StateSpaceOptions
diff --git a/bench/ltl2tgba/defs.in b/bench/ltl2tgba/defs.in
index 20729104f..8c6885c35 100644
--- a/bench/ltl2tgba/defs.in
+++ b/bench/ltl2tgba/defs.in
@@ -34,16 +34,17 @@ test -f "$srcdir/defs.in" || {
    exit 1
 }
 
-LBT='@LBT@'
-LBTT='@LBTT@'
+top_builddir="@top_builddir@"
+LBT="@LBT@"
+LBTT="@LBTT@"
 LBTT_TRANSLATE="@LBTT_TRANSLATE@"
-LTL2BA='@LTL2BA@'
-LTL2NBA='@LTL2NBA@'
-LTL2TGBA='@top_builddir@/src/tgbatest/ltl2tgba@EXEEXT@'
-ELTL2TGBA='@top_builddir@/src/tgbatest/eltl2tgba@EXEEXT@'
-MODELLA='@MODELLA@'
-SPIN='@SPIN@'
-WRING2LBTT='@WRING2LBTT@'
+LTL2BA="@LTL2BA@"
+LTL2NBA="@LTL2NBA@"
+LTL2TGBA="@top_builddir@/src/tgbatest/ltl2tgba@EXEEXT@"
+ELTL2TGBA="@top_builddir@/src/tgbatest/eltl2tgba@EXEEXT@"
+MODELLA="@MODELLA@"
+SPIN="@SPIN@"
+WRING2LBTT="@WRING2LBTT@"
 
 for var in LBT LTL2BA LTL2NBA MODELLA SPIN WRING2LBTT
 do
diff --git a/bench/ltl2tgba/known b/bench/ltl2tgba/known
old mode 100644
new mode 100755
index 7c2b872a4..fbe309bf1
--- a/bench/ltl2tgba/known
+++ b/bench/ltl2tgba/known
@@ -1,5 +1,7 @@
 #!/bin/sh
 # -*- shell-script -*-
+# Copyright (C) 2011 Laboratoire de Recherche et Developpement de
+# l'Epita (LRDE)
 # Copyright (C) 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
@@ -39,6 +41,7 @@ GlobalOptions
 #   ComparisonCheck = no
    ConsistencyCheck = no
 #   IntersectionCheck = no
+   TranslatorTimeout = 15min
 }
 
 StateSpaceOptions
diff --git a/bench/ltl2tgba/parseout.pl b/bench/ltl2tgba/parseout.pl
index d88dcb112..4b86dfc5e 100755
--- a/bench/ltl2tgba/parseout.pl
+++ b/bench/ltl2tgba/parseout.pl
@@ -1,5 +1,7 @@
 #!/usr/bin/env perl
 
+# Copyright (C) 2011 Laboratoire de Recherche et Développement de
+# l'Epita.
 # Copyright (C) 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
@@ -27,6 +29,18 @@ my $line = 0;
 my $tool = 0;
 my ($a, $b, $acc, $time);
 
+sub sep($)
+{
+    $n = shift;
+    $n =~ s/(\d{1,3}?)(?=(\d{3})+$)/$1\\,/g;
+    return $n;
+}
+
+format STDOUT3 =
+@<<<<<<<<<<<<<<<<<<<<< & @>>>>>> & @>>>>>> & @>>>>>>>>> & @>>>>>>>>>>> \\ % @>>
+$tool, sep($a), sep($b), sep($2), sep($3), sep($1)
+.
+
 format STDOUT2 =
 ||<:>@>>||@<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<||<)>@>>>>>||<)>@>>>>>||<)>@>>>||<)>@#####.##||<)>@>>>>>>>>||<)>@>>>>>>>>||<)>@>>||
 $num, $tool, $a, $b, $acc, $time, $2, $3, $1
@@ -39,7 +53,8 @@ $num, $tool
 $a, $b, $acc, $time, $2, $3, $1
 .
 
-$~ = STDOUT2 if (exists $ENV{'WIKI'});
+$~ = STDOUT2 if (exists $ENV{'WIKIOUTPUT'});
+$~ = STDOUT3 if (exists $ENV{'LATEXOUTPUT'});
 
 my %impl;
 
@@ -49,12 +64,12 @@ while (<>)
     {
 	$impl{$1} = $2 unless exists $impl{$1};
     }
-    if (/Pos\. formulae \|\s*([^|]*?)\s*\|\s*([^|]*?)\s*\|$/)
+    if (/All formulae\s*\|\s*([^|]*?)\s*\|\s*([^|]*?)\s*\|$/)
     {
         $acc = $1;
 	$time = $2 || 0;
     }
-    next unless /Pos\. formulae \|\s*(.*?)\s*\|\s*(.*?)\s*\|\s*(.*?)\s*\|/;
+    next unless /All formulae\s+\|\s*(.*?)\s*\|\s*(.*?)\s*\|\s*(.*?)\s*\|/;
     if ($line % 2)
     {
 	$num = $line >> 1;
diff --git a/bench/ltl2tgba/small b/bench/ltl2tgba/small
old mode 100644
new mode 100755
index 09d5bed1b..339e442eb
--- a/bench/ltl2tgba/small
+++ b/bench/ltl2tgba/small
@@ -1,5 +1,7 @@
 #!/bin/sh
 # -*- shell-script -*-
+# Copyright (C) 2011 Laboratoire de Recherche et Developpement de
+# l'Epita (LRDE)
 # Copyright (C) 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
@@ -38,6 +40,7 @@ GlobalOptions
 #   ComparisonCheck = no
    ConsistencyCheck = no
 #   IntersectionCheck = no
+   TranslatorTimeout = 15min
 }
 
 StateSpaceOptions