Denis Diderot University at Paris Joseph Fourier University at Grenoble Pierre Mendès France University at Grenoble
LIAFA laboratory VERIMAG laboratory (since October 2001)

TReX at work!

BARRE

TReX: A Tool for Reachability Analysis of CompleX Systems

BARRE

[Introduction   |  References   |  Examples   |  Download   |  Manual   |  Team ]




Introduction

TREX is a tool for automatic analysis of automata-based models equipped with variables belonging to different infinite/finite domains and with parameters. These models are, at the present time, parametric (continuous-time) timed automata, extended with integer counters and finite-domain variables, and communicating through unbounded lossy FIFO channels and shared variables. This model is a subset of the model taken in high-level languages like SDL.

At the present time, TREX does:

The general picture of the TREX environment is given below:
trex environment
The input model of TREX is given by a textual IF file. This file can be obtained by translation (using IF tools) of a graphical SDL specification, or of a textual LOTOS one. Also, the IF file can be used to do, after instantiation of parameters, finite model-checking with the CADP or KRONOS. The input model is the only mandatory input of TREX.
Additionally, the user can specify initial constraints on the parameters occurring in the model. These constraints play the role of an invariant: they are true in each reachable configuration explored by TREX. The exploration can begin either from the initial state of the model or from a symbolic initial configuration specified by the user.

The core of TREX are a forward/backward exploration algorithm and the symbolic representation structures for infinite sets of valuations for variables. The exploration algorithm is generic and can be used for any kind of data structures for which it is possible to provide a symbolic representation structure, a symbolic successor/predecessor function, and an extrapolation procedure.
In the current version, TREX provides three packages for symbolic representation of configurations:

The finite graph generated by TREX is in ALDEBARAN format, one of the graph formats of CADP toolbox. Using CADP, the graph can be minimized using different equivalence relations implemented in ALDEBARAN tool or it can be model-checked using XTL tool.
The symbolic reachable configurations generated by TREX can be used inside abstraction tools like InVest


Related publications


TREX examples

For each example, we give an informal description, the formal description using extended automata, the set of reachable configurations and/or the finite graph obtained with TREX. You can find here the format used for description of input model of TREX.


Download TREX

The stable version of TREX is version 1.3 released February, 14, 2003. A test version 1.4 is available on demand. TREX is entirely developed in C++.

You can find an history of TREX versions here.

The following computer architectures and operating systems are currently supported by TREX.1.0 :

In order to download TREX, please follow the following steps:

Release notes for TREX

Download FOAF

Inside TREX distribution you find also the FOAF library (libfoafmodel.a). FOAF is a library for representation and simplification of non-linear formulas over real and integer variables. For linear formulas on real variables, FOAF also provides an implementation of parameterized Fourier-Motzkin procedure for quantifier elimination. Here is a C++ file describing the use of this library. 

Download old version of TREX

You can download here TREX in version 1.0 released January,10, 2001.




Manual

For the moment, the only manual provided for TREX is given within the distribution, in a Unix man format. 


TREX people


Please send questions or comments about TREX here.
A mirror site is maintained at Verimag.
Last modified: November 25, 2003