Should CurrentMessage return empty set?

[lukecheeseman]

I am wondering about the CurrentMessage macro, given it's definition

CurrentMessage(c) == IF Len(queue[c]) > 0 THEN Head(queue[c]) ELSE {}

Are we expecting and intentionally permitting the cases where an empty queue gets interpreted as an empty message (and on a further point whether empty messages are expected). I do not think/or know of a place where this happens. I am finding it a bit difficult to decide whether an empty message is a possible case/permitted case. For example in Send the body of the message is not required to contain anything, however running(c) is required which entails that c's message queue is non empty by the invariant:

RunningIsScheduled ==
  \A c \in Cowns: running[c] => scheduled[c] /\ (c = Max(CurrentMessage(c)))

I am wondering if this is the intended outcome and whether it would be clearer to replace CurrentMessage(c) with Len(queue(c)) > 0 /\ LET msg=Head(queue(c)) IN... if this is always desired.