-- chapter6.csp

-- termination and sequential composition

-- A.W. Roscoe

-- This file complements my book on CSP, and is essentially just
-- a translation of some of the main CSP processes in chapter 6 into
-- the machine-readable version of CSP, with suggested things to do with them 
-- on FDR and ProBE.  

-- The following examples, being infinite-state, will not work on FDR
-- though they work well on ProBE

channel up, down

ZERO = up -> POS;ZERO

POS = up -> POS;POS
     [] down -> SKIP

-- Iteration can easily be defined (as it is not directly supported in
-- machine-readable CSP):

Iter(P) = P;Iter(P)

-- So we can get a one-place buffer as described in the text

T = {0,1}

channel left, right: T

COPY = left?x -> right!x -> COPY

assert COPY [FD= Iter(left?x -> right!x -> SKIP)
assert Iter(left?x -> right!x -> SKIP) [FD= COPY

-- and the more contrived version of the 2-place buffer:

TB = left?x -> TB'(x)

TB'(x) = right!x -> SKIP
      [] left?y -> right!x -> TB'(y)

IterBuff2 = Iter(TB)

-- A canonical N-place deterministic buffer:

BN(N,s) = #s<N & left?x -> BN(N,s^<x>)
       [] #s>0 & right!head(s) -> BN(N,tail(s))

assert IterBuff2 [FD= BN(2,<>)
assert BN(2,<>) [FD= IterBuff2