mix firebreak.spec (Firebreak v0.1.0)

Copy Markdown View Source

Generates a formal lifecycle spec per supervisor, derived purely from firebreak's supervision model (mix firebreak --format model). Each spec models the restart/escalation lifecycle and — only where firebreak found a synchronous cross-tree crossing — an external-caller availability property.

mix firebreak.spec                          # TLA+ + TLC config -> firebreak_specs/
mix firebreak.spec --lang quint             # Quint modules instead
mix firebreak.spec ../some_app --out specs  # analyse another project
mix firebreak.spec --no-compile             # static only

Run a generated spec:

# TLA+ (default)
java -cp tla2tools.jar tlc2.TLC -deadlock -config <Sup>.cfg <Sup>.tla
# Quint
quint verify --invariant SupNeverDies <Sup>.qnt

:one_for_all, :one_for_one, and :rest_for_one are templated (plus a :temporary synchronous-target refinement); other shapes are reported as skipped rather than modelled unfaithfully. TLA+ and Quint emit the same model.