Generates a Quint lifecycle module from a
Firebreak.Model bundle — the same supervision-lifecycle model as
Firebreak.Tla, in Quint's syntax.
Quint is TLA+'s modern, typed surface (Informal Systems); it checks via Apalache
or its own simulator. This is a second, independent consumer of the model IR —
proving the contract (notes/model-ir-contract.md) really is backend-agnostic.
The OTP semantics are a fixed template; the bundle supplies strategy, intensity,
and the actual crossings. Constants are inlined as pure val, so each module is
self-contained and directly checkable:
quint verify --invariant SupNeverDies <Sup>.qnt
quint verify --invariant ExtNeverStuck <Sup>.qnt # where a sync crossing existsSame dispatch and fidelity as the TLA+ generator: :one_for_all (shared-fate +
transient amplification), :one_for_one/:rest_for_one (windowed budget), and a
:temporary synchronous target (single-crash permanent loss).
Summary
Functions
Quint module for a bundle: {:ok, name, qnt} or {:unsupported, reason}.