Commit 7b6337f4 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent b2de0136
......@@ -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,
......
......@@ -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 $@
......
[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.
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