Examples small enough to be solved by hand
Small problems and their solutions
The following automata are all non-empty with some generic acceptance condition. The first column (problem) show the automata as marked graphs. The fourth column (solution) highlight highlight one accepting lasso (i.e., an accepting cycle with a prefix that connect it to the initial state). There is no guarantee that the accepting cycle is unique.
Sources
The rest of this page discuss the source of these examples.
Source in HOA format
The aut{1-25}.hoa files contain the corresponding automaton definition in HOA format.
To build autN.pdf and autN-acc.pdf from autN.hoa, do:
autfilt autN.hoa --dot='barf(Lato)g' | dot -T pdf > autN.pdf autfilt autN.hoa --highlight-accepting-run=5 --dot='barf(Lato)g' | dot -T pdf > autN-acc.pdf
The --dot=g and --highlight-accepting-run options are new in Spot 2.8.
Sources as a product
All these automata where randomly generated as the product of two non-empty random automata, with constraints on the number of states and acceptance conditions listed below.
| automata | left operand | right operand |
|---|---|---|
| 1-5 | 4-state Streett-2 | 4-state Rabin-2 |
| 6-10 | 5-state Streett-2 | 5-state Rabin-2 |
| 11-15 | 5-state random 8 | 5-state parity min odd 8 |
| 16-25 | 5-state random 8 | 5-state parity min even 8 |
The random 8 acceptance used in the last 15 automata allows
repetitions.
Those two sources automata are stored in aut{1-25}-src.hoa.
The right operand appears befor the left operand in this file.
autN.hoa can be regenerated from autN-src.hoa as follows:
autfilt -Hl autN-src.hoa | sed 1d | autfilt - --product autN-src.hoa > autN.hoa
The combination of autfilt -Hl to display one automaton per line and
sed 1d to delete the first line, actually outputs the second
automaton and pipe it to the last autfilt that performs a
--product with the first automaton in autN-src.hoa.
The product operand used were generated with different constraints:
Refresh
The following script regenerates all files using the commands described above.
for N in `seq 1 25`; do autfilt -Hl aut$N-src.hoa | sed 1d | autfilt - --product aut$N-src.hoa > aut$N.hoa autfilt aut$N.hoa --dot='barf(Lato)g' | dot -T pdf > aut$N.pdf autfilt aut$N.hoa --highlight-accepting-run=5 --dot='barf(Lato)g' | dot -T pdf > aut$N-acc.pdf done