FreeBSD Manual Pages
AUTCROSS(1) User Commands AUTCROSS(1) 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 follow- ing character sequences: %% a single % %H,%S,%L filename for the input automaton in (H) HOA, (S) Spin's never- claim, 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 sup- ported 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 out- put) --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_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 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 au- tomata. input.nondeterministic,output.nondetstates 1 if the automaton is nondeterministic, 0 if it is determinis- tic. 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 fol- lowing 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 al- ways 0. "timeout" The tool ran for more than the number of seconds speci- fied 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 sec- onds. This is reported for all executions, even failling ones. 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 randaut(1), genaut(1), autfilt(1), ltlcross(1) autcross (spot) 2.12.1 September 2024 AUTCROSS(1)
NAME | SYNOPSIS | DESCRIPTION | ENVIRONMENT VARIABLES | OUTPUT DATA | REPORTING BUGS | COPYRIGHT | SEE ALSO
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=autcross&sektion=1&manpath=FreeBSD+Ports+14.3.quarterly>