Saga 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
52
53
54
55
56
57

# Example 0073: Saga Pattern
# Long-running transaction with compensation
# Demonstrates: saga pattern, compensating transactions, rollback

State = enum('INIT', 'STEP1_DONE', 'STEP2_DONE', 'COMPLETED', 'COMPENSATING', 'ROLLED_BACK')

action Init:
    saga_state = State.INIT
    step1_committed = False
    step2_committed = False

atomic action ExecuteStep1:
    require saga_state == State.INIT

    step1_committed = True
    saga_state = State.STEP1_DONE

atomic action ExecuteStep2:
    require saga_state == State.STEP1_DONE

    # Step 2 can fail
    oneof:
        # Success path (atomic together)
        atomic:
            step2_committed = True
            saga_state = State.STEP2_DONE

        # Failure path - trigger compensation
        saga_state = State.COMPENSATING

atomic action Complete:
    require saga_state == State.STEP2_DONE

    saga_state = State.COMPLETED

atomic action CompensateStep1:
    require saga_state == State.COMPENSATING

    # Rollback step 1
    step1_committed = False
    saga_state = State.ROLLED_BACK

# Safety: if completed, both steps committed
always assertion CompletionInvariant:
    if saga_state == State.COMPLETED:
        return step1_committed and step2_committed
    return True

# Safety: if rolled back, step1 compensated
always assertion CompensationInvariant:
    if saga_state == State.ROLLED_BACK:
        return not step1_committed
    return True

atomic action NoOp:
    if saga_state == State.COMPLETED or saga_state == State.ROLLED_BACK:
        pass

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

gdoc_arrow_left_alt Optimistic Locking Pattern Snapshot Isolation Pattern gdoc_arrow_right_alt