README 10.5 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
2
3
Overview
========

4
Spot is a model-checking toolkit comprising:
5
  - a C++14 library with data-structures and algorithms for working
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
    with linear-time temporal logical formulas and ω-automata with
    any acceptance condition.
  - a set of command-line tools for easy access to those algorithms,
    with convenient interfaces to third-party tools also manipulating
    similar concepts.
  - Python bindings (including Jupyter interfaces) for the library,
    making it easier to play with and discover those concepts.


Documentation
=============

Some documentation can be found in the doc/ directory.

- doc/userdoc/ is basically a local copy of the web-site at
  https://spot.lrde.epita.fr/.  It contains several explanations and
  illustrations of the core concepts and tools; it has installation
  instructions; and also provide several code examples.

- doc/spot.html/ contains documentation for the C++ library.  It is
  generated automatically from the source code using Doxygen.

- doc/tl/tl.pdf contains documentation about the various temporal
  logic operators supported by Spot.  It provides semantics, syntax,
  and gives an exhaustive list of all implemented rewritings.

"make install" will also install man pages for command-line tools.
(These man pages can also be found in the spot/bin/man/ subdirectory
of the source tree.)  Additional documentation about these tools can
also be found in doc/userdoc/.

An important part of the documentation that is missing is the
documentation of the Python bindings.  Currently all we have is a
collection of examples, which are all collected at
http://spot.lrde.epita.fr/tut.html (or doc/userdoc/tut.html in the
source tree).  This is hardly ideal, but we do not have the resources
to maintain such a manual for the Python binding by hand.  If you have
an idea about how to generate a manual for the Python bindings
automatically, please do contribute!


History
=======

This project started in 2003 at LIP6 (www.lip6.fr).  The main author
moved to LRDE (www.lrde.epita.fr) in 2007, and all regular
contributors are now at LRDE.  The web site was moved from
spot.lip6.fr to spot.lrde.epita.fr in 2015, so do not be surprised if
you find links to the old site.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
55
56


57
58
59
Keeping in touch
================

60
61
62
63
If you have questions regarding Spot, or bug to report, 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.
64

65
66
We also run a low-traffic and read-only list for announcements of new
releases of Spot.  You may subscribe to that list at
67
68
69
https://www.lrde.epita.fr/mailman/listinfo/spot-announce


70
71
72
73
74
75
Installation
============

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

76
77
Spot requires a C++14-compliant compiler.  G++ 5.x or later, as well
as Clang++ 3.5 or later should work.
78

79
Spot expects a complete installation of Python (version 3.3 or later).
80
81
82
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
83

84
85
Optional third-party dependencies
----------------------------------
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
86

87
88
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
89

90
Spot used to distribute a modified version of LBTT (an LTL to Büchi
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
91
92
93
94
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
95
  http://www.lrde.epita.fr/dload/spot/lbtt-1.2.1a.tar.gz
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
96
97
If some lbtt binary is found on your system, it will be used in the
test suite in addition to ltlcross.
98
99
100
101
102
103
104
105
106


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.

107
In addition to its usual options, ./configure will accept some
108
109
flags specific to Spot:

110
  --disable-python
111
112
113
114
115
116
    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.
117

118
119
120
121
122
123
124
  --enable-doxygen
    Generate the Doxygen documentation for the code as part of the
    build.  This requires Doxygen to be installed.  Even if
    --enable-doxygen has not been given, you can force the
    documentation to be built by running "make doc" inside the doc/
    directory.

125
126
  --enable-devel
    Enable debugging symbols, turn off aggressive optimizations, and
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
127
    turn on assertions.  This option is effective by default in
128
    development versions (version numbers ending with a letter).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
129
130
131
132
133
134
135
136
137
138
139
140
141
142
    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

143
144
145
   --enable-glibgxx-debug
     Enable the debugging version libstdc++
     https://gcc.gnu.org/onlinedocs/libstdc++/manual/debug_mode_semantics.html
146
     Note that the debugging version of libstdc++ is incompatible with
147
148
149
150
     the regular version.  So if Spot is compiled with this option, all
     client code should be compiled with -D_GLIBCXX_DEBUG as well.  This
     options should normally only be useful to run Spot's test-suite.

151
152
153
154
   --enable-c++17
     Build everything in C++17 mode.  We use that in our build farm to
     ensure that Spot can be used in C++17 projects as well.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
155
Here are the meaning of the fine-tuning options, in case
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
156
--enable/disable-devel is not enough.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176

  --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.
177
178


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
179

180
181
182
183
184
185
Layout of the source tree
=========================

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

186
spot/             Sources for libspot.
187
   graph/         Graph representations.
188
   ltsmin/        Interface with DiVinE2 and SpinS.  (Not part of libspot.)
189
   kripke/        Kripke Structure interface.
190
   tl/            Temporal Logic formulas and algorithms.
191
   misc/          Miscellaneous support files.
192
   mc/            All algorithms useful for model checking
193
   parseaut/      Parser for automata in multiple formats.
194
   parsetl/       Parser for LTL/PSL formulas.
195
   priv/          Private algorithms, used internally but not exported.
196
197
   ta/            TA objects and cousins (TGTA).
   taalgos/       Algorithms on TA/TGTA.
198
   twa/           TωA objects and cousins (Transition-based ω-Automata).
199
   twacube/       TωA objects based on cube (not-bdd).
200
   twacube_algos/ TωAcube algorithms
201
   twaalgos/      Algorithms on TωA.
202
      gtec/       Couvreur's Emptiness-Check.
203
   gen/           Sources for libspotgen.
204
205
bin/              Command-line tools built on top of libspot.
   man/           Man pages for the above tools.
206
tests/            Test suite.
207
   core/          Tests for libspot and the binaries.
208
   ltsmin/	  Tests for the DiVinE2/SpinS interface.
209
   python/        Tests for Python bindings.
210
   sanity/        Tests for the coherence of the source base.
211
doc/              Documentation for Spot.
212
   org/           Source of userdoc/ as org-mode files.
213
   tl/            Documentation of the Temporal Logic operators.
214
215
   userdoc/       HTML documentation about command-line tools, and examples.
   spot.html/     HTML doc for C++ API (not distributed, use --enable-doxygen).
216
bench/            Benchmarks for ...
217
   dtgbasat/      ... SAT-based minimization of DTGBA,
218
   emptchk/       ... emptiness-check algorithms,
219
   ltl2tgba/      ... LTL-to-Büchi translation algorithms,
220
221
   ltlcounter/    ... translation of a class of LTL formulas,
   ltlclasses/    ... translation of more classes of LTL formulas,
222
   spin13/        ... compositional suspension and other improvements,
223
   stutter/       ... stutter-invariance checking algorithms,
224
   wdba/          ... WDBA minimization (for obligation properties).
225
226
python/           Python bindings for Spot and BuDDy
   ajax/          LTL-to-TGBA translator with web interface, using Javascript.
227
228
229

Third party software
--------------------
230

231
buddy/            A customized version of BuDDy 2.3 (a BDD library).
232
ltdl/             Libtool's portable dlopen() wrapper library.
233
lib/              Gnulib's portability modules.
234
utf8/             Nemanja Trifunovic's utf-8 routines.
235
elisp/		  Related emacs modes, used for building the documentation.
236
picosat/          A distribution of PicoSAT 965 (a satsolver library).
237

238
239
Build-system stuff
------------------
240
241
242

m4/      M4 macros used by configure.ac.
tools/   Helper scripts used during the build.
243
debian/  Configuration file to build Debian packages.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
244
245
246
247

-------------------------------------------------------------------------------
Local Variables:
mode: text
248
coding: utf-8
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
249
250
End:

251
252
 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
253
 LocalWords:  ltlast ltlenv ltlparse ltlvisit  misc tgba TGBA tgbaalgos
254
 LocalWords:  gtec Tarjan doc html PDF spotref pdf cgi ELTL LRDE tl
255
 LocalWords:  CGI ltl iface BDD Couvreur's emptchk kripke Kripke saba vm
256
 LocalWords:  eltlparse eltltest SABA sabaalgos sabatest ssp ltlcouter scc SCC
257
LocalWords:  optimizations kripkeparse  Automata IPython subdirectory
258
LocalWords:  neverparse ltlcounter ltlclasses parallelizing automata
259
260
LocalWords:  wdba WDBA ajax dve DiVinE ltdl Libtool's dlopen userdoc
LocalWords:  parseaut parsetl priv TGTA taalgos twa twaalgos dtgbasat
261
262
263
264
LocalWords:  DTGBA compositional invariance ltsmin SpinS Gnulib's PSL
LocalWords:  Jupyter Doxygen rewritings reimplementation ltlcross utf
LocalWords:  glibgxx libstdc GLIBCXX Javascript Nemanja Trifunovic's
LocalWords:  elisp emacs debian