Commit 01f58f5f authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* 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.
parent 860d085b
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
......
......@@ -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
......
......@@ -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
{
......
......@@ -12,6 +12,13 @@ Algorithm
Enabled = yes
}
Algorithm
{
Name = "Spot TBA"
Path = "${LBTT_TRANSLATE} --spot ./tbalbtt"
Enabled = yes
}
GlobalOptions
{
Rounds = 100
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment