-------------------------------------------------------------------------------
--	leader.m
--	leader selection protocol
-------------------------------------------------------------------------------
--	To verify ae_leader:
--		use LIVENESS "ae_leader"
--	To verify one_leader
--		use ASSERT(!leader) before setting leader
-------------------------------------------------------------------------------

CONST
	NumNodes	: 7;
	BufferSize	: 2 * NumNodes;

TYPE
	NodeID		: 0..NumNodes-1;
	BufferLength	: 0..BufferSize;
	BufferIndex	: 0..BufferSize-1;
	MsgStage	: ENUM { first, second };
	Message		: RECORD
				stage	: MsgStage;
				ID	: NodeID;
			  END;
	Channel		: RECORD
				length	: BufferLength;
				buffer  : ARRAY [BufferIndex] OF Message;
			  END;
	NodeState	: ENUM {
				start,
				active,
				inactive,
				inactiveget,
				getfirst,
				getsecond
			  };
	Node		: RECORD
				state	: NodeState;
				maxID	: NodeID;
				nbrID	: NodeID;
				NID	: NodeID;
				msgstage : MsgStage;
			  END;

VAR
	channels	: ARRAY [NodeID] OF Channel;
	nodes		: ARRAY [NodeID] OF Node;
	leader		: 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 stage: MsgStage; VAR ID: NodeID);
VAR
    i : BufferLength;
BEGIN
    assert(!isempty(Chan));
    stage := Chan.buffer[0].stage;
    ID    := Chan.buffer[0].ID;
    Chan.length := Chan.length-1;
    -- shift buffer 
    FOR i:= 0 TO Chan.length DO
	Chan.buffer[i] := Chan.buffer[i+1]
    END;
    CLEAR Chan.buffer[Chan.length];
END;

PROCEDURE output(VAR Chan: Channel; stage: MsgStage; ID: NodeID);
BEGIN
    assert(!isfull(Chan));
    Chan.buffer[Chan.length].stage := stage;
    Chan.buffer[Chan.length].ID    := ID;
    Chan.length := Chan.length+1;
END;

-------------------------------------------------------------------------------
--	node
-------------------------------------------------------------------------------

RULESET n: NodeID DO
ALIAS
	node: nodes[n];
	left: channels[n];
	right: channels[(n+1)%NumNodes]
DO

RULE "send first"
	node.state = start & !isfull(right)
==>
BEGIN
	output(right, first, node.maxID);
	node.state := active;
END;

RULE "active"
	node.state = active & !isempty(left)
==>
VAR
	stage	: MsgStage;
BEGIN
	input(left, stage, node.NID);
	IF stage = first THEN
		node.state := getfirst;
		node.nbrID := node.NID
	ELSIF stage = second THEN
		node.state := getsecond;
	ELSE
		ERROR "wrong message type";
	END;
END;

RULE "getfirst"
	node.state = getfirst & !isfull(right)
==>
BEGIN
	IF node.nbrID != node.maxID THEN
		output(right, second, node.nbrID);
		node.state := active;
	ELSIF node.maxID = NumNodes-1 THEN
		ASSERT(!leader);
		leader := true;
		node.state := active;
	ELSE
		ERROR "protocol fails"
	END
END;

RULE "getsecond"
	node.state = getsecond & !isfull(right)
==>
BEGIN
	IF node.nbrID > node.NID & node.nbrID > node.maxID THEN
		output(right, first, node.nbrID);
		node.state := active;
		node.maxID := node.nbrID;
	ELSE
		CLEAR node;
		node.state := inactive;
	END;
END;

RULE "inactive"
	node.state = inactive & !isempty(left)
==>
BEGIN
	input(left, node.msgstage, node.NID);
	node.state := inactiveget;
END;

RULE "inactive get"
	node.state = inactiveget & !isfull(right)
==>
BEGIN
	output(right, node.msgstage, node.NID);
	CLEAR node;
	node.state := inactive;
END;
	
ENDALIAS;
ENDRULESET;

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

LIVENESS "ae_leader"
	ALWAYS EVENTUALLY leader;

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

STARTSTATE
	CLEAR channels;
	CLEAR nodes;
	FOR i: NodeID DO
		nodes[i].maxID := NumNodes-1 - i;
	END;
	leader := false;
END;