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

* src/bin/man/ltlcross.x: Document %N, %T, %H.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2015-08-13 15:56:00 +02:00
parent 546304eabc
commit 868cabe4f6
1 changed files with 38 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -200,6 +200,44 @@ of course used the result of each translator. When the
\fB\-\-products\fR=\fIN\fR option is used, these values are averaged \fB\-\-products\fR=\fIN\fR option is used, these values are averaged
over the \fIN\fR products performed. over the \fIN\fR products performed.
[DEPRECATED OUTPUT SPECIFIERS]
Until version 1.2.6, the output of translators was specifed using the
following escape sequences.
.PP
.TP
%N
An output file containing a never claim.
.TP
%T
An output file in \fBlbtt\fR's format.
.TP
%D
An output file in \fBltl2dstar\fR's format.
.PP
Some development versions leading to 1.99.1 also featured
.PP
.TP
%H
An output file in the HOA format.
.PP
Different specifiers were needed because Spot implemented
different parsers for these formats. Nowadays, the parsers
for never claims, lbtt's format, and HOA format have been merged into
a single parser that is able to distinguish these three formats
automatically.
.B ltlcross
officially supports only two output specifiers
.TP
%O
An output file in either \fBlbtt\fR's format, as a never claim,
or in the HOA format
.TP
%D
An output file in \fBltl2dstar\fR's format.
.P
For backward compatibility, the sequences %N, %T, and %H are still
supported (as aliases for %O), but are deprecated.
[SEE ALSO] [SEE ALSO]
.BR randltl (1), .BR randltl (1),
.BR genltl (1), .BR genltl (1),