recife (TLA+/TLC) model-check adapter.
Stratified: pure promoters (trace->status, the violation rule-chain) ->
pure pipeline (normalize a raw recife result into a ModelCheckResult) ->
effectful boundary (check!, which runs a model through an INJECTED effect fn;
the default lazily resolves recife via requiring-resolve so this ns loads on
any classpath).
normalize maps recife's :trace discriminator to a status:
:trace :ok -> {:status :ok}
:trace [[idx state] ...] -> {:status :fail :details {:counterexample ...}}
:trace :error / other -> {:status :skip} (indeterminate; never :ok)
recife (TLA+/TLC) model-check adapter.
Stratified: pure promoters (trace->status, the violation rule-chain) ->
pure pipeline (normalize a raw recife result into a ModelCheckResult) ->
effectful boundary (`check!`, which runs a model through an INJECTED effect fn;
the default lazily resolves recife via requiring-resolve so this ns loads on
any classpath).
`normalize` maps recife's `:trace` discriminator to a status:
:trace :ok -> {:status :ok}
:trace [[idx state] ...] -> {:status :fail :details {:counterexample ...}}
:trace :error / other -> {:status :skip} (indeterminate; never :ok)(build-counterexample {:keys [trace trace-info]})Build a CounterexampleTrace from a recife result whose :trace is a counterexample vector of [idx state] pairs (index dropped, as recife.helpers/get-trace does).
Build a CounterexampleTrace from a recife result whose :trace is a counterexample vector of [idx state] pairs (index dropped, as recife.helpers/get-trace does).
(check! model-spec)(check! model-spec run-fn)Model-check model-spec, returning a normalized ModelCheckResult. The effect
is INJECTED: run-fn maps a ModelSpec to a raw recife result (default:
default-runner). recife-absent, nil, or a non-map result all normalize to
{:status :skip} — a skip is NEVER a pass.
Model-check `model-spec`, returning a normalized ModelCheckResult. The effect
is INJECTED: `run-fn` maps a ModelSpec to a raw recife result (default:
`default-runner`). `recife-absent`, nil, or a non-map result all normalize to
{:status :skip} — a skip is NEVER a pass.(classify-violation trace-info)(classify-violation trace-info rules)Classify a recife trace-info map as a :safety or :liveness refutation by folding the ordered rule-chain (first match wins). OCP: add a rule, not a branch. Total on the default chain (the terminal rule matches everything).
Classify a recife trace-info map as a :safety or :liveness refutation by folding the ordered rule-chain (first match wins). OCP: add a rule, not a branch. Total on the default chain (the terminal rule matches everything).
Ordered violation rules; first match wins. A temporal (liveness) refutation surfaces as a :back-to-state or :stuttering violation; a bare finite counterexample with no such marker is a safety (invariant) violation.
Ordered violation rules; first match wins. A temporal (liveness) refutation surfaces as a :back-to-state or :stuttering violation; a bare finite counterexample with no such marker is a safety (invariant) violation.
(default-runner {:keys [init-state components]})Effect fn: run model-spec through recife, returning the raw result map, or
recife-absent when recife is unresolvable. In run-local mode (recife's
default) run-model returns the result MAP directly; only the async subprocess
path returns a derefable — deref that, else use the map as-is.
Effect fn: run `model-spec` through recife, returning the raw result map, or `recife-absent` when recife is unresolvable. In run-local mode (recife's default) run-model returns the result MAP directly; only the async subprocess path returns a derefable — deref that, else use the map as-is.
A rule classifying a recife trace-info map as a safety/liveness refutation.
A rule classifying a recife trace-info map as a safety/liveness refutation.
(-match? rule trace-info)True iff this rule handles trace-info.
True iff this rule handles `trace-info`.
(-violation-class rule)The violation-type keyword this rule assigns.
The violation-type keyword this rule assigns.
(normalize raw)Normalize a raw recife get-result value into a ModelCheckResult. Total:
any value (incl. nil / a non-map) yields a {:status :details} map.
Normalize a raw recife `get-result` value into a ModelCheckResult. Total:
any value (incl. nil / a non-map) yields a {:status :details} map.Sentinel a runner returns when recife/TLC is not on the classpath.
Sentinel a runner returns when recife/TLC is not on the classpath.
(recife-trace->status trace)Map a recife result's :trace value to a normalized status. A non-empty vector is a counterexample (:fail); :ok is clean; anything else (:error, nil, empty) is indeterminate (:skip).
Map a recife result's :trace value to a normalized status. A non-empty vector is a counterexample (:fail); :ok is clean; anything else (:error, nil, empty) is indeterminate (:skip).
(rule match-fn klass)A violation rule from a predicate on trace-info and a violation-type.
A violation rule from a predicate on trace-info and a violation-type.
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 |