mix firebreak.lockstep (Firebreak v0.1.0)

Copy Markdown View Source

Generates a lockstep ctest scaffold per synchronous cross-tree crossing firebreak found — the dynamic counterpart to mix firebreak.spec (which generates TLA+). Where the TLA+ spec proves the cross-tree :noproc failure is reachable in a model, the lockstep scaffold is the starting point for a test that reproduces it in the running BEAM.

mix firebreak.lockstep                  # analyse current project -> firebreak_lockstep/
mix firebreak.lockstep ../some_app --out scenarios
mix firebreak.lockstep --no-compile     # static only

Each scaffold names the two coupled processes, sets up the lockstep harness, and marks three TODOs (start the target, drive the call, assert it's handled). It is written outside test/ and flunk/1s until completed, so it never breaks your suite before you finish and move it in. Requires {:lockstep, ...} as a test dependency in the target project.