A Layer 3 conformance failure: the implementation took a step its specification does not permit, or reached an abstract state the specification forbids.
kind is the finding, and the message is the layer's primary output:
kind | Meaning |
|---|---|
:not_enabled | the action's guard was false on the pre-state — the implementation did what the spec forbids there |
:diverged | the guard held, but no binding of the action's params reproduces the implementation's post-state |
:unmapped_but_moved | no action was claimed, yet the abstract state changed |
:invariant | the abstract post-state violates one of the spec's invariants |
:action_property | the abstract transition violates one of the spec's action properties |
:diverged is the common one, and it is more often the refinement mapping that is
wrong than the implementation. That is still a finding worth having: a mapping that does
not track the implementation invalidates every other check in the layer.
Summary
Types
@type t() :: %ExTLA.GenServer.Violation{ __exception__: term(), action: atom() | nil, detail: String.t() | nil, diff: [{atom(), term(), term()}] | nil, kind: :not_enabled | :diverged | :unmapped_but_moved | :invariant | :action_property, name: atom() | nil, params: map() | nil, post: ExTLA.State.t() | nil, pre: ExTLA.State.t() | nil, spec: module() }