Turn :quint/* metadata into the resolved driver replay consumes. The only
namespace that reflects, and only over the explicit :scan list. Rebuilt on
every call: no global registry, nothing cached between runs.
Turn `:quint/*` metadata into the resolved driver replay consumes. The only namespace that reflects, and only over the explicit `:scan` list. Rebuilt on every call: no global registry, nothing cached between runs.
(resolve-driver {:keys [scan key-ns actions state]
driver-name :name
:or {key-ns (quote quint)}
:as m})Build the resolved driver from a driver map.
Reads :scan (a vector of namespace symbols, required'd then reflected over)
under the qualifier in :key-ns, a symbol defaulting to quint. Explicit
:actions and :state in the map are merged on top and win.
:name names this driver, and only matters when a scanned namespace serves
more than one: a var annotated :quint/driver :ledger is read by the driver
named :ledger and ignored by the others, while an unannotated var is read
by all of them. A scoped annotation with no :name to match is
:unnamed-driver.
Returns the map replay/run-trace consumes — :actions, :readers,
:init, :halt, :ignore, :compare — with the remaining keys of the
driver map (:spec, :main, :init-action, :step-action, :action-path,
:nondet-path, :key-fn, …) passed through untouched for the caller.
Throws ex-info with :quint/error :empty-scan, :unnamed-driver,
:duplicate-action, :duplicate-state, :duplicate-init,
:duplicate-halt or :ambiguous-arity.
Build the resolved driver from a driver map. Reads `:scan` (a vector of namespace symbols, required'd then reflected over) under the qualifier in `:key-ns`, a symbol defaulting to `quint`. Explicit `:actions` and `:state` in the map are merged on top and win. `:name` names this driver, and only matters when a scanned namespace serves more than one: a var annotated `:quint/driver :ledger` is read by the driver named `:ledger` and ignored by the others, while an unannotated var is read by all of them. A scoped annotation with no `:name` to match is `:unnamed-driver`. Returns the map `replay/run-trace` consumes — `:actions`, `:readers`, `:init`, `:halt`, `:ignore`, `:compare` — with the remaining keys of the driver map (`:spec`, `:main`, `:init-action`, `:step-action`, `:action-path`, `:nondet-path`, `:key-fn`, …) passed through untouched for the caller. Throws `ex-info` with `:quint/error` `:empty-scan`, `:unnamed-driver`, `:duplicate-action`, `:duplicate-state`, `:duplicate-init`, `:duplicate-halt` or `:ambiguous-arity`.
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 |