61602a3bba
Suggested in #299. * doc/org/autfilt.org, doc/org/concepts.org, doc/org/dstar2tgba.org, doc/org/genaut.org, doc/org/hierarchy.org, doc/org/hoa.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/oaut.org, doc/org/randaut.org, doc/org/satmin.org, doc/org/tut11.org, doc/org/tut23.org, doc/org/tut24.org, doc/org/tut30.org, doc/org/tut31.org, doc/org/tut50.org, doc/org/tut51.org: Adjust all dot outputs to produce svg. * doc/org/arch.tex, doc/org/hierarchy.tex, doc/org/satmin.tex: Adjust to produce a pdf with 12pt text. * doc/Makefile.am: Adjust the generation of arch.svg, hierarchy.svg, and satmin.svg: From above. * doc/org/.dir-locals.el.in, doc/org/init.el.in: Adjust dot arguments to produce svg with 12pt text (the default was 14pt). * doc/org/spot.css: Use Lato as the main font for consistency with automata. * HACKING: pdf2svg is now required to build the doc.
1.9 KiB
1.9 KiB
genaut
This tool outputs ω-automata generated from scalable patterns.
These patterns are usually taken from the literature (see the
genaut(1) man page for references).
--ks-nca=RANGE A co-Büchi automaton with 2N+1 states for which
any equivalent deterministic co-Büchi automaton
has at least 2^N/(2N+1) states.
--l-dsa=RANGE A deterministic Streett automaton with 4N states
with no equivalent deterministic Rabin automaton
of less than n! states.
--l-nba=RANGE A Büchi automaton with 3N+1 states whose
complementary Streett automaton needs at least n!
states.
By default, the output format is HOA, but this can be controlled using the common output options for automata.
For instance:
genaut --ks-nca=2 --dot
The patterns can be specified using a range of the form N (a single
value), N..M (all values between N and M included), or ..M (all
values between 1 and M included).
genaut --ks-nca=..5 --stats='%F=%L has %s states'ks-nca=1 has 3 states ks-nca=2 has 5 states ks-nca=3 has 7 states ks-nca=4 has 9 states ks-nca=5 has 11 states