TLC as a resident service over JSON lines, with a persistent state graph - #2
Merged
Merged
Conversation
kiranandcode
changed the title
kiranandcode
added this pull request to stack #3
September 22, 2026 16:35
… close over JSON lines Adds tlc2.basis.Resident, one JVM that parses a spec once and keeps the checker, fingerprint set, queue and trace alive between requests, driven by JSON objects on stdin with replies on stdout; TLC's own printing goes to stderr so the protocol owns stdout. open returns the catalogue (actions with locations, invariants, implied actions, temporal properties, variables, constraints, symmetry) and explores nothing. check explores under a wall-clock or distinct-state budget, suspending the queue when it runs out and resuming on the next call; with continue it keeps going past the first violation (TLCGlobals.continuation) and reports every invariant's verdict: violated with its first level, last action and report count, no_violation_found when the run finished, or not_evaluated. Counterexamples come from tlc2.basis.Recorder, an IMessagePrinterRecorder that keeps TLC's messages as their code and objects and renders trace states through the Json module, so nothing parses the -tool text. Coverage and the fingerprint polynomial are decided at open, since TLC reads both into class-load statics. Verified by hand on a two-action counter spec: an invariant violation answers with a typed five-state trace; with continue, one run reports six violations of one invariant, none of the other, and the terminal deadlock; stats and close behave. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…s and the guards that blocked transitions; serve trace, neighbours, eval, screen and guard_profile tlc2.basis.GraphStore implements IStateWriter and sits on the hooks the checker already calls on every edge and, because it is constrained, on every guard that evaluated false. It appends each newly reached state's variable values to basis.states under the metadir (only the values: the TLCState header is unset on the states the hook receives), keeps the fingerprint index with level and first predecessor and the predecessor lists in memory, and tallies blocked guards per (action, conjunct) with one example state and its quantifier bindings. The checker's end-of-run close only syncs the file, so the store outlives the run. IStateWriter gains writeUnsatisfied(state, action, successor, pred, context), which Worker.addUnsatisfiedState now calls, so the bindings that made a guard false reach the writer; the default keeps the old behaviour. Tool reports a false guard on the general next-state path and on user-defined-operator guards too, not only when every primed variable was already assigned, so a spec whose actions start with their guards (the usual shape) is profiled. The resident serves the store: trace (the path from an initial state to a fingerprint along first predecessors, shortest with one worker), neighbours (recorded predecessors, and per action the successors computed afresh, with the variables each changes), eval (an expression parsed against the root module as the debugger does, in one stored state or a stored pair for primed expressions), screen (candidate state predicates over every stored state under a budget: holds_on_stored, violated with the first violating fingerprint and level, or not_evaluable with the parse error) and guard_profile. stats carries the store's counts. Verified by hand on the counter spec: 18 states and 27 edges stored, Dbl blocked six times by y<4 and Inc three times by x<5, a screen of four candidates (one violated twelve times from level 5, one unparsable), a six-state trace, a neighbourhood with one enabled action, and single- and two-state evaluation. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
tlc2.tool.coverage.CoverageWalk walks the ActionWrapper and OpApplNodeWrapper tree TLC's printer walks, but keeps every node with its location, source text, primary and secondary counts and whether it is primed, and lists per action and invariant the subexpressions no evaluation reached (a node counts as unevaluated only when nothing below it ran either, since a conjunction's own counter stays at zero while its conjuncts run, and assignment targets under a primed node are never evaluated). The printer skips zero-count subtrees and collapses consistent ones, which hides exactly the dead conjuncts a reader wants. Per variable it reports the HyperLogLog distinct-value estimate, null before exploration. It lives in the coverage package because the counters are package-private. The resident serves coverage, and registers: whether the reachable graph was exhausted and what stopped the run, the workers' out-degree buckets aggregated (ModelChecker gains a getWorkers accessor), the fingerprint set's statistics where its implementation keeps them, the optimistic fingerprint-collision probability, and whether liveness and coverage are on. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
tlc2.basis.Incremental parses the edited spec into a new Tool, pairs actions and invariants with the old ones by name and source text (an action or invariant also counts as changed when a changed root-module definition is named in its text, a conservative dependency test), and replays the old store into a new one: states reachable from the initial states along unchanged actions survive with those edges copied, survivors are re-expanded under the changed and added actions only, states reached for the first time under every action; successor generation, constraints and invariant evaluation all go through the new Tool, so the store stays a cache of TLC's answers. A sweep then evaluates every invariant on every stored state for exact verdicts, the first violation being the lowest-level one. Changed variables, initial predicate or config cannot be carried: the resident answers restart_required, since a second ModelChecker in one JVM trips over TLC's per-process worker and trace bookkeeping. The resident serves refresh (diff, survivors, dropped, re-expanded, new states, edges copied and generated, per-invariant verdicts, the store's sizes) and refuses check after an incremental refresh, whose store the store queries serve. GraphStore exposes its initial fingerprints and variable names; the Recorder can reset. Not carried: liveness, deadlock reporting, and the blocked-guard tallies for the re-expanded states. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
The resident opens with mode simulate: a Tool in simulation mode and a Simulator with depth, traces and seed (random and reported by default). A non-null traceActions value sizes the per-worker action-pair counters without TLC writing its dot files at the end. simulate runs until the traces, a violation or the budget (Simulator.stop), then answers the verdict, every violating behaviour as a typed trace, the simulator's statistics record and the follow matrix from Simulator.actionFlowAsJson, a public accessor over the private snapshot that reduces contexts to one vertex per definition and says whether the extended statistics were armed at class load. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
TLCGlobals.continuationTraceLimit bounds how many traces Worker and ModelChecker regenerate per invariant or implied action under -continue; further violations are still reported (and so counted) but not traced. A trace is rebuilt by re-running the next-state relation from an initial state, which dominated a Raft run whose invariant failed on most states. The resident sets the cap from a check's traces_per_property (default 1, -1 unlimited) and lists only traces that carry states. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
kiranandcode
force-pushed
the
kg/resident
branch
from
September 22, 2026 17:10
6c11249 to
69c5b4f
Compare
Review fixes for the incremental refresh and simulate paths. - The variables check compared the new spec with itself: the store's names came from TLC's static table, which the new parse had already replaced. Both lists now come from each tool's own declarations. - A config edit, a changed state or action constraint, view or symmetry set, or an old exploration that did not finish (budget, first violation, error, or anything left queued) now forces a full rerun. Copying an edge is sound only for a fully explored graph under the same constraints. - "Changed" is decided by a signature: the node's text, every user definition it reaches transitively across modules, and its context bindings, so an edit two definitions down or to a quantifier bound is seen. Split actions left unpaired are reported as added. - Refresh no longer stops a paused checker (stopping made the next check report a cut-short run as finished). When the new tool is not adopted, TLC's static variable tables are rebound to the old spec; if a definition slot was lost the paused run refuses to resume. - Refresh in simulate mode is refused instead of throwing. - A simulate call after a budget stop reports that stop again, marked not resumable, rather than a completed run. - The invariant verdicts of check use the same completeness test. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ns, store content - Recorder: a stuttering tail (TLC_STATE_PRINT3) arrives as a TLCStateInfo with a null state; record it as null instead of throwing, which broke every liveness counterexample ending in stuttering. TLC_STATE_PRINT1 now accepts the TLCStateInfo MP.printState always passes, so standalone and runtime-error states are kept. - ModelChecker: suspend() now holds the workers. Periodic work (checkpoints, liveness checks) suspends and resumes the queue itself and used to undo a resident's budget pause; it now resumes only when nobody holds them, and resume() defers to periodic work in progress. - Incremental: config substitutions (CONSTANT N <- Def, Op <- Def, [M] Op <- Def) are bound as tool objects, invisible to the signature walk. An edit to a substituted definition now forces a full rerun. - GraphStore: keep a state's content from the IsUnseen write, the one TLC enqueued, so a VIEW or SYMMETRY run with several workers cannot store a different concrete state than the one whose successors are recorded. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Collaborator
Author
|
Review round 2 fixes are in 7e6baef. Each fix was checked with a repro against both 818ec9d and the new head.
verus-tools-mcp 🤖 Generated with Claude Code |
- Tool: the false-guard sites added for the store (user-defined guards, the general path, and now = / \in / \subseteq guards on unprimed variables) report through a private falseGuard, not processUnsatisfied, so the debugger's frames are unchanged. IStateWriter's default writeUnsatisfied forwards only a fully assigned successor, so -dump dot,constrained no longer throws a NullPointerException fingerprinting a partial state. - guard_profile counts equality and membership guards (pc = "a"), and its note says what a count means, disjunctions included; after a refresh it says its tallies are stale. - refresh replays from the last fully explored graph. A replay cut short by its budget or a first violation is served but not replayed from, so the fix after a violation is incremental rather than a restart; a replay that fails is not adopted and the store stays. The reply adds complete, stopped_at_first_violation, adopted, replayed_from, and unchecked (temporal properties, implied actions, deadlock, guard tallies). Stores nothing refers to are closed and deleted. - GraphStore: fingerprinting and serialising run outside the lock, a per-thread serialiser reuses its buffer (ValueOutputStream.reset), and file writes are batched. open takes store: false to run without it; the heap cost is documented. - The continuation trace cap is per run, not per check call. - Tests: DotConstrainedGuardTest, GraphStoreGuardTest, TLCGlobalsContinuationTraceTest, and resident tests for refresh against fresh-run graphs, a pause held through checkpoints, and coverage. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The previous commit's edit rewrote the file with LF endings; only the reset() method and the non-final handle table are meant to change. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ation - Defns: a second parse in one JVM gave names the edit added the slots an earlier parse had given other names (slots live on process-global UniqueStrings), so INIT/NEXT/INVARIANT could resolve to the wrong definition after a refresh. New names now take slots above every slot already handed out in the process. - Incremental: a reached definition's signature now includes its formal parameters, and every INSTANCE ... WITH substitution passed through is recorded (by content, so moving text is no edit). Swapping F(a, b) to F(b, a), or which parameter a WITH expression replaces, was invisible. - Resident: `continue` is applied only to a run that is about to explore, and completeness/registers read the value the run explored under, not the global. A check with continue after a run stopped at its first violation made the next refresh replay the partial graph as complete. - Tests: ResidentRefreshDefinitionsTest, ResidentRefreshSignatureTest, ResidentContinuationTest (each fails without its fix). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ests - ModelChecker.suspend waited for the workers to park while holding the checker's monitor, which a worker takes to report a violation (under continuation, or a first violation) or the end of the run: a budgeted check could hang for good. It now waits outside the monitor. - Under continuation, reports past the per-property trace cap were kept as a message and an empty trace each (59k messages in one reply for a 64k state run). The recorder now counts them; check replies carry them as untraced_reports. - Tests: a budgeted, continuing check on four workers over a mostly violating spec (finishes, counts every report, keeps few messages), and incremental refreshes with four workers against fresh-run counts. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…e guard tallies, constraint rows - Incremental.diff pairs exact (name, signature) matches over every new action before pairing leftovers by name. The disjuncts of an unnamed Next share its name, so inserting one in front used to shift every pair: all actions reported changed and no edge carried. - coverage reads the tool the checker ran. After a refresh it used to walk the refreshed tool, which has no cost model, and answer an empty tree as enabled; it now serves the run's coverage marked stale. - GraphStore tallies false guards in a ConcurrentHashMap keyed by (action, conjunct node identity) with LongAdder counts, building text and location only on first insert. Four workers with the store went from 32.9s to 17.3s on a 923k-state spec (18.7M false guards); they had been slower than one worker. - Successors a state or action constraint excluded are tallied as kind "constraint" rows and counted as `excluded`, apart from the guards. Tests: ResidentRefreshPairingTest, a coverage-after-refresh case in ResidentCoverageTest, GraphStoreConstraintTest over a CONSTRAINT model. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ender at a time Refresh: a changed invariant that throws on a surviving state (or a failure while copying carried edges) now ends the replay with r.error, like a failing action does, so the reply is adopted:false with the error and the new store is released and TLC's statics rebound to the old spec. Resident.refresh also catches anything else the replay throws and treats it the same way, instead of answering `internal` and leaking the store. ModelChecker: the resident's suspend() and the periodic work (liveness, checkpoints) both wait in StateQueue.suspendAll(), which wakes a single waiter when the last worker parks. Two waiting at once left one asleep for good: a hung protocol, or a run whose workers never resume. Both now go through one lock (not the checker's monitor, which workers take on their way to the barrier). Tests: ResidentRefreshInvariantErrorTest; ResidentConcurrentSuspendTest, which hangs without the lock. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… TLCGet
A check whose budget ran out while the initial states were generated, in a
run that then ended there (an initial state violating an invariant, init
failing to evaluate), waited forever in StateQueue.suspendAll: no worker
ever started and nothing finished the queue. The checker thread now
finishes the queue when modelCheck returns, which wakes that wait.
A refresh evaluated constraints without the predecessor TLC sets, so the
usual TLCGet("level") depth bound failed every replay with a
ClassCastException. Setting it would not be enough: TLCGet depends on the
path to a state, which an edit can shorten, so copied edges are unsound.
Incremental.diff now asks for a full rerun when an action, the initial
predicate, a constraint or an invariant reaches TLCGet.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ace per report, exhausted only when complete - Recorder keeps TLC_INVARIANT_EVALUATION_FAILED apart from the violation counts; check reports such an invariant as not_evaluable with its error. - A reprint of the same behaviour (TLC_BEHAVIOR_UP_TO_THIS_POINT on a trace that already has states, as when an evaluation error is re-run for its call stack under continuation) replaces the states instead of appending. - registers derives exhausted from explorationComplete(), and stopped_by says error for a run that ended on an error rather than a violation. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…tions in stopped_by, initial PROPERTY violations - Under continuation TLC checks no further invariant on a state once one fails there, so an invariant it never reported may fail only on those states. For an exhausted run that reported a violation, the resident now evaluates the unreported invariants over the store (Incremental.sweep, restricted by name), or answers not_evaluated without a store. TLC's own -continue behaviour and output are unchanged. - registers.stopped_by: a continuation run that reported violations ends on NO_ERROR; decide exhausted vs exhausted_with_violations from the recorder. - TLC_PROPERTY_VIOLATED_INITIAL (a PROPERTY false in an initial state) is a violation: recorded with its property, verdict property_violated, stopped_by violation. Tests: ResidentContinuationInvariantsTest, ...NoStoreTest, ResidentPropertyInitialTest. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…overage, name slots restored, dead assignments listed - TLC checks invariants on successors a constraint excludes. GraphStore now keeps them (content once per fingerprint, each edge once), refresh carries their edges and checks invariants on excluded successors it generates, and the invariant sweeps (refresh verdicts, skipped invariants under continuation) cover them. Before, an invariant failing only on an excluded state came back no_violation_found. - Refresh evaluates constraints without a cost model: a refreshed tool has none, and Tool.isInModel threw ClassCastException on any refresh with a CONSTRAINT that generated new successors. - neighbours generates successors through Tool.getNextStatesUnrecorded, and the sweeps evaluate invariants with CostModel.DO_NOT_RECORD, so store queries no longer change the run's coverage. - A refresh that is not adopted restores every name's slot as it was before the parse, so a definition the edited spec declares a variable still evaluates as a definition. If one ever doesn't, every request that evaluates against the spec is refused with restart_required. - CoverageWalk lists an assignment that never ran (x' = 0 behind a guard that never held); a primed node counts when it runs. Tests: ResidentRefreshExcludedTest, ResidentContinuationExcludedTest, ResidentRefreshRestoreTest, and ResidentCoverageTest extended. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…pt after a resume without it runContinuation holds only the last check call's setting. A run paused under continuation and resumed with continue:false had already skipped further invariants on the states that violated one, yet the verdicts then called those invariants no_violation_found. A sticky everContinued flag now decides the store sweep; explorationComplete still reads runContinuation, since a run that ended on a violation without continuation is incomplete. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… survivors, serialiser reset order - refresh evaluates the edited spec's ASSUME clauses before replaying; a false (or unevaluable) one leaves the edit unadopted, as TLC would explore nothing. State-level PROPERTY formulas (implied inits) get a verdict over the stored initial states under `implied_inits`, and the open catalogue lists them. - Under a VIEW, a fingerprint in the old graph survives a replay only if the edit reaches it with the same concrete content; otherwise its old edges (generated from other content) are not carried and it is expanded under every action. - GraphStore.serialise resets the value stream before the byte buffer, so a write that threw part way cannot prefix the next stored state. - Tests: ResidentRefreshAssumptionTest; ResidentViewStoreTest (four workers, a VIEW whose hidden variable decides the successors; every stored state's successors match its recorded edges, before and after a refresh that matches a fresh run's 8 states and 13 edges). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…excluded initial states swept Refresh now answers restart_required whenever the old or edited spec has a VIEW or a SYMMETRY set. A fingerprint then names several concrete states and the store keeps whichever TLC reached first; a copied edge from another state could carry that content even when the edited spec never reaches it, and the replay explored it (a reported violation a fresh run did not find). Initial states a state constraint excludes are now kept in the store through a new IStateWriter.writeExcludedInitial hook (a no-op by default) that ModelChecker's init functor calls. TLC checks invariants and state-level properties on them, so the invariant sweeps, the implied-init check and the replay (which carries them and checks changed invariants on them) do too. Before, an edited invariant violated only there came back no_violation_found. Tests: ResidentRefreshViewTest (the repro), ResidentRefreshSymmetryTest, ResidentRefreshExcludedInitialTest; ResidentViewStoreTest now expects the full rerun. ResidentContinuationToggleTest gets a larger state space so its six-state budget reliably fires before the run ends (it failed 2 in 5). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…iteUnsatisfied documented TLC prints the state of an invariant or PROPERTY violated in an initial state only into its report's text, so the recorder's trace for it had no states: `check` answered `trace: null`, left it out of `traces`, and gave the invariant verdict `level: 0`. The recorder now keeps that text, and the resident completes each such trace with the stored initial state whose (ALIAS-evaluated) print matches it, excluded initial states included; without a store the state is kept as TLC printed it. The trace is at level 1 with action <Initial predicate>. IStateWriter: the writeUnsatisfied javadoc sat above writeExcludedInitial's; each method has its own again. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ped implied-action traces on replay, excluded initial states deduplicated in constant time - stats and registers mark themselves stale after an incremental refresh and report whether the refreshed store is the whole graph, as coverage and guard_profile already do. - ModelChecker.doNextCheckImplied gates its continuation trace on the per-property cap, as the invariant branch and Worker do, so the error replay prints no trace the recorder has already counted as capped. - GraphStore keeps excluded initial states in a LinkedHashSet instead of scanning a list under the lock. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…is an error, simulate mode tested The simulator's result code was stored but never read, so a simulation stopped by the next-state relation failing to evaluate (EC.GENERAL) reported no_violation_found with no trace. The reply now carries the result code, answers error for a non-zero code no violation explains (a budget stop excepted), and includes the last behaviour TLC printed, as check does. Tests cover a violation, an evaluation error and a final budget stop. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…tes checked on replay, stores removed on close Every parse resets TLC's model-value table, and a stored state names a model value by its index there. A refresh that was not adopted left the edited spec's table in place, so store queries decoded against the wrong numbering (or threw, after a parse failure). The table is now saved before the parse and restored with the other statics, and an edit that renumbers the model values the store was written under asks for a restart instead of replaying. The replay now checks that every state it carries over reads back with its stored fingerprint, and answers restart_required when one does not, instead of failing later with a NullPointerException. Closing the resident disposes its stores, so a refresh's metadir and store file no longer stay behind in the spec's directory. Store queries on a simulate session say it keeps no store. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…utions force a full rerun
The TLCGet check before an incremental refresh walked only the syntax
reachable from actions, init, constraints and invariants. A definition the
config substitutes in (CONSTANT Op <- Def, Op <- [M] Def) is bound as a
tool object, so a constraint reading TLCGet("level") through one slipped
past: the replay evaluated it without a predecessor, excluded nothing, and
ran to its budget (15.8M states where a fresh run finds 6) before the store
was adopted. Every substituted definition is now walked too, and TLCExt's
Trace and CounterExample, which read the predecessor chain, count as path
dependent alongside TLCGet.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…rror, violation traces kept Under continuation TLC keeps going after the next-state relation fails to evaluate, and with deadlock checking on it then reports the state whose expansion the error aborted as a deadlock, overwriting the error's code. The resident trusted that code: it called the graph exhausted, gave an invariant violated only past the aborted expansion `no_violation_found`, and let a refresh replay the incomplete store. AbstractChecker now keeps every error code it set; any that is not a violation makes the exploration incomplete, `registers` report `stopped_by: error` and `check` report `verdict: error` with the code. The Recorder cleared the open trace on every "behaviour up to this point", so an error's behaviour printed after a violation's overwrote that violation's trace and level. A violation's trace is printed once; a behaviour after it now opens a trace of its own, and only an evaluation failure's reprint replaces what came before. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
On Windows the temp directory's path has backslashes, which the tests pasted into request JSON unescaped, so Gson rejected every open with "Invalid escape sequence". ResidentHarness.spec now returns the path escaped for a JSON string literal. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
CI runs tests with OffHeapDiskFPSet and -XX:MaxDirectMemorySize=512k, so the fingerprint set evicts to disk every 65536 states. An eviction during init trips DiskFPSet's checkFile assertion; plain TLC on master fails the same spec about half the time, so this is not the resident's doing. The test only needs init to outlast a 1 ms budget: 50000 initial states do. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
On Windows another process (a virus scanner, the indexer) can hold a freshly written file open for a moment, so a single delete fails and the store's basis.states outlived the resident's shutdown in CI. Retry briefly, then leave it to deleteOnExit. The cleanup test now names what was left. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Tests pass -teSpecOutDir target/GeneratedTESpecs, and specs with a _TLCTrace POSTCONDITION write their .bin there before TLC creates the directory. Which test got there first used to be an accident of test order; with the resident's test classes added, CodePlexBug08EWD840FL1Test ran first on macOS and its postcondition failed (register 42 null). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
TLC deletes a run's metadir when the run ends, but on Windows a file another process still holds makes that fail, and CI found the session's metadir (state queue and fingerprint files) left in the spec directory. The session created that directory, so shutdown deletes what is left of it with GraphStore's retrying delete, once the checker has stopped. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… metadir A run's cleanup closes the shared trace but never the workers' own trace files (<spec>-<id>.st). The command-line tool exits so nothing notices; the resident outlives its run, and on Windows the still-open C-0.st kept the metadir from being deleted. Worker.closeTrace lets shutdown close them. Co-Authored-By: Claude Opus 5.5 (1M context) <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
1 participant
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.
Steps 2 to 5 of
verus-research/plans/s6-tlc-resident.md: the resident thetlc_*MCP tools drive, the store behind its queries, coverage as data, and incremental replay after an edit.Resident.
tlc2.basis.Residentis one JVM that parses a spec once and keeps the checker, fingerprint set, queue and trace alive between requests, over JSON lines on stdin/stdout with TLC's own printing on stderr.openreturns the catalogue and explores nothing;checkexplores under a budget, pausing and resuming the queue, and withcontinuereports every invariant's verdict;stats/registersread the counters (exhausted, what stopped the run, out-degree buckets, fingerprint-set statistics, collision probability);closeexits.tlc2.basis.Recorderkeeps TLC's messages as(code, objects)and renders counterexample states through theJsonmodule, so nothing parses@!@!@STARTMSGtext.Store.
tlc2.basis.GraphStoreimplementsIStateWriteron the hooks the checker already calls on every edge and, being constrained, on every guard that evaluated false: each reached state's variable values inbasis.statesunder the metadir, the fingerprint index with level and first predecessor, predecessor lists, and blocked-guard tallies per (action, conjunct) with an example state and its bindings. The resident servestrace,neighbours,eval(parsed against the root module as the debugger does),screenandguard_profileover it.Coverage.
tlc2.tool.coverage.CoverageWalkwalks the same tree the printer walks but keeps every node and lists the subexpressions no evaluation reached (the printer elides zero-count subtrees and collapses consistent ones, exactly the dead conjuncts a reader wants).Incremental.
tlc2.basis.Incrementalparses the edited spec into a new Tool and gives every action, invariant, initial predicate and constraint a signature: its text, every user definition it reaches transitively, and its context bindings (thepof an action split from\E p \in S). Actions pair by name and signature, invariants by name. It then replays the store: survivors keep their edges under unchanged actions and are re-expanded under changed and added actions only, new states under every action; a sweep then evaluates every invariant on every stored state. It answersrestart_requiredwhen the variables, init, a constraint, the view, the symmetry set or the config changed, or when the old exploration did not finish (budget, first violation, error, anything left queued), since a copied edge is sound only in a fully explored graph under the same constraints. A secondModelCheckerin one JVM trips over TLC's per-process bookkeeping. A paused checker is left parked through a refresh, and TLC's static variable tables are rebound to the old spec when the new tool is not adopted.Outside
tlc2.basis:IStateWriter.writeUnsatisfied(state, action, successor, pred, context)(default keeps the old behaviour);Toolreports a false guard on the general next-state path and on user-defined-operator guards, not only when every primed variable was already assigned;ModelChecker.getWorkers().Verified by hand and through the MCP tests on a two-action counter spec (typed traces, continuation verdicts, 18 states and 27 edges stored, guards tallied, screens, evaluation, coverage, four incremental refreshes in a row, a restart). Stacked on #1.
🤖 Generated with Claude Code