Generates a TLA+ lifecycle module + TLC config from a Firebreak.Model bundle.

The OTP semantics are a fixed template; the bundle supplies the parameters (strategy, intensity, the actual crossings). The spec is a pure function of firebreak's output — nothing hand-stitched. The external-caller property is emitted only where the bundle has a synchronous inbound crossing.

What it models:

• Restart intensity over a real time window. Crashes spend the budget within a sliding MaxSeconds window (a fixed-window approximation): a fast burst escalates, but Ticks that age the window past MaxSeconds reset it. So the escalation trace shows the crashes were close together in time.
• Escalation to the parent when the budget is exceeded.
• Cross-tree availability after escalation (ExtNeverStuck), where a sync crossing exists.
• :temporary target — a single crash is a permanent loss (never restarted), with the supervisor still alive.
• :one_for_all transient amplification (TargetTransientlySafe) — any one child crash transiently downs every child, so a cross-tree caller of any child is hit even by an unrelated sibling's crash. :one_for_one isolates, so it gets no such property — the contrast is the signal.

Templated: :one_for_all / :one_for_one / :rest_for_one. Not modelled: the exact sliding window (this is fixed-window), and per-sibling :rest_for_one ordering of the transient blast.