Circuit Breaker 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
43
44
45
46
47
48
49
50
51

# Example 0074: Circuit Breaker Pattern
# Prevents cascading failures with circuit states
# Demonstrates: circuit breaker, failure threshold, state transitions

State = enum('CLOSED', 'OPEN', 'HALF_OPEN')
FAILURE_THRESHOLD = 2

action Init:
    circuit_state = State.CLOSED
    failure_count = 0
    success_count = 0
    requests = 0

atomic action RequestSuccess:
    require requests < 5
    require circuit_state != State.OPEN  # Reject when open

    requests = requests + 1
    success_count = success_count + 1

    # Reset failures on success in half-open
    if circuit_state == State.HALF_OPEN:
        failure_count = 0
        circuit_state = State.CLOSED

atomic action RequestFailure:
    require requests < 5
    require circuit_state != State.OPEN  # Reject when open

    requests = requests + 1
    failure_count = failure_count + 1

    # Open circuit on threshold
    if failure_count >= FAILURE_THRESHOLD:
        circuit_state = State.OPEN

atomic action TryReset:
    require circuit_state == State.OPEN

    # Try half-open after timeout
    circuit_state = State.HALF_OPEN

# Safety: circuit opens after threshold
always assertion CircuitOpensOnFailures:
    if failure_count >= FAILURE_THRESHOLD:
        return circuit_state == State.OPEN or circuit_state == State.HALF_OPEN
    return True

atomic action NoOp:
    if requests >= 5:
        pass

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

gdoc_arrow_left_alt Idempotent Operations Pattern Rate Limiting Pattern gdoc_arrow_right_alt