Commit 4334abde authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

org: Fix UP links and center them on the page.

* doc/org/init.el.in: Center links.
* 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/randltl.org,
doc/org/satmin.org: Fix links.  Reported by Akim Demaille.
parent c2195600
#+TITLE: Reading and writing CSV files
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: file:tools.html
#+LINK_UP: tools.html
This page discusses features available in Spot's command-line
tools to produce an consume CSV files.
......
#+TITLE: =dstar2tgba=
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: file:tools.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.
......
#+TITLE: =genltl=
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: file:tools.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
......
......@@ -20,6 +20,11 @@
(setq org-babel-sh-command
(concat "PATH=@abs_top_builddir@/src/bin" path-separator "$PATH sh"))
(setq org-export-html-home/up-format
"<div id=\"org-div-home-and-up\" style=\"text-align:center;white-space:nowrap;\">
<a accesskey=\"h\" href=\"%s\">UP</a> | <a accesskey=\"H\" href=\"%s\">HOME</a>
</div>")
(setq org-publish-project-alist
'(("spot-html"
:base-directory "@abs_top_srcdir@/doc/org/"
......
#+TITLE: Common input and output options for LTL/PSL formulas
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: file:tools.html
#+LINK_UP: tools.html
Spot supports different syntaxes for LTL/PSL formulas. This pages
document the options, common to all tools where it makes sense, that
......
#+TITLE: =ltl2tgba=
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: file:tools.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
......
#+TITLE: =ltl2tgta=
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: file:tools.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.
......
#+TITLE: =ltlcross=
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: file:tools.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
......
#+TITLE: =ltlfilt=
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: file:tools.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:
......
#+TITLE: =randltl=
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: file:tools.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
......
#+TITLE: SAT-based Minimization of Deterministic (Generalized) Büchi Automata
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: file:tools.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.
......
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