f03ba4b56f
* src/bin/man/genltl.x, src/bin/man/ltlcheck.x, src/bin/man/ltlfilt.x, src/bin/man/randltl.x: Use .BR in the SEE ALSO section.
59 lines
2.1 KiB
Text
59 lines
2.1 KiB
Text
[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 are
|
|
written to \f(CWresults.json\fR.
|
|
|
|
.nf
|
|
% randltl \-n100 \-\-tree\-size=20..30 a b c | \e
|
|
ltlcheck \-T120 'ltl2tgba \-s %f >%N' 'spin \-f %s >%N' \-\-json=results.json
|
|
.fi
|
|
.LP
|
|
|
|
The next command compare 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).
|
|
|
|
.nf
|
|
% ltlcheck \-F input.ltl \-\-csv=results.csv \e
|
|
'lbt <%L >%T' \e
|
|
'ltl3ba \-f %s >%N' \e
|
|
'ltl2tgba \-\-lbtt %f >%T'
|
|
.fi
|
|
.LP
|
|
|
|
If you use ltlcheck in an automated testsuite just to check for
|
|
potential problems, avoid the \fB\-\-csv\fR and \fB\-\-json\fR
|
|
options: ltlcheck is faster when it does not have to compute these
|
|
statistics.
|
|
|
|
[SEE ALSO]
|
|
.BR randltl (1),
|
|
.BR genltl (1),
|
|
.BR ltlfilt (1),
|
|
.BR 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 translations.
|
|
|
|
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.
|