FreeBSD Manual Pages
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 de- tect 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 transla- tors) --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 follow- ing 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 au- tomatically. 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 se- quence of operators to unabbreviate before 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 sup- ported 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 out- put) --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 sim- pler 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 be- tween 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_TM- PDIR does not exist. If none of these environment variables ex- ist, or if their value is empty, files are created in the cur- rent 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 omit- ted 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 con- tains 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 al- ways -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 recog- nize 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 ran- domly 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 au- tomatically. 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 Tech- nology. 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 Bchi 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 imple- ments 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 posi- tive 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 re- sult of another translators, for instance checking the emptiness of Comp(P1)*P2. Our implementation will detect and reports problems (like inconsisten- cies between two translations) but unlike LBTT it does not offer an in- teractive mode to investigate such problems. Another major difference with LBTT is that ltlcross is not restricted to generalized Bchi acceptance. It supports Rabin and Streett automata via ltl2dstar's format, and automata with arbitrary acceptance condi- tions 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 sta- tistics 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 for- mulas 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 sup- ported 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 abbre- viated -H. REPORTING BUGS Report bugs to <spot@lrde.epita.fr>. COPYRIGHT Copyright (C) 2024 by the Spot authors, see the AUTHORS File for de- tails. 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.12.1 September 2024 LTLCROSS(1)
NAME | SYNOPSIS | DESCRIPTION | ENVIRONMENT VARIABLES | OUTPUT DATA | DEPRECATED OUTPUT SPECIFIERS | BIBLIOGRAPHY | EXAMPLES | REPORTING BUGS | COPYRIGHT | SEE ALSO
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=ltlcross&sektion=1&manpath=FreeBSD+Ports+14.3.quarterly>