Rules

Rule 1: getting hungry
s = thinking	$\rightarrow$	s := hungry
Rule 2: starting to eat
s = hungry, Hastoken	$\rightarrow$	s := eating
Rule 3: stoping to eat, keeping the token
s = eating, ReqList = $\emptyset$	$\rightarrow$	s := thinking
Rule 4: stoping to eat, sending the token
s = eating, ReqList $\neq$ EMPTY	$\rightarrow$	s:= thinking ;
		Next := last(ReqList);
		T.ReqList := tail(ReqList);
		send(head(ReqList), T); HasToken := FALSE;
		ReqList := EMPTY;
		for all k $\in$ T.ReqList do
		$\ensuremath{ {\mathbf V} }$ [k]:= $\ensuremath{ {\mathbf V} }$ [k] cat Myself;
Rule 5: requesting the token
s = hungry, Next $\neq$ nil	$\rightarrow$	send(Next, Request(Myself));
		Next := nil;
		$\ensuremath{ {\mathbf V} }$ [Myself] := EMPTY;
Rule 6: storing a request
Receive(R), s $\neq$ thinking	$\rightarrow$	put(ReqList, R.origin)
Rule 7: releasing the token
Receive(R), s = thinking, Next = nil	$\rightarrow$	T.ReqList := EMPTY;
		send(R.origin, T);
		HasToken := FALSE;
		Next := R.origin
Rule 8: forwarding a request
Receive(R), s = thinking, Next $\neq$ nil	$\rightarrow$	send(Next, R);
		Next := R.origin;
		$\ensuremath{ {\mathbf V} }$ [R.origin] := $\ensuremath{ {\mathbf V} }$ [R.origin] cat Myself;
Rule 9: receiving the token
Receive(T)	$\rightarrow$	Hastoken := TRUE;
		ReqList := T.ReqList cat ReqList
		$\ensuremath{ {\mathbf V} }$ [Myself] := EMPTY;