Firebreak.Model (Firebreak v0.1.0)

Copy Markdown View Source

A spec-generation IR: per supervisor, exactly the facts a lifecycle model needs — and nothing it doesn't.

Firebreak's analysis already knows the supervision strategy, restart intensity, ordered children (with restart types), the forest structure, and the resolved coupling edges. This module projects those into a self-contained bundle per supervisor so a backend (TLA+, a lockstep scenario, a sequence diagram) can be a pure function of the projection instead of re-deriving the forest.

Each bundle carries:

  • strategy + max_restarts/max_seconds — the restart model.
  • children (in declaration order, with the effective restart type and whether each is itself a supervisor) — the blast / escalation inputs. Order matters: :rest_for_one restarts a child and everything started after it.
  • parent — where a budget-exhausted supervisor escalates to.
  • inbound_crossings — the resolved edges that cross into this subtree from outside it, with sync/in_init. These (and only these) justify an external-caller availability property: a backend models the caller hitting :noproc only where firebreak actually found a synchronous crossing.

Deliberately excluded: anything behavioural (when/why a call fires). For the lifecycle layer the correct abstraction is "a crossing call may happen at any time", so topology is sufficient; protocol-level facts belong to a runtime tool.

A stable interface for backends

mix firebreak --format model emits this projection as JSON, versioned by a top-level schema_version. It is a documented, checkable contract that other tools can build on — Firebreak.Tla and Firebreak.Conformance are just the first two consumers. The full contract (the schema, the serialization conventions, the in/out design law, and a backend-author guide) lives in notes/model-ir-contract.md; valid?/1 checks a projection against it.

Summary

Types

bundle()
child()
crossing()

Functions

build(a)

One lifecycle bundle per supervisor in the analysis.

json(a)

The model projection as a versioned JSON document (mix firebreak --format model): %{"schema_version" => 1, "supervisors" => [bundle, ...]}.

schema_version()

The current model-IR schema version (see notes/model-ir-contract.md).

valid?(bundles)

Is bundles a well-formed model IR (the list build/1 returns)? A checkable form of the contract in notes/model-ir-contract.md, so an external producer or consumer can self-verify. Returns true/false; see validate/1 for reasons.

validate(bundles)

Validate a model IR (the build/1 list form). :ok, or {:error, reasons} listing every bundle that violates the contract.

Types

bundle()

@type bundle() :: %{
  supervisor: module(),
  strategy: atom() | nil,
  max_restarts: non_neg_integer() | nil,
  max_seconds: non_neg_integer() | nil,
  parent: module() | nil,
  children: [child()],
  inbound_crossings: [crossing()]
}

child()

@type child() :: %{
  module: module() | nil,
  restart: atom(),
  type: atom(),
  is_supervisor: boolean()
}

crossing()

@type crossing() :: %{
  from: module(),
  to: module(),
  kind: atom(),
  sync: boolean(),
  in_init: boolean()
}

Functions

build(a)

@spec build(Firebreak.Analysis.t()) :: [bundle()]

One lifecycle bundle per supervisor in the analysis.

json(a)

@spec json(Firebreak.Analysis.t()) :: String.t()

The model projection as a versioned JSON document (mix firebreak --format model): %{"schema_version" => 1, "supervisors" => [bundle, ...]}.

schema_version()

@spec schema_version() :: pos_integer()

The current model-IR schema version (see notes/model-ir-contract.md).

valid?(bundles)

@spec valid?([bundle()] | term()) :: boolean()

Is bundles a well-formed model IR (the list build/1 returns)? A checkable form of the contract in notes/model-ir-contract.md, so an external producer or consumer can self-verify. Returns true/false; see validate/1 for reasons.

validate(bundles)

@spec validate([bundle()] | term()) :: :ok | {:error, [String.t()]}

Validate a model IR (the build/1 list form). :ok, or {:error, reasons} listing every bundle that violates the contract.