Struct ActorRuntime 

pub struct ActorRuntime { /* private fields */ }

Runtime state of an actor

Corresponds to Lean: structure ActorRuntime

Implementations

impl ActorRuntime

pub fn empty(capacity: usize) -> Self

Create empty actor runtime

Corresponds to Lean: def ActorRuntime.empty (capacity : Nat) : ActorRuntime

pub fn can_receive(&self) -> bool

Check if actor can receive (mailbox not empty)

Corresponds to Lean: def ActorRuntime.can_receive (ar : ActorRuntime) : Bool

pub fn can_send(&self, target_capacity: usize) -> bool

Check if actor can send (pending queue not full)

Corresponds to Lean: def ActorRuntime.can_send (ar : ActorRuntime) (targetCapacity : Nat) : Bool

pub fn mailbox_has_space(&self) -> bool

Check if mailbox has space

Corresponds to Lean: def ActorRuntime.mailbox_has_space (ar : ActorRuntime) : Bool

pub fn enqueue_pending(&self, msg: Message) -> Self

Enqueue message to pending

Corresponds to Lean: def ActorRuntime.enqueue_pending

pub fn enqueue_pending_mut(&mut self, msg: Message)

Enqueue message to pending (mutating version)

pub fn deliver(&self) -> Self

Deliver message from pending to mailbox

Corresponds to Lean: def ActorRuntime.deliver

Returns the new state. If pending is empty or mailbox is full, returns unchanged state.

pub fn deliver_mut(&mut self) -> Result<bool, ActorError>

Deliver message from pending to mailbox (mutating version)

Returns Ok(true) if delivered, Ok(false) if mailbox full, Err if no pending.

Errors

Returns ActorError::NoMessage if the pending queue is empty.

pub fn consume(&self) -> (Self, Option<Message>)

Consume message from mailbox

Corresponds to Lean: def ActorRuntime.consume

Returns (new_state, Option<Message>).

pub fn consume_mut(&mut self) -> Option<Message>

Consume message from mailbox (mutating version)

pub fn set_blocked(&self, on: ActorId) -> Self

Set blocked state (for deadlock analysis)

Corresponds to Lean: def ActorRuntime.set_blocked

pub fn set_blocked_mut(&mut self, on: ActorId)

Set blocked state (mutating version)

pub fn unblock(&self) -> Self

Clear blocked state

Corresponds to Lean: def ActorRuntime.unblock

pub fn unblock_mut(&mut self)

Clear blocked state (mutating version)

pub fn blocked_on(&self) -> Option<ActorId>

Get the blocked-on actor (if any)

pub fn is_blocked(&self) -> bool

Check if actor is blocked

pub fn capacity(&self) -> usize

Get the capacity

pub fn pending_len(&self) -> usize

Get the pending queue length

pub fn mailbox_len(&self) -> usize

Get the mailbox length

pub fn pending_send(&self) -> Option<&Message>

Get the pending send message

pub fn set_pending_send(&mut self, msg: Option<Message>)

Set the pending send message

Trait Implementations

impl Clone for ActorRuntime

fn clone(&self) -> ActorRuntime

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ActorRuntime

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for ActorRuntime

fn default() -> Self

Returns the “default value” for a type.