[kixelated]

Finishes quest/m0/ci/tlc-cost.md and deletes it.

Problem

A TLC run took every core (-workers auto), stalling every other gated command behind it, and a killed run left its -metadir (tens of GB) in /tmp. The route model's SumOver recursed over SUBSET S on every use, and agents ran whole model directories that Nightly already covers.

Approach

• sh/tlc.py now runs both tla recipes. It runs TLC 1.8 on 4 workers at nice 19 with a 4 GB heap and -checkpoint 0, and adds the pinned Community Modules jar to TLC's classpath. Each run's metadir lives in .tmp/tlc/ and is removed when the run exits. The run holds a lock on it that the kernel drops when the run dies, so each new run removes the metadirs whose lock nobody holds, including a SIGKILLed run's. A lock over .tmp/tlc keeps a sweep from taking a metadir before its owner locks it. The script prints each run's core-seconds.
• RouteHandoff.tla sums with FoldSet through LOCAL Ext == INSTANCE FiniteSetsExt (EXTENDS clashes: the Community Modules' Functions defines Restrict too).
• Community Modules 202311011627 (-deps jar), pinned by URL and hash and fetched with nix store prefetch-file. nixpkgs tlaplus18 is a June 2023 TLC build (5b3286b). Later Community Modules releases call OpValue.eval, which that build lacks, and the plain jar misses jgrapht, which the override registry loads.
• Agents check single configs: the verify-* skills, REVIEW.md, and the js/*/verify/ READMEs no longer tell agents to run just test tla <dir>. Only Nightly runs whole directories.
• Nightly: Early.cfg and LagWide.cfg share one leg (route large), replacing a leg each. The skills quote times on 4 workers, and the subscribe counts are updated (below).
• quest/m1/route-inductive.md takes the quest's undecided item on RefinesClaims cost, and quest/m1/tla-native-checker.md notes the new TLC baseline and that the route model needs FiniteSetsExt.

Decisions

Per-config SYMMETRY: none added (✅ skip; rejected: add it to RouteHandoff.cfg and Early.cfg). The maintainer picked "add SYMMETRY where sound". The audit found it sound on only those two configs (graph {0,1},{1,2},{1,3},{2,3}, swapping relays 2 and 3). There it saves at most 2x, and only after SelectKey's m <= x tie-break (RouteHandoff.tla:178) moves to a new Order constant that all 9 route configs must set. Soundness also rests on a hand argument TLC does not check, which adding one link would silently break. Chosen without asking (the user is away). Per config:

Config	Why not
js/publish Publish.cfg, js/watch Watch.cfg	No constants to permute.
js/room Room.cfg	Kinds has one member and is compared to string literals.
js/watch Failover*.cfg	Relays = {1, 2} are numbers, and Init singles out relay 1.
failover/*.cfg	Relays are string literals in the spec, and E starts on A.
reconnect/*.cfg	Start = "a" fixes one of two endpoints; sessions are numbered in order.
resume/*.cfg	Tracks are 1..MaxTracks; track 1 is singled out and tracks come up in order.
subscribe/*.cfg	Groups = {0}; streams are ordered.
route Lag, Ring, Loop, LagWide	SelectKey's m <= x tie-break decides between the swapped relays. LagWide also fixes relay 1 in Scoped.
route Blind, Dead, Twice	Simulated, where symmetry does nothing. Blind and Dead also have no non-identity automorphism.
route RouteHandoff, Early	Sound, at most 2x, but costs the spec change above (skipped).

Also chosen without asking:

• The workers default is 4, matching Nightly's runners. A caller's own -workers comes after it and wins (checked: -workers 2 ran on 2); no doc suggests one.
• Only the route configs were measured before and after, since only that spec changed. For the other models only the worker count moved, which the native-checker quest measured near flat in core-seconds from 2 to 24 workers.
• RefinesClaims (not on main; moq-dev/moq#8564 adds it): the recommendation (check it on the smallest exhaustive config, not the simulated Blind.cfg) moves into the route-inductive quest's Plan. test(net): Apalache reads the route model but cannot step it #8564 edits the deleted quest file, so whichever PR lands second resolves that.

Validation

Before and after, through quest gate and the same wrapper on 4 workers, on the maintainer's host (32 cores, load average 20 to 45, so wall times are noisy). "Before" is main's RouteHandoff.tla copied to .tmp/. Simulated configs ran with -seed 1.

Config	Distinct states (before = after)	Core-s before	Core-s after	Wall before	Wall after
RouteHandoff.cfg	407,240	541	250	149s	60s
Ring.cfg	426,409	506	265	188s	83s
Lag.cfg	1,299,405	1,610	858	397s	373s
Early.cfg	4,178,590	4,079	2,611	995s	646s
LagWide.cfg	4,194,747	8,093	2,235	2,325s	484s
Loop.cfg (breaks RequestsLoopFree both times)	1,199,357 / 999,365 at the break	869	538	200s	127s
Twice.cfg (simulated, 4.0M states)	n/a	598	597	179s	205s
Dead.cfg (simulated, 4.8M states)	n/a	2,901	2,101	962s	660s
Blind.cfg (simulated, 4.8M states)	n/a	2,923	2,073	784s	604s
Total		22,120	11,528

Every verdict held, and every exhaustive config kept its distinct-state count. Loop stops at its first violation, so its count at the break depends on worker order.

• just test tla rs/moq-net/verify/reconnect js/room js/publish through both recipes: the passing configs exit 0 and the two open-finding configs exit 12, which sh/tla.sh accepts. Handover.cfg took 47 core-seconds for 1,240,975 states.
• Subscribe on 4 workers: SubscribeAccounting.cfg 77,667,780 distinct states in 3,319 core-seconds (832s), and Continuation.cfg 29,641,907 in 1,323 (288s). The skill said about 76.5M and 29.4M. That spec is untouched here, and the old figures were written in the same commit as the model (moq-dev/moq#8545), so they probably came from an earlier revision of it. Updated to 77.7M and 29.6M.
• SIGKILL: I started a LagWide.cfg run in its own process group and killed the group with SIGKILL after 15s. Its metadir (197 MB) stayed, and the next run removed it. sh/tlc.test.py (in just gh test) covers the sweep: a live lock survives, including one held only by a child, and a dead or lockless metadir is removed.
• The newer jar's foldSet override failed through INSTANCE with a NoSuchMethodError, which shows TLC applies the Java override there. This TLC build prints no line saying an override loaded.
• just check: everything passes except moq-relay runtime_uring::uring_startup_reports_the_memlock_limit, which this PR doesn't touch. It expects io_uring startup to fail on a too-small memlock limit, and this host's limit (ulimit -l 8192) lets it start.

Impact

Public API: none. Wire: none. Tooling: just rs tla and just js tla take the same arguments and now run TLC on 4 workers unless the arguments say otherwise.

Alternatives

• Calling the nixpkgs tlc wrapper: it hard-codes -cp, so the Community Modules jar could not be added.
• A newer TLC with the newest Community Modules: the quest pinned nixpkgs tlaplus18. When nixpkgs updates it, the Community Modules pin must move with it, as sh/tlc.py says.
• Packaging the jar in the flake: nix store prefetch-file --expected-hash gives the same pin without evaluating the flake.

Follow-ups

None.

Models

Size: M
Implementer: Claude Code, claude-opus-5-5, unknown effort (iterate, M)

(Written by Claude Opus 5.5)

Review

Rewritten by quest review after each round.

• Head: e2cfcb0

• Base: origin/main at 7df2ebf

• Reviewer: Codex, gpt-6.1-sol, high effort

• Session: 01a1d569-c3d3-7603-943d-3a9fdaf8c3cd, round 1

• Score: 9/10, Static review found no actionable defects, but runtime validation remains unverified because builds, tests, and quest commands were not run as instructed.

• Rounds: 1; findings 0: fixed 0, refuted 0, open 0

• Findings: none

[pullfrog]

✅ No new issues found.

Reviewed changes

I reviewed all 18 files: the new TLC wrapper, the FoldSet rewrite of the route model, the Nightly matrix merge, and the doc and quest updates. TLC could not run in this sandbox because it has no nix, so the state counts and core-second figures are the author's measurements.

• sh/tlc.py runs both tla recipes. It runs TLC on a pinned nixpkgs#jre with tla2tools.jar and the Community Modules -deps jar on the classpath, at nice 19, with a 4 GB heap and -workers 4 -checkpoint 0. The caller's arguments come after these, so a caller's own -workers wins. TLC runs from the repo root, so -config rs/… and -config js/… resolve as before. The jar path matches nixpkgs' tlaplus18 package ($out/share/java/tla2tools.jar).
• Metadir lifecycle.
  • Each run's metadir lives under .tmp/tlc/, which is gitignored.
  • Each metadir holds a flock, and its fd is passed to java, so an orphaned TLC keeps its metadir alive.
  • The startup sweep and the final removal both take the .tmp/tlc/.lock guard, so neither can catch the other mid-operation.
  • On SIGTERM, sys.exit makes subprocess.run kill the child before the finally removes the metadir. A child killed by a signal exits as 128 plus the signal number, and the exit codes 11 to 14 that sh/tla.sh checks pass through unchanged.
• RouteHandoff.tla SumOver. It now calls Ext!FoldSet(LAMBDA x, acc : f(x) + acc, 0, S) through a LOCAL instance of FiniteSetsExt, which avoids the Restrict clash. The argument order matches the Community Modules definition, op(element, acc).
• Nightly. Early.cfg and LagWide.cfg now share the route large leg. The route leg's exclusions are unchanged, and the 180-minute job timeout leaves room for both configs.
• Docs. The skills, REVIEW.md, and the js/*/verify/ READMEs now tell agents to run single configs. No other doc still tells them to run just test tla <dir>.

  ^{｜ View workflow run ｜ Using claude-opus-5-5 ｜ 𝕏}

[coderabbitai]

No actionable comments were generated in the recent review.

Walkthrough

The changes add a shared Python TLC runner with pinned Community Modules support and locked metadata-directory cleanup. JavaScript and Rust recipes delegate TLC execution to the runner, and tests cover metadata cleanup. The route model uses FoldSet for SumOver. The nightly matrix combines two route configurations into one job. Documentation updates commands, configuration guidance, state counts, runtimes, and nightly-run descriptions.

Merge Risk: Minimal · up to e2cfc

This change moves TLA+ model-checking runs to a shared runner with lower resource use and updates the related docs and nightly schedule. No actionable merge-blocking risk was found.

Pre-merge checks: 4

Check name	Status	Explanation
Title check		The title names the main change: TLC runs in the verify tooling now use fewer core-seconds and share the host, which matches the sh/tlc.py runner (4 workers, nice 19, lock-based metadir cleanup) a…
Linked Issues check		Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check		Check skipped because no linked issues were found for this pull request.
Description check		The description is specific and closely tied to the changeset. It explains the problem (TLC runs using all cores and leaving large metadirs behind), the approach (sh/tlc.py runner with 4 workers, nice…

Full details: Title check

Explanation

The title names the main change: TLC runs in the verify tooling now use fewer core-seconds and share the host, which matches the sh/tlc.py runner (4 workers, nice 19, lock-based metadir cleanup) and the measured core-second reduction in the description. It is a single, specific sentence and needs no remediation.

Full details: Description check

Explanation

The description is specific and closely tied to the changeset. It explains the problem (TLC runs using all cores and leaving large metadirs behind), the approach (sh/tlc.py runner with 4 workers, nice 19, locked metadirs under .tmp/tlc, and cleanup), the RouteHandoff.tla change to FoldSet, the doc and skill updates, the Nightly job consolidation, the per-config symmetry decisions, and before/after validation tables. It also lists the deleted quest file and the updated quest notes. The description matches the raw summary's listed file changes.

Finishing Touches

Simplify code

• Commit to this branch
• Create a new PR

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

• X
• Mastodon
• Reddit
• LinkedIn

Recent review info

Run configuration

• Source mode: Auto
• Repository: Unavailable
• Branch: Unavailable
• File: No configuration file from this repository applied
• Commit: Unavailable
• Layers: Organization UI
• Review profile: CHILL
• Plan: Advanced
• Run ID: 73cfd23c-87de-42a4-b694-b588fea3bf81

Commits

Reviewing files that changed from the base of the PR and between 1d4da9a and e2cfcb0.

Files selected for processing: 4

• .github/workflows/nightly.yml
• js/watch/verify/README.md
• quest/m0/ci/tlc-cost.md
• quest/m2/tla-native-recheck.md

Files with no reviewable changes: 1

• quest/m0/ci/tlc-cost.md

Included review availability: This review used your included allowance. Your plan provides up to 4 included reviews per hour; 2 remain after this review.

[kixelated]

The body measures only the route configs. A parallel run measured every other config too, before and after on 4 workers through quest gate (before: main's recipe with -workers 4; after: this PR's recipe as of an earlier head, with the same pinned Community Modules release). Every verdict held, and every passing exhaustive config kept its distinct-state count. Core-seconds stay flat outside the route model, as expected, since only the worker count and -checkpoint 0 change there:

Config	Core-s before	Core-s after
subscribe/SubscribeAccounting.cfg (77,667,780 states)	3,000	3,014
subscribe/Continuation.cfg (29,641,907)	1,131	1,119
resume/ResumeReader.cfg (14,334,670)	1,012	1,036
resume/ThreeRoutes.cfg (7,053,230)	354	374
failover/EndedRelay.cfg (breaks NoSkipWhileHeld both times)	3,889	3,772
failover/FailoverChain.cfg (1,961,020)	130	129
failover/Leave.cfg (2,162,238)	139	140
reconnect/Handover.cfg (1,240,975)	38	39
reconnect/RestartWait.cfg (236,751)	9	10
The four open-finding reconnect, subscribe, and js/watch configs, and the passing js configs	1 to 4 each	1 to 3 each

Its route numbers agree with the table above: 18,454 core-seconds before and 10,115 after over all nine route configs (-45%), with LagWide.cfg -59% and Early.cfg -44%.

(Written by Claude Opus 5.5 with high)

[pullfrog]

✅ No new issues found.

Reviewed changes

The only commit since the last review merges main, and the merge changes only quest docs.

• Re-pointed the quest links after main renamed the native-checker quest. main replaced quest/m1/tla-native-checker.md with quest/m2/tla-native-recheck.md. That quest now says #8628 replaced SumOver with FoldSet from FiniteSetsExt, which sh/tlc.py puts on TLC's classpath. It also drops its ## Required link to the deleted tlc-cost.md. Nothing in the tree still links to either removed quest file.

  ^{｜ View workflow run ｜ Using claude-opus-5-5 ｜ 𝕏}