Run the Quint CLI and collect the ITF files it writes. The only namespace that shells out.
Run the Quint CLI and collect the ITF files it writes. The only namespace that shells out.
(run! {:keys [spec] :as opts})Generate traces with quint run --mbt.
Takes the driver map's Quint keys: :spec (required), :main,
:init-action, :step-action, :seed, :traces, :max-steps and
:max-samples. A missing :seed is generated so a failure is reproducible.
:max-samples is attempts and :traces is traces written; Quint requires
the former to be at least the latter, so :traces acts as its floor.
Runs in a temporary directory, reads the ITF files back, and deletes the directory before returning
{:seed 42 :dir "/path/to/spec" :cmd ["quint" ...] :traces [{:name "run_0.itf.json" :json "..."}]}
:cmd is the reproduce line, not the literal argv: the scratch --out-itf
path is rewritten to a relative one, since the directory is already gone.
Throws ex-info with :quint/error :quint-not-found, :quint-failed
(carrying Quint's own stderr verbatim) or :no-traces.
Generate traces with `quint run --mbt`.
Takes the driver map's Quint keys: `:spec` (required), `:main`,
`:init-action`, `:step-action`, `:seed`, `:traces`, `:max-steps` and
`:max-samples`. A missing `:seed` is generated so a failure is reproducible.
`:max-samples` is attempts and `:traces` is traces written; Quint requires
the former to be at least the latter, so `:traces` acts as its floor.
Runs in a temporary directory, reads the ITF files back, and deletes the
directory before returning
{:seed 42 :dir "/path/to/spec" :cmd ["quint" ...]
:traces [{:name "run_0.itf.json" :json "..."}]}
`:cmd` is the reproduce line, not the literal argv: the scratch `--out-itf`
path is rewritten to a relative one, since the directory is already gone.
Throws `ex-info` with `:quint/error` `:quint-not-found`, `:quint-failed`
(carrying Quint's own stderr verbatim) or `:no-traces`.(test! {:keys [spec test] :as opts})Run one scripted Quint run through quint test and read its trace back.
Takes :spec and :test (both required), plus the optional :main,
:seed and :max-samples. :test is the name of a run in the spec and is
matched exactly. Returns the same shape as run!
{:seed 42 :dir "/path/to/spec" :cmd ["quint" ...] :traces [{:name "test_depositTest_0.itf.json" :json "..."}]}
Note that quint test emits no mbt:: variables at all, so the trace can
only drive an implementation if the spec records the action itself and the
driver says where with :action-path — see itf/itf->trace.
Throws ex-info with :quint/error :quint-not-found, :test-failed when
the spec's own .expect did not hold (a problem in the spec, not in the
implementation), :quint-failed for anything else non-zero, and :no-traces
when the name matched nothing — which Quint reports by exiting 0 and writing
no file.
Run one scripted Quint `run` through `quint test` and read its trace back.
Takes `:spec` and `:test` (both required), plus the optional `:main`,
`:seed` and `:max-samples`. `:test` is the name of a `run` in the spec and is
matched exactly. Returns the same shape as `run!`
{:seed 42 :dir "/path/to/spec" :cmd ["quint" ...]
:traces [{:name "test_depositTest_0.itf.json" :json "..."}]}
Note that `quint test` emits no `mbt::` variables at all, so the trace can
only drive an implementation if the spec records the action itself and the
driver says where with `:action-path` — see `itf/itf->trace`.
Throws `ex-info` with `:quint/error` `:quint-not-found`, `:test-failed` when
the spec's own `.expect` did not hold (a problem in the spec, not in the
implementation), `:quint-failed` for anything else non-zero, and `:no-traces`
when the name matched nothing — which Quint reports by exiting 0 and writing
no file.The Quint the fixtures were recorded from and the behaviour in docs/notes/itf-format.md was verified against.
The Quint the fixtures were recorded from and the behaviour in docs/notes/itf-format.md was verified against.
(version)The version of the quint on PATH, as a string. Throws ex-info with
:quint/error :quint-not-found if it is not there, :quint-failed if it
will not report a version.
The version of the `quint` on PATH, as a string. Throws `ex-info` with `:quint/error` `:quint-not-found` if it is not there, `:quint-failed` if it will not report a version.
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 |