/*
 * 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
ClearDebugCheckpoints();
		old_idx := Find_Old_Msg(Src, Dst);
		cur_node := Self_Id;
		Assert(!Isundefined(Net.Messages[old_idx].orig_client)) 
			"XXX orig_client undefined in old message";
		Assert(!Isundefined(Net.Messages[old_idx].am_reply_done)) 
			"XXX am_reply_done undefined in old message";
		Msg := Net.Messages[old_idx];
		cur_msg := Msg;
		Assert(!Isundefined(Net.Messages[old_idx].am_reply_done)) 
			"XXX 2 am_reply_done undefined in old message";
		Assert(!Isundefined(cur_msg.am_reply_done)) 
			"XXX 2 am_reply_done undefined in old message";
		cur_msg.am_reply_done := false;
		Assert (!Isundefined(cur_msg.orig_client)) 
			"all old messages must have orig_client defined";
		NW_ConsumeMsg(Net, old_idx);
		Me.PPBlocked := true;
		Assert(!Isundefined(cur_msg.am_reply_done)) 
			"XXX 3 am_reply_done undefined in old message";

		cur_id := Msg.Addr;

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

		/*
		 * MDD: Old version did not process queue while in transient state.	
                 * New version does.
	         */
#if 0
		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 := false; /* IsTransient(Me.Dram[Msg.Addr].State);*/
			b2 := Q_Empty(Me.Dram[Msg.Addr]);
			b3 := !b1 & !b2;
		End;
#else
		If (!Q_Empty(Me.Dram[Msg.Addr]))
		Then
			Q_ProcessQEvents(Msg.Addr, Me.Dram[Msg.Addr]);
		Endif;
#endif

		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;
		cur_msg.am_reply_done := false;
		Assert (!Isundefined(cur_msg.orig_client)) "all messages must have orig_client defined";
		NW_ConsumeMsg(Net, M_Index);
		Me.PPBlocked := true;

		cur_id := Msg.Addr;

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


		/*
		 * MDD: Old version did not process queue while in transient state.	
                 * New version does.
	         */
#if 0
		b1 := false; /* 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 := false; /* IsTransient(Me.Dram[Msg.Addr].State); */
			b2 := Q_Empty(Me.Dram[Msg.Addr]);
			b3 := !b1 & !b2;
		End;
#else
		If (!Q_Empty(Me.Dram[Msg.Addr]))
		Then
			Q_ProcessQEvents(Msg.Addr, Me.Dram[Msg.Addr]);
		Endif;
#endif
		Me.PPBlocked := false;
	End;

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

