Information Technology Reference
In-Depth Information
The traditional rst example of a process expressed in a new process algebra
is the simple vending machine
(Figure 3). It serves an indenite series of
customers by alternately accepting a coin and emitting a chocolate. The expected
behaviour of a single customer engaging in a single transaction is
VM
cust = df coin
:
choc
:
0
The behaviour of the whole population of customers is modelled by the un-
bounded set (!cust). This population can insert an indenite number of coins;
and at any time a lesser number of chocolates can be extracted. But we plan
to install a simple
that can serve only one customer at a time. To imple-
ment this sequentialisation, we need an internal control signal
VM
, by which the
machine signals to itself its own readiness for the next customer. The complete
denition of the vending machine is given in Figure 3.
nx
one
= df nx:
coin . choc
:
nx
:
0
many = df
(!one)
j
( nx
:
0 )
VM
= df
( new
nx
)many
Figure 3. Vending Machine
The operational semantics of the programming language is presented as a
collection of formulae, describing all the permitted steps that can be taken in the
execution of a complete program. Each kind of step is described by a transition
rule written in the form
P ! Q
,where
P
gives a pattern to be matched against
the current state of the program, and
Q
describes how the program is changed
after the step. For example, the rule
(
e:P
)
j
(
e:Q
)
!
(
P j Q
)
describes an execution step in which one process accepts a signal on
which is
sent by the other. Emission and acceptance of the signal are synchronised, and
their simultaneous occurrence is concealed; the subsequent behaviour is dened
as parallel execution of the rest of the two processes involved.
The reduction shown above can be applied directly to a complete program
consisting of a pair of adjacent processes written in the order shown and sep-
arated by the parallel operator
e
. But we also want to apply the reduction to
processes written in the opposite order, to processes which are embedded in a
larger network, and to pairs that are not even written adjacently in that net-
work. Such reductions can be described by a larger collection of formulae, for
example
j
(
e:Q
)
j
(
e:P
)
! Q j P
((
e:Q
)
j
(
e:P
))
j R !
(
Q j P
)
j R
(
e:Q j R
)
j
(
e:P
)
!
(
Q j R
)
j P
Search WWH ::




Custom Search