TPLib: Tropical Polyhedra Library

TPLib implements several algorithms to manipulate tropical polyhedra. Among 
others, it allows to compute:
* the extreme points and rays of tropical polyhedra, 
* tropical polar cones,
* the minimal representations by means of half-spaces,
* the tropical complex associated with a tropical polytope.

TPLib also provides abstract operations over tropical polyhedra (intersections,
convex hull of unions, etc), which are typically useful in applications to 
formal verification. 

Copyright (C) 2009-2013 Xavier ALLAMIGEON (xavier.allamigeon at inria.fr)

Version 1.0 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.

*******************************************************************************
CONTENTS

1. Command-line programs

Most of the algorithms implemented in TPLib can be directly called using 
command-line programs. They use standard input/output, and can be easily 
combined using pipes.

* compute_ext_rays computes the set of the extreme rays of a tropical 
polyhedral cone given by a system of inequalities (with integer or -oo 
coefficients), see [1,2].

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

The system of constraints are 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 (including the last one) 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 computes the set of the extreme rays of the polar of 
a tropical cone given by a generating set (with integer or -oo coefficients),
see [3].

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

The generators are given on the standard input, under the following format:
[g_1,...,g_d] 
Each generator (including the last one) 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]

* compute_halfspaces computes a minimal external representation by means of 
tropical half-spaces of a tropical cone given by a generating set, see [4].

It currently handles only the case of generating sets in which every vector 
has finite entries. Its usage is the same as compute_ext_rays_polar. 

Each half-space is displayed under the format:
(apex,list_of_sectors)

* compute_tropical_complex computes the tropical complex associated with a 
tropical cone given by a generating set (see [6]). Its usage is the same as
compute_ext_rays_polar. Only generating sets in which every vector has 
finite entries are supported.

It outputs the vertices of the complex, and the maximal cells of the 
complex (defined by adjacency with vertices). Note that each cell is seen as 
a usual polytope, and not as a tropical one.

Alternatively, compute_tropical_complex is able to output the tropical complex
under polymake format (http://www.polymake.org), by calling the option 
-polymake-output, followed by the name of the variable to be used in polymake.

Example:
compute_tropical_complex -polymake-output "cyclic_cplx" 4
[0,1,2,3]
[0,2,4,6]
[0,3,6,9]
[0,4,8,12]

* compute_tangent_hypergraph computes the tangent directed hypergraph of a 
point in a tropical cone (see [1,2]). By default, the cone is provided by a 
system of inequalities.

Usage: compute_tangent_hypergraph <d> <point> where d is the dimension of
the cone and <point> the point.

The system of inequalities must be given on the standard input.

Example:
$ compute_tangent_hypergraph 3 [0,1,3]
[-oo,0,-oo,1,-oo,-oo]
[-oo,-4,-3,0,-oo,-oo]
[-oo,-oo,-1,0,-6,-oo]
[0,-oo,-oo,-oo,-oo,-4]
[0,-8,-oo,-oo,-oo,-3]

The cone can be alternatively specified by a generating set, or a list of 
half-spaces, respectively using the options -generators and -half-spaces. 

Examples:
$ compute_tangent_hypergraph -generators 3 [0,1,3]
[0,1,3]
[0,4,1]
[0,9,4]

$ compute_tangent_hypergraph -half-spaces 4 [0,2,5,8]
([0,1,4,8],[1,3])
([0,3,6,10],[0,3])
([0,3,7,11],[0,2])
([0,3,7,11],[0,3])
([0,4,8,12],[0])
([0,1,5,9],[1])
([0,1,2,6],[2])
([0,1,2,3],[3])
([0,1,3,5],[0,3])
([0,1,2,4],[0,3])
([0,1,2,4],[1,3])
([0,1,3,7],[0,2])
([0,2,4,7],[0,3])
([0,2,5,9],[0,2])
([0,1,3,6],[1,3])

IMPORTANT NOTES:
* By default, command-line programs use the max-plus instantiation of tropical 
algebra. The min-plus instantiation can be used instead, by calling the option
-min-plus.

* The type of the underlying numerical data used by command-line programs can 
be parametrized using the option -numerical-data <type_of_numerical_data>. 
The following types are available:
** ocaml_int (default) - 31 bits OCaml's integers
** ocaml_float - double precision OCaml's floating-point numbers
** ocaml_big_int - OCaml's arbitrary-precision integers (quite slow)
** ocaml_big_rat - rationals over ocaml_big_int

If the optional OCaml librairies zarith and/or mlgmp are installed (see below),
the following additional types are available:
** zarith_int / zarith_rat - arbitrary-precision integers/rationals based on
zarith library
** mlgmp_int / mlgmp_rat - arbitrary-precision integers/rationals based on
mlgmp library

It is strongly recommended to use arbitrary-precision numerical data, in order 
to avoid errors due to overflows or rounding. OCaml's implementation of 
arbitrary-precision integers is very slow. We suggest to use zarith or mlgmp
instead.

-------------------------------------------------------------------------------

2. OCaml library

The most important OCaml modules are:
* tplib_core, which consists of the main algorithms on tropical polyhedra,
* tplib_abstract, which provides abstract operations over tropical polyhedra, 
to use them as a numerical abstract domain based on tropical polyhedra, 
see [1, Chapter 7], and also [5]. 

-------------------------------------------------------------------------------

3. Bindings to C

TPLib provides bindings of the module tplib_abstract to the language C. 
Examples can be found in the sub-directory "tests".

*******************************************************************************
INSTALLATION

./configure
make
make install 

Requirements:
* OCaml >= 3.12
* ocamlbuild (should ship with OCaml distribution)
* ocamlfind (also known as findlib)
* (optional) zarith (OCaml binding for GMP, see 
http://forge.ocamlcore.org/projects/zarith), 
or alternatively, mlgmp (OCaml bindings for GMP/MPFR)

We recommend to use the package manager OPAM (http://opam.ocamlpro.com) to 
install the dependencies.

*******************************************************************************
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 vertices of tropical
polyhedra using directed hypergraphs. Discrete & Computational Geometry, 
49(2):247–279, 2013. E-print arXiv:0904.3436v4.
[3] X. Allamigeon, S. Gaubert, and R. D. Katz. Tropical polar cones, 
hypergraph transversals, and mean payoff games. Linear Algebra Appl., 
435(7):1549–1574, 2011. E-print arXiv:1004.2778.
[4] X. Allamigeon and R.D. Katz. Minimal external representations of tropical 
polyhedra. Journal of Combinatorial Theory, Series A, 120(4):907–940, 2013. 
Eprint arXiv:1205.6314.
[5] 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). 
[6] M. Develin and B. Sturmfels. Tropical convexity. Doc. Math., 9:1–27 
(electronic), 2004. E-print arXiv:math.MG/0308254.
