tools-spin-sync

name	tools-spin-sync
description	Synchronize Spin/Promela models with current source code and re-verify
argument-hint	[model-name | all]

Ensure that existing Spin/Promela models in modelling/spin/ accurately reflect the current source code, then re-run model checking to confirm the properties still hold.

Input

The user provides one of:

• A specific model name (subdirectory under modelling/spin/, e.g. write-before-evict, no-lost-extents)
• all — synchronize every model found in modelling/spin/
• No argument — present the list of available models and ask the user to choose one or all

Steps

Step 1: Discover models

List all subdirectories under modelling/spin/ that contain a .pml file and a README.md. Each such directory is a model.

If no argument was provided, present the list and ask:

Which model(s) would you like to synchronize?

1. write-before-evict
2. no-lost-extents
3. (other models...) A. All of the above

Step 2: For each selected model, perform the synchronization

2a. Read the model's README.md

Extract from the README:

• The "Correspondence to Source Code" table — this maps model locations to source files and line ranges
• The "Properties Verified" table — the invariants the model checks
• The "System Abstraction" table — how real components map to Promela processes
• The "Assumptions / Stubs" section — what is abstracted away

2b. Read the current source code

For each entry in the Correspondence table, read the referenced source file and the indicated line range (plus ~50 lines of context on each side to detect if the logic has shifted).

2c. Read the existing .pml model

Read the full Promela specification to understand the current model logic.

2d. Identify divergences

Compare the model against the source and look for:

1. Structural changes — The source code logic has been refactored, moved to different functions/files, or the control flow has changed in ways the model doesn't capture.
2. New states or transitions — New code paths have been added (e.g., a new error handling branch, a new concurrent actor, a new state in an enum) that the model doesn't cover.
3. Removed paths — Code paths the model exercises no longer exist in the source.
4. Semantic changes — The synchronization protocol has changed (e.g., lock ordering, channel semantics, atomic sections) but the model still uses the old protocol.
5. Line range drift — The code is substantively the same but has shifted to different line numbers (cosmetic — update the README only).

2e. Report findings

For each model, report one of:

• IN SYNC — The model accurately reflects the current source. No changes needed. (Proceed directly to Step 3.)
• LINE DRIFT ONLY — The logic is unchanged but line numbers in the Correspondence table are stale. Update the README table. (Proceed to Step 3.)
• MODEL UPDATE REQUIRED — The source has diverged materially. List the specific divergences found.

2f. Update the model (if required)

If the model requires updating:

1. Explain the divergence to the user: what changed in the source, and how the model must adapt.
2. Update the .pml file to reflect the new source code logic. Preserve the existing model's style and conventions:
   • Keep the same parameter names and sizes (unless the change requires new parameters)
   • Keep the same property IDs (P1, P2, ...) where they still apply
   • Add new properties if new invariants are now relevant
   • Remove properties if they no longer apply (explain why)
   • Maintain the header comment block format
3. Update the README.md — refresh the Correspondence table with correct line ranges, update Properties Verified if changed, update System Abstraction if new processes were added/removed.

Step 3: Run model checking

For each model (whether updated or unchanged):

cd modelling/spin/<model-name>
make clean
make

Report the results:

• PASS: errors = 0, state count, depth reached, unreached states
• FAIL: assertion violation or invalid end-state found. In this case:
  1. Run spin -t -p <model>.pml to get the error trail
  2. Analyze the counterexample
  3. Determine if the model is wrong (fix it) or if a real bug was found (report it to the user with the trail)
  4. Re-run verification after fixes

If Spin is not installed (/usr/local/bin/spin missing), warn the user and skip verification.

Step 4: Summary report

Present a final summary table:

Model	Status	Divergences	Verification	States	Unreached
write-before-evict	IN SYNC	—	PASS	12345	0
no-lost-extents	UPDATED	new abort path	PASS	67890	0

Notes

• Models are always found at modelling/spin/<name>/<name_underscored>.pml (name uses hyphens for the directory, underscores for the .pml filename).
• The Makefile in each model directory provides the make/make clean targets.
• If a model update introduces new processes or significantly changes the state space, re-tune the parameters to keep verification tractable (<10M states). Document parameter changes in the README.
• Never delete existing properties unless the invariant is provably no longer meaningful. If unsure, keep it and note it as "legacy — source no longer exercises this path directly."
• If the source change reveals a potential real concurrency bug (model finds a valid counterexample that corresponds to reachable code), halt the sync and report the finding prominently to the user.