In order to ease the installation of some of the tools I develop(ped) (ReaX, argos2lus) along with their dependencies, I have setup an opam repository accessible through this page.


I quickly detail here the steps needed to compile and use packages available in my opam repository.

Opam eases the management and installation of libraries and tools, by automatically handling most of their dependencies.

Installing External Dependencies

Operations to perform these prerequisite steps depend on your operating system:

Installing & Initializing Opam, & Upgrading the OCaml Compiler

Install Opam first (GNU/Linux users can install a package named opam — OSX users can type brew install opam), and initialize it with opam init.

Some of the packages below require a recent version of the OCaml system (≥ 4.02.0) to compile — type ocaml -version to know what version you are using by default. If you need to upgrade it, then just run opam switch 4.02.1 (or choose a more recent version) and then eval `opam config env` (note that you can also use opam init --comp=4.02.1 to initialize opam directly with this version of the compiler).

Configuring Opam to use the Repository

Type the following command in a shell to make the repository available to opam (do not forget to type eval `opam config env` beforehand if necessary):

opam repo add nberth-repo "https://framagit.org/nberth/opam-repo/raw/master"

You can then proceed to install packages as indicated bellow.

Contents & Package-specific Installation Instructions

I list below some of the packages available in this repository. To set up a package, install first its external dependencies if some are listed, and then directly type its associated opam installation command. The versions available for each package are the most up-to-date as of March 3rd 2015; some may have been further upgraded since.


The mlgmpidl library provides OCaml bindings to the GMP and MPFR libraries.

External Dependencies
opam install mlgmpidl


The mlcuddidl library incorporates CUDD along with OCaml bindings for it.

opam install mlcuddidl


Provides the APRON library of numerical domains.

External Dependencies

All external dependencies of mlgmpidl.

opam install apron


Provides the Bddapron library of combined Boolean and numerical abstract domains.

External Dependencies

All external dependencies of APRON.

opam install bddapron


ReaTK is the reactive systems verification and synthesis toolkit. Along with a version of the ReaVer tool, this package provides the ReaX tool for solving discrete controller synthesis problems for infinite state systems given as Controllable-Nbac programs, plus several libraries for handling such files and models.

Installing ReaTK without some of its optional dependencies only builds the reatk.ctrlNbac library that allows to generate and manipulate Controllable-Nbac files; this permits to avoid installing most dependencies if only this library is needed (to compile recent versions of Heptagon/BZR for instance).

External Dependencies

All external dependencies of Bddapron (= external dependencies of mlgmpidl).


The following command only installs the reatk.ctrlNbac library if optional dependencies are missing:

opam install reatk

To install all libraries and tools, use the following:

opam install fixpoint bddapron reatk


BZReaX automates the compilation of Heptagon/BZR with ReaX.

opam install bzreax


ctrl2hdl is a compiler translating nodes, controllers, and functions produced by ReaX into hardware description languages (Verilog or VHDL); it can be used to execute Controllable-Nbac nodes, possibly involving controllable variables.

opam install ctrl2hdl


ctrl2lut is a compiler translating controllers produced by ReaX into stochastic reactive systems specified as Lutin programs; it can be used to execute Controllable-Nbac nodes, possibly involving controllable variables.

opam install ctrl2lut


Guardies is a static analysis tool that can be used to detect of potential leaks of confidential data or vulnerabilities in object-oriented programs given as Java bytecode.

External Dependencies

All external dependencies of ReaTK (= external dependencies of mlgmpidl).

opam install guardies


argos2lus is a compiler translating Argos programs into Lustre.

opam install argos2lus