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.
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 |