README 14.2 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++17 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
    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!


47 48 49
Keeping in touch
================

50 51 52 53
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.
54

55 56
We also run a low-traffic and read-only list for announcements of new
releases of Spot.  You may subscribe to that list at
57 58 59
https://www.lrde.epita.fr/mailman/listinfo/spot-announce


60 61 62 63 64 65 66 67 68 69
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.


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

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

76 77
Spot requires a C++17-compliant compiler.  G++ 7.x or later, as well
as Clang++ 5.0 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 86
Optional third-party dependencies
----------------------------------
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
87

88 89 90 91 92
Several tools and functions output automata as "dot files", to be
rendered graphically by tools from the GraphViz package.  Installing
GraphViz is therefore highly recommended if you plan to display
automata.

93 94
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
95

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


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.

113 114 115 116 117 118 119 120 121 122 123
If you plan to use the Python binding, we recommend you use one
of the following --prefix options when calling configure:

  --prefix /usr
  --prefix /usr/local  (the default)
  --prefix ~/.local    (if you do not have root permissions)

The reason is that all these locations are usually automatically
searched by Python.  If you use a different prefix directory, you may
have to tune the PYTHONPATH environment variable.

124
In addition to its usual options, ./configure will accept some
125 126
flags specific to Spot:

127
  --disable-python
128 129 130 131 132 133
    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.
134

135 136 137 138 139 140 141 142
  --enable-max-accsets=N
    Compile Spot so that it supports up to N acceptance sets.  The
    default is 32, so that the membership of each transition to
    any of the 32 acceptance sets can be represented by an
    "unsigned int" (interpreted as a bit-vector).  Using a larger
    N (it still has to be a multiple of 32) will consume more
    unsigned ints per transitions, costing both time and space.

143 144 145 146 147 148 149
  --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.

150 151
  --enable-devel
    Enable debugging symbols, turn off aggressive optimizations, and
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
152
    turn on assertions.  This option is effective by default in
153
    development versions (version numbers ending with a letter).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
154 155 156 157 158 159 160 161 162 163 164 165 166 167
    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

168 169 170
   --enable-glibgxx-debug
     Enable the debugging version libstdc++
     https://gcc.gnu.org/onlinedocs/libstdc++/manual/debug_mode_semantics.html
171
     Note that the debugging version of libstdc++ is incompatible with
172 173 174 175
     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.

176 177 178 179
   --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
180
Here are the meaning of the fine-tuning options, in case
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
181
--enable/disable-devel is not enough.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201

  --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.
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 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273
Troubleshooting installations
-----------------------------

Spot installs five types of files, in different locations.  It the
following, $prefix refers to the directory that was selected using
the --prefix option of configure (the default is /usr/local/).

1) command-line tools go into $prefix/bin/
2) shared or static libraries (depending on configure options)
   are installed into $prefix/lib/
3) Python bindings (if not disabled with --disable-python) typically
   go into a directory like $prefix/lib/pythonX.Y/site-packages/
   where X.Y is the version of Python found during configure.
4) man pages go into $prefix/man
5) header files go into $prefix/include

Depending on how you plan to use Spot, you may have to adjust some
variables such that all these files can be found by the other programs
that look for them.

To test if command-line tools are correctly installed, try running

  % ltl2tgba --version

If your shell reports that ltl2tgba is not found, add $prefix/bin
to you $PATH environment variable.

If the dynamic linker reports that some library (usually libspot.so or
libbddx.so) is not found, you probably have to instruct it to look into
some new directory.  If you installed Spot as root into a classical
system prefix such as /usr or /usr/local/ it may be the case that you
simply have to refresh the cache.  In GNU/Linux this is done by
running "ldconfig -v".  If you installed Spot into a non-standard
directory, you may have to add $prefix/lib some some environment
variable: that variable is called LD_LIBRARY_PATH in GNU/Linux, and
its DYLD_LIBRARY_PATH in Darwin.

To test the Python bindings, try running

  % python3
  >>> import spot
  >>> print(spot.version())

If you installed Spot with a prefix that is not one of those suggested
in the "Building and installing" section, it is likely that the above
import statement will fail to locate the spot package.  You can show
the list of directories that are searched by Python using:

  % python3
  >>> import sys
  >>> print(sys.path)

And you can modify that list of searched directories using the
PYTHONPATH environment variable.

To test if man pages can be found, simply try:

  % man spot

If man reports a message like "No manual entry for spot", add
$prefix/man to the MANPATH environment variable.

Finally header files are needed if you write some C++ that uses Spot.
In that case you may need to pass some -I option to the compiler to
add some "include" directory.  At link time, you may also need to add
some -L option if the libraries are not in some location that is
already searched by the linker.  The file doc/userdoc/compile.html (or
its on-line version at https://spot.lrde.epita.fr/compile.html)
discusses this topic a bit more.

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

275 276 277 278 279 280
Layout of the source tree
=========================

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

281
spot/             Sources for libspot.
282
   graph/         Graph representations.
283
   ltsmin/        Interface with DiVinE2 and SpinS.  (Not part of libspot.)
284
   kripke/        Kripke Structure interface.
285
   tl/            Temporal Logic formulas and algorithms.
286
   misc/          Miscellaneous support files.
287
   mc/            All algorithms useful for model checking
288
   parseaut/      Parser for automata in multiple formats.
289
   parsetl/       Parser for LTL/PSL formulas.
290
   priv/          Private algorithms, used internally but not exported.
291 292
   ta/            TA objects and cousins (TGTA).
   taalgos/       Algorithms on TA/TGTA.
293
   twa/           TωA objects and cousins (Transition-based ω-Automata).
294
   twacube/       TωA objects based on cube (not-bdd).
295
   twacube_algos/ TωAcube algorithms
296
   twaalgos/      Algorithms on TωA.
297
      gtec/       Couvreur's Emptiness-Check (old version).
298
   gen/           Sources for libspotgen.
299 300
bin/              Command-line tools built on top of libspot.
   man/           Man pages for the above tools.
301
tests/            Test suite.
302
   core/          Tests for libspot and the binaries.
303
   ltsmin/	  Tests for the DiVinE2/SpinS interface.
304
   python/        Tests for Python bindings.
305
   sanity/        Tests for the coherence of the source base.
306
doc/              Documentation for Spot.
307
   org/           Source of userdoc/ as org-mode files.
308
   tl/            Documentation of the Temporal Logic operators.
309 310
   userdoc/       HTML documentation about command-line tools, and examples.
   spot.html/     HTML doc for C++ API (not distributed, use --enable-doxygen).
311
bench/            Benchmarks for ...
312
   dtgbasat/      ... SAT-based minimization of DTGBA,
313
   emptchk/       ... emptiness-check algorithms,
314
   ltl2tgba/      ... LTL-to-Büchi translation algorithms,
315 316
   ltlcounter/    ... translation of a class of LTL formulas,
   ltlclasses/    ... translation of more classes of LTL formulas,
317
   spin13/        ... compositional suspension and other improvements,
318
   stutter/       ... stutter-invariance checking algorithms,
319
   wdba/          ... WDBA minimization (for obligation properties).
320
python/           Python bindings for Spot and BuDDy
321 322 323

Third party software
--------------------
324

325
buddy/            A customized version of BuDDy 2.3 (a BDD library).
326
ltdl/             Libtool's portable dlopen() wrapper library.
327
lib/              Gnulib's portability modules.
328
utf8/             Nemanja Trifunovic's utf-8 routines.
329
elisp/		  Related emacs modes, used for building the documentation.
330
picosat/          A distribution of PicoSAT 965 (a satsolver library).
331
spot/bricks/      A collection of useful C++ code provided by DiVinE
332

333 334
Build-system stuff
------------------
335 336 337

m4/      M4 macros used by configure.ac.
tools/   Helper scripts used during the build.
338
debian/  Configuration file to build Debian packages.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
339 340 341 342

-------------------------------------------------------------------------------
Local Variables:
mode: text
343
coding: utf-8
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
344 345
End:

346 347
 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
348
 LocalWords:  ltlast ltlenv ltlparse ltlvisit  misc tgba TGBA tgbaalgos
349
 LocalWords:  gtec Tarjan doc html PDF spotref pdf cgi ELTL LRDE tl
350
 LocalWords:  CGI ltl iface BDD Couvreur's emptchk kripke Kripke saba vm
351
 LocalWords:  eltlparse eltltest SABA sabaalgos sabatest ssp ltlcouter scc SCC
352
LocalWords:  optimizations kripkeparse  Automata IPython subdirectory
353
LocalWords:  neverparse ltlcounter ltlclasses parallelizing automata
354 355
LocalWords:  wdba WDBA ajax dve DiVinE ltdl Libtool's dlopen userdoc
LocalWords:  parseaut parsetl priv TGTA taalgos twa twaalgos dtgbasat
356 357 358 359
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