Rate Limiting Pattern

Token bucket rate limiter

Demonstrates: rate limiting, token bucket, capacity management

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44


# Example 0070: Rate Limiting Pattern
# Token bucket rate limiter
# Demonstrates: rate limiting, token bucket, capacity management

BUCKET_CAPACITY = 3
REFILL_AMOUNT = 1

action Init:
    tokens = BUCKET_CAPACITY
    requests_processed = 0
    requests_rejected = 0
    refills = 0

atomic action ProcessRequest:
    if tokens > 0:
        # Consume token and process
        tokens = tokens - 1
        requests_processed = requests_processed + 1
    else:
        # Reject when no tokens
        requests_rejected = requests_rejected + 1

atomic action RefillTokens:
    require refills < 2

    # Add tokens up to capacity
    if tokens < BUCKET_CAPACITY:
        tokens = tokens + REFILL_AMOUNT
        if tokens > BUCKET_CAPACITY:
            tokens = BUCKET_CAPACITY
        refills = refills + 1

# Safety: tokens never exceed capacity
always assertion TokensInBounds:
    return tokens >= 0 and tokens <= BUCKET_CAPACITY

# Safety: processed requests consumed tokens
always assertion ValidProcessing:
    consumed = BUCKET_CAPACITY - tokens + (refills * REFILL_AMOUNT)
    return requests_processed <= consumed

atomic action NoOp:
    if refills >= 2 and requests_processed >= 3:
        pass

Expected result (from fizz):

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 582, queued: 0
Skipping dotfile generation. Too many Nodes: 582
Valid Nodes: 582 Unique states: 582
IsLive: true
PASSED: Model checker completed successfully

Source on GitHub

Language features used

Assertions, Flow Modifiers