1.8. Engine🔗

An MailboxActors.Engine of type i is a 4-tuple ⟨behaviour, status, config, env⟩. The behaviour field carries a WellFormedBehaviour, embedding the non-overlapping guard proof.

Two predicates classify engines by mode:

• MailboxActors.Engine.isMailbox — the engine's mode is mail,

• MailboxActors.Engine.isProcessing — the engine's mode is process.

Every processing engine is automatically paired with a dedicated mailbox engine. The mailbox engine's behaviour governs delivery, filtering, and scheduling for its partner.