Clojure on the JVM only. See decisions/0005-clojure-only.md.
The system under test is a running application, not a value being threaded through a fold. quint-connect does three things to it, in a loop:
start it -> act on it -> read it and compare
(:quint/init) (an annotated fn) (annotated state readers)
The application never learns that Quint exists. It gains metadata keys, which are inert data, and nothing else: no context parameter, no return-value convention, no require, no protocol to satisfy. Everything quint-connect needs to observe is declared — on the atom, on the ref, or on a getter function, and that getter may live in the test namespace when the application has no such function of its own.
Everything else — the Quint CLI, ITF decoding, metadata scanning,
clojure.test integration, reporting — is plumbing around that loop.
Namespaces are shown by their last segment; all live under
org.clojars.aldebogdanov.quint-connect.*.
spec.qnt
| quint (shell out: quint run --mbt / quint test / quint verify)
v
*.itf.json ─────────────────────┐ (may be cached in test-resources/)
| itf (decode) │
v │
trace data (plain EDN) │
| │
| replay <── resolved driver <── registry (scan :quint/* metadata)
v ^
result data (plain EDN) |
| report driver map (overrides, complex cases)
v
human-readable failure
Two phases, deliberately split:
quint binary and a subprocess.See decisions/0003-two-phase.md.
All under org.clojars.aldebogdanov.quint-connect, matching the Clojars group
and artifact (org.clojars.aldebogdanov/quint-connect).
| namespace | kind | responsibility |
|---|---|---|
…quint-connect.itf | pure | ITF JSON -> EDN. Decode #bigint/#map/#set/#tup, records, sum types. Normalize variable names, split out mbt:: metadata. |
…quint-connect.registry | reflective | Read :quint/* metadata from an explicit list of namespaces; produce driver data. The only namespace that reflects. |
…quint-connect.replay | engine | Run the loop: init, act, read, compare. No I/O of its own. |
…quint-connect.report | pure | Result data -> string. Diffs, step context, coverage, reproduce hints. |
…quint-connect.quint | impure | Build and run quint commands, collect the ITF files they emit. |
…quint-connect.core | glue | Public API: driver, defdriver, check, check-run, verify, replay-file. |
…quint-connect.test | glue | clojure.test integration, and the one place that writes a failing trace to disk. |
…quint-connect.cli | impure | -main for generating and caching traces outside a test run (M8). |
Eight namespaces, none of which application code ever loads. If one passes ~200 lines, that is a signal to stop and reconsider, not to split it reflexively.
Two have passed it. itf stands at 230 and quint at 264.
itf was accepted at 230 on the condition that M7b not grow it, and M7b did
not: Apalache's dialect decodes through it unchanged, and #unserializable
never appeared, so the namespace is untouched since M7a. That condition held
and is now discharged.
quint grew with verify! and is the one to watch. It is three commands
against one CLI, sharing the version check, the scratch directory and the
collection of ITF files, and the seam a split would follow — one namespace per
subcommand — would triplicate all three. The honest reading is that it is over
budget and that the fix is not obvious, so it is written down here instead of
being performed. If a fourth subcommand arrives, that is the moment to reopen
it rather than now.
There is deliberately no keys namespace. An earlier design had one, existing
only to be aliased so that :quint/action would resolve to a fully-qualified
key; 0007 removed it along with the
:require it forced on every annotated namespace.
See decisions/0002-metadata-wiring.md for
why, and notes/clojure-metadata.md for the exact
mechanics, all verified against Clojure 1.12.5 by
dev/probes/meta_probe.clj.
| metadata key | goes on | meaning |
|---|---|---|
{:quint/action "deposit"} | function var | handler for that spec action; called with the picks as arguments |
{:quint/args [:who :amount]} | function var | pick names in argument order; defaults to :arglists; required for multi-arity |
{:quint/state :balances} | function var / IDeref var | supplies the value of that spec variable |
{:quint/state {:var :lastError :path [:e]}} | function var / IDeref var | supplies it from a nested position |
{:quint/state :*} | function var / IDeref var | supplies a whole map of spec variables, merged |
{:quint/init true} | function var | start or reset the application; run once per trace, before step 0 |
{:quint/halt true} | function var | stop it; run after every trace, in a finally |
{:quint/driver :ledger} | any annotated var | scope it to the driver(s) named; absent means every driver |
Keys are qualified by quint and require nothing
(decisions/0007-annotation-keys.md):
(ns bank.core) ; no :require, no dependency
(defn deposit {:quint/action "deposit"} [who amount] ...)
That an annotated namespace pulls in nothing is the point: this library belongs
in a :test alias, and an annotation must never be able to drag it onto a
production classpath.
quint is a shared keyword namespace, so a driver can move all six keys at
once with :key-ns, a symbol — {:key-ns 'acme.mbt} reads :acme.mbt/action
and friends. One qualifier per driver, no per-key override. The registry is
parameterised on it in exactly one place.
The cost is that an annotation left under the old qualifier while :key-ns
points elsewhere is read by nobody and reported by nobody, unless the namespace
scans empty. That gap is accepted and its shape is written down in
0007 §"The gap this leaves".
(ns bank.core)
(defn deposit ; picks {who, amount}
{:quint/action "deposit"}
[who amount] ; bound by parameter name
(swap! accounts update who + amount))
(defn withdraw ; parameter names differ from pick names
{:quint/action "withdraw" :quint/args [:who :amount]}
[account n]
...)
The return value is ignored. State is never inferred from what a handler gives back; it is read afterwards, from the declared readers. That is what lets an ordinary application function be annotated as-is.
Every parameter is a pick name, including the ones the body ignores. [_who _amount] asks for picks called :_who and :_amount, which no spec emits, so
both arrive as nil. That is exactly right for a handler that ignores them —
and it is not a way to skip a pick the handler does need. Name the parameter
after the pick, or give the real order in :quint/args.
If the real function needs something that is not a pick — a connection, a system map, a component — write a one-line wrapper in the test namespace and annotate that. Nothing in the application changes.
(ns bank.core)
;; on the var holding a reference
(def ^{:quint/state :balances} accounts (atom {}))
;; or on the reference object itself
(def queue (atom [] :meta {:quint/state :pending}))
;; nested value
(def ^{:quint/state {:var :lastError :path [:err]}} status (ref {:err ""}))
(ns bank.model-test) ; readers may live here when the app has none
(defn balances-from-db ; a query, called with no arguments
{:quint/state :balances}
[]
(into {} (map (juxt :who :amount)) (jdbc/execute! ds ["select who, amount from accounts"])))
(defn everything ; one reader, several spec variables
{:quint/state :*}
[]
{:balances (balances-from-db) :lastError (last-error)})
Resolution by var value: IDeref (atom, ref, agent, delay, volatile) is
dereferenced; a function is called with no arguments; :path is applied with
get-in afterwards. Metadata is read from the var and from the reference
object, with the var winning on conflict.
Readers are called fresh for every comparison — once per step. There is no cached view of the system, because a cached view is a lie waiting to happen.
for each trace:
:quint/init once per trace start / reset the app
read state, compare to trace state 0
for each following state:
action handler with picks
read state, compare
:quint/halt in a finally
(ns bank.system
(:require [mount.core :as mount]))
(defn start {:quint/init true} [] (mount/start))
(defn stop {:quint/halt true} [] (mount/stop))
There is no per-check hook. A fixture that must start once for the whole run
— a container, a database — is clojure.test's own use-fixtures, or a let
around the call to check; both already exist and neither needs this library's
help. A :setup/:teardown pair in the driver map is an M8 candidate and
nothing more.
Two properties fall out of this shape:
init, so an incomplete reset — a leftover atom, an
unrolled-back transaction — fails at step 0 of trace 2 with a diff, instead of
corrupting trace 17 mysteriously.init runs per trace, so make it cheap. Fifty traces mean fifty starts.
A reset-db! annotated with :quint/init is usually the right
granularity; a full mount/start may not be.The trace's own first action (mbt::actionTaken = "init", or whatever --init
names) is dispatched to the :quint/init function. Annotating an
action handler {:quint/action "init"} also works and takes precedence;
:quint/init exists so that renaming the spec's initializer does not
touch application code.
(q/defdriver bank
{;; --- where the model comes from -------------------------------------
:spec "spec/bank.qnt"
:main "bankTest" ; optional --main module
:init-action "init" ; optional --init action name
:step-action "step" ; optional --step action name
;; --- where the annotations are ---------------------------------------
:scan '[bank.core bank.system bank.model-test] ; required'd, then read
:key-ns 'quint ; qualifier for all five keys
;; --- complex cases: merged over whatever :scan found, and winning -----
:actions {"transfer" (fn [{:keys [from to amount]}] ...)} ; picks map
:state {:pending (fn [] (queue-depth))} ; spec var -> 0-arg fn
:ignore #{:lastError}
:compare {:balances my-fn}
;; --- where the action metadata lives ----------------------------------
;; Unset, the decoder reads mbt::actionTaken and mbt::nondetPicks. Set,
;; they are get-in paths into ordinary spec variables, for the traces that
;; carry no mbt:: at all — `quint test` and `quint verify`. The variable
;; each path starts at leaves the compared state.
:action-path [:lastAction]
:nondet-path [:lastPick]
:key-fn (fn [full-name] ...)}) ; variable name -> keyword
Handlers written in :actions take the picks map, not positional arguments,
because a complex case usually wants to destructure it. Annotated functions take
positional arguments because that is what makes annotating an existing function
possible without touching it.
Resolution, in order: require each :scan namespace -> read ns-interns
metadata -> assemble actions, readers and lifecycle -> merge the driver map on
top -> validate. The merged result is the resolved driver, an ordinary map
of data and functions, and it is what replay consumes. Nothing
downstream of the registry knows that metadata exists.
(q/driver m) is a function returning the resolved driver; q/defdriver is
(def name (q/driver m)) and nothing more.
:empty-scan — a namespace in :scan yielded no annotations. Almost always
the ^{...} (defn ...) trap; the message says so.:duplicate-action, :duplicate-state — two vars claim the same name. A
driver-map :actions or :state entry replacing one of them does not
suppress this. The annotations are still ambiguous, and quietly picking a
winner is the failure this layer exists to prevent; the override says which
function to call, not which of two declarations was meant.:duplicate-init, :duplicate-halt — two vars claim the same lifecycle
role, in one namespace or across the :scan. First-one-wins is not an
option here: the loser would never run, and an init that never runs
reappears as a divergence in a later trace that has nothing to do with it.:ambiguous-arity — multi-arity var without :quint/args.:unnamed-driver — a var scoped with :quint/driver in a driver that has no
:name to match it against. See
0009.At replay time, because each of these needs the trace: :no-init (it starts
with an action nothing is annotated for), :unknown-action,
:anonymous-action, :state-read-failed, plus a coverage report of handlers
the traces never exercised.
A spec variable that no reader supplies is not caught at construction. The
driver never sees the spec, only the annotations, so the first trace is what
reveals it — as a step-0 diff of that variable against nothing. Turning it into
a :missing-state at construction would mean parsing the spec, which is a
non-goal (§10); doing it at the first comparison instead is open, and unbuilt.
{:source "bank.qnt"
:vars [:balances :lastError]
:states [{:index 0 :action "init" :picks {}
:state {:balances {"alice" 0} :lastError ""}}
{:index 1 :action "overdraft" :picks {:who "bob" :amount 85}
:state {:balances {"alice" 0} :lastError "insufficient funds"}}]}
{:ok? false
:seed "42"
:traces 50
:steps 231 ; states actually replayed
:coverage {:used {"deposit" 88 "withdraw" 40}
:unused #{"overdraft"}} ; handler declared, spec never emitted it
:cmd ["quint" "run" "bank.qnt" ...] ; the reproduce line
:dir "/path/to/spec" ; where to run it
:failure {:trace 7
:trace-name "run_7.itf.json"
:trace-json "{...}" ; carried, not a path: see below
:step 3
:action "withdraw"
:handler #'bank.core/withdraw ; the var, when it came from an annotation
:picks {:who "alice" :amount 20}
:expected {:balances {"alice" 30}}
:actual {:balances {"alice" 50}}
:readers {:balances #'bank.core/accounts}
:diff [{...} {...} {...}] ; clojure.data/diff
:cause nil ; ex-info if the handler threw
:saved "test-resources/quint-connect/failures/bank-seed42-trace7.itf.json"}}
The failing trace travels as JSON rather than as a filename because the
scratch directory Quint wrote it to is deleted before check returns.
:saved is where it landed afterwards — see §7.
Result data is the contract. report and test are
consumers of it, not producers of parallel truth. Carrying the handler and
reader vars is the payoff of the annotation design: a failure points at the
file and line of the function that diverged and at the one that observed it.
| mode | trace source | when to use |
|---|---|---|
check | quint run --mbt (N random traces) | the default: broad conformance testing |
check-run | quint test --match ^name$ | one scripted scenario from a Quint run (see caveat below) |
verify | quint verify --invariant I | prove the spec, then replay the counterexample if there is one |
replay-file | a committed .itf.json | regression tests, CI without Quint |
Caveat, verified against Quint 0.32.0: quint test does not accept --mbt
and its traces contain no mbt::actionTaken/mbt::nondetPicks. Same for
quint verify. Only quint run --mbt yields action metadata. So check-run
and verify require the spec to track the action itself in a normal variable,
which is what :action-path / :nondet-path are for — the reason those two
modes are a milestone rather than a flag. Documented in
notes/itf-format.md, and demonstrated by
dev/fixtures/tracked.qnt, which is the same bank as bank.qnt with two
bookkeeping variables added and therefore replays against the same unchanged
dev/bank/core.clj.
All four modes are implemented. verify runs in a scratch working directory
rather than the spec's own, because Apalache writes an _apalache-out/
directory of logs into wherever it is invoked; that is the one place the
two-phase split bends, and it is recorded in
notes/itf-format.md.
check and replay-file are the two ends of one workflow, and the file
between them is the whole point of generating traces at random: a trace that
found a bug once must be able to find it again on a machine with no Quint.
qt/check divergence -> save-failure! -> test-resources/quint-connect/failures/
| mv, by a human
v
qt/replay-file test-resources/quint-connect/<spec>-seed<n>-trace<i>.itf.json
Two properties make this a workflow rather than a pile of files:
failures/ is gitignored and written
to on every divergence; promotion into test-resources/quint-connect/ is a
mv a human performs. A failing test never dirties the repository, and a
committed trace is always one someone chose to keep.Writing the file is the only reason test touches
the filesystem, and it is why the step lives there rather than in core:
q/check stays a function of data returning data.
JVM only, and the design spends that freely rather than pretending otherwise:
ns-interns + meta for the registry — reflection over vars, nothing deeper.clojure.java.process/exec (Clojure 1.12, no dependency) for running quint.clojure.data.json for parsing, behind one function in itf.clojure.data/diff for diffing.java.nio.file.Files/createTempDirectory for trace scratch space..clj. No reader conditionals anywhere.long when they fit and clojure.lang.BigInt otherwise.
See the large-integer trap in notes/itf-format.md —
a Quint bug, with its own fixture in M1.Every failure mode is an ex-info with :quint/error set to a keyword,
never a bare string or a bare assert:
(ex-info "quint exited 1" {:quint/error :quint-failed :cmd [...] :stderr "..."})
The keywords:
:quint-not-found :quint-failed :no-traces :test-failed :bad-itf
:bad-decode-path :name-collision :empty-scan :duplicate-action
:duplicate-state :duplicate-init :duplicate-halt :ambiguous-arity
:unnamed-driver :no-init :unknown-action :anonymous-action
:state-read-failed :save-failed
That list is the whole set, and it is checked against the source rather than
maintained by hand: grep -rho '(fail :[a-z-]*' src/ plus the two passed to
registry/no-duplicates!.
A state mismatch is not an exception — it is a value in the result map. Exceptions are for broken setups; divergence is the expected output of a testing tool.
:int in an
annotation would be a second, unchecked source of truth.:actions.| risk | mitigation |
|---|---|
^{...} (defn ...) silently loses metadata | :empty-scan error naming the trap; documented in three places |
an annotation stranded under the wrong :key-ns | none — caught only if the namespace scans empty; accepted in 0007 |
two scanned namespaces both annotating :quint/init | :duplicate-init / :duplicate-halt at construction, naming both vars |
| a spec variable no reader supplies | diverges against nothing on the first state carrying it; there is no :missing-state — see §5 |
an init that does not fully reset leaks between traces | state 0 is compared right after init; a leak fails immediately |
init per trace is expensive for a full system start | documented; prefer a cheap reset function over mount/start |
| ghost vars surviving a REPL reload | registry rebuilt per run; unused-handler coverage report |
forgotten require hiding a handler | :scan is explicit and required'd; no classpath-wide scan |
| annotations drifting from the spec's action names | :unknown-action plus the coverage report on every run |
reading state has side effects (a query, a delay) | readers are called once per step; document that they must be cheap and idempotent |
--mbt is experimental and may change | pin the tested version, assert quint --version, fixtures |
anonymous actions (any { all {a, b} }) produce "" | fail loudly with the rewrite instruction, as quint-connect does |
module-prefixed var names (bankTest::bank::balances) | strip to the last segment, error on collision, :key-fn escape |
| Quint mis-encodes integers >= 10^15 on its default backend | decode the broken form too; fixtures for both backends |
Can you improve this documentation?Edit on GitHub
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |