From a8f02ed8ca9cfbd90ae3c64214a568c54e6065ba Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 7 Jun 2015 16:49:53 +0200 Subject: [PATCH] org: add an index page * doc/org/index.org, doc/org/tut.org: New files. * doc/Makefile.am: Add them. * doc/org/setup.org: Adjust HOME link. * doc/org/tools.org: Adjust UP link. * debian/spot-doc.doc-base: The root is now index.html. --- debian/spot-doc.doc-base | 2 +- doc/Makefile.am | 2 ++ doc/org/index.org | 47 ++++++++++++++++++++++++++++++++++++++++ doc/org/setup.org | 2 +- doc/org/tools.org | 1 + doc/org/tut.org | 18 +++++++++++++++ 6 files changed, 70 insertions(+), 2 deletions(-) create mode 100644 doc/org/index.org create mode 100644 doc/org/tut.org diff --git a/debian/spot-doc.doc-base b/debian/spot-doc.doc-base index 392712351..40b5ca433 100644 --- a/debian/spot-doc.doc-base +++ b/debian/spot-doc.doc-base @@ -5,5 +5,5 @@ Abstract: User documentation for Spot Section: Science/Mathematics Format: HTML -Index: /usr/share/doc/spot/userdoc/tools.html +Index: /usr/share/doc/spot/userdoc/index.html Files: /usr/share/doc/spot/userdoc/*.html diff --git a/doc/Makefile.am b/doc/Makefile.am index a7cd88c82..9b29d8ca8 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -67,6 +67,7 @@ ORG_FILES = \ org/dstar2tgba.org \ org/genltl.org \ org/hoa.org \ + org/index.org \ org/ioltl.org \ org/ltl2tgba.org \ org/ltl2tgta.org \ @@ -78,6 +79,7 @@ ORG_FILES = \ org/randaut.org \ org/randltl.org \ org/tools.org \ + org/tut.org \ org/tut01.org \ org/tut02.org \ org/tut10.org \ diff --git a/doc/org/index.org b/doc/org/index.org new file mode 100644 index 000000000..9129259dd --- /dev/null +++ b/doc/org/index.org @@ -0,0 +1,47 @@ +#+TITLE: Spot +#+SETUPFILE: setup.org + +Spot is a C++11 library for ω-automata manipulation and model +checking. It has the following notable features: + +- Support for LTL (several syntaxes supported) and the linear fragment of PSL. +- Support for ω-automata with arbitrary acceptance condition. +- Support for transition-based acceptance (state-based acceptance + is supported by a reduction to transition-based acceptance). +- The automaton parser can read a stream of automata written in any of + three syntaxes ([[http://spinroot.com/spin/Man/never.html][never claims]], [[file:hoa.org][HOA]], or [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]]). +- Several algorithms for formula manipulation including: simplifying + formulas, testing implication or equivalence, testing + stutter-invariance, removing some operators by rewriting, ... +- Several algorithms for automata manipulation including: product, + emptiness checks, simulation-based reductions, + minimization of weak-DBA, removal of useless SCCs, + acceptance-condition transformations, etc. +- In addition to the C++ interface, most of its algorithms + are usable via [[file:tools.org][command-line tools]], and via Python bindings. +- One of the command-line tool, called [[file:ltlcross.org][=ltlcross=]] is a rewrite + of [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], but with support for PSL and arbitrary acceptance conditions. + It could for instance be used to test tools that translate + LTL into Rabin automata. + +* Documentation + +- [[file:tools.org][Command-line tools]] +- [[file:tut.org][Code examples]] + +* License + +Spot is distributed under a [[http://www.gnu.org/licenses/gpl-3.0.html][GNU GPL v3 license]]. + +A consequence is that if you distribute a tool built using Spot, you +*must* make the source code of that tool available as well. + +* Staying in touch + +=spot-announce@lrde.epita.fr= is an extremely low-traffic and +read-only mailing list for release announcements. If you want to stay +informed about future releases of Spot, we invite you to [[https://lists.lrde.epita.fr/listinfo/spot-announce][subscribe]]. + +[[mailto:spot@lrde.epita.fr][=spot@lrde.epita.fr=]] is a list for general discussions and questions +about Spot. [[https://lists.lrde.epita.fr/listinfo/spot][Subscribe here]] if you want to join, but feel free to send +in any question (in English) or bug report without subscribing. diff --git a/doc/org/setup.org b/doc/org/setup.org index a0e242178..ee72e3b88 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -1,3 +1,3 @@ #+OPTIONS: H:2 num:nil toc:t #+EMAIL: spot@lrde.epita.fr -#+HTML_LINK_HOME: http://spot.lip6.fr/ +#+HTML_LINK_HOME: index.html diff --git a/doc/org/tools.org b/doc/org/tools.org index a73fe6538..6f5707694 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -1,6 +1,7 @@ # -*- coding: utf-8 -*- #+TITLE: Command-line tools installed by Spot 1.99 #+SETUPFILE: setup.org +#+HTML_LINK_UP: index.html This document introduces command-line tools that are installed with the Spot library. We give some examples to highlight possible diff --git a/doc/org/tut.org b/doc/org/tut.org new file mode 100644 index 000000000..81ac4a508 --- /dev/null +++ b/doc/org/tut.org @@ -0,0 +1,18 @@ +#+TITLE: Code Examples +#+SETUPFILE: setup.org +#+HTML_LINK_UP: index.html + + +This section contains code examples for using Spot. This is a work in +progress. Feel free to [[mailto:spot@lrde.epita.fr][send]] suggestion of small tasks you would like +to see illustrated here. + + +* Examples with Shell, Python, and C++ + +All the following pages show how to perform the same task using the +three interfaces supported by Spot: shell commands, Python, or C++. + +- [[file:tut01.org][Parsing and Printing LTL Formulas]] +- [[file:tut02.org][Relabeling Formulas]] +- [[file:tut10.org][Translating an LTL formula into a never claim]]