/*
 * Copyright (c) 1996 by Satish Chandra, Brad Richards, Mark D. Hill, 
 * James R. Larus, and David A. Wood.
 *
 * Teapot is distributed under the following conditions:
 * 
 *     You may make copies of Teapot for your own use and modify those copies.
 * 
 *     All copies of Teapot must retain our names and copyright notice.
 * 
 *     You may not sell Teapot or distributed Teapot in conjunction with a
 *     commercial product or service without the expressed written consent of
 *     the copyright holders.
 * 
 * THIS SOFTWARE IS PROVIDED ``AS IS'' AND WITHOUT ANY EXPRESS OR IMPLIED
 * WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.
 * 
 */
--      tab: 4
----------------------------------------------------------------------------
--                    Read a message from the network
--                    and do appropriate stuff
----------------------------------------------------------------------------

Ruleset Src : NODE Do
Ruleset Dst : NODE Do
Alias Net : Network[Src][Dst] Do
Alias Me : Nodes[Dst] Do
Alias Self_Id : Dst Do


	Rule "PP picks old msg from network"
		Msg_Too_Old(Src, Dst) &
		(!Me.PPBlocked) &
		Space_in_Network(Dst) 
	==>
	Var
		Msg : Message;
		b1 : boolean;
		b2 : boolean;
		b3 : boolean;
		-- idx : 0..ChanMax-1;
	Begin
		old_idx := Find_Old_Msg(Src, Dst);
		cur_node := Self_Id;
		Msg := Net.Messages[old_idx];
		cur_msg := Msg;
		NW_ConsumeMsg(Net, old_idx);
		Me.PPBlocked := true;

		cur_id := Msg.Addr;
		-- If (IsRequest(Msg.MType)) Then
			--PredictRace(Src, Msg);
		-- Endif;

		DispatchState(Me.Dram[Msg.Addr].State, Msg.MType, Msg.Addr, Me.Dram[Msg.Addr], Src);
		b1 := IsTransient(Me.Dram[Msg.Addr].State);
		b2 := Q_Empty(Me.Dram[Msg.Addr]);
		b3 := !b1 & !b2;
		While (b3) Do
			Q_ProcessHead(Msg.Addr, Me.Dram[Msg.Addr]);
			b1 := IsTransient(Me.Dram[Msg.Addr].State);
			b2 := Q_Empty(Me.Dram[Msg.Addr]);
			b3 := !b1 & !b2;
		End;
		Me.PPBlocked := false;
	End;


Ruleset M_Index : 0..ChanMax-1 Do	-- nondeterministically choose a msg

	Rule "PP picks a msg from the network"
		(M_Index < Net.Count) &	
		(!Me.PPBlocked) &
		Space_in_Network(Dst) &
		(!Msg_Too_Old(Src, Dst))
	==>
	Var
		Msg : Message;
		b1 : boolean;
		b2 : boolean;
		b3 : boolean;
	Begin
		Age_Messages(Src, Dst);
		cur_node := Self_Id;
		Msg := Net.Messages[M_Index];
		cur_msg := Msg;
		NW_ConsumeMsg(Net, M_Index);
		Me.PPBlocked := true;

		cur_id := Msg.Addr;
		-- If (IsRequest(Msg.MType)) Then
			-- PredictRace(Src, Msg);
		-- Endif;

		DispatchState(Me.Dram[Msg.Addr].State, Msg.MType, Msg.Addr, Me.Dram[Msg.Addr], Src);

		b1 := IsTransient(Me.Dram[Msg.Addr].State);
		b2 := Q_Empty(Me.Dram[Msg.Addr]);
		b3 := !b1 & !b2;
		While (b3) Do
			Q_ProcessHead(Msg.Addr, Me.Dram[Msg.Addr]);
			b1 := IsTransient(Me.Dram[Msg.Addr].State);
			b2 := Q_Empty(Me.Dram[Msg.Addr]);
			b3 := !b1 & !b2;
		End;
		Me.PPBlocked := false;
	End;

End; -- ruleset M_Index
End; -- alias Self_Id
End; -- alias Me
End; -- alias Net
End; -- ruleset Dst
End; -- ruleset Src

