From 868cabe4f62caa740bca48eddfe78926c8c779cc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 13 Aug 2015 15:56:00 +0200 Subject: [PATCH] * src/bin/man/ltlcross.x: Document %N, %T, %H. --- src/bin/man/ltlcross.x | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/src/bin/man/ltlcross.x b/src/bin/man/ltlcross.x index 0e59de5d9..d2352b70e 100644 --- a/src/bin/man/ltlcross.x +++ b/src/bin/man/ltlcross.x @@ -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 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] .BR randltl (1), .BR genltl (1),