README 7.75 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
2
3
4
5
6
7
8
9
10
11
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
a few handy command-line utilities, and some (limited) Python
bindings.

12
13
14
15
16
17
18
19
20
21
22
23
24
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


25
26
27
28
29
30
Installation
============

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

31
Spot requires a C++11-compliant compiler.
32

33
34
35
36
Spot expects a complete installation of Python (version 2.0 or later).
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
43
44
45


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
46
47
48
49
50
51
52
53
54

Spot used to distribute a modified version of LBTT (an LTL to Büchi
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
  http://spot.lip6.fr/dl/lbtt-1.2.1a.tar.gz
If some lbtt binary is found on your system, it will be used in the
test suite in addition to ltlcross.
55
56
57
58
59
60
61
62
63


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.

64
In addition to its usual options, ./configure will accept some
65
66
flags specific to Spot:

67
68
69
70
71
72
73
  --disable-python
    Turn off the compilation of Python bindings.  These bindings are
    currently used to run a couple of tests, and to build the CGI
    script that translates LTL formulae on-line.  You may safely
    disable these, especially if you do not have a working Python
    installation or if you are attempting some cross-compilation.

74
75
  --enable-devel
    Enable debugging symbols, turn off aggressive optimizations, and
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
76
    turn on assertions.  This option is effective by default in
77
    development versions (version numbers ending with a letter).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
    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
93
--enable/disable-devel is not enough.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113

  --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.
114
115


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
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
man pages can also be found in the src/bin/man/ subdirectory of the
source tree.)  Additional documentation about these tools can be
found on-line at http://spot.lip6.fr/userdoc/tools.html



133
134
135
136
137
138
Layout of the source tree
=========================

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

139
src/              Sources for libspot.
140
141
   bin/           User tools built using the Spot library.
      man/        Man pages for the above tools.
142
   dstarparse/    Parser for the output of ltl2dstar.
143
144
   graph/         Graph representations.
   graphtest/     Graph representations.
145
   hoaparse/      Parser for HOA automata and Spin's never claims.
146
   kripke/        Kripke Structure interface.
147
148
   kripkeparse/   Parser for explicit Kripke.
   kripketest/    Tests for kripke explicit.
149
150
151
152
153
154
   ltlast/        LTL abstract syntax tree (including nodes for ELTL).
   ltlenv/        LTL environments.
   ltlparse/      Parser for LTL formulae.
   ltlvisit/      Visitors of LTL formulae.
   ltltest/       Tests for ltlast/, ltlenv/, ltlparse/, and ltlvisit/.
   misc/          Miscellaneous support files.
155
   priv/          Private algorithms, used internally but not exported.
156
157
158
   tgba/          TGBA objects and cousins.
   tgbaalgos/     Algorithms on TGBA.
      gtec/       Couvreur's Emptiness-Check.
159
160
   ta/            TA objects and cousins (TGTA).
   taalgos/       Algorithms on TA/TGTA.
161
   tgbatest/      Tests for tgba/, tgbaalgos/, ta/ and taalgos/.
162
163
   sanity/        Sanity tests for the whole project.
doc/              Documentation for libspot.
164
   org/           Source of userdoc/ as org-mode files.
165
   tl/            Documentation of the Temporal Logic operators.
166
   userdoc/       HTML documentation about the command-line tools.
167
   spot.html/     HTML reference manual for the library.
168
bench/            Benchmarks for ...
169
   dtgbasat/      ... SAT-based minimization of DTGBA,
170
171
172
   emptchk/       ... emptiness-check algorithms,
   ltl2tgba/      ... LTL-to-Büchi translation algorithms,
   ltlcounter/    ... translation of a class of LTL formulae,
173
   ltlclasses/    ... translation of more classes of LTL formulae,
174
   spin13/        ... compositional suspension and other improvements,
175
   wdba/          ... WDBA minimization (for obligation properties).
176
   stutter/       ... stutter-invariance checking algorithms
177
178
179
wrap/             Wrappers for other languages.
   python/        Python bindings for Spot and BuDDy
      tests/      Tests for these bindings
180
      ajax/       LTL-to-TGBA translator with web interface, using Ajax.
181
iface/            Interfaces to other libraries.
182
   ltsmin/        Interface with DiVinE2 and SpinS.
183
184
185

Third party software
--------------------
186

187
buddy/            A customized version of BuDDy 2.3 (a BDD library).
188
ltdl/             Libtool's portable dlopen() wrapper library.
189
lib/              Gnulib's portability modules.
190
utf8/             Nemanja Trifunovic's utf-8 routines.
191

192
193
Build-system stuff
------------------
194
195
196

m4/      M4 macros used by configure.ac.
tools/   Helper scripts used during the build.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
197
198
199
200
201
202
203
204
205

-------------------------------------------------------------------------------
Local Variables:
mode: text
End:

 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
 LocalWords:  ltlast ltlenv ltlparse ltlvisit ltltest misc tgba TGBA tgbaalgos
206
 LocalWords:  gtec Tarjan tgbatest doc html PDF spotref pdf cgi ELTL
207
 LocalWords:  CGI ltl iface BDD Couvreur's emptchk kripke Kripke saba vm
208
 LocalWords:  eltlparse eltltest SABA sabaalgos sabatest ssp ltlcouter scc SCC
209
210
211
LocalWords:  formulae optimizations kripkeparse kripketest Automata
LocalWords:  neverparse ltlcounter ltlclasses parallelizing automata
LocalWords:  wdba WDBA ajax dve DiVinE ltdl Libtool's dlopen