Commit graph

6 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
b23296cf61 Allow lbtt not to be built, and skip relevant tests.
* m4/lbtt.m4: Turn the missing lbtt error into a warning,
and do not configure lbtt wen --without-included-lbtt is specified.
* bench/ltl2tgba/defs.in: Abort if lbtt is missing.
* src/tgbatest/defs.in (need_lbtt): New function to skip
tests that require lbtt.
* src/tgbatest/babiak.test, src/tgbatest/ltl2neverclaim.test,
src/tgbatest/spotlbtt.test: Call need_lbtt.
2012-09-25 19:55:06 +02:00
Alexandre Duret-Lutz
6a3cf7538c bin/ltl2tgba: New user binary.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: New class to
capture the postprocessing logic.
* src/tgbaalgos/Makefile.am: Add them.
* src/bin/ltl2tgba.cc, src/bin/man/ltl2tgba.x: New files.
* src/bin/Makefile.am, src/bin/man/Makefile.am: Add them.
* src/tgbatest/spotlbtt.test: Prune the list of configurations slightly.
* src/tgbatest/spotlbtt2.test: New file.
* src/tgbatest/Makefile.am: Add it.
* bench/ltl2tgba/algorithms, bench/ltl2tgba/defs.in: Adjust to
use the new binary.
* NEWS: Update.
2012-09-12 18:53:16 +02:00
Alexandre Duret-Lutz
4a9bbbafe2 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.
2012-05-02 09:59:33 +02:00
Alexandre Duret-Lutz
1a823fea96 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-26 18:14:53 +02:00
Damien Lefortier
edd4b2b532 Add an algorithm (from Couvreur) working on BDDs to reduce the
size of TGBAs represented as BDDs by deleting unaccepting SCCs.

* src/eltlparse/eltlparse.yy: Remove a warning.
* src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh: Add a
new function delete_unaccepting_scc in both classes.
* src/tgbatest/eltl2tgba.cc, src/tgbatest/spotlbtt.test: Use this
new function in LaCIM for ELTL and bench it.
* src/tgbatest/defs.in: Fix it.
* bench/ltl2tgba/algorithms, bench/ltl2tgba/defs.in: Add LaCIM for
ELTL in benchs.
2009-09-07 14:26:42 +02:00
Alexandre Duret-Lutz
a7cf769a24 * 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-15 13:38:23 +00:00