NAME

autcross - cross-compare tools that process automata

SYNOPSIS

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

DESCRIPTION

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.

Input:

-F, --file=FILENAME: process automata from FILENAME

Specifying tools to call:

--list-shorthands: 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 %
%H,%S,%L: 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
%O: filename for the automaton output in HOA, never claim, LBTT, or ltl2dstar's format

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.

autcross behavior:

--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
--language-preserved: expect that each tool preserves the input language
--no-checks: do not perform any sanity checks
--stop-on-error: stop on first execution error or failure to pass sanity checks (timeouts are OK)

Statistics 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)
--omit-missing: do not output statistics for timeouts or failed translations

Simplification level (for complementation):

--high: all available optimizations (slow, default)
--low: minimal optimizations (fast)
--medium: moderate optimizations

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)
-q, --quiet: suppress all normal output in absence of errors
--save-bogus=[>>]FILENAME: save automata for which problems were detected in FILENAME
--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 tools failed to output something we understand, or failed sanity checks (statistics were output nonetheless)
2: autcross 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 files.

input.source: Location of the input automaton fed to the tool.
input.name: Name of the input automaton, if any. This is supported by the HOA format.
input.ap,output.ap,: Number of atomic proposition in the input and output automata.
input.states,output.states: Number of states in the input and output automata.
input.edges,output.edges: Number of edges in the input and output automata.
input.transitions,output.transitions: Number of transitions in the input and output automata.
input.acc_sets,output.acc_sets: Number of acceptance sets in the input and output automata.
input.scc,output.scc: Number of strongly connected components in the input and output automata.
input.nondetstates,output.nondetstates: Number of nondeterministic states in the input and output automata.
input.nondeterministic,output.nondetstates: 1 if the automaton is nondeterministic, 0 if it is deterministic.
input.alternating,output.alternating: 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:

"ok": 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.
"timeout": 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.
"signal": 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.

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

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.