%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%	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).