The Mealy machines we consider are 5-uple of the shape:
< Q, qinit,I, O, T, &lambda>, where:
- Q is a finite set of states;
- qinit &isin Q denotes an initial state.;
- I (resp. O) is a finite set of input (resp. output) events;
- T &sube Q × Q is the transition relation;
- &lambda is a labeling function: &lambda : T × IB &rarr 2O
.
 |
- IB is the set of Boolean expressions built from atom in I;
- 2O is the set of subsets of O.
|