From 7b6337f456efc6d25b593e93a3416b13c14e6d3f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 14 Oct 2012 17:37:26 +0200 Subject: [PATCH] ltlcheck: Add a man page. * src/bin/man/ltlcheck.x: New file. * src/bin/man/Makefile.am: Add it. * src/bin/ltlcheck.cc: Arrange help text. --- src/bin/ltlcheck.cc | 13 ++++++------- src/bin/man/Makefile.am | 12 +++++++++++- src/bin/man/ltlcheck.x | 43 +++++++++++++++++++++++++++++++++++++++++ 3 files changed, 60 insertions(+), 8 deletions(-) create mode 100644 src/bin/man/ltlcheck.x diff --git a/src/bin/ltlcheck.cc b/src/bin/ltlcheck.cc index f65c5cb93..ae7dee06d 100644 --- a/src/bin/ltlcheck.cc +++ b/src/bin/ltlcheck.cc @@ -64,17 +64,12 @@ const char argp_program_doc[] ="\ Call several LTL/PSL translators and cross-compare their output to detect \ bugs, or to gather statistics. The list of formulas to use should be \ supplied on standard input, or using the -f or -F options.\v\ -Examples:\n\ - Compare neverclaims produced by ltl2tgba and spin for 100 random formulas,\n\ - limiting runtime to 2 minutes:\n\ - % randltl -n100 --tree-size=20..30 a b c | \\\n\ - ltlcheck -T120 'ltl2tgba -s %f > %N' 'spin -f %s > %N' > results.json \n\ -\n\ Exit status:\n\ 0 everything went fine (timeouts are OK too)\n\ 1 some translator failed to output something we understand, or failed\n\ sanity checks (statistics were output nonetheless)\n\ - 2 ltlcheck aborted on error\n"; + 2 ltlcheck aborted on error\n\ +"; #define OPT_STATES 1 @@ -97,6 +92,10 @@ static const argp_option options[] = "the formula as a file in Spot, Spin, or LBT's syntax", 0 }, { "%N,%T", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "the output automaton as a Never claim, or in LBTT's format", 0 }, + { 0, 0, 0, 0, + "If either %l, %L, or %T are used, any input formula that does " + "not use LBT-style atomic propositions (i.e. p0, p1, ...) will be " + "relabeled automatically.", 0 }, /**************************************************/ { 0, 0, 0, 0, "State-space generation:", 4 }, { "states", OPT_STATES, "INT", 0, diff --git a/src/bin/man/Makefile.am b/src/bin/man/Makefile.am index 72bb7b905..9fa95657c 100644 --- a/src/bin/man/Makefile.am +++ b/src/bin/man/Makefile.am @@ -22,7 +22,14 @@ x_to_1 = $(top_builddir)/tools/x-to-1 convman = ARGP_HELP_FMT=header-col=0 $(SHELL) "$(x_to_1)" \ "$(PERL)" "$(top_srcdir)/tools/help2man -N -L 'en_US.UTF-8'" -dist_man1_MANS = ltlfilt.1 genltl.1 randltl.1 ltl2tgba.1 ltl2tgta.1 +dist_man1_MANS = \ + genltl.1 \ + ltl2tgba.1 \ + ltl2tgta.1 \ + ltlcheck.1 \ + ltlfilt.1 \ + randltl.1 + MAINTAINERCLEANFILES = $(dist_man1_MANS) EXTRA_DIST = $(dist_man1_MANS:.1=.x) @@ -32,6 +39,9 @@ ltl2tgba.1: $(common_dep) $(srcdir)/ltl2tgba.x $(srcdir)/../ltl2tgba.cc ltl2tgta.1: $(common_dep) $(srcdir)/ltl2tgta.x $(srcdir)/../ltl2tgta.cc $(convman) ../ltl2tgta$(EXEEXT) $(srcdir)/ltl2tgta.x $@ +ltlcheck.1: $(common_dep) $(srcdir)/ltlcheck.x $(srcdir)/../ltlcheck.cc + $(convman) ../ltlcheck$(EXEEXT) $(srcdir)/ltlcheck.x $@ + ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc $(convman) ../ltlfilt$(EXEEXT) $(srcdir)/ltlfilt.x $@ diff --git a/src/bin/man/ltlcheck.x b/src/bin/man/ltlcheck.x new file mode 100644 index 000000000..523667179 --- /dev/null +++ b/src/bin/man/ltlcheck.x @@ -0,0 +1,43 @@ +[NAME] ltlcheck \- translate LTL/PSL formulas into Büchi automata +[DESCRIPTION] +.\" Add any additional description here +[EXAMPLES] +The following commands compare never claims produced by ltl2tgba(1) +and spin(1) and 100 random formulas, using a timeout of 2 minutes. A +trace of the execution of the two tools, including any potential issue +detected, is reported on standard error, while statistics gathered +(normally sent to standard output) are redicted to \f(CWresults.json\fR. + +\f(CW% randltl -n100 --tree-size=20..30 a b c | \e +.br +ltlcheck -T120 'ltl2tgba -s %f > %N' 'spin -f %s > %N' > results.json\fR + +The next command compare lbt, ltl3ba, and ltl2tgba(1) on a set of +formulas saved in file \f(CWinput.ltl\fR. Statistis are again +redirected to \f(CWresults.json\fR. Note the use of \f(CW%L\fR to +indicate that the LBT formula should be written into a file, and +\f(CW%T\fR to read the output in LBTT's format (which is a superset of +the format output by LBT). + +\f(CW% ltlcheck -F input.ltl 'lbt < %L > %T' 'ltl2tgba --lbtt %f > %T'\fR + +[SEE ALSO] +randltl(1), genltl(1), ltlfilt(1), ltl2tgba(1) + +[BIBLIOGRAPHY] +ltlcheck is a Spot-based reimplementation of a tool called LBTT. LBTT +was developped by Heikki Tauriainen at the Helsinki University of +Technology. The main motivation for the reimplementation was to +support PSL, and output more statistics about the translation. + +The sanity checks performed on the result of each translator (by +either LBTT or ltlcheck) are described in the following paper. Our +implementation will detect and reports problems (like inconsistencies +between two translations) but unlike LBTT it does not offer an +interactive mode to investigate such problems. + +.TP +th02 +H. Tauriainen and K. Heljanko: Testing LTL formula translation into +Büchi automata. Int. J. on Software Tools for Technology Transfer. +Volume 4, number 1, October 2002.