Generates lockstep concurrency-test scaffolds from firebreak's model IR — the dynamic counterpart to the TLA+ backend.
A cross_tree_coupling finding is a static claim: from synchronously calls
to, which lives in a different supervision subtree, so a restart of to
during the call can surface :noproc in from. Firebreak.Tla proves that
failure is reachable in a model; lockstep can reproduce it in the running
BEAM and leave behind a regression test. This module bridges the two: for each
synchronous cross-tree crossing in the IR (Firebreak.Model), it emits a
lockstep ctest scaffold that sets up the harness, names the two processes, and
marks the three app-specific steps a developer must fill in.
It is deliberately a scaffold, not a runnable test: firebreak can't know how
to start an arbitrary process or what "handled correctly" means for a given
caller. The generated ctest flunk/1s until completed, and is written outside
test/ so it never breaks a suite before the developer opts in.
Pure function of the model IR — see notes/model-ir-contract.md.
Summary
Functions
One {filename, contents} lockstep scaffold per synchronous cross-tree
crossing, deduped by {from, to}.
Functions
@spec generate(Firebreak.Analysis.t()) :: [{String.t(), String.t()}]
One {filename, contents} lockstep scaffold per synchronous cross-tree
crossing, deduped by {from, to}.