-
Notifications
You must be signed in to change notification settings - Fork 0
/
README
249 lines (202 loc) · 9.83 KB
/
README
1
2
3
4
5
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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
Overview
========
Spot is a model-checking toolkit comprising:
- a C++11 library with data-structures and algorithms for working
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.
Keeping in touch
================
If you have questions regarding Spot, or bug to report, please send
them to <[email protected]>. 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 a low-traffic and read-only list for announcements of new
releases of Spot. You may subscribe to that list at
https://www.lrde.epita.fr/mailman/listinfo/spot-announce
Installation
============
Requirements
------------
Spot requires a C++11-compliant compiler.
G++ 4.8 or later, as well as Clang++ 3.5 or later should work.
Spot expects a complete installation of Python (version 3.3 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).
Optional third-party dependencies
----------------------------------
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.
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://www.lrde.epita.fr/dload/spot/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.
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.
In addition to its usual options, ./configure will accept some
flags specific to Spot:
--disable-python
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.
--enable-devel
Enable debugging symbols, turn off aggressive optimizations, and
turn on assertions. This option is effective by default in
development versions (version numbers ending with a letter).
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
--enable-glibgxx-debug
Enable the debugging version libstdc++
https://gcc.gnu.org/onlinedocs/libstdc++/manual/debug_mode_semantics.html
Note that the debugging version of libstdc++ is incompatible with
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.
Here are the meaning of the fine-tuning options, in case
--enable/disable-devel is not enough.
--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.
Layout of the source tree
=========================
Core directories
----------------
spot/ Sources for libspot.
graph/ Graph representations.
ltsmin/ Interface with DiVinE2 and SpinS. (Not part of libspot.)
kripke/ Kripke Structure interface.
tl/ Temporal Logic formulas and algorithms.
misc/ Miscellaneous support files.
parseaut/ Parser for automata in multiple formats.
parsetl/ Parser for LTL/PSL formulas.
priv/ Private algorithms, used internally but not exported.
ta/ TA objects and cousins (TGTA).
taalgos/ Algorithms on TA/TGTA.
twa/ TωA objects and cousins (Transition-based ω-Automata).
twaalgos/ Algorithms on TωA.
gtec/ Couvreur's Emptiness-Check.
bin/ Command-line tools built on top of libspot.
man/ Man pages for the above tools.
tests/ Test suite.
core/ Tests for libspot and the binaries.
ltsmin/ Tests for the DiVinE2/SpinS interface.
python/ Tests for Python bindings.
sanity/ Tests for the coherence of the source base.
doc/ Documentation for Spot.
org/ Source of userdoc/ as org-mode files.
tl/ Documentation of the Temporal Logic operators.
userdoc/ HTML documentation about the command-line tools.
spot.html/ HTML reference manual for the library.
bench/ Benchmarks for ...
dtgbasat/ ... SAT-based minimization of DTGBA,
emptchk/ ... emptiness-check algorithms,
ltl2tgba/ ... LTL-to-Büchi translation algorithms,
ltlcounter/ ... translation of a class of LTL formulas,
ltlclasses/ ... translation of more classes of LTL formulas,
spin13/ ... compositional suspension and other improvements,
stutter/ ... stutter-invariance checking algorithms,
wdba/ ... WDBA minimization (for obligation properties).
python/ Python bindings for Spot and BuDDy
ajax/ LTL-to-TGBA translator with web interface, using Javascript.
Third party software
--------------------
buddy/ A customized version of BuDDy 2.3 (a BDD library).
ltdl/ Libtool's portable dlopen() wrapper library.
lib/ Gnulib's portability modules.
utf8/ Nemanja Trifunovic's utf-8 routines.
elisp/ Related emacs modes, used for building the documentation.
picosat/ A distribution of PicoSAT 965 (a satsolver library).
Build-system stuff
------------------
m4/ M4 macros used by configure.ac.
tools/ Helper scripts used during the build.
debian/ Configuration file to build Debian packages.
-------------------------------------------------------------------------------
Local Variables:
mode: text
coding: utf-8
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 misc tgba TGBA tgbaalgos
LocalWords: gtec Tarjan doc html PDF spotref pdf cgi ELTL LRDE tl
LocalWords: CGI ltl iface BDD Couvreur's emptchk kripke Kripke saba vm
LocalWords: eltlparse eltltest SABA sabaalgos sabatest ssp ltlcouter scc SCC
LocalWords: optimizations kripkeparse Automata IPython subdirectory
LocalWords: neverparse ltlcounter ltlclasses parallelizing automata
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 PSL
LocalWords: Jupyter Doxygen rewritings reimplementation ltlcross utf
LocalWords: glibgxx libstdc GLIBCXX Javascript Nemanja Trifunovic's
LocalWords: elisp emacs debian