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

Copy Markdown

Reusable verification template for GenServer request/response handlers.

Generates a TLX spec from a declarative description of fields (state variables), calls, and casts. Each call/cast becomes an action with optional guards and partial next-state updates.

Usage

defmodule MyApp.ReconcilerSpec do
  use TLX.Patterns.OTP.GenServer,
    fields: [status: :idle, deps_met: true],
    calls: [
      check: [next: [status: :in_sync]],
      apply: [
        guard: [status: :drifted, deps_met: true],
        next: [status: :in_sync]
      ]
    ],
    casts: [
      drift_signal: [next: [status: :drifted]]
    ]

  # Extend with your own invariants or properties
  invariant :apply_requires_deps, e(ite(status == :in_sync, true, true))
end

Generated entities

  • One variable per field with its default value
  • One action per call/cast — with optional guard and partial next-state
  • valid_<field> invariant for each atom (non-boolean) field

Guards

Guards are keyword lists where each pair becomes an equality check, combined with and:

guard: [status: :drifted, deps_met: true]
# generates: guard e(status == :drifted and deps_met == true)

Partial next-state

Only the fields listed in next: get next calls. Unspecified fields are automatically UNCHANGED in TLA+ emission:

calls: [check: [next: [status: :in_sync]]]
# Only updates status; deps_met remains unchanged