The half of decoding that the driver steers: reading a decoded state through
:state-path, :action-path and :nondet-path.
Nothing here sees JSON. itf turns ITF into values and hands each decoded
state over; these functions decide where in it the action, the picks and the
state to compare are, and say so loudly when a path leads nowhere. A path is
about the spec's own variables, which is why it can be wrong in ways the ITF
never is.
The half of decoding that the driver steers: reading a decoded state through `:state-path`, `:action-path` and `:nondet-path`. Nothing here sees JSON. `itf` turns ITF into values and hands each decoded state over; these functions decide where in it the action, the picks and the state to compare are, and say so loudly when a path leads nowhere. A path is about the spec's own variables, which is why it can be wrong in ways the ITF never is.
(paths! opts)The decode paths in a driver's options, checked.
Takes the options map, of which it reads :state-path, :action-path and
:nondet-path. Returns a map of those that are set. Throws ex-info with
:quint/error :bad-decode-path for one that is not a vector.
The decode paths in a driver's options, checked. Takes the options map, of which it reads `:state-path`, `:action-path` and `:nondet-path`. Returns a map of those that are set. Throws `ex-info` with `:quint/error` `:bad-decode-path` for one that is not a vector.
(tracked st {:keys [state-path action-path nondet-path]})One decoded state, read through the driver's paths.
Takes the state as itf decodes it — {:index :action :picks :state} — and
the map paths! returns. Returns the same state with :action and :picks
taken from ordinary state variables, for traces that carry no mbt::
metadata — quint test and quint verify emit none, and a Choreo-style spec
tracks them itself. Each path's root variable leaves :state: it is the
spec's own bookkeeping, and the implementation must not be asked to supply
it.
:state-path goes first. The state becomes the record found there, and the
other two paths are read inside it, so their roots are its fields.
Throws ex-info with :quint/error :bad-decode-path when a path does not
lead to a record of state, an action name or a record of picks, or when the
paths' roots would leave nothing to compare.
One decoded state, read through the driver's paths.
Takes the state as `itf` decodes it — `{:index :action :picks :state}` — and
the map `paths!` returns. Returns the same state with `:action` and `:picks`
taken from ordinary state variables, for traces that carry no `mbt::`
metadata — `quint test` and `quint verify` emit none, and a Choreo-style spec
tracks them itself. Each path's root variable leaves `:state`: it is the
spec's own bookkeeping, and the implementation must not be asked to supply
it.
`:state-path` goes first. The state becomes the record found there, and the
other two paths are read inside it, so their roots are its fields.
Throws `ex-info` with `:quint/error` `:bad-decode-path` when a path does not
lead to a record of state, an action name or a record of picks, or when the
paths' roots would leave nothing to compare.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 |