Firebreak.Quint (Firebreak v0.1.0)

Copy Markdown View Source

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 exists

Same 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}.

Functions

generate(bundle)

@spec generate(map()) :: {:ok, String.t(), String.t()} | {:unsupported, String.t()}

Quint module for a bundle: {:ok, name, qnt} or {:unsupported, reason}.