modelsync

Overview ¶

Command modelsync keeps bide's Go code and its TLA+ models (spec/tla) in step. It is the path rule of milestone M4 in docs/design/formal-models.md (section 6.3).

The Go code a model describes is wrapped in region markers that name the model, by its directory under spec/tla, and the model actions (PlusCal labels or TLA+ operators) the region implements:

// protocol:claims begin Claim ClaimRetry ClaimInsert
...
// protocol:claims end

modelsync runs two checks.

The consistency check reads the working tree. Every marker is well formed and paired (regions of one model do not nest; regions of different models may overlap); every action a marker names is defined in the model's spec (spec/tla/<model>/<Model>.tla) and listed in the model-to-code map of spec/tla/README.md; and every action the map lists has at least one marker, unless the README lists it as having no Go region. The README marks a map table with the comment "<!-- modelsync: map <model> -->" on the line before it, and the actions without Go code with "<!-- modelsync: no-code <model> <Action> ... -->". A renamed action, in the spec, the map or the code, fails one of these.

The path rule (with -base) diffs the merge base of -base and -head against -head. If a change touches a marked region of a model (a line inside it, its markers, or lines deleted from it) and changes no file under spec/tla/<model>/, the check fails, unless a commit message in the range or a description file (-body) holds an override line:

Protocol-Impact: none (<reason>)
Protocol-Impact: claims,flows none (<reason>)

The first form covers every model; the second only the models it names. The reason is required. Each override used is printed as a warning (a GitHub annotation under Actions), so it is visible in the check's log and on the pull request.

Usage, from the repository root:

go run ./internal/tools/modelsync                          # the consistency check only
go run ./internal/tools/modelsync -base origin/main        # and the path rule against main
go run ./internal/tools/modelsync -base B -head H -body pr-body.txt

The exit status is 0 when clean, 1 on findings, and 2 when the check could not run.