tchecker/INSTALL.md

Binary distributions can be found from the Releases page. The instructions below are for installation from the sources. Please, notice that these instructions have only been tested on Linux (Ubuntu and Debian) and Mac OS X. The installation instructions below may not work for other operating systems. Please contact us in case of problem.

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.12)
• 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 (>= 3.2.0) -- probably works with versions starting from v3

Notice that TChecker versions prior to v0.5 were using Catch2 v2. From release v0.5, we are using Catch2 v3. Please refer to Catch2 GitHub repository for sources if Catch2 is not provided by your packaging system.

Building and installing TChecker

We assume that all dependencies have been successfully installed.

Clone the repository:

git clone https://github.com/ticktac-project/tchecker.git

This will create a directory tchecker in the current directory, that contains a fully functional local clone 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. A standard solution is to build a directory build/ inside the directory tchecker/:

cd tchecker
mkdir build
cd build

Then, the configuration depends on your system.

Linux users

Run the following command to configure the build (from inside directory build/):

cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=/path/to/install

In the command above, /path/to/install shall be replaced by the desired installation path. Please, refer to Configuration options for details.

Mac OS X users

The 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. Mac OS X users will need to install a newer version using MacPorts or Brew (or another packaging system). Then, run the following command to configure the build (from inside directory build/):

cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=/path/to/install -DCMAKE_PREFIX_PATH=/path/to/bison

In the command above, /path/to/bison shall be replaced by the actual path to the newer bison executable. And /path/to/install shall be replaced by the desired installation path. Please, refer to Configuration options for details.

Configuration options

• 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.

• 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 installation directory (i.e. the directory specified with option CMAKE_INSTALL_PREFIX).

make -j
make doc
make install

The installation procedure creates four directories: bin, lib, include and share/doc/tchecker/html in the installation directory. The TChecker tools 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.