FreeBSD Manual Pages

home | help

LTLCROSS(1) User Commands LTLCROSS(1)

NAME
ltlcross - cross-compare LTL/PSL translators to omega-automata

SYNOPSIS
ltlcross [OPTION...] [COMMANDFMT...]

DESCRIPTION
Call several LTL/PSL translators and cross-compare their output to detect
bugs, or to gather statistics. The list of formulas to use should be sup-
plied on standard input, or using the -f or -F options.

Input options:
-f, --formula=STRING
process the formula STRING

-F, --file=FILENAME[/COL]
process each line of FILENAME as a formula; if COL is a positive in-
teger, assume a CSV file and read column COL; use a negative COL to
drop the first line of the CSV file

--lbt-input
read all formulas using LBT's prefix syntax

--lenient
parenthesized blocks that cannot be parsed as subformulas are con-
sidered as atomic properties

Specifying translators to call:
--list-shorthands
list availabled shorthands to use in COMMANDFMT

--reference=COMMANDFMT register one translator and assume it is correct
(do not check it for error, but use it to check other translators)

--relabel
always relabel atomic propositions before calling any translator

-t, --translator=COMMANDFMT
register one translator to call

-T, --timeout=NUMBER
kill translators after NUMBER seconds

COMMANDFMT should specify input and output arguments using the following
character sequences:

%% a single %

%f,%s,%l,%w
the formula as a (quoted) string in Spot, Spin, LBT, or Wring's syn-
tax

%F,%S,%L,%W
the formula as a file in Spot, Spin, LBT, or Wring's syntax

%O the automaton output in HOA, never claim, LBTT, or ltl2dstar's for-
mat

If either %l, %L, or %T are used, any input formula that does not use
LBT-style atomic propositions (i.e. p0, p1, ...) will be relabeled automat-
ically. Likewise if %s or %S are used with atomic proposition that compat-
ible with Spin's syntax. You can force this relabeling to always occur
with option --relabel. The sequences %f,%s,%l,%w,%F,%S,%L,%W can option-
ally be "infixed" by a bracketed sequence of operators to unabbreviate be-
fore outputting the formula. For instance %[MW]f will rewrite operators M
and W before outputting it. Furthermore, if COMMANDFMT has the form
"{NAME}CMD", then only CMD will be passed to the shell, and NAME will be
used to name the tool in the output.

Parsing of automata:
--trust-hoa=BOOL
If false, properties listed in HOA files are ignored, unless they
can be easily verified. If true (the default) any supported prop-
erty is trusted.

ltlcross behavior:
--allow-dups
translate duplicate formulas in input

--determinize-max-edges=N
attempt to determinize non-deterministic automata so they can be
complemented, unless the deterministic automaton would have more
than N edges. Without this option or -D, determinizations are at-
tempted up to 5000 edges.

--determinize-max-states=N
attempt to determinize non-deterministic automata so they can be
complemented, unless the deterministic automaton would have more
than N states. Without this option or -D, determinizations are at-
tempted up to 500 states.

-D, --determinize
always determinize non-deterministic automata so that they can be
complemented; also implicitly sets --products=0

--fail-on-timeout
consider timeouts as errors

--ignore-execution-failures
ignore automata from translators that return with a non-zero exit
code, but do not flag this as an error

--no-checks
do not perform any sanity checks (negated formulas will not be
translated)

--no-complement
do not complement deterministic automata to perform extra checks

--stop-on-error
stop on first execution error or failure to pass sanity checks
(timeouts are OK)

State-space generation:
--density=FLOAT
probability, between 0.0 and 1.0, to add a transition between two
states (0.1 by default)

--products=[+]INT
number of products to perform (1 by default), statistics will be av-
eraged unless the number is prefixed with '+'

--seed=INT
seed for the random number generator (0 by default)

--states=INT
number of the states in the state-spaces (200 by default)

Statistics output:
--ambiguous, --unambiguous
output statistics about ambiguous automata [not supported for alter-
nating automata]

--automata
store automata (in the HOA format) into the CSV or JSON output

--csv[=[>>]FILENAME]
output statistics as CSV in FILENAME or on standard output (if '>>'
is used to request append mode, the header line is not output)

--json[=[>>]FILENAME]
output statistics as JSON in FILENAME or on standard output

--omit-missing
do not output statistics for timeouts or failed translations

--strength
output statistics about SCC strengths (non-accepting, terminal,
weak, strong) [not supported for alternating automata]

Output options:
--color[=WHEN]
colorize output; WHEN can be 'never', 'always' (the default if
--color is used without argument), or 'auto' (the default if --color
is not used)

--grind=[>>]FILENAME
for each formula for which a problem was detected, write a simpler
formula that fails on the same test in FILENAME

-q, --quiet
suppress all normal output in absence of error

--save-bogus=[>>]FILENAME
save formulas for which problems were detected in FILENAME

--save-inclusion-products=[>>]FILENAME
save automata representing products built to check inclusion between
automata

--verbose
print what is being done, for debugging

If an output FILENAME is prefixed with '>>', it is open in append mode in-
stead of being truncated.

Miscellaneous options:
--help
print this help

--version
print program version

Mandatory or optional arguments to long options are also mandatory or op-
tional for any corresponding short options.

Exit status:
0 everything went fine (without --fail-on-timeout, timeouts are OK)

1 some translator failed to output something we understand, or failed
sanity checks (statistics were output nonetheless)

2 ltlcross aborted on error

ENVIRONMENT VARIABLES
SPOT_TMPDIR, TMPDIR
These variables control in which directory temporary files (e.g.,
those who contain the input and output when interfacing with trans-
lators) are created. TMPDIR is only read if SPOT_TMPDIR does not
exist. If none of these environment variables exist, or if their
value is empty, files are created in the current directory.

SPOT_TMPKEEP
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.

formula
The formula translated.

tool The tool used to translate this formula. This is either the value
of the full COMMANDFMT string specified on the command-line, or, if
COMMANDFMT has the form {SHORTNAME}CMD, the value of SHORTNAME.

exit_status, exit_code
Information about how the execution of the translator went. If the
option --omit-missing is given, these two columns are omitted and
only the lines corresponding to successful translation are output.
Otherwise, exit_status is a string that can take the following val-
ues:

"ok" The translator ran succesfully (this does not imply that the
produced automaton is correct) and ltlcross could parse the
resulting automaton. In this case exit_code is always 0.

"timeout"
The translator ran for more than the number of seconds speci-
fied with the --timeout option. In this case exit_code is
always -1.

"exit code"
The translator terminated with a non-zero exit code.
exit_code contains that value.

"signal"
The translator terminated with a signal. exit_code contains
that signal's number.

"parse error"
The translator terminated normally, but ltlcross could not
parse its output. In this case exit_code is always -1.

"no output"
The translator terminated normally, but without creating the
specified output file. In this case exit_code is always -1.

time A floating point number giving the run time of the translator in
seconds. This is reported for all executions, even failling ones.

Unless the --omit-missing option is used, data for all the following
columns might be missing.

states, edges, transitions, acc
The number of states, edges, transitions, and acceptance sets in the
translated automaton. Column edges counts the number of edges (la-
beled by Boolean formulas) in the automaton seen as a graph, while
transitions counts the number of assignment-labeled transitions that
might have been merged into a formula-labeled edge. For instance an
edge labeled by true will be counted as 2^3=8 transitions if the au-
tomaton uses 3 atomic propositions.

scc, nonacc_scc, terminal_scc, weak_scc, strong_scc
The number of strongly connected components in the automaton. The
scc column gives the total number, while the other columns only
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).

nondet_states, nondet_aut
The number of nondeterministic states, and a Boolean indicating
whether the automaton is nondeterministic.

terminal_aut, weak_aut, strong_aut
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).

product_states, product_transitions, product_scc
Size of the product between the translated automaton and a randomly
generated state-space. For a given formula, the same state-space is
of course used the result of each translator. When the --products=N
option is used, these values are averaged over the N products per-
formed.

DEPRECATED OUTPUT SPECIFIERS
Until version 1.2.6, the output of translators was specifed using the fol-
lowing escape sequences.

%N An output file containing a never claim.

%T An output file in lbtt's format.

%D An output file in ltl2dstar's format.

Some development versions leading to 1.99.1 also featured

%H An output file in the HOA format.

Different specifiers were needed because Spot implemented different parsers
for these formats. Nowadays, these parsers have been merged into a single
parser that is able to distinguish these four formats automatically. ltl-
cross officially supports only one output specifier:

%O An output file in either lbtt's format, ltl2dstar's format, as a
never claim, or in the HOA format

For backward compatibility, the sequences %D, %H, %N, and %T, are still
supported (as aliases for %O), but are deprecated.

BIBLIOGRAPHY
If you would like to give a reference to this tool in an article, we sug-
gest you cite the following paper:

* Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0.
Proceedings of ATVA'13. LNCS 8172.

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.

The sanity checks performed on the result of each translator (by either
LBTT or ltlcross) are described in the following paper:

* H. Tauriainen and K. Heljanko: Testing LTL formula translation into
BA1/4chi automata. Int. J. on Software Tools for Technology Trans-
fer. Volume 4, number 1, October 2002.

LBTT did not implement Test 2 described in this paper. ltlcross implements
a slight variation: when an automaton produced by some translator is deter-
ministic, its complement is built and used for additional cross-comparisons
with other tools. If the translation P1 of the positive formula and the
translation N1 of the negative formula both yield deterministic automata
(this may only happen for obligation properties) then the emptiness check
of Comp(P1)*Comp(N1) is 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 in-
stance checking the emptiness of Comp(P1)*P2.

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.

Another major difference with LBTT is that ltlcross is not restricted to
generalized BA1/4chi acceptance. It supports Rabin and Streett automata
via ltl2dstar's format, and automata with arbitrary acceptance conditions
via the HOA format.

EXAMPLES
The following commands compare never claims produced by ltl2tgba(1),
spin(1), and lbt for 100 random formulas, using a timeout of 2 minutes.
Because 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 poten-
tial issue detected, is reported on standard error, while statistics are
written to results.json.

% randltl -n100 --tree-size=20..30 a b c | \
ltlcross -T120 ltl2tgba spin lbt --json=results.json

The next command compares lbt, ltl3ba, and ltl2tgba(1) on a set of formulas
saved in file input.ltl. Statistics are again writen as CSV into re-
sults.csv. This examples specify the input and output for each tool, to
show how this can be done. Note the use of %L to indicate that the formula
passed t for the formula in spin(1)'s format, and %f 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.

% ltlcross -F input.ltl --csv=results.csv \
'lbt <%L >%O' \
'ltl3ba -f %s >%O' \
'ltl2tgba -H %f >%O'

Rabin or Streett automata output by ltl2dstar in its historical format can
be read from a file specified with %D instead of %O. For instance:

% ltlcross -F input.ltl \
'ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds %L %D' \
'ltl2dstar --automata=streett --ltl2nba=spin:ltl2tgba@-Ds %L %D' \

However, we now recommand to use the HOA output of ltl2dstar, as supported
since version 0.5.2:

% ltlcross -F input.ltl \
'ltl2dstar --output-format=hoa --ltl2nba=spin:ltl2tgba@-Ds %L %O' \
'ltl2dstar --output-format=hoa --automata=streett --ltl2nba=spin:ltl2tgba@-Ds %L %O' \

In more recent versions of ltl2dstar, --output-format=hoa can be abbrevi-
ated -H.

REPORTING BUGS
Report bugs to <spot@lrde.epita.fr>.

COPYRIGHT
Copyright (C) 2025 by the Spot authors, see the AUTHORS File for details.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/li-
censes/gpl.html>.
This is free software: you are free to change and redistribute it. There
is NO WARRANTY, to the extent permitted by law.

SEE ALSO
randltl(1), genltl(1), ltlfilt(1), ltl2tgba(1), ltldo(1)

ltlcross (spot) 2.14.5 January 2026 LTLCROSS(1)

Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=ltlcross&sektion=1&manpath=FreeBSD+Ports+15.1.quarterly>

home | help

Header And Logo

Peripheral Links

Site Navigation

FreeBSD Manual Pages

Header And Logo

Peripheral Links

Search

Site Navigation

FreeBSD Manual Pages