\* Model-checking configuration for RateLimiter.tla
\* Run with: java -cp tla2tools.jar tlc2.TLC MC -config RateLimiter.cfg
\*
\* Uses small constants: 2 senders, 1 channel, MaxTokens=2, WindowLen=3,
\* CooldownLen=2, MaxTime=15.
\*
\* MaxTime must be large enough for all timer expirations. ConsumeToken
\* has a guard (clock + WindowLen + CooldownLen <= MaxTime) to prevent
\* late-window activity that would make liveness vacuously false.
\*
\* Deadlock checking is disabled because the bounded clock creates
\* terminal states (all Idle, clock=MaxTime) that are artifacts of
\* the finite model, not real deadlocks.

CONSTANTS
    Senders <- const_Senders
    Channels <- const_Channels
    MaxTokens <- const_MaxTokens
    WindowLen <- const_WindowLen
    CooldownLen <- const_CooldownLen
    MaxTime <- const_MaxTime

SPECIFICATION Spec

VIEW StateView

CHECK_DEADLOCK FALSE

INVARIANTS
    TypeOK
    BudgetNonNegative
    NoDeliveryAfterExhaustion
    DeliveredBound

PROPERTIES
    EventualRefill
    CooldownResolves
    WindowResets
