AUTCROSS

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.

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:

%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

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

expect that each tool complements the input language

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

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

--version

print program version

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

Exit status:

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.

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:

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

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

Copyright © 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)