Sending a message to an instrumented server and getting the outcome as a value.
A conformance violation raises inside the server, which reaches a caller as an exit —
and GenServer.call/3 re-raises it. ExTLA.Replay and ExTLA.Simulation both report what
happened rather than propagate it, so they send the :"$gen_call" themselves, tagged
with a monitor reference, and read the reply or the :DOWN out of the mailbox. Both
outcomes are then ordinary messages.
Not a public API: it exists so that the two callers share one definition of "the server answered, refused, or died of a conformance finding".
Summary
Functions
Call server — any GenServer.server(): a pid, a registered name, {name, node},
{:global, _} or {:via, _, _} — with message, reporting the outcome instead of
raising it.
Deliver whatever ExTLA.Refinement.concrete_message/2 returned, by the route it names.
Types
@type outcome() :: {:ok, term()} | {:violation, ExTLA.GenServer.Violation.t()} | {:stopped, term()} | {:timeout, timeout()}
Functions
Call server — any GenServer.server(): a pid, a registered name, {name, node},
{:global, _} or {:via, _, _} — with message, reporting the outcome instead of
raising it.
Every shape is the pid path. The server is resolved once with GenServer.whereis/1
and the monitor and the send both take the pid; a name that resolves to nothing is
{:stopped, :noproc} with nothing sent. So every shape behaves the same: a violation
raised under a registered name is reported as a violation (the :DOWN is matched on the
monitor reference alone, not on the name), and a server that has just died is
{:stopped, :noproc} rather than an invalid destination raise from send/2. A process
that dies between the lookup and the send is the dead-pid case: a no-op send and a
:noproc :DOWN.
Deliver whatever ExTLA.Refinement.concrete_message/2 returned, by the route it names.
{:call, msg} {:"$gen_call", from, msg} handle_call/3
{:cast, msg} {:"$gen_cast", msg} handle_cast/2
{:info, msg} msg handle_info/2
msg a callA term is a message and a message does not carry how it arrives, so the mapping has to
say. A bare term means a call. A mapping whose actions are handled by handle_cast/2 or
handle_info/2 clauses must name that route: delivered as a call, the message would reach
handle_call/3, find no matching clause, and a correct server would be reported as not
following the trace.
When a cast is done
A call hands back "answered, refused, or died" as a value. A cast has no reply, and a driver that moved on before it was handled would compare the next action against a stale state.
The completion signal is a :get_state system message sent straight after. It goes
through the same mailbox, so it is ordered behind the cast: when its reply arrives, the
cast has been handled. Measured rather than assumed — a cast incrementing a counter,
followed by this, replies {:ok, %{n: 1}}.
It is sent raw rather than through :sys.get_state/2 because that function exits the
caller on a timeout or a dead server, and turning an exit back into a value needs a
try/rescue. This whole module exists to avoid exactly that: it sends the $gen_call by
hand and reads the monitor, so all four outcomes are ordinary messages. The cast path is
the same shape, which is why it costs one receive and no extra process.
No extra round-trip in either caller: ExTLA.Replay and ExTLA.Simulation each already read
the server's state once per step, to map the post-state through abstract/1.