Go backward to
Summation
Go up to
Top
Go forward to
Examples
Example
Received values to be acknowledged.
D
:=
in
(
x
).
out
(
x
).
ackout
.
ackin
.
D
D
acknowledges input after it has delivered value as output and received acknowledgement.
Synchronization actions
ackout
,
ackin
.
Combination of
n
copies of
D
:
D
(n)
:=
D
^
D
^...^
D
D
(n)
behaves like
single
copy of
D
!
D
^
D
=
D
!
Alternative definition:
D'
:=
in
(
x
).
ackin
.
out
(
x
).
ackout
.
D'
D'
(n)
=
Buff
'
n
< >.
Slightly modified specification
Buff
'
n
.
Author:
Wolfgang Schreiner
Last Modification: June 8, 1998