Installation of TChecker

Please, notice that TChecker has only been tested on Linux and Mac OS X. The installation instructions below may not work for other operating systems.

Requirements

TChecker depends on several softwares and libraries listed below. Linux users can install most softwares using the packaging system shipped along with their distribution. Mac OS X users can install the required software using an external packaging system like Brew or MacPorts.

• a C++ compiler with decent C++17 support (Clang >= 3.6 or GNU g++ >= 6 should work. Apple LLVM >= 10.0.0 works)
• CMake (>= 2.8)
• flex (>= 2.5.35)
• bison (>= 3.0.4)
• The Boost library (>= 1.65.0 -- probably works with earlier versions)
• Doxygen (>= 1.8.15 -- probably works with earlier versions)
• Catch2 (>= 2.7.0)

Catch2 can be obtained from Catch2 github repository. Please, refer to Catch2 tutorial for installation instructions.

Building and installing TChecker

We assume that all dependencies have been successfully installed.

Clone the repository:

git clone https://github.com/fredher/tchecker.git

This will create a directory tchecker in the current directory, that contains a fully functional local git repository of the project.

Configure the build

We use cmake to build the project. We recommend to build TChecker out of the source directory. This allows to easily remove the files generated by cmake and by the compiler. This also allows cmake to build a project for your favorite IDE out of the source directory.

The following command first create a build directory, and then runs cmake from the build.

mkdir build
cd build
cmake ../tchecker -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=/path/to/install

This command should be launched from the current directory. Several options shall be specified to cmake, in particular:

• CMAKE_INSTALL_PREFIX specifies the path where TChecker shall be installed. Default directory is /usr/local. You may need administrator privileges to write into /usr/local. Hence, it may be relevant to install TChecker in your account. For instance, to install in directory local in your account: -DCMAKE_INSTALL_PREFIX=$HOME/local.

• CMAKE_BUILD_TYPE specifies to build a Debug or a Release version of TChecker. The difference is that the Debug version runs many checks. It is safer but a lot slower. We recommend to build a Release version.

• if cmake fails to find some of the dependencies, you may need to specify the directories to the software using option CMAKE_PREFIX_PATH and CMAKE_MODULE_PATH.

  • Mac OS X users: the default version of bison that is shipped with Apple development tools is quite old, and it does not support some of the features required by TChecker. You will need to install a newer version using MacPorts or Brew (or another packaging system). Then, you will need to specify the path to the new bison binary adding -DCMAKE_PREFIX_PATH=/usr/local/opt/bison/bin to the command above (the exact path depends your system).

  • Linux users: you will need to install the package libboost-all-dev, but cmake will not be able to find it. You will need to specify the path to cmake adding -DCMAKE_MODULE_PATH=/usr/share/cmake-3.10/Modules to the command above (the exact path depends on your system).

• you may build a project for you favorite IDE adding option -G my_ide to the command above (my_ide should be replaced by your favorite IDE, see the output of cmake -h for available generators).

Building and installing TChecker

The commands below build TChecker and its documentation in the build directory, and then install TChecker in the chosen directory (i.e. the directory specified with option CMAKE_INSTALL_PREFIX).

make -j5
make doc
make install

The installation procedure creates four directories: bin, lib, include and share/doc/tchecker/html in the installation directory. The TChecker tool can be found in directory bin (see Using TChecker). The development tools are provided in the other directories: the headers in include, the library in lib, and the Doxygen documentation in share/doc/tchecker/html.