Malli value objects for the recife (TLA+/TLC) model-check adapter, registered into the hive-spi schema registry.
Registered keys (contributed to the schema registry):
:hive.recife/model-spec a ModelSpec descriptor
:hive.recife/raw-result a permissive model of recife get-result output
:hive.recife/counterexample a normalized violation trace
:hive.recife/result a normalized ModelCheckResult
ModelCheckResult contract: [:map {:closed true} [:status #{:ok :fail :skip}] [:details :map]]. :ok = no violation; :fail = a counterexample exists (in :details under :counterexample); :skip = indeterminate (recife/TLC absent, no spec, or a TLC error) — never conflate :skip with :ok.
Malli value objects for the recife (TLA+/TLC) model-check adapter, registered
into the hive-spi schema registry.
Registered keys (contributed to the schema registry):
:hive.recife/model-spec a ModelSpec descriptor
:hive.recife/raw-result a permissive model of recife `get-result` output
:hive.recife/counterexample a normalized violation trace
:hive.recife/result a normalized ModelCheckResult
ModelCheckResult contract: [:map {:closed true} [:status #{:ok :fail :skip}]
[:details :map]]. :ok = no violation; :fail = a counterexample exists (in
:details under :counterexample); :skip = indeterminate (recife/TLC absent, no
spec, or a TLC error) — never conflate :skip with :ok.A normalized violation trace: the classified violation kind, the trace length (>= 1 — a counterexample always has an initial state), and the sequence of global-state maps (the recife [idx state] pairs with the index dropped).
A normalized violation trace: the classified violation kind, the trace length (>= 1 — a counterexample always has an initial state), and the sequence of global-state maps (the recife [idx state] pairs with the index dropped).
The single normalized output of the adapter.
The single normalized output of the adapter.
Descriptor of a recife model: the init global-state, the opaque recife components (procs/invariants/properties), and the DECLARED names of the safety invariants + liveness properties the spec carries.
Descriptor of a recife model: the init global-state, the opaque recife components (procs/invariants/properties), and the DECLARED names of the safety invariants + liveness properties the spec carries.
Permissive model of what recife get-result returns. The :trace key is the
status discriminator: :ok (clean) | :error (TLC error) | a vector of
[idx state] pairs (a counterexample). Modeled for GENERATION of the adapter
input; open so real recife maps (with :seed/:fp/:simulation/... ) also match.
Permissive model of what recife `get-result` returns. The :trace key is the status discriminator: :ok (clean) | :error (TLC error) | a vector of [idx state] pairs (a counterexample). Modeled for GENERATION of the adapter input; open so real recife maps (with :seed/:fp/:simulation/... ) also match.
The schema keys this ns contributes to the hive-spi registry.
The schema keys this ns contributes to the hive-spi registry.
The two TLC property classes a counterexample can refute.
The two TLC property classes a counterexample can refute.
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 |