cc498e7080
* doc/org/autcross.org, doc/org/autfilt.org, doc/org/citing.org, doc/org/compile.org, doc/org/concepts.org, doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/genaut.org, doc/org/genltl.org, doc/org/hierarchy.org, doc/org/hoa.org, doc/org/index.org, doc/org/install.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltlfilt.org, doc/org/ltlgrind.org, doc/org/ltlsynt.org, doc/org/oaut.org, doc/org/randaut.org, doc/org/randltl.org, doc/org/satmin.org, doc/org/tut.org, doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org, doc/org/tut04.org, doc/org/tut10.org, doc/org/tut11.org, doc/org/tut12.org, doc/org/tut20.org, doc/org/tut21.org, doc/org/tut22.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, doc/org/tut52.org, doc/org/tut90.org, doc/org/upgrade2.org: Run ispell-buffer on all these. * bin/autfilt.cc, python/spot/__init__.py: Fix typos in help texts noticed while spell-checking the org files.
65 lines
2.2 KiB
Org Mode
65 lines
2.2 KiB
Org Mode
# -*- coding: utf-8 -*-
|
|
#+TITLE: =genaut=
|
|
#+DESCRIPTION: Spot command-line tool that generates ω-automata from known patterns
|
|
#+INCLUDE: setup.org
|
|
#+HTML_LINK_UP: tools.html
|
|
#+PROPERTY: header-args:sh :results verbatim :exports both
|
|
|
|
This tool outputs ω-automata generated from scalable patterns.
|
|
|
|
These patterns are usually taken from the literature (see the
|
|
[[./man/genaut.1.html][=genaut=]](1) man page for references).
|
|
|
|
#+BEGIN_SRC sh :exports results
|
|
genaut --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d'
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
#+begin_example
|
|
--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.
|
|
--m-nba=RANGE An NBA with N+1 states whose determinization needs
|
|
at least N! states
|
|
#+end_example
|
|
|
|
|
|
By default, the output format is [[file:hoa.org][HOA]], but this can be controlled using
|
|
[[file:oaut.org][the common output options for automata.]]
|
|
|
|
For instance:
|
|
#+NAME: kscobuchi2
|
|
#+BEGIN_SRC sh :exports code
|
|
genaut --ks-nca=2 --dot
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC dot :file kscobuchi2.svg :var txt=kscobuchi2 :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:kscobuchi2.svg]]
|
|
|
|
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).
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
genaut --ks-nca=..5 --stats='%F=%L has %s states'
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
: 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
|
|
|
|
# LocalWords: utf genaut html args scalable SRC sed nca dsa nba svg
|
|
# LocalWords: kscobuchi txt
|