-------------------------------------------------------------------------------
--	sieve.m
-------------------------------------------------------------------------------
--	To verify ae_finish
--		use LIVENESS "ae_finish"
--	To verify ee_fail
--		use its negative INVARIANT "not ee_fail"
-------------------------------------------------------------------------------

CONST

	--------------------------------------------------------
	-- Combinations of NumFilter and NextPrime:
	--    NUM :  1   2   3    4   5   6   7   8   9  10
	--  PRIME :  2   3   5    7  11  13  17  19  23  29  31
	--  for consumer.N = 4
	--    MAX :  11  13  17  19  23  29  31
	--------------------------------------------------------

	NumFilters	: 7;
	MaxNumber	: 31;
	BufferSize	: 1;

TYPE

	FilterID	: 0..NumFilters-1;
	Number		: 1..MaxNumber;
	BufferLength	: 0..BufferSize;
	BufferIndex	: 0..BufferSize-1;
	Generator	: RECORD
				state	: ENUM { sending, sentall, genend };
				next	: Number;
			  END;
	Channel		: RECORD
				length	: BufferLength;
				buffer  : ARRAY [BufferIndex] OF Number;
			  END;
	FilterState	: ENUM { notset, nodata, holddata };
	Filter		: RECORD
				state	: FilterState;
				prime	: Number;
				number	: Number;
			  END;
	Consumer	: RECORD
				N	: 0..4;
				MAX	: Number;
			  END;			
VAR
	gen		: Generator;
	channels	: ARRAY [0..NumFilters] OF Channel;
	filters		: ARRAY [FilterID] OF Filter;
	consumer	: Consumer;
	finish		: boolean;
	fail		: boolean;

-------------------------------------------------------------------------------
--	buffered channel
-------------------------------------------------------------------------------

FUNCTION isfull(Chan: Channel) : boolean;
BEGIN
    RETURN Chan.length = BufferSize;
END;

FUNCTION isempty(Chan: Channel) : boolean;
BEGIN
    RETURN Chan.length = 0;
END;

PROCEDURE input(VAR Chan: Channel; VAR v: Number);
VAR
    i : BufferLength;
BEGIN
    assert(!isempty(Chan));
    v    := Chan.buffer[0];
    Chan.length := Chan.length-1;
    -- shift buffer 
    IF Chan.length > 0 THEN
    	FOR i:= 0 TO Chan.length-1 DO
	    Chan.buffer[i] := Chan.buffer[i+1]
    	END;
    END;
    CLEAR Chan.buffer[Chan.length];
END;

PROCEDURE output(VAR Chan: Channel; v: Number);
BEGIN
    assert(!isfull(Chan));
    Chan.buffer[Chan.length] := v;
    Chan.length := Chan.length+1;
END;

-------------------------------------------------------------------------------
--	The number generator
-------------------------------------------------------------------------------

ALIAS right: channels[0] DO

RULE "generator sending"
	gen.state = sending & !isfull(right)
==>
BEGIN
	output(right, gen.next);
	IF gen.next < MaxNumber THEN
		gen.next := gen.next+1;
	ELSE
		gen.state := sentall;
	END;
END;

ENDALIAS;

-------------------------------------------------------------------------------
--	Filters
-------------------------------------------------------------------------------

RULESET n: FilterID DO
ALIAS
	filter: filters[n];
	left: channels[n];
	right: channels[n+1]
DO

RULE "set prime"
	filter.state = notset & !isempty(left)
==>
BEGIN
	input(left, filter.prime);
	filter.state := nodata
END;

RULE "get number"
	filter.state = nodata & !isempty(left)
==>
VAR
	N : Number;
BEGIN
	input(left, N);
	IF N % filter.prime != 0 THEN
		filter.number := N;
		filter.state := holddata;
	END;
END;

RULE "send number"
	filter.state = holddata & !isfull(right)
==>
BEGIN
	output(right, filter.number);
	CLEAR filter.number;
	filter.state := nodata;
END;
	
ENDALIAS;
ENDRULESET;

-------------------------------------------------------------------------------
--	The consumer
-------------------------------------------------------------------------------

ALIAS left: channels[NumFilters] DO

RULE "consumer get"
	consumer.N > 0 & !isempty(left)
==>
VAR
	X: Number;
BEGIN
	input(left, X);
	consumer.N := consumer.N-1;
	IF consumer.N = 0 THEN
		IF X = consumer.MAX THEN
			finish := true;
		ELSE
			fail := true;
		END;
	END;
END;

ENDALIAS;

-------------------------------------------------------------------------------

LIVENESS "ae_finish"
	ALWAYS EVENTUALLY finish;

INVARIANT "not ee_fail"
	!fail;

-------------------------------------------------------------------------------

STARTSTATE
	CLEAR channels;
	CLEAR filters;
	gen.state := sending;
	gen.next := 2;
	consumer.N := 4;
	consumer.MAX := MaxNumber;
	finish := false;
	fail := false;
END;