Database Reference
In-Depth Information
Fig. 6.3
Synchronization process
Thus, the synchrony of the conversations between
M
U
and
M
R
can be represented
by the transition diagram in Fig.
6.3
. The states of the machines are progressively
enumerated from their initial states, w.r.t. a deterministic transition system
TrS
=
(S
P
,
→
P
)
(in Definition
37
), where
S
P
=
i, st(j)
|
i
is the address of an instruction of
P,
st(j)
S
M
is the state of a machine before the execution of this
i
th
instruction
∈
is the set of the configurations and
→
P
is a function defined for any
(i, st(k))
∈
S
P
by
((i, st(j)),(k,f (st(j
+
1
))))
∈→
P
if
(i,f,k)
∈
P
and
f
is not the identity
function, in the way that for any
j
,
st(j
st(j)
, i.e., the index of the next state
is incremented only if that state is different from the current state.
The
(
+
1
)
=
∗
1
)
and
(
∗
3
)
are the pre/post embedded statements of the host program
f
3
λIn
∗
EU
(
(Program 1),
(
∗
2
)
is a repetition of the composition
t
1
◦
{}
)
◦
t
3
◦
, where
, and
(
∗
4
)
is a repetition of composition
t
1
◦
λIn
∗
ER
(
{}
)
◦
{}=∅
NOP, which is the
identity function.
