genaut.org 2.16 KB
Newer Older
1
2
3
# -*- coding: utf-8 -*-
#+TITLE: =genaut=
#+DESCRIPTION: Spot command-line tool that generates ω-automata from known patterns
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
4
#+INCLUDE: setup.org
5
#+HTML_LINK_UP: tools.html
6
#+PROPERTY: header-args:sh :results verbatim :exports both
7
8
9
10
11
12

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

13
#+BEGIN_SRC sh :exports results
14
15
16
17
genaut --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d'
#+END_SRC

#+RESULTS:
18
19
20
21
22
23
24
25
26
27
28
29
30
#+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
31
32
33
34
35
36
37


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
38
#+BEGIN_SRC sh :exports code
39
genaut --ks-nca=2 --dot
40
41
#+END_SRC

42
#+BEGIN_SRC dot :file kscobuchi2.svg :var txt=kscobuchi2 :exports results
43
44
45
46
  $txt
#+END_SRC

#+RESULTS:
47
[[file:kscobuchi2.svg]]
48
49
50
51
52

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
53
#+BEGIN_SRC sh :results verbatim :exports both
54
genaut --ks-nca=..5 --stats='%F=%L has %s states'
55
56
57
#+END_SRC

#+RESULTS:
58
59
60
61
62
: 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
63
64
65

#  LocalWords:  utf genaut html args scalable SRC sed nca dsa nba svg
#  LocalWords:  kscobuchi txt