index.org 4.15 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
# -*- coding: utf-8 -*-
2
3
#+TITLE: Spot: a platform for LTL and ω-automata manipulation
#+DESCRIPTION: Spot is a library and tool suite for LTL and ω-automata
4
#+KEYWORDS: Spot,C++14,library,platform,framework,tool-suite,LTL,PSL,omega-automata
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
5
#+SETUPFILE: setup.org
6
#+HTML_HEAD_EXTRA: <style>#org-div-home-and-up { display: none; }</style>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
7

8
Spot is a C++14 library for LTL, ω-automata manipulation and model
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
9
10
checking.  It has the following notable features:

11
12
13
14
- Support for [[file:concepts.org::#ltl][LTL]] (several syntaxes supported) and
  [[file:concepts.org::#psl][the linear fragment of PSL]].
- Support for ω-automata with [[file:concepts.org::#acceptance-condition][arbitrary acceptance condition]].
- Support for [[file:concepts.org::#trans-acc][transition-based acceptance]] (state-based acceptance is
15
  supported by a reduction to transition-based acceptance).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
16
- The automaton parser can read a stream of automata written in any of
17
  four syntaxes ([[file:hoa.org][HOA]], [[http://spinroot.com/spin/Man/never.html][never claims]], [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]], [[http://www.ltl2dstar.de/docs/ltl2dstar.html][DSTAR]]).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
18
19
- Several algorithms for formula manipulation including: simplifying
  formulas, testing implication or equivalence, testing
20
  stutter-invariance, removing some operators by rewriting, translation
21
  to automata, testing membership to the [[file:hierarchy.org][temporal hierarchy of Manna & Pnueli]]...
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22
- Several algorithms for automata manipulation including: product,
23
24
  emptiness checks, simulation-based reductions, minimization of
  weak-DBA, removal of useless SCCs, acceptance-condition
25
26
  transformations, determinization, [[file:satmin.org][SAT-based minimization of
  deterministic automata]], etc.
27
- In addition to the C++ interface, most of its algorithms are usable
28
29
30
31
32
  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.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
33

34
35
36
* Latest version

The latest version is *{{{LASTRELEASE}}}* and was released on
37
*{{{LASTDATE}}}*.  Please see the [[file:install.org][download and installation instructions]].
38

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
39
40
* Documentation

41
- [[file:concepts.org][Basic concepts]].
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
42
43
- [[file:tools.org][Command-line tools]].
- [[file:tut.org][Code examples]].
44
- [[http://spot.lrde.epita.fr/doxygen/][Doxygen documentation]], generated automatically from the source code.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
45
- [[https://spot.lrde.epita.fr/tl.pdf][Definition of the temporal operators supported by Spot]].
46
- [[file:upgrade2.org][Help for upgrading existing code written for Spot 1.2.x to Spot 2]].
47

48
* Try Spot On-line
49

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
50
- [[http://spot.lrde.epita.fr/trans.html][Our on-line translator]] provides a convenient way to translate LTL or
51
52
53
54
  PSL formulas into automata.
- [[http://spot-sandbox.lrde.epita.fr/][spot-sandbox]] is a Jupyter notebook with a complete installation of
  Spot that allows you to try the [[file:tools.org][command-line tools]] (using a shell
  interface) as well as the Python bindings (in an IPython notebook).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
55
56
57
58
59
60

* 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
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
61
62
*must* make the source code of that tool available as well, under a
compatible license.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
63
64
65
66
67
68
69
70
71
72

* 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.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
73
74
75
76
77

* Citing

Our [[file:citing.org][citing page]] has a list of papers you could cite if you need to
reference Spot in an academic publication.