org.clojars.aldebogdanov.quint-connect.quint — org.clojars.aldebogdanov/quint-connect 0.7.0

Run the Quint CLI and collect the ITF files it writes. The only namespace that shells out.

minimum-version clj

The oldest Quint whose --mbt traces can be trusted. Before 0.33.0 the rust evaluator could write a dead-ended sample's action and picks onto state 0 of the next trace (Quint #2012), and replay dispatches state 0 by that label. See docs/decisions/0014-quint-floor.md.

run! clj

(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, :max-samples and :backend. 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! clj

(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, :max-samples and :backend. :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.

tested-version clj

The Quint the fixtures were recorded from and the behaviour in docs/notes/itf-format.md was verified against.

verify! clj

(verify! {:keys [spec invariant temporal backend] :as opts})

Check an invariant or a temporal property with quint verify, which runs Apalache, or TLC.

Takes :spec and one of :invariant or :temporal — the name of a val, or of a temporal definition such as an action property — plus the optional :main, :init-action, :step-action, :max-steps and :backend, which selects the model checker here (:apalache or :tlc), not the evaluator. 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.

With :backend :tlc, a violated property writes no trace either: Quint writes --out-itf only from Apalache. So under TLC that outcome is also :quint-failed, with a message that says so and quotes Quint's first line — there is no counterexample to replay, and the verdict is in that line. TLC also ignores :max-steps and explores every reachable state, so a spec whose state space has no end never finishes under it.

:temporal needs :backend :tlc. Under Apalache, Quint first asks on stdin whether to go ahead, its temporal support being experimental; left open it waits for ever, and closed it exits 0 having checked nothing — a pass. And it cannot be combined with :invariant: Quint gives one verdict for the two, which could not say which was violated. Both recorded with dev/probes/temporal_probe.sh.

Throws ex-info with :quint/error :bad-options for either misuse above, before Quint runs; :quint-not-found; or :quint-failed when there is nothing to check, or quint exited non-zero without writing a counterexample — carrying Quint's own stderr, which is where the reason is.

version clj

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