autwords
Table of Contents
autwords enumerates all lasso-shaped words accepted by an
ω-automaton. A lasso-shaped word is represented as a finite stem
followed by a finite cycle repeated infinitely, and is written as
STEM;cycle{CYCLE}.
The lengths of the stem and the cycle can be bounded using the
--stem=RANGE and --cycle=RANGE options (default: 0.. and
1..), and the number of words can be limited with
--max-count=N (or -n N). The --count (or -c) option
outputs only the number of found words.
Examples
The following command generates a Büchi automaton for GFa & GFb,
and enumerates the first three lasso-shaped accepted words:
ltl2tgba 'GFa & FGb' | autwords -n 3
a & b; cycle{a & b}
a & b; cycle{!a & b; a & b}
a & b; cycle{a & b; !a & b}
The next command counts the number of words that have a step of size 1 and a cycle size of at most 2.
ltl2tgba 'GFa & GFb' | autwords --stem=1 --cycle=1..2 -c
40
If the automaton has an empty language, autwords silently exits with
status 1:
ltl2tgba 'GFa & G!a' | autwords; echo "exit: $?"
exit: 1