Decode Quint's ITF trace files into EDN. Pure: no file or process I/O. What Quint emits, and why parts of it are odd, is in docs/notes/itf-format.md.
Decode Quint's ITF trace files into EDN. Pure: no file or process I/O. What Quint emits, and why parts of it are odd, is in docs/notes/itf-format.md.
(itf->trace itf)(itf->trace itf opts)Decode a parsed ITF map into a trace.
Takes the map from json->itf and optionally
:key-fn full variable name -> keyword; defaults to the last ::
segment and never sees mbt:: names
:action-path path to a variable holding the action name, for traces
with no mbt::actionTaken
:nondet-path path to a variable holding the picks, likewise
Names keep Quint's camelCase. Returns
{:source "bank.qnt" :vars [:balances :lastError] :states [{:index 0 :action "init" :picks {} :state {...}} ...]}
:vars comes from the state keys, not the file's vars array, which Quint
emits with duplicate mbt:: entries. Traces without mbt:: variables and
without the two paths decode with :action nil and :picks empty.
The paths are vectors for get-in, applied to the decoded state, and the
variable each one starts at is not part of :state: the spec's own
bookkeeping is not state the implementation has to supply. They take
precedence over mbt:: variables when a trace happens to carry both.
Throws ex-info with :quint/error :bad-itf for a malformed file or an
unsupported encoding, :name-collision when two variables normalize alike,
:bad-decode-path when a path is not a vector or does not lead to an action
name or a record of picks.
Decode a parsed ITF map into a trace.
Takes the map from `json->itf` and optionally
:key-fn full variable name -> keyword; defaults to the last `::`
segment and never sees `mbt::` names
:action-path path to a variable holding the action name, for traces
with no `mbt::actionTaken`
:nondet-path path to a variable holding the picks, likewise
Names keep Quint's camelCase. Returns
{:source "bank.qnt"
:vars [:balances :lastError]
:states [{:index 0 :action "init" :picks {} :state {...}} ...]}
`:vars` comes from the state keys, not the file's `vars` array, which Quint
emits with duplicate `mbt::` entries. Traces without `mbt::` variables and
without the two paths decode with `:action` nil and `:picks` empty.
The paths are vectors for `get-in`, applied to the decoded state, and the
variable each one starts at is not part of `:state`: the spec's own
bookkeeping is not state the implementation has to supply. They take
precedence over `mbt::` variables when a trace happens to carry both.
Throws `ex-info` with `:quint/error` `:bad-itf` for a malformed file or an
unsupported encoding, `:name-collision` when two variables normalize alike,
`:bad-decode-path` when a path is not a vector or does not lead to an action
name or a record of picks.(json->itf s)Parse ITF file contents. Takes the JSON as a string, returns the raw ITF map
with string keys and undecoded values. Throws ex-info with :quint/error
:bad-itf if it is not a JSON object.
Parse ITF file contents. Takes the JSON as a string, returns the raw ITF map with string keys and undecoded values. Throws `ex-info` with `:quint/error` `:bad-itf` if it is not a JSON object.
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 |