Information Technology Reference
In-Depth Information
The
LossySync
differs from the
Sync
channel only in one coloring, i.e. col-
oring (2) where the sink node is not ready to accept data, but there is data
available at the source end. In this situation the
LossySync
permits flow at the
source end and loses the data item. Otherwise, no-flow behaviors are possible
only when no data is available at the source end.
Nodes are encoded in the same way as channels in the coloring semantics. As
usual, we build nodes out of mergers and replicators. Figure 1 depicts the valid
colorings of the
Merger
primitive. An interesting fact here is that intuitively the
colorings allow a propagation of no-flow reasons through the connector. Note
also that it is sucient to allow no-flow reasons from both sides in channels
only, which leads to a smaller number of coloring in the nodes.
To deal with context-dependency in our encoding in
mCRL2
we incorporate
the coloring model. We encode the different colors as simple data parameters of
actions. We therefore introduce a new datatype
sort
Colored
=
struct
flow
(
data
:
Data
)
|
noflowG
|
noflowR
where
Data
is the global datatype as introduced in the constraint automata
encoding presented in the previous section. The idea is that we explicitly model
no-flow actions and wrap actual data items into flow actions. We use here
noflowG
and
noflowR
as abbreviations for respectively
no-flow-give-reason
and
no-flow-require-reason
. With this setup, the encoding of the primitives is straight-
forward. For instance, the
Sync
channel is defined as
Sync
=
Σ
d
:
Data
A
(
flow
(
d
))
|
B
(
flow
(
d
)) +
(1)
A
(
noflowR
)
|
B
(
noflowG
)+
(2)
A
(
noflowG
)
|
B
(
noflowR
)+
(3)
B
(
noflowG
)
·
A
(
noflowG
)
|
Sync
;
(4)
where each line corresponds to a coloring in Figure 1(b). In the same way, the
LossySync
can be specified as
LossySync
=
Σ
d
:
Data
A
(
flow
(
d
))
|
B
(
flow
(
d
)) +
(1)
A
(
flow
)
|
B
(
noflowG
)+
(2)
A
(
noflowG
)
|
B
(
noflowR
)+
(3)
B
(
noflowG
)
·
A
(
noflowG
)
|
LossySync
;
(4)
and finally, the
Merger
can be encoded as
Merger
=
Σ
d
:
Data
A
(
flow
(
d
))
|
B
(
noflowG
)
|
C
(
flow
(
d
)) +
(1)
Σ
d
:
Data
A
(
noflowG
)
|
B
(
flow
(
d
))
|
C
(
flow
(
d
)) +
(2)
A
(
noflowR
)
|
B
(
noflowR
)
|
C
(
noflowG
)+
(3)
C
(
noflowR
)
·
A
(
noflowG
)
|
B
(
noflowG
)
|
Merger
;
(4)
The other channels are encoded analogously.
