From 56ed13a96da724e35a57c674d183153272f0b472 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 7 Jan 2015 19:30:13 +0100 Subject: [PATCH] org: factor headers into setup.org * 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. --- doc/Makefile.am | 1 + doc/org/autfilt.org | 5 ++--- doc/org/csv.org | 5 ++--- doc/org/dstar2tgba.org | 5 ++--- doc/org/genltl.org | 5 ++--- doc/org/ioltl.org | 5 ++--- doc/org/ltl2tgba.org | 5 ++--- doc/org/ltl2tgta.org | 5 ++--- doc/org/ltlcross.org | 5 ++--- doc/org/ltlfilt.org | 5 ++--- doc/org/ltlgrind.org | 5 ++--- doc/org/oaut.org | 5 ++--- doc/org/randaut.org | 5 ++--- doc/org/randltl.org | 5 ++--- doc/org/satmin.org | 5 ++--- doc/org/setup.org | 3 +++ doc/org/tools.org | 3 +-- 17 files changed, 33 insertions(+), 44 deletions(-) create mode 100644 doc/org/setup.org diff --git a/doc/Makefile.am b/doc/Makefile.am index 08fcf79e3..60048e3d5 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -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 diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 5b7301d2f..7ddbc7592 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -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. diff --git a/doc/org/csv.org b/doc/org/csv.org index 5a64e6e11..16ea5102f 100644 --- a/doc/org/csv.org +++ b/doc/org/csv.org @@ -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. diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index ce5481ae7..ff22815bb 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -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. diff --git a/doc/org/genltl.org b/doc/org/genltl.org index dcefa1255..9105d61c4 100644 --- a/doc/org/genltl.org +++ b/doc/org/genltl.org @@ -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 diff --git a/doc/org/ioltl.org b/doc/org/ioltl.org index 988b7c614..9062cc4d0 100644 --- a/doc/org/ioltl.org +++ b/doc/org/ioltl.org @@ -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 diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index cca6caec8..3bb93a0ec 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -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 diff --git a/doc/org/ltl2tgta.org b/doc/org/ltl2tgta.org index d971f4f0f..30385484f 100644 --- a/doc/org/ltl2tgta.org +++ b/doc/org/ltl2tgta.org @@ -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. diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 1e73b087d..1442fb36a 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -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 diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index 8094c8686..2b8448732 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -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: diff --git a/doc/org/ltlgrind.org b/doc/org/ltlgrind.org index 44d9b6878..942e32d52 100644 --- a/doc/org/ltlgrind.org +++ b/doc/org/ltlgrind.org @@ -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 diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 5c6405b04..ad4dbf33f 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -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 diff --git a/doc/org/randaut.org b/doc/org/randaut.org index 828109201..7e23f2510 100644 --- a/doc/org/randaut.org +++ b/doc/org/randaut.org @@ -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. diff --git a/doc/org/randltl.org b/doc/org/randltl.org index dc2fe0cb9..11554315b 100644 --- a/doc/org/randltl.org +++ b/doc/org/randltl.org @@ -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 diff --git a/doc/org/satmin.org b/doc/org/satmin.org index d894c7909..143ecddd9 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -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. diff --git a/doc/org/setup.org b/doc/org/setup.org new file mode 100644 index 000000000..a0e242178 --- /dev/null +++ b/doc/org/setup.org @@ -0,0 +1,3 @@ +#+OPTIONS: H:2 num:nil toc:t +#+EMAIL: spot@lrde.epita.fr +#+HTML_LINK_HOME: http://spot.lip6.fr/ diff --git a/doc/org/tools.org b/doc/org/tools.org index 4f7645180..3a8fc3545 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -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