-------------------------------------------------------------------------
-- Rether protocol
-- Realtime First (RTF) version
-- translated to Murphi by Yifei Dong
-- October 1998
-------------------------------------------------------------------------

CONST
    NUM_NODES	: 5;		-- number of nodes in the network
    NUM_SLOTS	: 3;		-- number of RT+NRT time slots per cycle
    NUM_MAXRT	: NUM_SLOTS-1;	-- maximal number of RT time slots
    MAX_NODE_ID	: NUM_NODES-1;

TYPE
    NodeID	: 0..MAX_NODE_ID;
    SlotsNum	: 0..NUM_SLOTS;
    Token	: RECORD
			servingRealtime	: BOOLEAN;
			realtimeMode	: ARRAY [NodeID] OF BOOLEAN;
			rtSlots		: SlotsNum;
			nrtSlotsAvail	: SlotsNum;
			nextNRTNode	: NodeID;
		  END;
    NodeState	: ENUM {
			NODE_START,
			NODE_RT,
			NODE_NRT
		  };
    CycleState	: ENUM {
			CYCLE_START,
			CYCLE_MIDDLE,
			CYCLE_END
		  };
    Action	: ENUM {
			null,
			rt,
			nrt,
			reserve,
			startcycle,
			endcycle
		  };

VAR
    token	: Token;
    gottoken	: ARRAY [NodeID] OF BOOLEAN;
    state	: ARRAY [NodeID] OF NodeState;
    cyclestate	: CycleState;

    -- auxilary monitoring variables
    action	: Action;
    num_starts	: -1..2;
    reservednow	: ARRAY [NodeID] OF BOOLEAN;	-- reserved RT in this cycle
    reservedlast: ARRAY [NodeID] OF BOOLEAN;	-- reserved RT in last cycle
    RTserved	: ARRAY [NodeID] OF BOOLEAN;	-- served RT in this cycle
    NRTserved	: ARRAY [NodeID] OF BOOLEAN;	-- served RT in this cycle

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

PROCEDURE incID(VAR n:NodeID);
BEGIN
    n := (n+1) % NUM_NODES;
END;

PROCEDURE observe(node:NodeID; a:Action);
VAR
    n: NodeID;
BEGIN
    action := a;

    SWITCH a

    CASE reserve:
	reservednow[node] := true;
	RTserved[node] := false;

    CASE rt:
	-- property rt-1
	ASSERT(! reservednow[node]);	-- node is not researved in this cycle
	-- property rtf
	ASSERT(FORALL i:NodeID DO !NRTserved[i] END);
	RTserved[node] := true;

    CASE nrt:
	NRTserved[node] := true;

    CASE startcycle:
	num_starts := num_starts+1;
	ASSERT(num_starts <= 1);	-- property cc-2
	FOR n:=0 TO MAX_NODE_ID DO
	    reservedlast[n] := reservednow[n];
	END;
	CLEAR reservednow;
	CLEAR RTserved;
	CLEAR NRTserved;

    CASE endcycle:
	num_starts := num_starts-1;
	-- property rt-2
	ASSERT(FORALL i:NodeID DO reservedlast[i] -> RTserved[i] END);
	-- property rtt
	ASSERT(EXISTS i:NodeID DO RTserved[i] END);
	-- property nrt
	ASSERT(EXISTS i:NodeID DO NRTserved[i] END);
    END;

END;

PROCEDURE PassTokenTo(node:NodeID);
BEGIN
    ASSERT(! gottoken[node]);
    gottoken[node] := true;
END;

PROCEDURE releaseRT(node:NodeID);
BEGIN
    ASSERT(token.realtimeMode[node]);
    IF token.rtSlots > 1 THEN
	token.rtSlots := token.rtSlots - 1;
	token.realtimeMode[node] := FALSE;
    END;
END;

PROCEDURE reserveRT(node:NodeID);
BEGIN
    ASSERT(! token.realtimeMode[node]);
    IF token.rtSlots < NUM_MAXRT THEN
	observe(node, reserve);
	token.rtSlots := token.rtSlots + 1;
	token.realtimeMode[node] := TRUE;
    END;
END;

PROCEDURE rtPassToken(node:NodeID);
VAR
    n : NodeID;
BEGIN
    state[node] := NODE_START;
    -- If there is the next RT node, pass the token to it
    IF node < MAX_NODE_ID THEN
	FOR n := node+1 TO MAX_NODE_ID DO
	    IF token.realtimeMode[n] THEN
		PassTokenTo(n);
		RETURN;
	    END;
	END;
    END;
    -- else pass the token to the next NRT node
    token.servingRealtime := FALSE;
    PassTokenTo(token.nextNRTNode);
END;

PROCEDURE nrtPassToken(node:NodeID);
BEGIN
    state[node] := NODE_START;
    incID(token.nextNRTNode);
    ASSERT(token.nrtSlotsAvail > 0);
    token.nrtSlotsAvail := token.nrtSlotsAvail - 1;
    IF token.nrtSlotsAvail > 0 THEN
	PassTokenTo(token.nextNRTNode);
    ELSE
	cyclestate := CYCLE_END;
    END;
END;

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

RULESET node:NodeID DO

RULE "get token"
    state[node] = NODE_START &
	gottoken[node]
==>
BEGIN
    gottoken[node] := FALSE;
    IF token.servingRealtime THEN
	ASSERT(token.realtimeMode[node]);
	observe(node, rt);
	state[node] := NODE_RT;
    ELSE
	observe(node, nrt);
	state[node] := NODE_NRT;
    ENDIF;
END;

RULE "realtime mode -- release"
    state[node] = NODE_RT
==>
BEGIN
    releaseRT(node);
    rtPassToken(node);
END;

RULE "realtime mode -- no release"
    state[node] = NODE_RT
==>
BEGIN
    rtPassToken(node);
END;

RULE "non-realtime mode -- reserve"
    state[node] = NODE_NRT
	& ! token.realtimeMode[node]
==>
BEGIN
    reserveRT(node);
    nrtPassToken(node);
END;

RULE "non-realtime mode -- no reserve"
    state[node] = NODE_NRT
==>
BEGIN
    nrtPassToken(node);
END;

ENDRULESET;

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

RULE "start of cycle"
    cyclestate = CYCLE_START
==>
VAR
    n: NodeID;
BEGIN
    observe(0, startcycle);
    token.servingRealtime := TRUE;
    -- pass the token to the first RT node
    FOR n := 0 TO MAX_NODE_ID DO
	IF token.realtimeMode[n] THEN
	    cyclestate := CYCLE_MIDDLE;
	    PassTokenTo(n);
	    RETURN;
	END;
    END;
    ERROR "no realtime node";
END;

RULE "end of cycle"
    cyclestate = CYCLE_END
==>
VAR
    n : NodeID;
BEGIN
    observe(0, endcycle);
    token.nrtSlotsAvail := NUM_SLOTS - token.rtSlots;
    cyclestate := CYCLE_START;
END;

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


LIVENESS "ns"
	ALWAYS EVENTUALLY NRTserved[0];

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

STARTSTATE
    CLEAR token;
    token.realtimeMode[0] := TRUE;
    token.rtSlots := 1;
    token.nextNRTNode := 0;
    token.nrtSlotsAvail := NUM_SLOTS - token.rtSlots;
    CLEAR gottoken;
    CLEAR state;
    cyclestate := CYCLE_START;
    CLEAR action;
    num_starts := 0;
    CLEAR reservednow;
    CLEAR reservedlast;
    CLEAR RTserved;
    CLEAR NRTserved;
END;