Commit graph

10 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
b708ab778f genltl: add formulas from three papers
Fixes #166.

* bin/genltl.cc: Add option --dac-patterns, --eh-patterns,
--sb-patterns.
* NEWS, bin/man/genltl.x, doc/org/genltl.org: Document them.
* bench/ltl2tgba/formulae.ltl: Delete.
* bench/ltl2tgba/known: Use genltl instead.
* bench/ltl2tgba/Makefile.am, bench/ltl2tgba/README: Update.
* tests/core/ltl2tgba2.test: New test case, using genltl.
* tests/Makefile.am: Add it.
2016-05-05 18:39:13 +02:00
Alexandre Duret-Lutz
fd5d59984b bench: fix bench/ltl2tgba for new bin location
* bench/ltl2tgba/Makefile.am, bench/ltl2tgba/defs.in:
Update location of tools.
* NEWS: Mention the fix.
2016-05-05 18:15:44 +02:00
Alexandre Duret-Lutz
f65c621a55 ltlcross: report exit_status and exit_code columns in CSV and JSON
* src/bin/ltlcross.cc: Report exit_status and exit_code columns in CSV
and JSON files.  Also output lines for failed translations, and add
a --omit-missing option to disable that.  Move the time column right
after exit_status and exit_code.
* src/bin/man/ltlcross.x: Document each column of the output.
* bench/ltl2tgba/tools: Use the "{name}cmd" notation.
* bench/ltl2tgba/sum.py: Adjust to the new columns.
* bench/ltl2tgba/README: Update to point to the man page for a
description of the columns.
* bench/ltl2tgba/Makefile.am: Build results.pdf as said announced in
README.
* bench/spin13/html.bottom: Update code to ignore these two new
columns and lines with null values.
* src/tgbatest/ltlcross3.test: Add tests.
* doc/org/ltlcross.org: Adjust examples.
* NEWS: Mention this.
2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
212cb835fc bench/ltl2tgba: Adjust to support different config files.
* bench/ltl2tgba/algorithms: Rename as...
* bench/ltl2tgba/tools: ... this.
* bench/ltl2tgba/README, bench/ltl2tgba/Makefile.am,
bench/ltl2tgba/defs.in, bench/ltl2tgba/big, bench/ltl2tgba/small,
bench/ltl2tgba/known: Adjust.
* bench/ltl2tgba/tools.sim: New file, extracted from ./algorithms.
2013-04-15 15:31:43 +02:00
Alexandre Duret-Lutz
86558f1a5c Add missing copyright notice.
* bench/ltl2tgba/Makefile.am, bench/ltl2tgba/sum.py: Add copyright
notice.
2013-01-06 21:44:15 +01:00
Alexandre Duret-Lutz
885a535184 Rewrite the ltl2tgba bench using ltlcross
* bench/ltl2tgba/sum.py: New file.
* bench/ltl2tgba/.gitignore, bench/ltl2tgba/Makefile.am,
bench/ltl2tgba/README, bench/ltl2tgba/algorithms, bench/ltl2tgba/big,
bench/ltl2tgba/defs.in, bench/ltl2tgba/known, bench/ltl2tgba/small:
Rewrite this benchmark completely.  Also drop support of Wring and
Modella, as we cannot get them to work reliably.
* bench/ltl2tgba/formulae.ltl: Rewrite in Spot's syntax.
* bench/ltl2tgba/lbtt2csv.pl, bench/ltl2tgba/ltl2baw.in,
bench/ltl2tgba/parseout.pl: Delete these scripts, no
longer needed.
* configure.ac: Do not output ltl2baw.pl anymore.
2013-01-06 18:57:50 +01:00
Thomas Badie
242386b19a Add missing dependencies to the ltl2tgba benchmark Makefile.
* bench/ltl2tgba/Makefile.am (run): Remove wfair.txt.
(small.txt, big.txt, known.txt) Add a dependency to ltl2tgba.
2012-08-21 14:31:23 +02:00
Thomas Badie
3acc53d55a Add a bench script for the output of `lbtt'.
* bench/ltl2tgba/lbtt2csv.pl: Write a perl script to change the
format outputted by `lbtt' into a csv format.
* bench/ltl2tgba/Makefile.am: Add the script to EXTRA_DIST.
2012-06-20 14:04:57 +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
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