genaut.org 1.91 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
# -*- coding: utf-8 -*-
#+TITLE: =genaut=
#+DESCRIPTION: Spot command-line tool that generates ω-automata from known patterns
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html

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 :results verbatim :exports results
genaut --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d'
#+END_SRC

#+RESULTS:
17
:       --ks-nca=RANGE         A co-Büchi automaton with 2N+1 states for which
18 19
:                              any equivalent deterministic co-Büchi automaton
:                              has at least 2^N/(2N+1) states.
20 21 22
:       --l-dsa=RANGE          A deterministic Streett automaton with 4N states
:                              with no equivalent deterministic Rabin automaton
:                              of less than n! states.
23 24 25
:       --l-nba=RANGE          A Büchi automaton with 3N+1 states whose
:                              complementary Streett automaton needs at least n!
:                              states.
26 27 28 29 30 31 32 33


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 :results verbatim :exports code
34
genaut --ks-nca=2 --dot
35 36 37 38 39 40 41 42 43 44 45 46 47
#+END_SRC

#+BEGIN_SRC dot :file kscobuchi2.png :cmdline -Tpng :var txt=kscobuchi2 :exports results
  $txt
#+END_SRC

#+RESULTS:
[[file:kscobuchi2.png]]

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
48
#+BEGIN_SRC sh :results verbatim :exports both
49
genaut --ks-nca=..5 --stats='%F=%L has %s states'
50 51 52
#+END_SRC

#+RESULTS:
53 54 55 56 57
: 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