LTLCROSS

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

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

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 supplied 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 integer, 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 considered 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 notcheck 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:

%f,%s,%l,%w

the formula as a (quoted) string in Spot, Spin, LBT, or Wring’s syntax

%F,%S,%L,%W

the formula as a file in Spot, Spin, LBT, or Wring’s syntax

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 automatically. Likewise if %s or %S are used with atomic proposition that compatible 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 optionally be "infixed" by a bracketed sequence of operators to unabbreviate before outputing the formula. For instance %[MW]f will rewrite operators M and W before outputing 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 property 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 attempted 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 attempted up to 500 states.

-D, --determinize

always determinize non-deterministic automata so that theycan 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 averaged 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 alternating 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 instead of being truncated.

Miscellaneous options:

--version

print program version

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

Exit status:

SPOT_TMPDIR, TMPDIR

These variables control in which directory temporary files (e.g., those who contain the input and output when interfacing with translators) 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.

The following columns are output in the CSV or JSON files.
formula

The formula translated.

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 values:

"timeout"

The translator ran for more than the number of seconds specified 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.

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 (labeled 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 automaton 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 performed.

Until version 1.2.6, the output of translators was specifed using the following escape sequences.

Some development versions leading to 1.99.1 also featured

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. ltlcross officially supports only one output specifier:

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

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

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:

LBTT did not implement Test 2 described in this paper. ltlcross implements a slight variation: when an automaton produced by some translator is deterministic, 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 instance 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 Büchi acceptance. It supports Rabin and Streett automata via ltl2dstar’s format, and automata with arbitrary acceptance conditions via the HOA format.

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 potential 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 results.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 abbreviated -H.

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

Copyright © 2023 Laboratoire de Recherche de l’Epita (LRE) License GPLv3+: GNU GPL version 3 or later.
This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law.

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