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.
process automata from FILENAME
list availabled shorthands to use in COMMANDFMT
register one tool to call
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
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
If false, properties listed in HOA files are ignored, unless they can be easily verified. If true (the default) any supported property is trusted.
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)
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
all available optimizations (slow, default)
minimal optimizations (fast)
colorize output; WHEN can be ’never’, ’always’ (the default if --color is used without argument), or ’auto’ (the default if --color is not used)
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.
print this help
print program version
Mandatory or optional arguments to long options are also mandatory or optional for any corresponding short options.
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.
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.
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.
The tool terminated normally, but autcross could not parse its output. In this case exit_code is always -1.
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 <email@example.com>.
© 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.
randaut(1), genaut(1), autfilt(1), ltlcross(1)