diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 65e445dfb110f5893981b3ed92f6166d5f794a09..316ce6eedccb45069d08230bf12bc2607ea1bc33 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =autfilt= +#+DESCRIPTION: Spot command-line tool for filtering, tranforming, and converting ω-automata. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/compile.org b/doc/org/compile.org index f9627b7bb22c1f835c52bdb4bbbf8505387ffe77..5aa47111ace07c3d1b21d61150ef81ad42ea11a7 100644 --- a/doc/org/compile.org +++ b/doc/org/compile.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Compiling against Spot +#+DESCRIPTION: How to compile C++11 programs using Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 847975308cba639dfb46037b4d604830f30332d6..ea86e9e18f7fd16ef986efe9c6f6efc32956ce84 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Concepts +#+DESCRIPTION: Informal explanation of various concepts used in Spot. #+SETUPFILE: setup.org #+HTML_LINK_UP: index.html diff --git a/doc/org/csv.org b/doc/org/csv.org index 6ae9cc65b4c35da019dee19fbf4ff2dad80a1e5b..4a4d6e37d0839bdc713a65eb64ce9d3c4e24a6c1 100644 --- a/doc/org/csv.org +++ b/doc/org/csv.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+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 #+HTML_LINK_UP: tools.html diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index 70122ed3eaab0b9eee56740809d9c8e0e8780746..7a64539e85664dfa2ecfe6262b6234fc144ed52b 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =dstar2tgba= +#+DESCRIPTION: Spot command-line tool for converting automata into Transition-based Generalized Büchi Automata. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/genltl.org b/doc/org/genltl.org index 60f84994258dc00c99d92f1ce537cb10731229b0..11df831174a3447d376224f98a1ad77f81d86426 100644 --- a/doc/org/genltl.org +++ b/doc/org/genltl.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =genltl= +#+DESCRIPTION: Spot command-line tool that generates LTL formulas from known patterns #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/hoa.org b/doc/org/hoa.org index 64dae991e79159fcdd3a506e3543e3b6099b95b2..4fae279705251d3bfb124c49eaede7b3574a9ccb 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -1,4 +1,5 @@ #+TITLE: Support for the Hanoi Omega Automata (HOA) Format +#+DESCRIPTION: Details about support of the HOA format in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/index.org b/doc/org/index.org index d79945db9bf1e746c6bc78c28ace112fa798baac..bffc627ae45dbb8b25a991cf6f5d76bd22936d57 100644 --- a/doc/org/index.org +++ b/doc/org/index.org @@ -1,9 +1,11 @@ # -*- 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 #+HTML_HEAD_EXTRA: -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: - Support for [[file:concepts.org::#ltl][LTL]] (several syntaxes supported) and @@ -22,11 +24,11 @@ checking. It has the following notable features: weak-DBA, removal of useless SCCs, acceptance-condition transformations, determinization, 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 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. + 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 [[http://www.tcs.hut.fi/Software/lbtt/][LBTT]], but + with support for PSL and automata with arbitrary acceptance + conditions. It can be used to test tools that translate LTL into + ω-automata, or benchmark them. * Latest version diff --git a/doc/org/install.org b/doc/org/install.org index f96a7410d53e5d6d08ca78d3f3b3dc33301cce36..c60d5c64d74b96ffa34305a0ce903d9727551cef 100644 --- a/doc/org/install.org +++ b/doc/org/install.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Installing Spot +#+DESCRIPTION: Different ways to install the Spot package #+SETUPFILE: setup.org #+HTML_LINK_UP: index.html diff --git a/doc/org/ioltl.org b/doc/org/ioltl.org index 3873aaf16cb03ddec25d9282787b6b31cbaaa21b..be7d106958e40935a891ddfdfa8ac376b5c491f1 100644 --- a/doc/org/ioltl.org +++ b/doc/org/ioltl.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+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 #+HTML_LINK_UP: tools.html diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index b75a7ddaf3a2b5ea6e7937bedf984d71a9896508..d85e2ceade209b99e71114b436f30aa92606996a 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =ltl2tgba= +#+DESCRIPTION: Spot command-line tool for translating LTL into Transition-based Generalized Büchi Automata. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/ltl2tgta.org b/doc/org/ltl2tgta.org index ff290d87f3e2f06bb54a9e6763f5179284c72c72..a7e3d6fdb8e6bbcc597e6196a69d96aa71864dbf 100644 --- a/doc/org/ltl2tgta.org +++ b/doc/org/ltl2tgta.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =ltl2tgta= +#+DESCRIPTION: Spot command-line tool for translating LTL into Transition-based Generalized Testing Automata. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index eaada3dedb870d77d9bfcfeeae8eae02c716ec62..db69fea88c8689c21c8b96440313d222b00d897f 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =ltlcross= +#+DESCRIPTION: Spot command-line tool for cross-comparing the output of LTL translators. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org index 1b5d4b4817e8184901b494996b05e022d4f29fcd..37bd1efa39abe28262e203b9f2684a2b79c54ec5 100644 --- a/doc/org/ltldo.org +++ b/doc/org/ltldo.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =ltldo= +#+DESCRIPTION: Spot's wrapper for third-party LTL translators #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index 7f48010f77e61b6a6a0628a96d88453828795576..cf5bca47dcf24f3cfce282bda0904c0d39272b97 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =ltlfilt= +#+DESCRIPTION: Spot command-line tool for filtering, tranforming, and converting LTL formulas. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/ltlgrind.org b/doc/org/ltlgrind.org index d1729f7374fd706bb14cc461c447ad3f78cb31cc..6c33b8d9a475990dcfb35ddd81b85a56bd747044 100644 --- a/doc/org/ltlgrind.org +++ b/doc/org/ltlgrind.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =ltlgrind= +#+DESCRIPTION: Spot command-line tool for mutating LTL formulas. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/oaut.org b/doc/org/oaut.org index b9cf5e85c12e90a4bf22cdf92fca8e268ede70f2..9572ae3777774ca1c3fe4265a2c4c4d2ba06a9aa 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Common output options for automata +#+DESCRIPTION: Options for input and output of ω-automata in Spot's command-line tools #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/randaut.org b/doc/org/randaut.org index f51f63a04f2d7c1f70aed8c13b1495acf7a51f87..2ef48d1dcd779980a7ca14b158caf49494d9e3d7 100644 --- a/doc/org/randaut.org +++ b/doc/org/randaut.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =randaut= +#+DESCRIPTION: Spot command-line tool for generating random ω-automata. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/randltl.org b/doc/org/randltl.org index 839dc066b295eea59fe00b629a0da15bcbf6facb..110601d6a7073b63112c96dfb676a511b39e9b6f 100644 --- a/doc/org/randltl.org +++ b/doc/org/randltl.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: =randltl= +#+DESCRIPTION: Spot command-line tool for generating random LTL formulas. #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/satmin.org b/doc/org/satmin.org index 92586c76f6105e5a42bc28f5b036b4e633b5665b..bdd0240c267765039dff62e022282c2fd7cb4bce 100644 --- a/doc/org/satmin.org +++ b/doc/org/satmin.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: SAT-based Minimization of Deterministic ω-Automata +#+DESCRIPTION: Spot command-line tools for minimizing ω-automata #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html diff --git a/doc/org/tools.org b/doc/org/tools.org index acdcaa0e9c921dafb0c0d67bf3b1603ee90af327..81acd065cbb06c9e0e1a332d34a027eb89ffd578 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Command-line tools installed by Spot {{{SPOTVERSION}}} +#+DESCRIPTION: List of all the command-line tools installed by Spot {{{SPOTVERSION}}} #+SETUPFILE: setup.org #+HTML_LINK_UP: index.html diff --git a/doc/org/tut.org b/doc/org/tut.org index 457fc1f4ec8e1c12c26f5b87170513f1815e91dc..609dc981e8c6a7602aa0f9418662941a0bb78053 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Code Examples +#+DESCRIPTION: Directory of code examples for using Spot in C++11, Python, and shell. #+SETUPFILE: setup.org #+HTML_LINK_UP: index.html diff --git a/doc/org/tut01.org b/doc/org/tut01.org index 9fdfda015299b0b64f632c4d556b3f6b65cb8dc3..d2641f62a011fb82843bd20c683ac07b198ed543 100644 --- a/doc/org/tut01.org +++ b/doc/org/tut01.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Parsing and Printing LTL Formulas +#+DESCRIPTION: Code example for parsing and printing formulas in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut02.org b/doc/org/tut02.org index d9e307a5161a27a1da9dc860e175b091da9eb568..c02510ae1f42f6e2ac2af064e7d77a7112de4123 100644 --- a/doc/org/tut02.org +++ b/doc/org/tut02.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Relabeling Formulas +#+DESCRIPTION: Code example for relabeling formulas in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut03.org b/doc/org/tut03.org index 7240243fbf44921c5ba249ed7c397b8794ef18e0..68cebe2922428b96b475201dcba55588757b5956 100644 --- a/doc/org/tut03.org +++ b/doc/org/tut03.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Constructing and transforming formulas +#+DESCRIPTION: Code example for constructing and transforming formulas in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut10.org b/doc/org/tut10.org index b25f55bffae5ca58f3b27890a1d8cd1678306768..7772d279490e185f7cc7ac77eba1b5e3a51070b0 100644 --- a/doc/org/tut10.org +++ b/doc/org/tut10.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Translating an LTL formula into a never claim +#+DESCRIPTION: Code example for translating formulas in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut20.org b/doc/org/tut20.org index f138f54195d0e46788ebe4591db06dd72ab55e49..c0b6dcf8e68da8b3b1d9cb7a1ef73c0731e672c4 100644 --- a/doc/org/tut20.org +++ b/doc/org/tut20.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Converting a never claim into HOA +#+DESCRIPTION: Code example for parsing and printing ω-automata in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut21.org b/doc/org/tut21.org index 2140063d1cdc976378d44f541c51e798d58a1297..a0b3ebedc25b1a82cc98f91a152470a1a106e71d 100644 --- a/doc/org/tut21.org +++ b/doc/org/tut21.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Custom print of an automaton +#+DESCRIPTION: Code example for iterating over ω-automata in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut22.org b/doc/org/tut22.org index da6ca6d7f9d239be11e22281bc3ed77640cfd7a7..35f68416b7b56f88480614d6b3dc245a2775c1f5 100644 --- a/doc/org/tut22.org +++ b/doc/org/tut22.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Creating an automaton by adding states and transitions +#+DESCRIPTION: Code example for constructing ω-automata in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/tut30.org b/doc/org/tut30.org index bd82228cbe0aa093f0bf17da2eadb58a47eaf53d..118c7a6f4313eb02e3a476b82c886f2d3588b892 100644 --- a/doc/org/tut30.org +++ b/doc/org/tut30.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Converting Rabin (or Other) to Büchi, and simplifying it +#+DESCRIPTION: Code example for converting ω-automata in Spot #+SETUPFILE: setup.org #+HTML_LINK_UP: tut.html diff --git a/doc/org/upgrade2.org b/doc/org/upgrade2.org index 9c4bdfbf2bb7a6f82b3deedfaa922a5308a670f6..e2618e4f59c10a0afe8088b653e49c6d3660693d 100644 --- a/doc/org/upgrade2.org +++ b/doc/org/upgrade2.org @@ -1,5 +1,6 @@ # -*- coding: utf-8 -*- #+TITLE: Upgrading from Spot 1.2.6 +#+DESCRIPTION: Help for upgrading code to Spot 2.0 #+SETUPFILE: setup.org #+HTML_LINK_UP: index.html