From 4a9bbbafe2d6b92ed45f156163a16c48cc04c916 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 2 May 2012 09:59:33 +0200
Subject: [PATCH] Add ltl3ba to the ltl2tgba benchmark.

* configure.ac: Search for ltl3ba.
* bench/ltl2tgba/defs.in: Define LTL3BA and HAVE_LTL3BA.
* bench/ltl2tgba/algorithms: Use LTL3BA. Also add simulation options
for LTL2BA.
* bench/ltl2tgba/README: Slight wording changes.
---
 bench/ltl2tgba/README     |  9 ++++----
 bench/ltl2tgba/algorithms | 46 +++++++++++++++++++++++++++++++++++++++
 bench/ltl2tgba/defs.in    |  9 +++++---
 configure.ac              |  1 +
 4 files changed, 58 insertions(+), 7 deletions(-)

diff --git a/bench/ltl2tgba/README b/bench/ltl2tgba/README
index 3420b8bd4..189cc26c3 100644
--- a/bench/ltl2tgba/README
+++ b/bench/ltl2tgba/README
@@ -162,7 +162,8 @@ Notes:
     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.)
+    others.  This normally indicates bugs in the translator (incorrect
+    output) or timeouts.  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
index 5fe7ba868..113ae92d2 100644
--- a/bench/ltl2tgba/algorithms
+++ b/bench/ltl2tgba/algorithms
@@ -15,6 +15,37 @@ Algorithm
    Enabled = $HAVE_LTL2BA
 }
 
+Algorithm
+{
+   Name = "ltl3ba"
+   Path = "lbtt-translate"
+   Parameters = "--spin $LTL3BA"
+   Enabled = $HAVE_LTL3BA
+}
+
+Algorithm
+{
+   Name = "ltl3ba -M"
+   Path = "lbtt-translate"
+   Parameters = "--spin '$LTL3BA -M'"
+   Enabled = $HAVE_LTL3BA
+}
+
+Algorithm
+{
+   Name = "ltl3ba -S"
+   Path = "lbtt-translate"
+   Parameters = "--spin '$LTL3BA -S'"
+   Enabled = $HAVE_LTL3BA
+}
+
+Algorithm
+{
+   Name = "ltl3ba -M -S"
+   Path = "lbtt-translate"
+   Parameters = "--spin '$LTL3BA -M -S'"
+   Enabled = $HAVE_LTL3BA
+}
 
 Algorithm
 {
@@ -87,6 +118,14 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot FM Sim (TGBA)"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -f -t -R3 -r7 -x -RDS -F'"
+   Enabled = yes
+}
+
 Algorithm
 {
    Name = "Spot FM WDBA (TGBA)"
@@ -95,4 +134,11 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot FM WDBA+Sim (TGBA)"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -f -t -R3 -r7 -x -Rm -RDS -F'"
+   Enabled = yes
+}
 EOF
diff --git a/bench/ltl2tgba/defs.in b/bench/ltl2tgba/defs.in
index 8c6885c35..1969e8962 100644
--- a/bench/ltl2tgba/defs.in
+++ b/bench/ltl2tgba/defs.in
@@ -1,6 +1,8 @@
-# -*- shell-script -*-
+# -*- shell-script; coding: utf-8 -*-
+# Copyright (C) 2012 Laboratoire de Recherche et Développement 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
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
 # This file is part of Spot, a model checking library.
@@ -39,6 +41,7 @@ LBT="@LBT@"
 LBTT="@LBTT@"
 LBTT_TRANSLATE="@LBTT_TRANSLATE@"
 LTL2BA="@LTL2BA@"
+LTL3BA="@LTL3BA@"
 LTL2NBA="@LTL2NBA@"
 LTL2TGBA="@top_builddir@/src/tgbatest/ltl2tgba@EXEEXT@"
 ELTL2TGBA="@top_builddir@/src/tgbatest/eltl2tgba@EXEEXT@"
@@ -46,7 +49,7 @@ MODELLA="@MODELLA@"
 SPIN="@SPIN@"
 WRING2LBTT="@WRING2LBTT@"
 
-for var in LBT LTL2BA LTL2NBA MODELLA SPIN WRING2LBTT
+for var in LBT LTL2BA LTL3BA LTL2NBA MODELLA SPIN WRING2LBTT
 do
   if eval 'test -z "$'$var'"'; then
     eval HAVE_$var=no
diff --git a/configure.ac b/configure.ac
index 24d3dc35d..b3414bae4 100644
--- a/configure.ac
+++ b/configure.ac
@@ -89,6 +89,7 @@ AM_CONDITIONAL([NEVER], [false])
 AC_PATH_PROG([DOT], [dot])
 AC_CHECK_PROG([LBT], [lbt], [lbt])
 AC_CHECK_PROG([LTL2BA], [ltl2ba], [ltl2ba])
+AC_CHECK_PROG([LTL3BA], [ltl3ba], [ltl3ba])
 AC_CHECK_PROG([MODELLA], [modella], [modella])
 AC_CHECK_PROG([LTL2NBA], [script4lbtt.py], [script4lbtt.py])
 AC_CHECK_PROG([PERL], [perl], [perl])