TPLib: Tropical Polyhedra Library

TPLib allows to compute a description by extreme points and rays of tropical 
polyhedra defined by means of inequalities, and conversely. 

It also provides a numerical abstract domain based on tropical polyhedra, 
in order to infer min-/max- invariants over programs.

Copyright (C) 2009 Xavier ALLAMIGEON (xavier.allamigeon at m4x.org)

The library was developped when the author was at EADS Innovation Works, with 
the support of the programme of the French National Agency of Research (ANR), 
project ``ASOPT'', number ANR-08-SEGI-005.

*******************************************************************************
DESCRIPTION

The library consists of the following components:

* tplib_core provides two algorithms computing a description by extreme points 
and rays of tropical polyhedra defined by means of inequalities, and 
conversely. These algorithms are described in [1, Chapter 5], see also [2,3].

* compute_ext_rays is a program built from tplib_core, and which computes 
the set of the extreme rays of a tropical cone given by a system of 
inequalities (with integer or -oo coefficients)

Usage: compute_ext_rays <d> where <d> is the dimension of the cone

The system of constraints must be given on the standard input, under the 
following format:
[a_1,...,a_d,b_1,...,b_d] 
to represent the inequality 
max(a_1+x_1,...,a_d+x_d) >= max(b_1+x_1,...,b_d+x_d).
Each constraint must be followed by a newline separator.

Example:
$ compute_ext_rays 5 
[-oo,2,-1,4,-oo,2,2,-oo,4,2]                                                  
[1,-oo,4,5,4,-oo,4,-oo,5,4]

* compute_ext_rays_polar is also built from tplib_core, and computes the set 
of the extreme rays of the polar of a tropical cone given by a generating set
(with integer or -oo coefficients)

Usage: compute_ext_rays_polar <d> where <d> is the dimension of the cone

The generators must be given on the standard input, under the following 
format:
[g_1,...,g_d] 
Each generator must be followed by a newline separator.

Example:
$ compute_ext_rays_polar 5 
[-oo,4,2,3,4]                                                                             
[4,-oo,-5,4,-1]                                                                           
[-oo,-oo,2,3,-1]

* tplib_abstract provides a numerical abstract domain based on tropical 
polyhedra, see [3, Chapter 7], and also [4]. 

* tplib_abstract<x> (x = 0 or 1) is an instantiation of tplib_abstract 
following the interface of APRON abstract domains of level <x>, see [5].

*******************************************************************************
HOW TO BUILD

make <name_of_the_component>

Requirements:
* OCaml >= 3.11
* ocamlbuild
* APRON library for tplib_abstract0 and tplib_abstract1

By default, compute_ext_rays and compute_ext_rays_polar are copied into the 
subdir ./bin, the other components in the subdir ./lib

*******************************************************************************
REFERENCES

[1] X. Allamigeon. Static analysis of memory manipulations by abstract 
interpretation -- Algorithmics of tropical polyhedra, and application to 
abstract interpretation. PhD thesis. 
[2] X. Allamigeon, S. Gaubert, E. Goubault. Computing the Extreme Points of 
Tropical Polyhedra. http://arxiv.org/pdf/0904.3436v2
[3] X. Allamigeon, S. Gaubert, E. Goubault. The tropical double description 
method. Proceedings of STACS'10.
[4] X. Allamigeon, S. Gaubert, E. Goubault. Inferring Min and Max Invariants 
Using Max-plus Polyhedra. Proceedings of the 15th International Static Analysis 
Symposium (SAS'08). 
[5] APRON numerical abstract domain library. http://apron.cri.ensmp.fr/library/