# Snapshot Isolation Pattern

> Snapshot isolation as a runnable model: transactions read from a snapshot and commit only if their write sets do not conflict, checked for lost updates.

Canonical: https://fizzbee.io/design/patterns/snapshot-isolation/
Source: https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/13-02-03-snapshot-isolation


Transactions read from snapshot, commit if no conflicts

**Demonstrates:** snapshot isolation, read/write sets, conflict detection

```fizz
# Example 0066: Snapshot Isolation Pattern
# Transactions read from snapshot, commit if no conflicts
# Demonstrates: snapshot isolation, read/write sets, conflict detection

action Init:
    committed_value = 0
    txn1_snapshot = None
    txn1_write = None
    txn1_committed = False
    txn2_snapshot = None
    txn2_write = None
    txn2_committed = False

atomic action Txn1Begin:
    require txn1_snapshot == None

    txn1_snapshot = committed_value

atomic action Txn1Write:
    require txn1_snapshot != None
    require txn1_write == None

    txn1_write = txn1_snapshot + 1

atomic action Txn1Commit:
    require txn1_write != None
    require not txn1_committed

    # Commit if no conflict (value unchanged since snapshot)
    if committed_value == txn1_snapshot:
        committed_value = txn1_write
        txn1_committed = True

atomic action Txn2Begin:
    require txn2_snapshot == None

    txn2_snapshot = committed_value

atomic action Txn2Write:
    require txn2_snapshot != None
    require txn2_write == None

    txn2_write = txn2_snapshot + 10

atomic action Txn2Commit:
    require txn2_write != None
    require not txn2_committed

    # Commit if no conflict
    if committed_value == txn2_snapshot:
        committed_value = txn2_write
        txn2_committed = True

# Safety: if both committed, one saw the other's write
always assertion NoLostUpdates:
    if txn1_committed and txn2_committed:
        # Both committed - one must have read the other's result
        return txn2_snapshot == txn1_write or txn1_snapshot == txn2_write
    return True

atomic action NoOp:
    pass
```
Run it in the FizzBee playground: https://fizzbee.io/play


**Expected result** (from `fizz`):

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

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/13-02-03-snapshot-isolation)

## Language features used

[Assertions](/reference/language/assertions/), [Flow Modifiers](/reference/language/flow-modifiers/)