AUTWORDS

autwords \- enumerate lasso-shaped words accepted by omega-automata

autwords [OPTION...] [FILENAME...]

autwords reads omega-automata and enumerates accepted words that have a lasso shape: a finite stem followed by a finite cycle that repeats forever. The lengths of the stem and cycle can be bounded using the --stem and --cycle options.

Enumerate lasso-shaped accepted words of ω-automata, printing one word per line.

Input:

-F, --file=FILENAME

process the automaton in FILENAME

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

Lasso-size bounds:

--cycle=RANGE

restrict cycle length to RANGE (default: 1..)

--stem=RANGE

restrict stem length to RANGE (default: 0..)

RANGE may have one of the following forms: ’INT’, ’INT..INT’, ’..INT’, or ’INT..’

Output options:

-c, --count

print only a count of words per automaton (may not terminate if the size of the words is not restrictued)

-n, --max-count=NUM

stop after outputting NUM words per automaton

-o, --output=FILENAME

write output to FILENAME instead of standard output

Miscellaneous:

--version

print program version

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

Exit status:

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

Copyright © 2026 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.

ltl2tgba(1), autfilt(1), autdo(1), autcross(1)