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.2 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://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.


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 with used in an IPython notebook, and are
    also used 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 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 on-line at http://spot.lip6.fr/userdoc/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.
   dstarparse/    Parser for the output of ltl2dstar.
   graph/         Graph representations.
   graphtest/     Graph representations.
   hoaparse/      Parser for HOA automata and Spin's never claims.
   kripke/        Kripke Structure interface.
   kripkeparse/   Parser for explicit Kripke.
   kripketest/    Tests for kripke explicit.
   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.
   priv/          Private algorithms, used internally but not exported.
   ta/            TA objects and cousins (TGTA).
   taalgos/       Algorithms on TA/TGTA.
   tgbatest/      Tests for twa/, twaalgos/, ta/ and taalgos/.
   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 formulae,
   ltlclasses/    ... translation of more classes of LTL formulae,
   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 ltltest misc tgba TGBA tgbaalgos
 LocalWords:  gtec Tarjan tgbatest 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:  formulae optimizations kripkeparse kripketest Automata
LocalWords:  neverparse ltlcounter ltlclasses parallelizing automata
LocalWords:  wdba WDBA ajax dve DiVinE ltdl Libtool's dlopen