README 7.82 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
2
3
4
5
6
7
8
Overview
========

Spot is a model-checking library developed collaboratively by LRDE
and LIP6. It provides algorithms and data structures to implement
the automata-theoretic approach to LTL model checking.

It is mainly meant to be used as a C++ library, but it also comes with
9
a few handy command-line utilities, and some Python bindings.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
10

11
12
13
14
15
16
17
18
19
20
21
22
23
Keeping in touch
================

If you have questions regarding Spot, a bug reports, please send them
to <spot@lrde.epita.fr>.  This is a public mailing list which you may
subscribe to at https://www.lrde.epita.fr/mailman/listinfo/spot but you
should feel free to post without subscribing.

We also run an extremely low traffic list for announcements of
new releases of Spot.  You may subscribe to that list at
https://www.lrde.epita.fr/mailman/listinfo/spot-announce


24
25
26
27
28
29
Installation
============

Requirements
------------

30
Spot requires a C++11-compliant compiler.
31
G++ 4.8 or later, as well as Clang++ 3.5 or later should work.
32

33
Spot expects a complete installation of Python (version 3.3 or later).
34
35
36
Especially, Python's headers files should be installed.  If you don't
have Python installed, and do NOT want to install it, you should run
configure with the --disable-python option (see below).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
37

38
39
Optional third-party dependencies
----------------------------------
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
40

41
42
If the SAT-solver glucose is found on your system, it will be used by
our test suite to test our SAT-based minimization algorithm.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
43

44
Spot used to distribute a modified version of LBTT (an LTL to Büchi
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
45
46
47
48
test bench), mostly fixing errors reported by recent compilers.
However Spot now distributes its own reimplementation of LBTT, called
ltlcross, so the use of LBTT is completely optional.  The last
modified version of LBTT we used to distribute can now be found at
49
  http://www.lrde.epita.fr/dload/spot/lbtt-1.2.1a.tar.gz
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
50
51
If some lbtt binary is found on your system, it will be used in the
test suite in addition to ltlcross.
52
53
54
55
56
57
58
59
60


Building and installing
-----------------------

Spot follows the traditional `./configure && make && make check &&
make install' process.  People unfamiliar with the GNU Build System
should read the file INSTALL for generic instructions.

61
In addition to its usual options, ./configure will accept some
62
63
flags specific to Spot:

64
  --disable-python
65
66
67
68
69
70
    Turn off the compilation of Python bindings.  These bindings
    offers a convenient interface when used in an IPython notebook,
    and are also used to build the CGI script that translates LTL
    formulas on-line.  You may safely disable these, especially if you
    do not have a working Python 3.2+ installation or if you are
    attempting some cross-compilation.
71

72
73
  --enable-devel
    Enable debugging symbols, turn off aggressive optimizations, and
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
74
    turn on assertions.  This option is effective by default in
75
    development versions (version numbers ending with a letter).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
    It is equivalent to
      --enable-debug
      --enable-warnings
      --enable-assert
      --enable-optimizations=-O
  --disable-devel
    Disable development options.  This is the case by default in
    releases (version numbers NOT ending with a letter).
    It is equivalent to
      --disable-debug
      --disable-warnings
      --disable-assert
      --enable-optimizations

Here are the meaning of the fine-tuning options, in case
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
91
--enable/disable-devel is not enough.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111

  --disable-assert
  --enable-assert
    Control assertion checking.

  --disable-warnings
  --enable-warnings
    Whether warnings should be output.  Note that during development
    we consider warnings to be errors.

  --disable-debug
  --enable-debug
    Whether to compile extra debugging code.

  --enable-optimizations
  --enable-optimizations=FLAGS
  --disable-optimizations
    Whether the compilation should be optimized.  When FLAGS are
    given, use these as optimization flags.  Otherwise, pick working
    flags from a built-in list.
112
113


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
114
115
116
117
118
119
120
121
122
123
124
Documentation
=============

Some documentation can be found in the doc/ directory.

- doc/spot.html/ contains documentation for the C++ library.

- doc/tl/tl.pdf contains documentation about the various temporal
  logic operators supported by Spot

"make install" will install man pages for command-line tools.  (These
125
man pages can also be found in the spot/bin/man/ subdirectory of the
126
source tree.)  Additional documentation about these tools can be found
127
in doc/userdoc/, or online at https://spot.lrde.epita.fr/tools.html
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
128
129
130



131
132
133
134
135
136
Layout of the source tree
=========================

Core directories
----------------

137
spot/             Sources for libspot.
138
139
   bin/           User tools built using the Spot library.
      man/        Man pages for the above tools.
140
   graph/         Graph representations.
141
   kripke/        Kripke Structure interface.
142
   tl/            Temporal Logic formulas and algorithms.
143
   misc/          Miscellaneous support files.
144
   parseaut/      Parser for automata in multiple formats.
145
   parsetl/       Parser for LTL/PSL formulas.
146
   priv/          Private algorithms, used internally but not exported.
147
148
   ta/            TA objects and cousins (TGTA).
   taalgos/       Algorithms on TA/TGTA.
149
   tests/         Tests for the whole library.
150
151
   twa/           TωA objects and cousins (Transition-based ω-Automata).
   twaalgos/      Algorithms on TωA.
152
      gtec/       Couvreur's Emptiness-Check.
153
   sanity/        Sanity tests for the whole project.
154
doc/              Documentation for Spot.
155
   org/           Source of userdoc/ as org-mode files.
156
   tl/            Documentation of the Temporal Logic operators.
157
   userdoc/       HTML documentation about the command-line tools.
158
   spot.html/     HTML reference manual for the library.
159
bench/            Benchmarks for ...
160
   dtgbasat/      ... SAT-based minimization of DTGBA,
161
   emptchk/       ... emptiness-check algorithms,
162
   ltl2tgba/      ... LTL-to-Büchi translation algorithms,
163
164
   ltlcounter/    ... translation of a class of LTL formulas,
   ltlclasses/    ... translation of more classes of LTL formulas,
165
   spin13/        ... compositional suspension and other improvements,
166
   stutter/       ... stutter-invariance checking algorithms,
167
   wdba/          ... WDBA minimization (for obligation properties).
168
169
170
wrap/             Wrappers for other languages.
   python/        Python bindings for Spot and BuDDy
      tests/      Tests for these bindings
171
      ajax/       LTL-to-TGBA translator with web interface, using Ajax.
172
spot-if/          Interfaces between Spot and other libraries.
173
   ltsmin/        Interface with DiVinE2 and SpinS.
174
175
176

Third party software
--------------------
177

178
buddy/            A customized version of BuDDy 2.3 (a BDD library).
179
ltdl/             Libtool's portable dlopen() wrapper library.
180
lib/              Gnulib's portability modules.
181
utf8/             Nemanja Trifunovic's utf-8 routines.
182
elisp/		  Related emacs modes, used for building the documentation.
183

184
185
Build-system stuff
------------------
186
187
188

m4/      M4 macros used by configure.ac.
tools/   Helper scripts used during the build.
189
debian/  Configuration file to build Debian packages.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
190
191
192
193

-------------------------------------------------------------------------------
Local Variables:
mode: text
194
coding: utf-8
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
195
196
End:

197
198
 LocalWords:  Python's BuDDy LBTT LTL Büchi lbtt gspn DIR GreatSPN Soheib Yann
 LocalWords:  Baarir Thierry Mieg CVS Università di Torino devel src libspot ac
199
 LocalWords:  ltlast ltlenv ltlparse ltlvisit  misc tgba TGBA tgbaalgos
200
 LocalWords:  gtec Tarjan doc html PDF spotref pdf cgi ELTL LRDE tl
201
 LocalWords:  CGI ltl iface BDD Couvreur's emptchk kripke Kripke saba vm
202
 LocalWords:  eltlparse eltltest SABA sabaalgos sabatest ssp ltlcouter scc SCC
203
LocalWords:  optimizations kripkeparse  Automata IPython subdirectory
204
LocalWords:  neverparse ltlcounter ltlclasses parallelizing automata
205
206
207
LocalWords:  wdba WDBA ajax dve DiVinE ltdl Libtool's dlopen userdoc
LocalWords:  parseaut parsetl priv TGTA taalgos twa twaalgos dtgbasat
LocalWords:  DTGBA compositional invariance ltsmin SpinS Gnulib's