From 01f58f5fbfccecb064417bb29a974ae6b37b57e1 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 29 Jul 2003 11:21:18 +0000
Subject: [PATCH] * src/tgbatest/Makefile.am (check_PROGRAMS): Add tbalbtt.
 (tbalbtt_SOURCES, tbalbtt_CXXFLAGS): New variables. *
 src/tgbatest/spotlbtt.cc [TBA]: Build tba proxies conditionally. *
 src/tgbatest/spotlbtt.test: Include tbalbtt in the tests.

---
 ChangeLog                  |  7 +++++++
 src/tgbatest/Makefile.am   |  3 +++
 src/tgbatest/spotlbtt.cc   | 13 ++++++++++---
 src/tgbatest/spotlbtt.test |  7 +++++++
 4 files changed, 27 insertions(+), 3 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 6d50a756f..1d7fb6651 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,10 @@
+2003-07-29  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
+
+	* src/tgbatest/Makefile.am (check_PROGRAMS): Add tbalbtt.
+	(tbalbtt_SOURCES, tbalbtt_CXXFLAGS): New variables.
+	* src/tgbatest/spotlbtt.cc [TBA]: Build tba proxies conditionally.
+	* src/tgbatest/spotlbtt.test: Include tbalbtt in the tests.
+
 2003-07-28  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
 	* src/tgba/tgbatba.hh, src/tgba/tgbatba.cc
diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am
index 4f6d7dcdc..6f60dfb62 100644
--- a/src/tgbatest/Makefile.am
+++ b/src/tgbatest/Makefile.am
@@ -13,6 +13,7 @@ check_PROGRAMS = \
   mixprod \
   readsave \
   spotlbtt \
+  tbalbtt \
   tgbaread \
   tripprod
 
@@ -26,6 +27,8 @@ ltlmagic_SOURCES = ltlmagic.cc
 ltlprod_SOURCES  = ltlprod.cc
 mixprod_SOURCES  = mixprod.cc
 readsave_SOURCES = readsave.cc
+tbalbtt_SOURCES  = spotlbtt.cc
+tbalbtt_CXXFLAGS = -DTBA
 tgbaread_SOURCES = tgbaread.cc
 tripprod_SOURCES = tripprod.cc
 spotlbtt_SOURCES = spotlbtt.cc
diff --git a/src/tgbatest/spotlbtt.cc b/src/tgbatest/spotlbtt.cc
index 48e498c2d..519f5977b 100644
--- a/src/tgbatest/spotlbtt.cc
+++ b/src/tgbatest/spotlbtt.cc
@@ -7,7 +7,7 @@
 #include "ltlparse/public.hh"
 #include "tgbaalgos/ltl2tgba.hh"
 #include "tgbaalgos/lbtt.hh"
-
+#include "tgba/tgbatba.hh"
 
 void
 syntax(char* prog)
@@ -48,10 +48,17 @@ main(int argc, char** argv)
 
   if (f)
     {
-      spot::tgba_bdd_concrete* a = spot::ltl_to_tgba(f, dict);
+      spot::tgba* a;
+      spot::tgba* c = a = spot::ltl_to_tgba(f, dict);
       spot::ltl::destroy(f);
+#ifdef TBA
+      spot::tgba* d = a = new spot::tgba_tba_proxy(a);
+#endif
       spot::lbtt_reachable(std::cout, a);
-      delete a;
+#ifdef TBA
+      delete d;
+#endif
+      delete c;
     }
   else
     {
diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test
index 15510624e..76b133c6b 100755
--- a/src/tgbatest/spotlbtt.test
+++ b/src/tgbatest/spotlbtt.test
@@ -12,6 +12,13 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot TBA"
+   Path = "${LBTT_TRANSLATE} --spot ./tbalbtt"
+   Enabled = yes
+}
+
 GlobalOptions
 {
    Rounds = 100