alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/doc/org/index.org
Alexandre Duret-Lutz c035ea1822 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.
2016-05-10 10:23:01 +02:00

3.8 KiB
Raw Blame History

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…
  • Several algorithms for automata manipulation including: product, emptiness checks, simulation-based reductions, minimization of weak-DBA, removal of useless SCCs, acceptance-condition transformations, determinization, 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

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.

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.