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

Copy Markdown

Reusable verification template for gen_statem/GenStateMachine state machines.

Generates a TLX spec from a declarative description of states, initial state, and event-driven transitions. The generated spec includes a state variable, one action per event, and a valid_state invariant.

Usage

defmodule MyApp.ConnectionSpec do
  use TLX.Patterns.OTP.StateMachine,
    states: [:disconnected, :connecting, :connected],
    initial: :disconnected,
    events: [
      connect:    [from: :disconnected, to: :connecting],
      connected:  [from: :connecting,   to: :connected],
      disconnect: [from: :connected,    to: :disconnected]
    ]

  # Extend with your own properties
  property :eventually_connected,
    always(eventually(e(state == :connected)))
end

Generated entities

  • variable :state, <initial> — the state variable
  • One action per event — guarded by state == from, sets state to to
  • invariant :valid_state — state is always in the declared set

Multi-source events

When the same event name appears multiple times (different from states), a single action with branches is generated:

events: [
  reset: [from: :connecting, to: :disconnected],
  reset: [from: :connected,  to: :disconnected]
]

Generates:

action :reset do
  branch :from_connecting do
    guard e(state == :connecting)
    next :state, :disconnected
  end
  branch :from_connected do
    guard e(state == :connected)
    next :state, :disconnected
  end
end

Temporal properties

No temporal properties are auto-generated — they require fairness assumptions that depend on your specific system. Common patterns to add:

# Liveness: the system always eventually reaches a state
property :eventually_idle, always(eventually(e(state == :idle)))

# No deadlock (if all states have outgoing transitions)
# TLC's built-in deadlock detection already checks this