Commit 22aba2c4 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

genaut: add missing documentation

* bin/man/genaut.x, doc/org/genaut.org: New files.
* bin/man/Makefile.am, doc/Makefile.am: Add them.
* doc/org/tools.org, bin/man/randaut.x, bin/man/randltl.x,
bin/man/genltl.x: Link to them.
parent d9022f79
## -*- coding: utf-8 -*-
## Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
## Développement de l'Epita (LRDE).
## Copyright (C) 2012-2017 Laboratoire de Recherche et Développement
## de l'Epita (LRDE).
##
## This file is part of Spot, a model checking library.
##
......@@ -27,6 +27,7 @@ convman7 = ARGP_HELP_FMT=header-col=0 $(SHELL) "$(x_to_1)" \
dist_man1_MANS = \
autfilt.1 \
dstar2tgba.1 \
genaut.1 \
genltl.1 \
ltl2tgba.1 \
ltl2tgta.1 \
......@@ -64,6 +65,9 @@ ltldo.1: $(common_dep) $(srcdir)/ltlcross.x $(srcdir)/../ltldo.cc
ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc
$(convman) ../ltlfilt$(EXEEXT) $(srcdir)/ltlfilt.x $@
genaut.1: $(common_dep) $(srcdir)/genaut.x $(srcdir)/../genaut.cc
$(convman) ../genaut$(EXEEXT) $(srcdir)/genaut.x $@
genltl.1: $(common_dep) $(srcdir)/genltl.x $(srcdir)/../genltl.cc
$(convman) ../genltl$(EXEEXT) $(srcdir)/genltl.x $@
......
[NAME]
genaut \- generate ω-automata from scalable patterns
[DESCRIPTION]
.\" Add any additional description here
[BIBLIOGRAPHY]
Prefixes used in pattern names refer to the following papers:
.TP
ks
D. Kuperberg, M. Skrzypczak: On Determinisation of Good-for-Games
Automata. Proceddings of ICALP'15.
[SEE ALSO]
.BR autfilt (1),
.BR genltl (1),
.BR randaut (1),
.BR randltl (1)
......@@ -63,4 +63,7 @@ D. Tabakov and M. Y. Vardi: Optimized Temporal Monitors for SystemC.
Proceedings of RV'10. LNCS 6418.
[SEE ALSO]
.BR genaut (1),
.BR ltlfilt (1),
.BR randaut (1),
.BR randltl (1)
......@@ -3,5 +3,7 @@ randaut \- generate random automata
[DESCRIPTION]
.\" Add any additional description here
[SEE ALSO]
.BR genltl (1),
.BR genaut (1),
.BR randltl (1),
.BR autfilt (1)
......@@ -10,6 +10,7 @@ we suggest you cite the following paper:
Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0.
Proceedings of ATVA'13. LNCS 8172.
[SEE ALSO]
.BR genaut (1),
.BR genltl (1),
.BR ltlfilt (1),
.BR randaut (1)
......@@ -84,6 +84,7 @@ ORG_FILES = \
org/compile.org \
org/concepts.org \
org/dstar2tgba.org \
org/genaut.org \
org/genltl.org \
org/hoa.org \
org/hierarchy.org \
......
# -*- 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:
: --ks-cobuchi=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.
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
genaut --ks-cobuchi=2 --dot
#+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).
#+BEGIN_SRC sh :results verbatim :exports code
genaut --ks-cobuchi=..5 --stats='%F=%L has %s states'
#+END_SRC
#+RESULTS:
: ks-cobuchi=1 has 3 states
: ks-cobuchi=2 has 5 states
: ks-cobuchi=3 has 7 states
: ks-cobuchi=4 has 9 states
: ks-cobuchi=5 has 11 states
......@@ -50,6 +50,7 @@ corresponding commands are hidden.
- [[file:dstar2tgba.org][=dstar2tgba=]] Convert \omega-automata with any acceptance into
variants of Büchi automata.
- [[file:randaut.org][=randaut=]] Generate random \omega-automata.
- [[file:genaut.org][=genaut=]] Generate ω-automata from scalable patterns.
- [[file:autfilt.org][=autfilt=]] Filter, convert, and transform \omega-automata.
- [[file:ltldo.org][=ltldo=]] Run LTL/PSL formulas through other tools using common [[file:ioltl.org][input]]
and [[file:oaut.org][output]] interfaces.
......@@ -64,11 +65,13 @@ convenience, you can browse their HTML versions:
[[./man/autfilt.1.html][=autfilt=]](1),
[[./man/dstar2tgba.1.html][=dstar2tgba=]](1),
[[./man/genaut.1.html][=genaut=]](1),
[[./man/genltl.1.html][=genltl=]](1),
[[./man/ltl2tgba.1.html][=ltl2tgba=]](1),
[[./man/ltl2tgta.1.html][=ltl2tgta=]](1),
[[./man/ltlcross.1.html][=ltlcross=]](1),
[[./man/ltldo.1.html][=ltldo=]](1),
[[./man/ltlgrind.1.html][=ltlgrind=]](1),
[[./man/ltlfilt.1.html][=ltlfilt=]](1),
[[./man/randaut.1.html][=randaut=]](1),
[[./man/randltl.1.html][=randltl=]](1),
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment