alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

org: factor headers into setup.org

Browse source 
* doc/org/setup.org: New file.
* doc/Makefile.am: Distribute it.
* doc/org/autfilt.org, doc/org/csv.org, doc/org/dstar2tgba.org,
doc/org/genltl.org, doc/org/ioltl.org, doc/org/ltl2tgba.org,
doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltlfilt.org,
doc/org/ltlgrind.org, doc/org/oaut.org, doc/org/randaut.org,
doc/org/randltl.org, doc/org/satmin.org, doc/org/tools.org: Use
setup.org.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-07 19:30:13 +01:00
parent 15852b4e93
commit 56ed13a96d
17 changed files with 33 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

1
doc/Makefile.am
View file

@ -77,6 +77,7 @@ ORG_FILES = \
org/tools.org \
org/satmin.org \
org/satmin.tex \
org/setup.org \
$(srcdir)/org/satmin.png
$(srcdir)/org/satmin.png: org/satmin.tex

5
doc/org/autfilt.org
View file

@ -1,7 +1,6 @@
#+TITLE: =autfilt=
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
The =autfilt= tool can filter, transform, and convert a stream of automata.

5
doc/org/csv.org
View file

@ -1,7 +1,6 @@
#+TITLE: Reading and writing CSV files
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
This page discusses features available in Spot's command-line
tools to produce an consume CSV files.

5
doc/org/dstar2tgba.org
View file

@ -1,7 +1,6 @@
#+TITLE: =dstar2tgba=
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
This tool converts deterministic Rabin and Streett automata, presented
in [[http://www.ltl2dstar.de/docs/ltl2dstar.html][the format output by =ltl2dstar=]], into Büchi automata.

5
doc/org/genltl.org
View file

@ -1,7 +1,6 @@
#+TITLE: =genltl=
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
This tool generates LTL formulas according to scalable patterns.
These pattern are usually taken from the literature (see the man page

5
doc/org/ioltl.org
View file

@ -1,7 +1,6 @@
#+TITLE: Common input and output options for LTL/PSL formulas
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
Spot supports different syntaxes for LTL/PSL formulas. This page
documents the options, common to all tools where it makes sense, that

5
doc/org/ltl2tgba.org
View file

@ -1,7 +1,6 @@
#+TITLE: =ltl2tgba=
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
This tool translates LTL or PSL formulas into two kinds of Büchi
automata, or to monitors. The default is to output Transition-based

5
doc/org/ltl2tgta.org
View file

@ -1,7 +1,6 @@
#+TITLE: =ltl2tgta=
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
This tool generates various form of Testing Automata, i.e., automata
that observe the /changes/ of atomic propositions, not their values.

5
doc/org/ltlcross.org
View file

@ -1,7 +1,6 @@
#+TITLE: =ltlcross=
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
=ltlcross= is a tool for cross-comparing the output of LTL-to-Büchi
translators. It is actually a Spot-based clone of [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], the

5
doc/org/ltlfilt.org
View file

@ -1,7 +1,6 @@
#+TITLE: =ltlfilt=
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
This tool is a filter for LTL formulas. (It will also work with PSL
formulas.) It can be used to perform a number of tasks. Essentially:

5
doc/org/ltlgrind.org
View file

@ -1,7 +1,6 @@
#+TITLE: =ltlgrind=
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
This tool lists formulas that are similar to but simpler than a given
formula by applying simple mutations to it, like removing operands or

5
doc/org/oaut.org
View file

@ -1,7 +1,6 @@
#+TITLE: Common output options for automata
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
Spot supports different output syntaxes for automata. This page
documents the options, common to all tools where it makes sense, that

5
doc/org/randaut.org
View file

@ -1,7 +1,6 @@
#+TITLE: =randaut=
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
The =randaut= tool generates random (connected) automata.

5
doc/org/randltl.org
View file

@ -1,7 +1,6 @@
#+TITLE: =randltl=
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
This tool generates random formulas. By default, it will generate one
random LTL formula using atomic propositions supplied on the

5
doc/org/satmin.org
View file

@ -1,7 +1,6 @@
#+TITLE: SAT-based Minimization of Deterministic (Generalized) Büchi Automata
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html
#+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html
This page explains how to use [[file:ltl2tgba.org][=ltl2tgba=]] or [[file:dstar2tgba.org][=dstar2tgba=]] to minimize
deterministic automata using a SAT solver.

3
doc/org/setup.org Normal file
View file

@ -0,0 +1,3 @@
#+OPTIONS: H:2 num:nil toc:t
#+EMAIL: spot@lrde.epita.fr
#+HTML_LINK_HOME: http://spot.lip6.fr/

3
doc/org/tools.org
View file

@ -1,6 +1,5 @@
#+TITLE: Command-line tools installed by Spot 1.99
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+SETUPFILE: setup.org
This document introduces command-line tools that are installed with
the Spot library. We give some examples to highlight possible