(back to TReX home page) ( back to TReX home page)


TReX Examples

Format Description
Version 1.0 - Date 01/01/10

Modelisation format

Each process is composed with a finite-control part and an eventually infinite data-part.

Each process is modelised by a graph representation in which

Where :

file.scf format

TReX provides the reachable configurations set of a system in "file.scf" (option -r file.scf). This file contains at most 3 parts : the reachable configurations set, the correspondence between control states of the system and states in the symbolic graph (with option -sg file.aut) and the time consumption.

We give bottom an example of file.scf :

========== Reachable Symbolic Configurations ==========
( system control state, property control state, valuation of boolean and enumerative variables,
clocks valuations,
counters valuations,
channels contents,
constraints conjunction of parameters  ->
clocks valuation,
counters valuations,
channels contents,
constraints conjunction of parameters

========== Correspondence with Symbolic Graph  ==========
[ symbolic graph control state -- ( system control state,  valuation of boolean and enumerative variables, property control state) ]
[ ...]

========== Time Statistics ==========

child : x.xx
self  : x.xx
total : x.xx

The symbolic reachable configurations are ordered by  system finite control part  which is the association of the system control state, the property control state (option -p prop.if) and the valuation of booleans and enumerative variables. For each finite control value it may be few data valuations separated by "->".

In the time statistics one can read the time ellapsed in child processes (Omega, Reduce) and in execution of TReX (self).

file.aut format

The symbolic graph is given under the aldebaran format.

des ( initial state, #transitions, #control state)
(ei, label, ef)
(ei, label, ef)

where ei, ef are symbolic graph state and label is either the name corresponding of transition's model. either "i" the internal label.

The aldebaran tool belongs to the more general toolkit CADP (where you can find tools for visualising the graph, performing minimisation on it, uso...)