TCLTL is a model checker for timed-automata.

It is based on TChecker (for generating the state-space) and Spot (for
LTL model checking), and developped as part of the tick-tac project.


To compile:

  1. Install a recent release of Spot (at least 2.8.3)

     https://spot.lrde.epita.fr/install.html

     In what follows, we assume you have run "make install" and that
     Spot is installed in /usr/local/ (the default destination).

  2. Install the git version of TChecker

     https://github.com/ticktac-project/tchecker/wiki/Installation-of-TChecker

     You need to pass -DLIBTCHECKER_ENABLE_SHARED=1 to cmake so that a
     shared library is built.

     In what follows, we assume you have run "make install" and that
     TChecker is also installed in /usr/local/.  Under GNU/Linux you
     may need to run "sudo ldconfig" after "make install" so that
     libtchecker.so can be found by ld.so.

  3. Finally, compile and install tcltl:

     If you start from a git checkout, you should first install autoconf, automake,
     libtool, swig, perl, python3-dev, then do

     $ cd tcltl
     $ autoreconf -vfi
     $ ./configure [OPTIONS]
     $ make
     $ make install

     If you start from a tarball, do

     $ tar zxvf tcltl-X.Y.tar.gz
     $ cd tcltl-X.Y
     $ ./configure [OPTIONS]
     $ make
     $ make install

     If Spot is installed in a non-default directory, you can specify
     its location by passing --with-spot=PREFIXDIR as an option to
     configure.  PREFIXDIR should be the directory that contains the
     lib/ and include/ directories where Spot is installed.

     You may disable the Python bindings with --disable-python.