Commit graph

443 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
4334abdeed org: Fix UP links and center them on the page.
* doc/org/init.el.in: Center links.
* doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/genltl.org,
doc/org/ioltl.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org,
doc/org/ltlcross.org, doc/org/ltlfilt.org, doc/org/randltl.org,
doc/org/satmin.org: Fix links.  Reported by Akim Demaille.
2014-02-06 22:28:37 +01:00
Alexandre Duret-Lutz
17dd281b33 * doc/org/ltlfilt.org: Typo, reported by Fabrice Kordon. 2014-02-04 07:58:52 +01:00
Alexandre Duret-Lutz
35612f3626 Release Spot 1.2.2
* NEWS, configure.ac, doc/org/tools.org: Set version to 1.2.2.
2014-01-24 11:16:07 +01:00
Alexandre Duret-Lutz
4d7638a269 Release Spot 1.2.1.
* NEWS, configure.ac, doc/org/tools.org: Bump version to 1.2.1.
2013-12-11 10:40:33 +01:00
Alexandre Duret-Lutz
846e33b9e5 ltl2tgba: Add a --csv-escape option and document CSV I/O.
* src/bin/common_output.cc, src/bin/common_output.hh:
(output_formula_checked, aut_stat_printer): New.
* src/bin/genltl.cc, src/bin/randltl.cc, src/bin/ltlfilt.cc: Call
output_formula_checked() instead of output_formula().
* src/bin/ltl2tgba.cc: Use aut_stat_printer and add option --csv-escape.
* doc/org/csv.org: New file to document CSV I/O.
* doc/Makefile.am: Add it.
* doc/org/ioltl.org, doc/org/ltlfilt.org, doc/org/ltl2tgba.org,
doc/org/tools.org: Link to csv.org
2013-12-06 11:09:36 +01:00
Alexandre Duret-Lutz
8c5875314c * doc/org/satmin.org: Typo 2013-12-06 11:09:11 +01:00
Alexandre Duret-Lutz
d719c706f4 ltlcross: report statistics about Rabin and Streett automata
* src/bin/ltlcross.cc: Implement it.
* src/bin/man/ltlcross.x, doc/org/ltlcross.org, NEWS: Document it.
* src/tgbatest/ltl2dstar.test, src/tgbatest/ltlcross3.test: Test it.
2013-11-22 08:59:13 +01:00
Alexandre Duret-Lutz
2b10745dfb ltlcross: support --products=+N
* src/bin/ltlcross.cc: Implement it.
* NEWS, doc/org/ltlcross.org: Document it.
* src/tgbatest/ltlcross3.test: Test it.
2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
3e3d320de5 doc: add suggestions for bibliographic references
* doc/org/tools.org, src/bin/man/genltl.x, src/bin/man/ltl2tgba.x,
src/bin/man/ltl2tgta.x, src/bin/man/ltlcross.x, src/bin/man/ltlfilt.x,
src/bin/man/randltl.x: Add bibliographic references, mostly to
the ATVA'13 paper.
2013-11-22 02:13:57 +01: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
7de25a32ef ltlcross: support short names
* NEWS: Mention it.
* doc/org/ltlcross.org: Document it.
* src/bin/ltlcross.cc: Implement it.
* src/tgbatest/Makefile.am, src/tgbatest/defs.in,
src/tgbatest/ltlcross4.test: Test it.
2013-11-22 02:13:57 +01:00
Alexandre Duret-Lutz
925a807f4f * doc/org/ltlcross.org: Show how to call ltl3dra and fix typos. 2013-11-22 02:07:13 +01:00
Alexandre Duret-Lutz
2cda03f8ce * doc/org/ltlcross.org: Typos, reported by František Blahoudek. 2013-11-11 18:51:12 +01:00
Alexandre Duret-Lutz
54c01cfcdf * doc/org/ltlfilt.org: Typo. 2013-10-11 17:52:37 +02:00
Alexandre Duret-Lutz
c0a845b274 Release Spot 1.2.
* NEWS, configure.ac, doc/org/tools.org: Bump version to 1.2.
2013-10-01 13:23:47 +02:00
Alexandre Duret-Lutz
87b65b9bce relabel: implement relabeling of Boolean subexpressions.
* src/ltlast/multop.cc, src/ltlast/multop.hh (multop::boolean_operands,
multop::boolean_count): New methods.
* src/ltlvisit/relabel.cc, src/ltlvisit/relabel.hh
(relabel): Take an optional relabeling_map as parameter.
(relabel_bse): New.
* src/ltltest/ltlrel.test, src/ltltest/ltlrel.cc: New files.
* src/ltltest/Makefile.am: Add them.
* src/bin/ltlfilt.cc: Add option --relabel-bool.
* src/ltltest/ltlfilt.test: Test it.
* NEWS: Mention it.
* doc/org/ltlfilt.org: Illustrate it.
2013-09-28 09:02:30 +02:00
Alexandre Duret-Lutz
ce5ea829bd tools: Add a --format option
* src/bin/common_output.cc: Add option --format and implement
it.
* src/bin/ltlfilt.cc, src/bin/randltl.cc: Document the
supported %-sequences.
* src/bin/genltl.cc: Document the %-sequences, and supply
the name of the pattern to output_formula().
* doc/org/genltl.org, doc/org/ioltl.org, doc/org/ltlfilt.org,
NEWS: Document it.
* src/ltltest/latex.test: Use it.
2013-09-22 23:56:56 +02:00
Alexandre Duret-Lutz
3076c3da4e org: document SAT-based minimization
* doc/org/satmin.org, doc/org/satmin.tex: New files.
* doc/Makefile.am: Add them.
* doc/org/tools.org: Point to satmin.org.
* NEWS: Mention satmin.html.
2013-09-16 08:39:06 +02:00
Alexandre Duret-Lutz
1ab46b0864 postproc: Add option to output Complete automata.
* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Tweak set_pref()
to also accept Any|Complete, Small|Complete, or Deterministic|Complete.
* src/bin/common_post.hh, src/bin/common_post.cc: Add option --complete
and set comp.
* src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc: Pass
comp to set_pref().
* src/tgbaalgos/complete.cc: Preserve state-based acceptance.
* src/tgbatest/dstar.test, src/tgbatest/ltlcross2.test,
src/tgbatest/nondet.test: Augment tests.
* doc/org/dstar2tgba.org, doc/org/ltl2tgba.org, NEWS: Document.
2013-09-08 20:43:52 +02:00
Alexandre Duret-Lutz
1029d08a77 ltlcross: Complement deterministic automata.
* src/bin/ltlcross.cc: Complement deterministic automata,
and use them for additional intersection checks.
* NEWS, doc/org/ltlcross.org, src/bin/man/ltlcross.x: Document it.
2013-08-26 17:27:42 +02:00
Alexandre Duret-Lutz
f704513b6b org: document dstar2tgba.
* doc/org/dstar2tgba.org: New file.
* doc/org/tools.org: Link to it.
* doc/Makefile.am: Distribute it.
* NEWS: Mention the generated web page.
2013-08-26 17:27:39 +02:00
Alexandre Duret-Lutz
d3b81809c8 dstar2tgba: new command.
* src/bin/dstar2tgba.cc, src/bin/man/dstar2tgba.x: New files.
* src/bin/Makefile.am, src/bin/man/Makefile.am: Add them.
* NEWS: Mention it.
* src/bin/ltl2tgba.cc, src/tgbaalgos/stats.cc, doc/org/ltl2tgba.org:
Rename the %S sequence as %c, for consistency with dstar2tgba.
* src/tgbatest/ltl2dstar.test: Add more tests.
* src/tgbatest/ltl2dstar2.test: New file.
* src/tgbatest/Makefile.am: Add it.
2013-08-23 17:02:30 +02:00
Alexandre Duret-Lutz
e7522056ca ltlcross: give an example of accepted word for nonempty cross-products
* src/tgbaalgos/word.cc, src/tgbaalgos/word.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbatest/ltlcrossce.test: New file.
* src/tgbatest/Makefile.am: Add it.
* src/bin/ltlcross.cc: Compute and display an accepted word
for nonempty cross-products.
* NEWS, doc/org/ltlcross.org: Document it.
2013-07-29 01:14:38 +02:00
Alexandre Duret-Lutz
9d6d53ed92 Release Spot 1.1.4.
* NEWS, configure.ac, doc/org/tools.org: Update version.
2013-07-29 00:27:59 +02:00
Alexandre Duret-Lutz
00bf8d1641 * doc/org/ioltl.org: Typos. 2013-07-09 21:08:28 +02:00
Alexandre Duret-Lutz
026830d159 Release Spot 1.1.3.
* configure.ac, doc/org/tools.org, NEWS: Set version to 1.1.3.
2013-07-09 14:03:07 +02:00
Alexandre Duret-Lutz
372a086cb7 Improve ltlfilt.org
* doc/org/ltlfilt.org: Mention that the --stutter-invariant check
use automata.  Fix a typo.
2013-06-09 18:55:57 +02:00
Alexandre Duret-Lutz
424f04ca11 Release Spot 1.1.2.
* configure.ac, NEWS, doc/org/tools.org: Bump version to 1.1.2.
2013-06-09 18:05:20 +02:00
Alexandre Duret-Lutz
27a18a0410 Release Spot 1.1.1
* NEWS, configure.ac, doc/org/tools.org: Bump version.
2013-05-13 16:20:29 +02:00
Alexandre Duret-Lutz
5a6b50acbb org: Augment the load-path.
* doc/org/init.el.in: Add emacs-goodies-el to the load-path, so that
org-mode has a better chance to find htmlize.
2013-05-13 16:12:32 +02:00
Alexandre Duret-Lutz
b457e78fb0 * doc/org/ltlfilt.org: Add an example with --stutter-invariant. 2013-05-13 16:10:09 +02:00
Alexandre Duret-Lutz
54b25b8c8e ltlcross: more documentation
* doc/org/ltlcross.org: Describe statistics, and mention --products=N.
2013-05-13 16:09:50 +02:00
Alexandre Duret-Lutz
556ba6df9e Release Spot 1.1
* configure.ac, doc/org/tools.org: Bump version number.
* NEWS: Likewise, plus some missing entries.
2013-04-28 16:31:20 +02:00
Alexandre Duret-Lutz
ea3a66cace * doc/org/ltl2tgba.org: Typo. 2013-04-28 00:23:11 +02:00
Alexandre Duret-Lutz
fec939c1a6 ltlcross: count SCCs of various strenghts
* src/bin/ltlcross.cc: Implement the counters.
* doc/org/ltlcross.org: Update the documentation.
* bench/ltl2tgba/sum.py: Do not assume a fixed column for the time.
* NEWS: Update.
2013-04-27 20:33:51 +02:00
Alexandre Duret-Lutz
ba6fe9e183 * doc/org/init.el.in: Disable org-publish-use-timestamps-flag. 2013-04-26 11:49:06 +02:00
Alexandre Duret-Lutz
69dcff5ab0 org: Make sure ../../src/bin is searched first.
We used to set PATH in emacs, but because babel executes "sh" via
shell-command, the configuration of the main shell may supersedes ours.

* doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org,
doc/org/ltlfilt.org, doc/org/randltl.org, doc/org/tools.org,
doc/org/genltl.org: Move all local-file variable to...
* doc/org/.dir-locals.el: ... here.  And also set the PATH
in org-babel-sh-command.
* doc/org/init.el.in: Set the PATH in org-babel-sh-command.
2013-04-11 19:02:45 +02:00
Alexandre Duret-Lutz
1f4e035147 * doc/org/ioltl.org: Fix link to ltl2dstar. 2013-04-09 15:05:56 +02:00
Alexandre Duret-Lutz
e23203b819 org: batch-generate userdoc/ and distribute it
* doc/org/init.el.in, doc/org/syntax.css: New files.
* configure.ac: Generate init.el from init.el.in, and check for
emacs.
* doc/Makefile.am: Build userdoc/ from org/ and distribute userdoc/.
* README: Mention org/ and userdoc/.
2013-04-09 15:05:56 +02:00
Alexandre Duret-Lutz
c24270bbf5 org: upgrade to 1.0.2
* doc/org/tools.org: Update to 1.0.2.
* doc/org/ltl2tgba.org: Mention monitors in the intro.
2013-04-09 15:05:56 +02:00
Alexandre Duret-Lutz
d1ad744887 org: update for 1.0.1
* doc/org/ioltl.org: Mention ltl2dstar and the changes to the prefix
parser.
* doc/org/ltlcross.org: Mention bench/ltl2tgba/sum.py.
* doc/org/tools.org: Bump version number.
2013-04-09 15:05:56 +02:00
Alexandre Duret-Lutz
152a46b961 Add a .dir-locals.el for org files.
* doc/org/.dir-locals.el: New files.
* doc/Makefile.am (EXTRA_DIST): Distribute it.
2013-04-09 15:05:56 +02:00
Alexandre Duret-Lutz
345b8c5b14 doc: add org-mode documentation for user tools
* doc/org/.gitignore, doc/org/genltl.org, doc/org/ioltl.org,
doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org,
doc/org/ltlfilt.org, doc/org/randltl.org, doc/org/tools.org: New files.
2013-04-09 15:05:56 +02:00