```%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%	XL Code for Eratosthenes' Sieve:
%%	patterned after, but slightly diffrent from,
%%	the Bell Labs bench suite from Doron Peled
%%	Y.S.R., 23 Dec 96.
%%	Parameterized and adapted for XL, C.R., June 98.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%-----------------------------------------------------------------------------
%%	The generator process
%%	generates integer from Cur to Max
%%	 and send it through channel "right"
generator(Cur, Max) ::=
out(right, Cur) o
Cur1 is Cur+1 o
if( Cur =< Max
,	generator(Cur1, Max)
,	end
).

%%-----------------------------------------------------------------------------
%%	The filter process

unit ::=
in(left, P) o
filter(P).

filter(P) ::=
in(left, N) o
if( 0 is N mod P
,	true
,	out(right, N)
) o
filter(P).

%%-----------------------------------------------------------------------------
%%	The consumer process

consumer(N, MAX) ::=
in(left, X) o
N1 is N-1 o
if( N1 > 0
,	consumer(N1, MAX)
,	if( X == MAX
,	action(finish)
,	action(fail)
) o
end
).

%%-----------------------------------------------------------------------------
%%	A one-buffer channel

chan ::=
in(left, X) o
out(right, X) o
chan.

%%-----------------------------------------------------------------------------
%%	The sieve system
%%	N_UNIT	: number of filters
%%	PRIME	: the (NUM+1)th prime number
%%	N_OVER	: number of overflow prime numbers
%%	MAX	: the (NFILTER+NOVER)th primer number
%%	Table of prime:
%%	      N :   1   2   3   4   5   6   7   8   9  10  11
%%	  PRIME :   2   3   5   7  11  13  17  19  23  29  31
%%	Table of (N_UNIT, MAX) for N_OVER=4:
%%	 N_UNIT :   1   2   3   4   5   6   7   8   9  10  11
%%	    MAX :  11  13  17  19  23  29  31  37  41  43  47

sieve3 ::=
( generator(2, 17) @ [right/ci(0)]
| chan @ [left/ci(0), right/co(0)]
| unit @ [left/co(0), right/ci(1)]
| chan @ [left/ci(1), right/co(1)]
| unit @ [left/co(1), right/ci(2)]
| chan @ [left/ci(2), right/co(2)]
| unit @ [left/co(2), right/ci(3)]
| chan @ [left/ci(3), right/co(3)]
| consumer(4, 17) @ [left/co(3)]
) \ { ci(_), co(_) }.

sieve4 ::=
( generator(2, 19) @ [right/ci(0)]
| chan @ [left/ci(0), right/co(0)]
| unit @ [left/co(0), right/ci(1)]
| chan @ [left/ci(1), right/co(1)]
| unit @ [left/co(1), right/ci(2)]
| chan @ [left/ci(2), right/co(2)]
| unit @ [left/co(2), right/ci(3)]
| chan @ [left/ci(3), right/co(3)]
| unit @ [left/co(3), right/ci(4)]
| chan @ [left/ci(4), right/co(4)]
| consumer(4, 19) @ [left/co(4)]
) \ { ci(_), co(_) }.

sieve5 ::=
( generator(2, 23) @ [right/ci(0)]
| chan @ [left/ci(0), right/co(0)]
| unit @ [left/co(0), right/ci(1)]
| chan @ [left/ci(1), right/co(1)]
| unit @ [left/co(1), right/ci(2)]
| chan @ [left/ci(2), right/co(2)]
| unit @ [left/co(2), right/ci(3)]
| chan @ [left/ci(3), right/co(3)]
| unit @ [left/co(3), right/ci(4)]
| chan @ [left/ci(4), right/co(4)]
| unit @ [left/co(4), right/ci(5)]
| chan @ [left/ci(5), right/co(5)]
| consumer(4, 23) @ [left/co(5)]
) \ { ci(_), co(_) }.

sieve6 ::=
( generator(2, 29) @ [right/ci(0)]
| chan @ [left/ci(0), right/co(0)]
| unit @ [left/co(0), right/ci(1)]
| chan @ [left/ci(1), right/co(1)]
| unit @ [left/co(1), right/ci(2)]
| chan @ [left/ci(2), right/co(2)]
| unit @ [left/co(2), right/ci(3)]
| chan @ [left/ci(3), right/co(3)]
| unit @ [left/co(3), right/ci(4)]
| chan @ [left/ci(4), right/co(4)]
| unit @ [left/co(4), right/ci(5)]
| chan @ [left/ci(5), right/co(5)]
| unit @ [left/co(5), right/ci(6)]
| chan @ [left/ci(6), right/co(6)]
| consumer(4, 29) @ [left/co(6)]
) \ { ci(_), co(_) }.

sieve7 ::=
( generator(2, 31) @ [right/ci(0)]
| chan @ [left/ci(0), right/co(0)]
| unit @ [left/co(0), right/ci(1)]
| chan @ [left/ci(1), right/co(1)]
| unit @ [left/co(1), right/ci(2)]
| chan @ [left/ci(2), right/co(2)]
| unit @ [left/co(2), right/ci(3)]
| chan @ [left/ci(3), right/co(3)]
| unit @ [left/co(3), right/ci(4)]
| chan @ [left/ci(4), right/co(4)]
| unit @ [left/co(4), right/ci(5)]
| chan @ [left/ci(5), right/co(5)]
| unit @ [left/co(5), right/ci(6)]
| chan @ [left/ci(6), right/co(6)]
| unit @ [left/co(6), right/ci(7)]
| chan @ [left/ci(7), right/co(7)]
| consumer(4, 31) @ [left/co(7)]
) \ { ci(_), co(_) }.

%%=============================================================================
%%	Properties

% should be Yes
ae_finish += diam(-nil, tt) /\ box(-finish, ae_finish).

% should be No
ee_fail += diam(fail, tt) \/ diam(-nil, ee_fail).
```