b2a5d5aa62
* src/bin/ltlcheck.cc: Add option --json and --csv. * src/bin/man/ltlcheck.x: Adjust examples. * src/tgbatest/ltlcheck.test: Do not output any statistic. * src/tgbatest/ltlcheck2.test: Output both JSON and CSV stats.
56 lines
2.1 KiB
Text
56 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]
|
|
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 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.
|