205 lines
7.6 KiB
Text
205 lines
7.6 KiB
Text
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 Python bindings.
|
|
|
|
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
|
|
|
|
|
|
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
|
|
|
|
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.
|
|
|
|
|
|
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
|
|
in doc/userdoc/, or on-line at http://spot.lrde.lip6.fr/tools.html
|
|
|
|
|
|
|
|
Layout of the source tree
|
|
=========================
|
|
|
|
Core directories
|
|
----------------
|
|
|
|
src/ Sources for libspot.
|
|
bin/ User tools built using the Spot library.
|
|
man/ Man pages for the above tools.
|
|
graph/ Graph representations.
|
|
kripke/ Kripke Structure interface.
|
|
kripkeparse/ Parser for explicit Kripke.
|
|
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.
|
|
tests/ Tests for the whole library.
|
|
twa/ TωA objects and cousins (Transition-based ω-Automata).
|
|
twaalgos/ Algorithms on TωA.
|
|
gtec/ Couvreur's Emptiness-Check.
|
|
sanity/ Sanity tests for the whole project.
|
|
doc/ Documentation for libspot.
|
|
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,
|
|
wdba/ ... WDBA minimization (for obligation properties).
|
|
stutter/ ... stutter-invariance checking algorithms
|
|
wrap/ Wrappers for other languages.
|
|
python/ Python bindings for Spot and BuDDy
|
|
tests/ Tests for these bindings
|
|
ajax/ LTL-to-TGBA translator with web interface, using Ajax.
|
|
iface/ Interfaces to other libraries.
|
|
ltsmin/ Interface with DiVinE2 and SpinS.
|
|
|
|
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.
|
|
|
|
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
|
|
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
|
|
LocalWords: neverparse ltlcounter ltlclasses parallelizing automata
|
|
LocalWords: wdba WDBA ajax dve DiVinE ltdl Libtool's dlopen
|