Repository navigation
Conversation
cursor#776 checked each rule with one worker per CPU and reran a broken rule with one worker for the shortest path. The compiler port (cursor#977) pinned one worker and Java's default heap for every TLC run. Restore the all-CPU first run, keep one worker where the output depends on it, and let each TLC run's heap grow to half the memory Java sees. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
#776 had TLC check each rule with one worker per CPU, then rerun a broken rule with one worker so the shortest path is the same on every run. #977 pinned
-workers 1 -fp 0 -lncheck finalfor every TLC run with no heap flag, so Java's default of 25% of RAM applies. I found no stated reason for this, so I assume it was lost in the port.On a 12-core Mac mini, a 31-million-state model ran for about 50 minutes on one core, then hit
OutOfMemoryError: Java heap spacein the final liveness pass. On a 4-core server with a 1.4 GB heap, it slowed from about 1.3 million to about 20,000 new states per minute once the heap filled.os.availableParallelism(), orSTATECHART_WORKERS).RERUN_STATES), or an invariant or deadlock breaks, it runs again with one worker (PINNED_FLAGSunchanged) and uses that result. Shortest paths and small-model output stay identical, since multi-worker BFS does not guarantee the shortest counterexample ( Ignore flaky DumpLoadTraceTest AliasSub auto-worker tests; add AliasSub2 tests. tlaplus/tlaplus#1326).ChartBound) and the chart run stay at one worker.PROPERTYkeeps the multi-worker trace, which can differ between runs. SKILL.md's "with one worker" sentence now describes all this.-XX:MaxRAMPercentage=50. I left out-XX:+UseParallelGCbecause SKILL.md's note ontlc.outrelies on the first-warning behaviour. Happy to add it if you prefer.A 1,283,467-state model with a liveness property went from 68.6 s to 25-27 s on 12 cores and from 2 min 20 s to 57 s on 4, with the same verdicts and state count.
The new
test/workers.test.tsruns two models above 100,000 states with 2 workers and with 1. When the rules hold, both give the same outcomes and state count. When an invariant breaks, both give the same shortest path. Full suite on macOS: 266 pass, 69 skipped, 1 fail. The failure is the symlinked-launcher test intest/cli.test.ts, which fails the same way onmain.We vendor pstack in our own plugin and carry this patch there in the meantime.
🤖 Generated with Claude Code