Table of Contents


autcross - cross-compare tools that process automata


autcross [OPTION...] [COMMANDFMT...]


Call several tools that process automata and cross-compare their output to detect bugs, or to gather statistics. The list of automata to use should be supplied on standard input, or using the -F option.


-F, --file=FILENAME

process automata from FILENAME

Specifying tools to call:


list availabled shorthands to use in COMMANDFMT

-t, --tool=COMMANDFMT

register one tool to call

-T, --timeout=NUMBER

kill tools after NUMBER seconds

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


a single %


filename for the input automaton in (H) HOA, (S) Spin’s neverclaim, or (L) LBTT’s format

%M, %[val]M

the name of the input automaton, with an optional default value


filename for the automaton output in HOA, never claim, LBTT, or ltl2dstar’s format

Parsing of automata:


If false, properties listed in HOA files are ignored, unless they can be easily verified. If true (the default) any supported property is trusted.

autcross behavior:


consider timeouts as errors


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


expect that each tool complements the input language


expect that each tool preserves the input language


do not perform any sanity checks


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

Statistics output:


output statistics as CSV in FILENAME or on standard output (if ’>>’ is used to request append mode, the header line is not output)


do not output statistics for timeouts or failed translations

Simplification level (for complementation):


all available optimizations (slow, default)


minimal optimizations (fast)


moderate optimizations

Output options:


colorize output; WHEN can be ’never’, ’always’ (the default if --color is used without argument), or ’auto’ (the default if --color is not used)

-q, --quiet

suppress all normal output in absence of errors


save automata for which problems were detected in FILENAME


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:


print this help


print program version

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

Exit status:


everything went fine (without --fail-on-timeout, timeouts are OK)


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


autcross aborted on error



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.


When this variable is defined, temporary files are not removed. This is mostly useful for debugging.


The following columns are output in the CSV files.

Location of the input automaton fed to the tool.


Name of the input automaton, if any. This is supported by the HOA format.


Number of atomic proposition in the input and output automata.


Number of states in the input and output automata.


Number of edges in the input and output automata.


Number of transitions in the input and output automata.


Number of acceptance sets in the input and output automata.


Number of strongly connected components in the input and output automata.


Number of nondeterministic states in the input and output automata.


1 if the automaton is nondeterministic, 0 if it is deterministic.


1 if the automaton has some universal branching, 0 otherwise.

exit_status, exit_code Information about how the execution of the tool went. exit_status is a string that can take the following values:


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


The tool ran for more than the number of seconds specified with the --timeout option. In this case exit_code is always -1.

"exit code"

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


The tool terminated with a signal. exit_code contains that signal’s number.

"parse error"

The tool terminated normally, but autcross could not parse its output. In this case exit_code is always -1.

"no output"

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


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


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


Copyright © 2024 by the Spot authors, see the AUTHORS File for details. 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.


randaut(1), genaut(1), autfilt(1), ltlcross(1)