Commit c035ea18 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

org: add a description for each page

Part of #176.

* doc/org/autfilt.org, doc/org/compile.org, doc/org/concepts.org,
doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/genltl.org,
doc/org/hoa.org, doc/org/install.org, doc/org/ioltl.org,
doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org,
doc/org/ltldo.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, doc/org/tut.org,
doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut10.org, doc/org/tut20.org, doc/org/tut21.org,
doc/org/tut22.org, doc/org/tut30.org, doc/org/upgrade2.org: Here.
* doc/org/index.org: Also add keywords in case it is useful, and
use a more descripting title for search engines.
parent 0278735e
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: =autfilt= #+TITLE: =autfilt=
#+DESCRIPTION: Spot command-line tool for filtering, tranforming, and converting ω-automata.
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Compiling against Spot #+TITLE: Compiling against Spot
#+DESCRIPTION: How to compile C++11 programs using Spot
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html #+HTML_LINK_UP: tut.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Concepts #+TITLE: Concepts
#+DESCRIPTION: Informal explanation of various concepts used in Spot.
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: index.html #+HTML_LINK_UP: index.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Reading and writing CSV files #+TITLE: Reading and writing CSV files
#+DESCRIPTION: Examples showing how to read and write CSV files using Spot's command-line tools.
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: =dstar2tgba= #+TITLE: =dstar2tgba=
#+DESCRIPTION: Spot command-line tool for converting automata into Transition-based Generalized Büchi Automata.
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: =genltl= #+TITLE: =genltl=
#+DESCRIPTION: Spot command-line tool that generates LTL formulas from known patterns
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
#+TITLE: Support for the Hanoi Omega Automata (HOA) Format #+TITLE: Support for the Hanoi Omega Automata (HOA) Format
#+DESCRIPTION: Details about support of the HOA format in Spot
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Spot #+TITLE: Spot: a platform for LTL and ω-automata manipulation
#+DESCRIPTION: Spot is a library and tool suite for LTL and ω-automata
#+KEYWORDS: Spot,C++11,library,platform,framework,tool-suite,LTL,PSL,omega-automata
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_HEAD_EXTRA: <style>#org-div-home-and-up { display: none; }</style> #+HTML_HEAD_EXTRA: <style>#org-div-home-and-up { display: none; }</style>
Spot is a C++11 library for ω-automata manipulation and model Spot is a C++11 library for LTL, ω-automata manipulation and model
checking. It has the following notable features: checking. It has the following notable features:
- Support for [[file:concepts.org::#ltl][LTL]] (several syntaxes supported) and - Support for [[file:concepts.org::#ltl][LTL]] (several syntaxes supported) and
...@@ -22,11 +24,11 @@ checking. It has the following notable features: ...@@ -22,11 +24,11 @@ checking. It has the following notable features:
weak-DBA, removal of useless SCCs, acceptance-condition weak-DBA, removal of useless SCCs, acceptance-condition
transformations, determinization, etc. transformations, determinization, etc.
- In addition to the C++ interface, most of its algorithms are usable - In addition to the C++ interface, most of its algorithms are usable
via [[file:tools.org][command-line tools]], and via Python bindings. via [[file:tools.org][command-line tools]], and via [[file:tut.org][Python bindings]].
- One command-line tool, called [[file:ltlcross.org][=ltlcross=]], is a rewrite of - One command-line tool, called [[file:ltlcross.org][=ltlcross=]], is a rewrite of [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], but
[[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], but with support for PSL and arbitrary acceptance conditions. with support for PSL and automata with arbitrary acceptance
It could for instance be used to test tools that translate LTL into conditions. It can be used to test tools that translate LTL into
Rabin automata. ω-automata, or benchmark them.
* Latest version * Latest version
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Installing Spot #+TITLE: Installing Spot
#+DESCRIPTION: Different ways to install the Spot package
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: index.html #+HTML_LINK_UP: index.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Common input and output options for LTL/PSL formulas #+TITLE: Common input and output options for LTL/PSL formulas
#+DESCRIPTION: Options for input and output of temporal logic formulas in Spot's command-line tools
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: =ltl2tgba= #+TITLE: =ltl2tgba=
#+DESCRIPTION: Spot command-line tool for translating LTL into Transition-based Generalized Büchi Automata.
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: =ltl2tgta= #+TITLE: =ltl2tgta=
#+DESCRIPTION: Spot command-line tool for translating LTL into Transition-based Generalized Testing Automata.
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: =ltlcross= #+TITLE: =ltlcross=
#+DESCRIPTION: Spot command-line tool for cross-comparing the output of LTL translators.
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: =ltldo= #+TITLE: =ltldo=
#+DESCRIPTION: Spot's wrapper for third-party LTL translators
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: =ltlfilt= #+TITLE: =ltlfilt=
#+DESCRIPTION: Spot command-line tool for filtering, tranforming, and converting LTL formulas.
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: =ltlgrind= #+TITLE: =ltlgrind=
#+DESCRIPTION: Spot command-line tool for mutating LTL formulas.
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Common output options for automata #+TITLE: Common output options for automata
#+DESCRIPTION: Options for input and output of ω-automata in Spot's command-line tools
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: =randaut= #+TITLE: =randaut=
#+DESCRIPTION: Spot command-line tool for generating random ω-automata.
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: =randltl= #+TITLE: =randltl=
#+DESCRIPTION: Spot command-line tool for generating random LTL formulas.
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: SAT-based Minimization of Deterministic ω-Automata #+TITLE: SAT-based Minimization of Deterministic ω-Automata
#+DESCRIPTION: Spot command-line tools for minimizing ω-automata
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tools.html #+HTML_LINK_UP: tools.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Command-line tools installed by Spot {{{SPOTVERSION}}} #+TITLE: Command-line tools installed by Spot {{{SPOTVERSION}}}
#+DESCRIPTION: List of all the command-line tools installed by Spot {{{SPOTVERSION}}}
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: index.html #+HTML_LINK_UP: index.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Code Examples #+TITLE: Code Examples
#+DESCRIPTION: Directory of code examples for using Spot in C++11, Python, and shell.
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: index.html #+HTML_LINK_UP: index.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Parsing and Printing LTL Formulas #+TITLE: Parsing and Printing LTL Formulas
#+DESCRIPTION: Code example for parsing and printing formulas in Spot
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html #+HTML_LINK_UP: tut.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Relabeling Formulas #+TITLE: Relabeling Formulas
#+DESCRIPTION: Code example for relabeling formulas in Spot
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html #+HTML_LINK_UP: tut.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Constructing and transforming formulas #+TITLE: Constructing and transforming formulas
#+DESCRIPTION: Code example for constructing and transforming formulas in Spot
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html #+HTML_LINK_UP: tut.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Translating an LTL formula into a never claim #+TITLE: Translating an LTL formula into a never claim
#+DESCRIPTION: Code example for translating formulas in Spot
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html #+HTML_LINK_UP: tut.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Converting a never claim into HOA #+TITLE: Converting a never claim into HOA
#+DESCRIPTION: Code example for parsing and printing ω-automata in Spot
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html #+HTML_LINK_UP: tut.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Custom print of an automaton #+TITLE: Custom print of an automaton
#+DESCRIPTION: Code example for iterating over ω-automata in Spot
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html #+HTML_LINK_UP: tut.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Creating an automaton by adding states and transitions #+TITLE: Creating an automaton by adding states and transitions
#+DESCRIPTION: Code example for constructing ω-automata in Spot
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html #+HTML_LINK_UP: tut.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Converting Rabin (or Other) to Büchi, and simplifying it #+TITLE: Converting Rabin (or Other) to Büchi, and simplifying it
#+DESCRIPTION: Code example for converting ω-automata in Spot
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: tut.html #+HTML_LINK_UP: tut.html
......
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
#+TITLE: Upgrading from Spot 1.2.6 #+TITLE: Upgrading from Spot 1.2.6
#+DESCRIPTION: Help for upgrading code to Spot 2.0
#+SETUPFILE: setup.org #+SETUPFILE: setup.org
#+HTML_LINK_UP: index.html #+HTML_LINK_UP: index.html
......
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