Mailbox Actors

3.3. Effect Execution🔗

MailboxActors.EffectEvalStep interprets effects against the current system state, producing a successor state. One constructor per effect kind:

  • E-Noop — no state change.

  • E-Send — appends a message to the transit pool if the target exists, is a processing engine, and the type index matches; otherwise a silent no-op.

  • E-Terminate — sets the engine's status to terminated.

  • E-Update — replaces the engine's execution environment.

  • E-MFilter — transitions the engine to ready f, installing a new message acceptance filter.

  • E-Spawn — creates a child processing engine and its paired mailbox atomically, if the allocated addresses are fresh; otherwise just advances nextId.

  • E-Chain — sequences two effects: evaluates e₁, then e₂ on the resulting state.

After effect execution, MailboxActors.resolvePostStatus determines the final status: if the engine is still busy it resets to ready (fun _ => true) (accept all); otherwise the current status (terminated or ready f) is preserved.