Information Technology Reference
In-Depth Information
The above translation aims at accounting for the intuition that
Op
1
must
take place before
Op
2
. However, we cannot translate
Op
1
;
Op
2
immediatly as
[
Op
2
]
π
, because in general
π
-calculus would not allow the resulting syn-
tax (e.g.,
Op
1
]
π
.
[
.R
would not be a valid expression). Therefore, we adapt the
suggestion offered by Milner [4] (in Example 5.27), which requires every opera-
tion to signal its own termination with a
done
event.
(
P
+
Q
)
Definition 15 (Sequence).
Let
Op
be an operation and
n
be an integer such
that
n
≥
1
.Thena
sequence
of
n
compositions of
Op
is defined as:
Op
;
Seq
(
Op, n
−
1)
n>
1
Seq
(
Op, n
)=
Op
n
=1
Definition 16 (Unbounded Sequence).
Let
Op
an operation. Then an
un-
bounded sequence
of compositions of
Op
is defined as:
Forever
(
Op
)=
Op
;
Forever
(
Op
)
The translation of these two kinds of sequences to
π
-calculus follows, of course,
from the translation of the sequential composition operator.
Definition 17 (Choice).
Let
Op
1
and
Op
2
be operations. Then their composi-
tion as a
choice
is also an operation and is written as:
Op
1
+
Op
2
Moreover,
Op
2
]
π
Definition 18 (Parallel Composition).
Let
Op
1
,
Op
2
,
...
,
Op
n
be
n
opera-
tions. Then their
parallel composition
is also an operation and is written as:
[
Op
1
+
Op
2
]
π
=[
Op
1
]
π
+[
Op
1
Op
2
...
Op
n
Moreover,
[
Op
1
Op
2
...
Op
n
]
π
=(
νstart
)[
Op
1
]
π
{
start/done
}|
[
Op
2
]
π
{
start/done
}|
...
|
[
Op
n
]
π
{
start/done
}|
start.start.....start
.done
n
times
The translation for the parallel composition is not straightforward because it is
necessary to ensure that
done
is sent only once in the composed operation. That
is to say, the parallel composition of
n
operations
2
is an operation itself, and it
only terminates when each of its components terminates.
3.2 Core Operations
We can now provide a core of operations upon which others can be built.
2
We define the operator for
n
operations instead of just two because this avoids the
problem of establishing its associativity properties.
Search WWH ::
Custom Search