Default event handler

[paulthomson]

@pdeligia and I have been discussing the default event handler. Is it an essential feature?

I am not sure how to soundly reason about this as a visible operation. If it is essential, I think it requires having a visible operation every time the Inbox is checked (to see if it is empty), even if the default event handler does not fire, although this would only occur if the current state has a default event handler. Actually, I think it could be modelled as follows: every time the Inbox is checked (to see if it is empty), make this a visible operation of sending an event to yourself. Then, if the default event handler fires, make the processing of the event a receive operation that receives the event from the previous "fake send". If the default event handler does not fire, the sent event is never received (just like an ignored event). This ensures that, after receiving some event, the Inbox check will have a scheduling point before it (so we can explore the possibility of another event being sent to us before this check, or not) and then the following receive will typically be reduced (i.e. ignored) by all scheduling strategies anyway.