# Write-Ahead Log Pattern

> A write-ahead log as a runnable model: changes are logged before they are applied, checked so the data always matches the last applied log entry.

Canonical: https://fizzbee.io/design/patterns/write-ahead-log/
Source: https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/13-07-01-write-ahead-log


Durability through logging before applying changes

**Demonstrates:** WAL, durability, crash recovery

```fizz
# Example 0075: Write-Ahead Log Pattern
# Durability through logging before applying changes
# Demonstrates: WAL, durability, crash recovery

MAX_WRITES = 2

action Init:
    log = []
    applied_index = 0
    data_value = 0

atomic action WriteToLog:
    require len(log) < MAX_WRITES

    # Log entry before applying
    entry = record(index=len(log), value=len(log) + 1)
    log.append(entry)

atomic action ApplyLogEntry:
    require applied_index < len(log)

    # Apply logged entry to data
    entry = log[applied_index]
    data_value = entry.value
    applied_index = applied_index + 1

atomic action Recover:
    # Recovery: replay unapplied log entries
    if applied_index < len(log):
        entry = log[applied_index]
        data_value = entry.value
        applied_index = applied_index + 1

# Safety: applied index never exceeds log
always assertion AppliedWithinLog:
    return applied_index <= len(log)

# Safety: data reflects applied entries
always assertion DataMatchesLog:
    if applied_index > 0:
        return data_value == log[applied_index - 1].value
    return data_value == 0

atomic action NoOp:
    if len(log) >= MAX_WRITES and applied_index >= len(log):
        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: 6, queued: 0
Valid Nodes: 6 Unique states: 6
IsLive: true
PASSED: Model checker completed successfully
```

[Source on GitHub](https://github.com/fizzbee-io/fizzbee/tree/main/examples/references/13-07-01-write-ahead-log)

## Language features used

[Assertions](/reference/language/assertions/), [Flow Modifiers](/reference/language/flow-modifiers/), [Data Structures](/reference/language/data-structures/)