TLX.Patterns.OTP.Supervisor (TLX v0.5.2)

Copy Markdown

Reusable verification template for OTP Supervisor restart strategies.

Generates a TLX spec that models the supervisor's restart mechanism: per-child crash and restart actions, strategy-specific restart behavior, escalation when the restart bound is exceeded, and a bounded_restarts invariant.

Usage

defmodule MyApp.SupervisorSpec do
  use TLX.Patterns.OTP.Supervisor,
    strategy: :one_for_one,
    max_restarts: 3,
    children: [:db, :cache, :web]
end

Strategies

  • :one_for_one — only the crashed child is restarted
  • :one_for_all — all children are restarted when any crashes
  • :rest_for_one — the crashed child and all children after it (in declaration order) are restarted

Generated entities

For each child :name:

  • variable :name_status, :running — child status
  • action :crash_name — guarded by name_status == :running
  • action :restart_name — strategy-specific, guarded by crashed + bound

Global:

  • variable :restart_count, 0 — restart counter
  • action :escalate — when restart_count >= max_restarts and any child crashed
  • invariant :bounded_restarts — restart_count <= max_restarts

Time modeling

The restart counter is modeled without a time window. This verifies the bound is never exceeded, which is the critical safety property. Time-based window reset is not modeled in v1.