Struct AllocationSnapshot 

pub struct AllocationSnapshot {
    pub num_nodes: u64,
    pub registry: ResourceRegistry<u64, u64>,
    pub budget: Budget,
}

An allocation snapshot: the accepted node set plus the running cost / budget figures, over a node universe 0..num_nodes bounded by capacity.

Fields

num_nodes: u64

|Nodes|: the node universe is the index range 0..num_nodes.

registry: ResourceRegistry<u64, u64>

ResourceRegistry component mapping accepted nodes to their costs.

budget: Budget

Budget component charged by the registered costs.

Implementations

impl AllocationSnapshot

pub fn new(capacity: u64, num_nodes: u64) -> AllocationSnapshot

Construct the empty snapshot: nothing accepted, full budget remaining. Realises the TLA+ Init predicate and establishes both invariants.

pub fn contains_exec(&self, n: u64) -> bool

Executable membership test; links to the contains spec so callers can discharge the n ∉ accepted precondition of accept_node.

pub fn accept_node(&mut self, n: u64, node_cost: u64)

Accept node n at cost node_cost. Realises the TLA+ AcceptNode action: its three guards are requires, and both invariants are re-established as ensures (the inductive preservation step).