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