Idempotent Operations Pattern

 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

# Example 0067: Idempotent Operations Pattern
# Operations that can be safely retried
# Demonstrates: idempotency, deduplication, request IDs

action Init:
    processed_ids = set()
    counter = 0
    requests = 0

atomic action SendRequest:
    require requests < 3

    request_id = requests
    requests = requests + 1

    # Process if not already processed (idempotent)
    if request_id not in processed_ids:
        processed_ids.add(request_id)
        counter = counter + 1

atomic action RetryRequest:
    require requests > 0

    # Retry with existing request ID
    request_id = oneof range(requests)

    # Idempotent: no effect if already processed
    if request_id not in processed_ids:
        processed_ids.add(request_id)
        counter = counter + 1

# Safety: counter never exceeds unique requests
always assertion IdempotencyInvariant:
    return counter <= requests

# Safety: processed IDs match counter
always assertion ProcessedCorrectly:
    return counter == len(processed_ids)

atomic action NoOp:
    if requests >= 3:
        pass

StateSpaceOptions: options:{max_actions:100 max_concurrent_actions:2}
Nodes: 7, queued: 0
Valid Nodes: 4 Unique states: 4
IsLive: true
PASSED: Model checker completed successfully

gdoc_arrow_left_alt Eventual Consistency Pattern Circuit Breaker Pattern gdoc_arrow_right_alt