Struct RateLimit 

pub struct RateLimit {
    pub budget: Budget,
    pub window_duration: u64,
    pub max_clock: u64,
    pub window_start: u64,
    pub clock: u64,
}

A per-window operation bound: at most max_per_window acquires per window_duration clock units, the window re-anchored at window_start.

Fields

budget: Budget

Budget component for operations admitted in the current window.

window_duration: u64

WindowDuration (constant): the window length in clock units.

max_clock: u64

MaxClock (constant): the model’s clock bound (Tick’s guard).

window_start: u64

window_start ∈ Nat: when the current window was anchored.

clock: u64

clock ∈ Nat: the runtime-given clock.

Implementations

impl RateLimit

pub fn new( max_per_window: u64, window_duration: u64, max_clock: u64, ) -> RateLimit

Construct the initial state: count = 0, window_start = 0, clock = 0. Realises the TLA+ Init predicate and establishes all three invariants.

pub fn try_acquire(&mut self) -> bool

Try to acquire one operation. The whole three-branch TLA+ IF is this one method: on an expired window, re-anchor AND grant in the same step (window_start’ = clock, count’ = 1); on headroom, grant (count’ + 1); otherwise reject (UNCHANGED). Returns whether the acquire was granted.

pub fn tick(&mut self)

Advance the runtime-given clock by one. Realises the TLA+ Tick action: its guard (clock < MaxClock) is a requires, so the action is callable exactly when the TLA+ action is enabled.