Purpose

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.

Setup

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.

mlgmpidl

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

External Dependencies
Installation
opam install mlgmpidl

mlcuddidl

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

Installation
opam install mlcuddidl

APRON

Provides the APRON library of numerical domains.

External Dependencies

All external dependencies of mlgmpidl.

Installation
opam install apron

Bddapron

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

External Dependencies

All external dependencies of APRON.

Installation
opam install bddapron

ReaTK

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

Installation

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

BZReaX automates the compilation of Heptagon/BZR with ReaX.

Installation
opam install bzreax

ctrl2hdl

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.

Installation
opam install ctrl2hdl

ctrl2lut

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.

Installation
opam install ctrl2lut

Guardies

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

Installation
opam install guardies

argos2lus

argos2lus is a compiler translating Argos programs into Lustre.

Installation
opam install argos2lus
⤒