Skills3History

quint-connect-ts-debugcore

Diagnose quint-connect test failures. StateMismatchError (state diverged at step N, has traceIndex, stepIndex, expected, actual), TraceReplayError (handler threw, has action, cause), NoTracesError (wrong --main module or unsatisfiable spec), QuintError (quint run exited non-zero), QuintNotFoundError (quint CLI not on PATH). Reproduce failures deterministically with seed. Inspect raw ITF traces via traceDir. Use when a quint-connect test fails and you need to understand why.

288 lines

quint-connect-ts-itf-decodingcore

Decode Quint ITF JSON encoding to native JS types for quint-connect drivers and state checks. ITFBigInt for {"#bigint":"N"} to bigint, ITFSet for {"#set":[...]} to Set, ITFMap for {"#map":[[k,v],...]} to Map, ITFTuple, ITFVariant, ItfOption for Quint Option (Some/None to T | undefined). Fully-qualified state variable names ("testmod::specmod::var"). Zod (@firfi/quint-connect/zod) and Effect Schema (@firfi/quint-connect/effect) variants. transformITFValue. Structural deep comparison for Maps and Sets. Use when writing ITF decoders, debugging decode errors, or comparing complex state.

294 lines

quint-connect-ts-setupcore

Scaffold a quint-connect model-based test from a Quint spec. Covers defineDriver (typed mode with per-field picks, raw mode with step callback), run/quintRun, stateCheck, RunOptions (spec, nTraces, maxSteps, seed, backend), simple API (@firfi/quint-connect, Standard Schema) vs Effect API (@firfi/quint-connect/effect, Effect Schema), vitest helpers (quintTest, quintIt), Config (statePath, nondetPath), pickFrom. Use when setting up a new quint-connect test, wiring a driver, choosing an API surface, or adding state checking.

365 lines