Enum Label 

pub enum Label {
    Send {
        model: Model,
        dst: Tid,
        val: Val,
    },
    Recv {
        pred: Arc<Pred>,
        blocking: bool,
    },
    Nondet {
        set: Arc<[Val]>,
    },
    Error {
        msg: Arc<str>,
    },
}

Event label. Blocking is scheduler state, not a graph event, so it has no label here. Nondet carries only the option set; the value it resolved to is a separate graph annotation, just as a receive’s read value is its rf edge rather than part of its label.

The heap-carrying variants hold their payload behind an Arc, so cloning a Label shares it; labels are immutable, so the sharing is sound.

Variants

Send

Fields

model: Model

dst: Tid

val: Val

Recv

Fields

pred: Arc<Pred>

blocking: bool

Nondet

Data non-determinism: set is the finite option set, kept sorted and deduplicated so the minimum is set[0] and enumeration is deterministic.

Fields

set: Arc<[Val]>

Error

Fields

msg: Arc<str>

Implementations

impl Label

pub fn send(model: Model, dst: Tid, val: impl Into<Val>) -> Self

pub fn recv(pred: Pred) -> Self

Blocking receive: waits for a matching message.

pub fn recv_nb(pred: Pred) -> Self

Non-blocking receive: may read nothing (a timeout).

pub fn nondet(set: impl IntoIterator<Item = impl Into<Val>>) -> Self

Non-deterministic choice over the finite option set set (sorted and deduplicated).

pub fn error(msg: impl Into<String>) -> Self

pub fn is_send(&self) -> bool

pub fn is_recv(&self) -> bool

pub fn is_nondet(&self) -> bool

pub fn is_error(&self) -> bool

pub fn model(&self) -> Option<Model>

pub fn dst(&self) -> Option<Tid>

pub fn val(&self) -> Option<&'static str>

A send’s payload resolved to its bytes. None for non-sends. Prefer payload when the interned handle suffices (no resolve).

pub fn payload(&self) -> Option<Val>

A send’s payload as the stored (interned, Copy) Val. None for non-sends. Use val when the bytes are needed.

pub fn pred(&self) -> Option<&Pred>

pub fn blocking(&self) -> Option<bool>

pub fn nd_set(&self) -> Option<&[Val]>

The option set of a nondet label (None for any other label). The value it resolved to is not here; that is the graph’s nd annotation.

Trait Implementations

impl Clone for Label

fn clone(&self) -> Label

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Label

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

Formats the value using the given formatter.

impl Eq for Label

impl PartialEq for Label

fn eq(&self, other: &Label) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for Label