The public API: build a driver, then check an implementation against a spec.
The public API: build a driver, then check an implementation against a spec.
(check driver opts)Generate traces with Quint and replay every one against the implementation.
Takes a resolved driver and an options map merged over it — :traces,
:max-steps, :max-samples, :seed. Returns
{:ok? false :seed 42 :traces 50 :steps 231 :cmd ["quint" ...] :coverage {:used {...} :unused #{...}} :failure {... :trace 7 :trace-name "run_7.itf.json" :trace-json "..."}}
Stops at the first trace that diverges. The failing trace's JSON is carried in the result rather than a path, because the temporary directory Quint wrote it to is deleted before returning.
Throws whatever quint/run! and replay/run-trace throw: generation and
setup problems are exceptions, divergence is this map.
Generate traces with Quint and replay every one against the implementation.
Takes a resolved driver and an options map merged over it — `:traces`,
`:max-steps`, `:max-samples`, `:seed`. Returns
{:ok? false :seed 42 :traces 50 :steps 231 :cmd ["quint" ...]
:coverage {:used {...} :unused #{...}}
:failure {... :trace 7 :trace-name "run_7.itf.json" :trace-json "..."}}
Stops at the first trace that diverges. The failing trace's JSON is carried
in the result rather than a path, because the temporary directory Quint wrote
it to is deleted before returning.
Throws whatever `quint/run!` and `replay/run-trace` throw: generation and
setup problems are exceptions, divergence is this map.(check-run driver opts)Replay one scripted Quint run against the implementation.
Takes a resolved driver and an options map merged over it; :test names a
run in the spec and is required. Returns what check returns, with
:traces 1.
quint test emits no mbt:: variables, so the spec must record the action
it took in an ordinary variable and the driver must say where with
:action-path — and :nondet-path too, for actions that take picks.
Without them the trace has no action to dispatch and replay throws
:unknown-action.
A scripted run is a scenario a human wrote down: use it for the case that
must keep working, and check for the cases nobody thought of.
Replay one scripted Quint `run` against the implementation. Takes a resolved driver and an options map merged over it; `:test` names a `run` in the spec and is required. Returns what `check` returns, with `:traces` 1. `quint test` emits no `mbt::` variables, so the spec must record the action it took in an ordinary variable and the driver must say where with `:action-path` — and `:nondet-path` too, for actions that take picks. Without them the trace has no action to dispatch and replay throws `:unknown-action`. A scripted run is a scenario a human wrote down: use it for the case that must keep working, and `check` for the cases nobody thought of.
(defdriver name m)(def name (driver m)), and nothing more.
`(def name (driver m))`, and nothing more.
(driver m)Resolve a driver map into the driver check and replay-file consume.
See registry/resolve-driver for the keys and the errors it throws.
Resolve a driver map into the driver `check` and `replay-file` consume. See `registry/resolve-driver` for the keys and the errors it throws.
(replay-file driver path)Replay one committed ITF file. Needs no Quint installed — this is what makes
a recorded failure a deterministic regression test. Returns a
replay/run-trace result.
Replay one committed ITF file. Needs no Quint installed — this is what makes a recorded failure a deterministic regression test. Returns a `replay/run-trace` result.
(verify driver opts)Check an invariant with Apalache, and replay the counterexample if there is one.
Takes a resolved driver and an options map merged over it; :invariant names
a val in the spec and is required. :max-steps bounds the search. Returns
what check returns, plus :invariant:
{:ok? false :traces 1 :steps 2 :cmd [...] :dir "..." :invariant {:name "underFifty" :holds? false :trace-name "verify.itf.json" :trace-json "..."} :coverage {...} :failure nil}
A violated invariant is :ok? false whether or not the implementation
agrees with the counterexample, because those are two different facts and
both are reported. :invariant says the spec's own property does not hold.
:failure says the implementation diverged from the counterexample, and is
nil when it did not — which means the implementation reproduces the spec's
bug faithfully. That is a real answer, not a pass, and it points at the spec.
A holding invariant returns :ok? true with :traces 0 and no trace to
replay, since quint verify writes no file in that case.
Counterexamples carry no mbt:: variables, so the driver needs the same
:action-path a scripted run needs; without it replay throws
:unknown-action.
Throws whatever quint/verify! and replay/run-trace throw.
Check an invariant with Apalache, and replay the counterexample if there is
one.
Takes a resolved driver and an options map merged over it; `:invariant` names
a `val` in the spec and is required. `:max-steps` bounds the search. Returns
what `check` returns, plus `:invariant`:
{:ok? false :traces 1 :steps 2 :cmd [...] :dir "..."
:invariant {:name "underFifty" :holds? false
:trace-name "verify.itf.json" :trace-json "..."}
:coverage {...}
:failure nil}
A violated invariant is `:ok? false` whether or not the implementation
agrees with the counterexample, because those are two different facts and
both are reported. `:invariant` says the spec's own property does not hold.
`:failure` says the implementation diverged from the counterexample, and is
nil when it did not — which means the implementation reproduces the spec's
bug faithfully. That is a real answer, not a pass, and it points at the spec.
A holding invariant returns `:ok? true` with `:traces` 0 and no trace to
replay, since `quint verify` writes no file in that case.
Counterexamples carry no `mbt::` variables, so the driver needs the same
`:action-path` a scripted run needs; without it replay throws
`:unknown-action`.
Throws whatever `quint/verify!` and `replay/run-trace` throw.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 |