STOP no actions SKIP successful termination CHAOS(a) the choatic process (on events in a) c -> p simple prefix c ?x ?x':a !y -> p complex prefix p ; q sequential composition p /\ q interrupt p \ a hiding p [[ c <- c' ]] renaming p [] q external choice p |~| q internal choice p [> q untimed timeout b & q boolean guard p ||| q interleaving p [| a |] q sharing p [ a || a' ] q alphabetised parallel p [ c <-> c' ] q linked parallel ; x:s @ p replicated sequential composition [] x:a @ p replicated external choice |~| x:a @ p replicated internal choice (a must be non-empty) ||| x:a @ p replicated interleave [| a' |] x : a @ p replicated sharing || x:a @ [a'] p replicated alphabetised parallel [ c <-> c' ] x:s @ p replicated linked parallel (s must be non-empty)
As a consequence of the laws of CSP,
p ||| q = p [| {} |] q ; x:<> @ p = SKIP [] x:{} @ p = STOP ||| x:{} @ p = SKIP [| a |] x:{} @ p = SKIP || x:{} @ [a] p = SKIP
By definition
CHAOS(a) = |~| x:a @ x -> CHAOS(a) |~| STOP p [> q = (p [] q) |~| q
The general form of the prefix operator is
cf->p where c is a communication
channel, f a number of communication fields and p is the
process which is the scope of the prefix.
A communication field can be
!x output ?x:a constrained input ?x unconstrained input
Note that the set a in the constrained input must match the protocol, so it must be a subset of the values that would be permitted by the unconstrained input.
Fields are processed left to right with the binding produced by any input fields available to any subsequent fields. For example, we can write
channel ints : Int.Int
P = ints?x?y:{x-1..x+1} -> SKIP
Output fields behave as suggested by the equivalence
c !x f -> p = c.x f -> p
The proportion of the channel matched by an input fields is based only on the input pattern. There is no lookahead, so if
channel c : {0..9}.{0..9}.Bool
P = c?x!true -> SKIP -- this will not work
Q = c?x.y!true -> SKIP -- but this will
then P is not correctly defined.
The input pattern x will match the next complete value from the
channel ({0..9}) and true will then fail to match the
next copy of {0..9}.
In the case of @@ patterns, the decomposition is based on the
left-hand side of the pattern.
If an input occurs as the final communication field it will match any remaining values, as in
channel c : Bool.{0..9}.{0..9}
P = c!true?x -> SKIP -- this will work
Q = c!true?x.y -> SKIP -- this will also work
This special case allows for the construction of generic buffers.
BUFF(in,out) = in?x -> out!x -> BUFF(in, out)
is a one place buffer for any pair of channels.
Dots do not directly form part of a prefix: any which do occur are either part of the channel c, or the communication fields. (FDR1 took the approach that dots simply repeated the direction of the preceding communication field. This is a simplification which holds only in the absence of datatype tags.)
The guard construct `b & P' is a convenient shorthand
for
if b then P else STOP
and is commonly used with the external choice operator (`[]'), as
COUNT(lo,n,hi) = lo < n & down -> COUNT(lo,n-1,hi) [] n < hi & up -> COUNT(lo,n+1, hi)
This exploits the CSP law that p[]STOP=p.
The linked parallel and renaming operations both use the comprehension syntax for expressing complex linkages and renamings.(15) For example,
p [ right.i<->left.((i+1)%n), send<->recv | i<-{0..n-1} ] q
p [[ left.i<-left.((i+1)%n), left.0<-send | i<-{0..n-1} ]]
Both the links (c<->c') and the renaming pairs (c<-c',
read `becomes') take channels of the same type on each side and extend
these pointwise as required.
For example,
p [[ c <- d ]]
is a process which behaves like p except all occurrences of
channel c in p are replaced by channel d (so that
c `becomes' d).
This is defined when extensions(c) is the same as
extensions(d) and is then the same as
p [[ c.x <- d.x | x<-extensions(c) ]]
The replicated operators allow multiple generators between the operator and the `@' sign in the same way as comprehensions. The terms are evaluated left-to-right, with the rightmost term varying most quickly. So
; x:<1..3>, y:<1..3>, x!=y @ c!x.y->SKIP
is the same as
c.1.1->c.1.2->c.2.1->c.2.3->c.3.1->c.3.2->SKIP
The linked parallel operator generalises the chaining operator
(>>) of [Hoare85].
For example, if COPY implements a single place buffer,
COPY(in,out) = in?x -> out!x -> COPY(in,out)
then we can implement an n-place buffer by
BUFF(n,in,out) = [out<->in] i:<1..n> @ COPY(in, out)
Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.