Information Technology Reference
In-Depth Information
port names. Note that this does not affect the generality of our approach as
we can always make these sets disjoint by applying an appropriate renaming of
ports.
For each state
s
of a given constraint automaton
A
, we define the
mCRL2
process
proc
(
A
,s
) over the action set
P
(
N
)as
,s
)=
s →t
N
,t
)
,
(1)
where
N
=
x∈N
x
represents the multiaction composed from all ports in the
proc
(
A
· proc
(
A
set. Thus, for example,
x∈{A,B,C}
x
=
A
|
B
|
C
. In this view, it comes natural
to have for the synchronization
N
1
|
N
2
of actions
N
1
and
N
2
the union of the
underlying port names
N
1
∪
N
2
. If the action
N
1
claims flow at the ports of the
set
N
1
and the action
N
2
does so for the ports of the set
N
2
, supposedly there
is flow at the ports of the set
N
1
∪
N
2
.
As an example, consider the synchronous FIFO
F
which behaves similarly
to the usual
FIFO
except that it also can dispense a data item from its buffer
and simultaneously accept a new one. Its semantics is given by the constraint
automaton and the corresponding
mCRL2
processes below.
{
A
}
proc
(
F,q
1
)=
A
· proc
(
F
,q
2
);
q
1
q
2
{
A, B
}
proc
(
F
,q
2
)=
B
· proc
(
F
,q
1
)+
A
|
B
· proc
(
F
,q
2
);
{
B
}
In essence, as discussed in Section 4, the translation recursively decomposes a
Reo connector into two subconnectors and puts the
mCRL2
processes obtained for
these subconnectors in parallel, yielding the process for the main connector. To
prove the correctness of this approach formally, we introduce two operations, a
synchronous product
γ
for constraint automata and a synchronized merge
γ
A
for
mCRL2
processes. Thus, given a constraint automaton
for which we have
A
=
A
1
γ
A
2
, we translate the constraint automata
A
2
, say into the
mCRL2
processes
P
1
and
P
2
,andobtain
P
1
γ
P
2
as the translation of
A
1
and
A
.
→
1
,s
0
)
,
→
2
,s
0
)
be two con-
Definition 2.
Let
A
1
=(
S
1
,
N
1
,
A
2
=(
S
2
,
N
2
,
straint automata with disjoint sets of port names
N
1
and
N
2
, respectively. A
port
synchronization function
γ
:
N→N
1
×N
2
is defined as
γ
(
n
)=(
γ
1
(
n
)
,γ
2
(
n
))
through the pair of injective functions
γ
1
:
N→N
1
and
γ
2
:
N→N
2
that map
port names from a new set
N
into port names from the sets
N
1
and
N
2
.
Intuitively,
γ
(
n
)=(
x, y
) represents a renaming of
x
∈N
1
and
y
∈N
2
to
the same common element
n
∈N
. In the context of the port synchronization
N
1
for
N
2
for
function
γ
,wewrite
N
1
\
γ
1
[
N
N
2
\
γ
2
[
N
]and
]. If, for subsets
N
1
⊆N
1
,
N
2
⊆N
2
, it holds that
γ
−
1
[
N
1
]=
γ
−
2
[
N
2
]wewrite
N
1
|
γ
N
2
=(
N
1
∩N
1
)
γ
−
1
1
(
N
2
∩N
2
)
.
∪
[
N
1
]
∪
(2)
From Equation (2) we see that
N
1
|
γ
N
2
is the union
N
1
∪
N
2
but with the
parts of
N
1
and
N
2
that are identified via
γ
1
and
γ
2
replaced by the shared
