 ( 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.
• The control part  is constitued with a finite set of control states and a finite valuation for boolean or enumerative variables.
• The data part is constitued with for example valuations of lossy fifo channels, counters or clocks.

Each process is modelised by a graph representation in which

• control states are the circles
• transition's labels are of the form "l : g / op ". Where :
• "l " : is the transition's name.
• " g " : is the transition's guard. It could be a constraints conjunction on counters, booleans, enumeratives variables, clocks and parameters. It could also be the emptiness test for lossy fifo channel (empty(M) where M is a channel).
• " op " : is a set of affectation operations of the form :
• Boolean :  b1 := b2 or b1 := true or b1 := false or b1 := not(b2),  where b1 and b2 are booleans variables.
• Enumerative variables : e1 := v   where e1 is a enumerative variable and v a valuation for e1.
• Counters : c1 := c2 + b1 or c1 := b1 where c1, c2 are two counters (may be the same one), b1 is an integer or an integer parameter.
• Clocks : x1 := x2 or reset(x1) where x1, x2 are two clocks.
• Lossy fifo channel : f!m or f?m or nop, where f is a channel and m a message. f!m means the sending of m through f, f?m represents the reception of m through f and nop has no effect on the file contents.
•    I(q1) : is an clock invariant for the control state q1. This is a conjunction of constraints on clocks and parameters which indicates generally the maximum delay that a clock could spend in the state.

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