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
:state-path path to a record holding all of the state, as Choreo's s
does; its fields are then the variables
: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 decoded states, not the file's vars array, which
Quint emits with duplicate mbt:: entries. Traces without mbt:: variables
and without the paths decode with :action nil and :picks empty.
The three paths are read by itf.paths/tracked, which says what each does:
:state-path narrows the state to a record, the other two are read inside it
and take precedence over mbt:: variables, and the variable each of those
two starts at leaves :state.
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, 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.
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
:state-path path to a record holding all of the state, as Choreo's `s`
does; its fields are then the variables
: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 decoded states, not the file's `vars` array, which
Quint emits with duplicate `mbt::` entries. Traces without `mbt::` variables
and without the paths decode with `:action` nil and `:picks` empty.
The three paths are read by `itf.paths/tracked`, which says what each does:
`:state-path` narrows the state to a record, the other two are read inside it
and take precedence over `mbt::` variables, and the variable each of those
two starts at leaves `:state`.
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, 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.(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 |