/*
 * 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.
 * 
 */


Function Q_Empty(Var info: INFO):boolean;
Begin
	Alias Queue : info.Queue Do
		If (Queue.Count = 0) Then
			return true;
		Else
			return false;
		End;
	End; -- alias Queue
End;


/*
 *------------------------------------------------------------------
 *
 * Q_ProcessQEvents --
 *
 *          XXX The original version (Q_ProcessHead)
 *          of this was too weak.
 *          it just dispatched the first item from the
 *          queue. It got called after every time we
 *          handled an external event, but it didn't 
 *          get called if we were in a transient state.
 * 
 *          This was too weak because we could think
 *          we were deadlocked even if there was
 *          an event sitting in the queue that would
 *          make progress.
 * 
 *          New version will make at least one pass
 *          through the entire queue and attempt to process all
 *          items that are in the queue when the routine
 *          is first called at least once. 
 * 
 *          If the queue's length changes during a pass
 *          we made progress, so we'll make another pass.
 * 
 *          XXX This still doesn't guarantee progress
 *          if there is no deadlock. What we should
 *          really do is keep chewing on the queue
 *          until nothing changes, but that seems
 *          hard. The current version is more conservative
 *          so it is OK.
 *
 * Results:
 *      None.
 *
 * Side effects:
 *      None.
 *
 *------------------------------------------------------------------
 */
#if 0 /* orig version */
Procedure Q_ProcessHead(id:ID; Var info: INFO);
Var
	Msg : Message;
	Src : NODE;
	i: 0..QueueMax;
Begin
	Alias Queue : info.Queue Do
		If (Queue.Count > 0) Then
			Msg := Queue.Elems[0].Msg;
			Src := Queue.Elems[0].Src;
			For i:= 0 to Queue.Count - 2 Do
				Queue.Elems[i] := Queue.Elems[i+1];
			End;
			Undefine Queue.Elems[Queue.Count - 1];
			Queue.Count := Queue.Count - 1;
			cur_node := cur_node; /* ugly, but this is the way it works */
			cur_msg := Msg;
			cur_id := Msg.Addr;
			Assert(Src != cur_node) "Dequeuing message from self";
			DispatchState(info.State, Msg.MType, Msg.Addr, info, 
					Src);
		End;
	End;
End;
#endif 

Procedure Q_ProcessQEvents(id:ID; Var info: INFO);
Var
	Msg : Message;
	Src : NODE;
	i: 0..QueueMax;
	remainingToTry: 0..QueueMax;
	countLastPass: 0..QueueMax;
	makeAnotherPass : BOOLEAN;
Begin
  Alias Queue : info.Queue Do
    countLastPass := 0;
    makeAnotherPass := true;
    --
    -- XXX Weaker than necessary ending condition. See comment above.
    --
    -- XXX DANGER DANGER DANGER XXX
    -- Apparant bug in Murphi; complex statements in while loop seem
    -- to break (so do not do "While (foo | (bar != baz)) Do".
    -- Instead do doit := foo | (bar != baz); while ( doit ) or whatever.
    -- XXX DANGER DANGER DANGER XXX     
    While (makeAnotherPass) Do
      countLastPass := Queue.Count;
      remainingToTry := Queue.Count;
      While (remainingToTry > 0) Do
	Msg := Queue.Elems[0].Msg;
	Src := Queue.Elems[0].Src;
	For i:= 0 to Queue.Count - 2 Do
	  Queue.Elems[i] := Queue.Elems[i+1];
	End;
	Undefine Queue.Elems[Queue.Count - 1];
	Queue.Count := Queue.Count - 1;
	cur_node := cur_node; /* ugly, but this is the way it works */
	cur_msg := Msg;
	cur_id := Msg.Addr;
	Assert(Src != cur_node) "Dequeuing message from self";
	DispatchState(info.State, Msg.MType, Msg.Addr, info, Src);
	remainingToTry := remainingToTry - 1;
      End;
      makeAnotherPass := countLastPass != Queue.Count;
    End;
  End;
End;
