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

%%: a single %
%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
%O: the automaton output in HOA, never claim, LBTT, or ltl2dstar's format

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:

--help: print this help
--version: print program version

Mandatory or optional arguments to long options are also mandatory or optional 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 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.

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

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

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

DEPRECATED OUTPUT SPECIFIERS

Until version 1.2.6, the output of translators was specifed using the following 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. ltlcross 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 suggest 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 Büchi automata. Int. J. on Software Tools for Technology Transfer. 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 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.

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

REPORTING BUGS

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

COPYRIGHT

Copyright © 2022 Laboratoire de Recherche et Développement de l'Epita. License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>.
This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law.