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.
(verify! {:keys [spec invariant] :as opts})Check an invariant with quint verify, which runs Apalache.
Takes :spec and :invariant (both required), plus the optional :main,
:init-action, :step-action and :max-steps. Returns
{:holds? true :cmd ["quint" ...] :dir "/path/to/spec" :traces []} {:holds? false :cmd ["quint" ...] :dir "/path/to/spec" :traces [{:name "verify.itf.json" :json "..."}]}
The outcome is not in the exit code. Holding exits 0; a counterexample, an
unknown invariant name, a spec that does not typecheck and a missing file all
exit 1. What separates them is whether a trace was written, which is what
this branches on — recorded in docs/notes/itf-format.md §quint verify and
reproducible with dev/probes/verify_probe.sh.
An invariant that holds writes no trace, so an empty result is the pass here
and not the :no-traces error that run! and test! raise.
Runs in a scratch directory rather than the spec's own, because Apalache
writes _apalache-out/ into the working directory; those logs are deleted
with the scratch directory. Apalache is downloaded on first use and a run can
take minutes.
Throws ex-info with :quint/error :quint-not-found, or :quint-failed
when quint exited non-zero without writing a counterexample — carrying
Quint's own stderr, which is where the reason is.
Check an invariant with `quint verify`, which runs Apalache.
Takes `:spec` and `:invariant` (both required), plus the optional `:main`,
`:init-action`, `:step-action` and `:max-steps`. Returns
{:holds? true :cmd ["quint" ...] :dir "/path/to/spec" :traces []}
{:holds? false :cmd ["quint" ...] :dir "/path/to/spec"
:traces [{:name "verify.itf.json" :json "..."}]}
The outcome is not in the exit code. Holding exits 0; a counterexample, an
unknown invariant name, a spec that does not typecheck and a missing file all
exit 1. What separates them is whether a trace was written, which is what
this branches on — recorded in docs/notes/itf-format.md §`quint verify` and
reproducible with dev/probes/verify_probe.sh.
An invariant that holds writes no trace, so an empty result is the pass here
and not the `:no-traces` error that `run!` and `test!` raise.
Runs in a scratch directory rather than the spec's own, because Apalache
writes `_apalache-out/` into the working directory; those logs are deleted
with the scratch directory. Apalache is downloaded on first use and a run can
take minutes.
Throws `ex-info` with `:quint/error` `:quint-not-found`, or `:quint-failed`
when quint exited non-zero without writing a counterexample — carrying
Quint's own stderr, which is where the reason is.(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 |