Projection that tracks pending operations and asserts progress (liveness).

Traditional SPBT focuses on safety properties - invariants that must never be violated. Liveness properties are different: they guarantee that something good eventually happens.

Safety vs Liveness

What This Projection Detects

• Deadlock - System hangs forever, no invariant violated
• Livelock - System is busy but makes no useful progress
• Starvation - One client always succeeds, another never does
• Infinite retry loops - System keeps retrying without bound

How It Works

1. Track commands that start operations (e.g., CreateTransfer)
2. Track events that complete operations (e.g., TransferCompleted, TransferFailed)
3. Periodically check for operations pending "too long"
4. Report stuck operations as liveness violations

Configuration

defmodule MyModel do
  def assertion_projections do
    [
      {PropertyDamage.Model.Projection.Liveness, [
        max_pending_duration_ms: 10_000,
        required_completions: %{
          CreateTransfer => [TransferCompleted, TransferFailed],
          CreateOrder => [OrderConfirmed, OrderRejected]
        }
      ]}
    ]
  end
end

Options

• :max_pending_duration_ms - How long before an operation is "stuck" (default: 10_000)
• :required_completions - Map of command module => list of completion event modules
• :check_interval - How often to check (in step count, default: 10)

Limitations

• Requires wall-clock time, complicating deterministic replay
• Timeout thresholds are arbitrary
• Can't detect "infinite but slow progress" (livelock with occasional success)