diff --git a/bin/man/Makefile.am b/bin/man/Makefile.am index a4dcbfdbe..bbf314adf 100644 --- a/bin/man/Makefile.am +++ b/bin/man/Makefile.am @@ -1,6 +1,6 @@ ## -*- 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 $@ diff --git a/bin/man/genaut.x b/bin/man/genaut.x new file mode 100644 index 000000000..0035b7faa --- /dev/null +++ b/bin/man/genaut.x @@ -0,0 +1,16 @@ +[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) diff --git a/bin/man/genltl.x b/bin/man/genltl.x index 74fcfb4f2..5935f4c2d 100644 --- a/bin/man/genltl.x +++ b/bin/man/genltl.x @@ -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) diff --git a/bin/man/randaut.x b/bin/man/randaut.x index e71a60309..ecd32ffb4 100644 --- a/bin/man/randaut.x +++ b/bin/man/randaut.x @@ -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) diff --git a/bin/man/randltl.x b/bin/man/randltl.x index c3167fecf..cce4714fb 100644 --- a/bin/man/randltl.x +++ b/bin/man/randltl.x @@ -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) diff --git a/doc/Makefile.am b/doc/Makefile.am index 5dbe70a30..220ab4b36 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -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 \ diff --git a/doc/org/genaut.org b/doc/org/genaut.org new file mode 100644 index 000000000..a2d8f51a3 --- /dev/null +++ b/doc/org/genaut.org @@ -0,0 +1,51 @@ +# -*- 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 diff --git a/doc/org/tools.org b/doc/org/tools.org index 1b4aadb4c..9c9339c5c 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -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),