21e2d9bb32
* doc/org/index.org: Add links to the hierarchy and sat-minimization. * doc/org/satmin.org: Show how to use glucose.
4.2 KiB
Spot: a platform for LTL and ω-automata manipulation
Spot is a C++11 library for LTL, ω-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 four syntaxes (HOA, never claims, LBTT, DSTAR).
- Several algorithms for formula manipulation including: simplifying formulas, testing implication or equivalence, testing stutter-invariance, removing some operators by rewriting, translation to automata, testing membership to the temporal hierarchy of Manna & Pnueli…
- Several algorithms for automata manipulation including: product, emptiness checks, simulation-based reductions, minimization of weak-DBA, removal of useless SCCs, acceptance-condition transformations, determinization, SAT-based minimization of deterministic automata, etc.
- In addition to the C++ interface, most of its algorithms are usable via command-line tools, and via Python bindings.
- One command-line tool, called
ltlcross, is a rewrite of 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
The latest version is {{{LASTRELEASE}}} and was released on {{{LASTDATE}}}. Please see the download and installation instructions.
Documentation
- Basic concepts.
- Command-line tools.
- Code examples.
- Doxygen documentation, generated automatically from the source code.
- Definition of the temporal operators supported by Spot.
- Help for upgrading existing code written for Spot 1.2.x to Spot 2.
Try Spot On-line
- Our on-line translator provides a convenient way to translate LTL or PSL formulas into automata.
- spot-sandbox is a Jupyter notebook with a complete installation of Spot that allows you to try the command-line tools (using a shell interface) as well as the Python bindings (in an IPython notebook).
License
Spot is distributed under a 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, under a compatible license.
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 subscribe.
spot@lrde.epita.fr is a list for general discussions and questions
about Spot. Subscribe here if you want to join, but feel free to send
in any question (in English) or bug report without subscribing.
Citing
Our citing page has a list of papers you could cite if you need to reference Spot in an academic publication.