alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

man: improve typesetting and prepare for html output

Browse source 
* src/bin/man/autfilt.x, src/bin/man/dstar2tgba.x,
src/bin/man/ltl2tgba.x, src/bin/man/ltlcross.x,
src/bin/man/ltlgrind.x, src/bin/man/randltl.x, src/bin/man/spot-x.x:
Improve typesetting and cross-references.
* tools/help2man: Adjust to better detect the optional arguments.
Detect options that are not separated from their description by two
spaces.  Argp output some of those.
* tools/man2html.pl: New file.
* Makefile.am: Distribute it.
* src/bin/ltlfilt.cc: Fix description of --define.
* src/bin/ltlgrind.cc: Fix duplicate description for --help and
--version.  Reorder --help output slightly.
* NEWS: Mention the few fixes.
This commit is contained in:
Alexandre Duret-Lutz 2015-08-12 19:13:45 +02:00
parent 5b75ad5abd
commit f7b65001e9
13 changed files with 290 additions and 159 deletions
Download patch file Download diff file Expand all files Collapse all files

158
src/bin/man/ltlcross.x
View file

@ -1,58 +1,89 @@
.\" -*- coding: utf-8 -*-
[NAME]
ltlcross \- cross-compare LTL/PSL translators to 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 are
written to \f(CWresults.json\fR.
The following commands compare never claims produced by
.BR ltl2tgba (1),
.BR spin (1),
and
.B lbt
for 100 random formulas, using a timeout of 2 minutes. Because
.B ltlcross
knows those tools, there is no need to specify their input and
output. A trace of the execution of the two tools, including any
potential issue detected, is reported on standard error, while
statistics are written to \f(CWresults.json\fR.
.PP
.in +4n
.nf
.ft C
% randltl \-n100 \-\-tree\-size=20..30 a b c | \e
ltlcross \-T120 'ltl2tgba \-s %f >%N' 'spin \-f %s >%N' \-\-json=results.json
ltlcross \-T120 ltl2tgba spin lbt \-\-json=results.json
.fi
.LP
The next command compares lbt, ltl3ba, and ltl2tgba(1) on a set of
formulas saved in file \f(CWinput.ltl\fR. Statistics are again writen
as CSV into \f(CWresults.csv\fR. Note the use of \f(CW%L\fR to
indicate that the formula passed to lbt should be written into a file
in LBT's format, and \f(CW%T\fR to read the output in LBTT's format
(which is a superset of the format output by LBT).
.PP
The next command compares
.BR lbt ,
.BR ltl3ba ,
and
.BR ltl2tgba (1)
on a set of formulas saved in file \f(CWinput.ltl\fR.
Statistics are again writen
as CSV into \f(CWresults.csv\fR. This examples specify the
input and output for each tool, to show how this can be done.
Note the use of \f(CW%L\fR to indicate that the formula passed t
for the formula in
.BR spin (1)'s
format, and \f(CW%f\fR for the
formula in Spot's format. Each of these tool produces an
automaton in a different format (respectively, LBTT's format,
Spin's never claims, and HOA format), but Spot's parser can
distinguish and understand these three formats.
.PP
.in +4n
.nf
.ft C
% ltlcross \-F input.ltl \-\-csv=results.csv \e
'lbt <%L >%T' \e
'ltl3ba \-f %s >%N' \e
'ltl2tgba \-\-lbtt %f >%T'
'lbt <%L >%O' \e
'ltl3ba \-f %s >%O' \e
'ltl2tgba \-H %f >%O'
.fi
.LP
Rabin or Streett automata output by ltl2dstar can be read from a
file specified with \f(CW%D\fR. For instance:
.PP
Rabin or Streett automata output by
.B ltl2dstar
can be read from a
file specified with \f(CW%D\fR instead of \f(CW%O\fR. For instance:
.PP
.in +4n
.nf
.ft C
% ltlcross \-F input.ltl \e
'ltl2dstar \-\-ltl2nba=spin:path/ltl2tgba@\-s %L %D' \e
'ltl2dstar \-\-automata=streett \-\-ltl2nba=spin:path/ltl2tgba@\-s %L %D' \e
'ltl2dstar \-\-ltl2nba=spin:ltl2tgba@\-s %L %D' \e
'ltl2dstar \-\-automata=streett \-\-ltl2nba=spin:ltl2tgba@\-s %L %D' \e
.fi
.LP
However because Spot only supports Büchi acceptance, these Rabin and
.PP
However, for historical reasons these Rabin and
Streett automata are immediately converted to TGBA before further
processing by ltlcross. This is still interesting to search for bugs
processing by
.BR ltlcross .
This is still interesting to search for bugs
in translators to Rabin or Streett automata, but the statistics might
not be very relevant.
not be very relevant. If statistics matters to you and you do not want
this conversion to occur, use the HOA format to interface with ltl2dstar:
.PP
.in +4n
.nf
.ft C
% ltlcross \-F input.ltl \e
'ltl2dstar \-\-output\-format=hoa \-\-ltl2nba=spin:ltl2tgba@\-s %L %O' \e
'ltl2dstar \-\-output\-format=hoa \-\-automata=streett \-\-ltl2nba=spin:ltl2tgba@\-s %L %O' \e
.fi
.PP
If you use ltlcross in an automated testsuite just to check for
potential problems, avoid the \fB\-\-csv\fR and \fB\-\-json\fR
options: ltlcross is faster when it does not have to compute these
statistics.
[ENVIRONMENT VARIABLES]
.TP
\fBSPOT_TMPDIR\fR, \fBTMPDIR\fR
These variables control in which directory temporary files (e.g.,
@ -61,28 +92,22 @@ translators) are created. \fBTMPDIR\fR is only read if
\fBSPOT_TMPDIR\fR does not exist. If none of these environment
variables exist, or if their value is empty, files are created in the
current directory.
.TP
\fBSPOT_TMPKEEP\fR
When this variable is defined, temporary files are not removed.
This is mostly useful for debugging.
[OUTPUT DATA]
The following columns are output in the CSV or JSON files.
.TP 7
.TP
\fBformula\fR
The formula translated.
.TP
\fBtool\fR
The tool used to translate this formula. This is either the value of the
full \fICOMMANDFMT\fR string specified on the command-line, or,
if \fICOMMANDFMT\fR has the form \f(CW{\fISHORTNAME\fR\f(CW}\fR\FiCMD\fR,
if \fICOMMANDFMT\fR has the form \f(CW{\fISHORTNAME\fR\f(CW}\fR\fICMD\fR,
the value of \fISHORTNAME\fR.
.TP
\fBexit_status\fR, \fBexit_code\fR
Information about how the execution of the translator went. If the
@ -90,60 +115,51 @@ option \fB\-\-omit\-missing\fR is given, these two columns are omitted
and only the lines corresponding to successful translation are output.
Otherwise, \fBexit_status\fR is a string that can take the following
values:
.RS
.TP
\f(CW"ok"\fR
The translator ran succesfully (this does not imply that the produced
automaton is correct) and ltlcross could parse the resulting
automaton. In this case \fBexit_code\fR is always 0.
.TP
\f(CW"timeout"\fR
The translator ran for more than the number of seconds
specified with the \fB\-\-timeout\fR option. In this
case \fBexit_code\fR is always -1.
.TP
\f(CW"exit code"\fR
The translator terminated with a non-zero exit code.
\fBexit_code\fR contains that value.
.TP
\f(CW"signal"\fR
The translator terminated with a signal.
\fBexit_code\fR contains that signal's number.
.TP
\f(CW"parse error"\fR
The translator terminated normally, but ltlcross could not
parse its output. In this case \fBexit_code\fR is always -1.
.TP
\f(CW"no output"\fR
The translator terminated normally, but without creating the specified
output file. In this case \fBexit_code\fR is always -1.
.RE
.TP
\fBtime\fR
A floating point number giving the run time of the translator in seconds.
This is reported for all executions, even failling ones.
.PP
Unless the \fB\-\-omit\-missing\fR option is used, data for all the
following columns might be missing.
.TP
\fBin_type\fR, \fBin_states\fR, \fBin_edges\fR, \fBin_transitions\fR, \fBin_acc\fR , \fBin_scc\fR
These columns are only output if \f(CW%D\fR appears in any command
specification, i.e., if any of the tools output some Streett or Rabin
automata. In this case \fBin_type\fR contains a string that is either
\f(CWDRA\fR (Deterministic Rabin Automaton) or \f(CWDSA\fR
(Deterministic Streett Automaton). The other columns respectively
give the number of states, edges, transitions, acceptance pairs, and
strongly connected components in that automaton.
\fBin_type\fR, \fBin_states\fR, \fBin_edges\fR, \fBin_transitions\fR,
\fBin_acc\fR , \fBin_scc\fR These columns are only output if
\f(CW%D\fR appears in any command specification, i.e., if any of the
tools output some Streett or Rabin automata. In this case
\fBin_type\fR contains a string that is either \f(CWDRA\fR
(Deterministic Rabin Automaton) or \f(CWDSA\fR (Deterministic Streett
Automaton). The other columns respectively give the number of states,
edges, transitions, acceptance pairs, and strongly connected
components in that automaton.
.TP
\fBstates\fR, \fBedges\fR, \fBtransitions\fR, \fBacc\fR
The number of states, edges, transitions, and acceptance sets in the
@ -153,13 +169,12 @@ translated automaton. Column \fBedges\fR counts the number of edges
that might have been merged into a formula-labeled edge. For instance
an edge labeled by \f(CWtrue\fR will be counted as 2^3=8 transitions if
the automaton mention 3 atomic propositions.
.PP
If the translator produced a Streett or Rabin automaton, these columns
contains the size of a TGBA (or BA) produced by ltlcross from that
Streett or Rabin automaton. Check \fBin_states\fR, \fBin_edges\fR,
\fBin_transitions\fR, and \fBin_acc\fR for statistics about the actual
input automaton.
.TP
\fBscc\fR, \fBnonacc_scc\fR, \fBterminal_scc\fR, \fBweak_scc\fR, \fBstrong_scc\fR
The number of strongly connected components in the automaton. The
@ -168,18 +183,15 @@ count the SCCs that are non-accepting (a.k.a. transiant), terminal
(recognizes and accepts all words), weak (do not recognize all words,
but accepts all recognized words), or strong (accept some words, but
reject some recognized words).
.TP
\fBnondet_states\fR, \fBnondet_aut\fR
The number of nondeterministic states, and a Boolean indicating whether the
automaton is nondeterministic.
.TP
\fBterminal_aut\fR, \fBweak_aut\fR, \fBstrong_aut\fR
Three Boolean used to indicate whether the automaton is terminal (no
weak nor strong SCCs), weak (some weak SCCs but no strong SCCs), or strong
(some strong SCCs).
.TP
\fBproduct_states\fR, \fBproduct_transitions\fR, \fBproduct_scc\fR
Size of the product between the translated automaton and a randomly
@ -198,18 +210,21 @@ over the \fIN\fR products performed.
[BIBLIOGRAPHY]
If you would like to give a reference to this tool in an article,
we suggest you cite the following paper:
.PP
.TP
\(bu
Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0.
Proceedings of ATVA'13. LNCS 8172.
.PP
ltlcross is a Spot-based reimplementation of a tool called LBTT. LBTT
.B ltlcross
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 translations.
.PP
The sanity checks performed on the result of each translator (by
either LBTT or ltlcross) are described in the following paper:
.PP
.TP
\(bu
H. Tauriainen and K. Heljanko: Testing LTL formula translation into
@ -227,7 +242,12 @@ equivalent to Test 2 of Tauriainen and Heljanko. If only one
automaton is deterministic, say P1, it can still be used to check we
can be used to check the result of another translators, for instance
checking the emptiness of Comp(P1)*P2.
.PP
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.
.PP
Another major difference with LBTT is that ltlcross is
not restricted to generalized Büchi acceptance. It supports
Rabin and Streett automata via ltl2dstar's format, and automata
with arbitrary acceptance conditions via the HOA format.