Petrex.Runner (petrex v1.0.0)

Copy Markdown View Source

Runs one net instance in a GenServer.

The runner holds a token marking and fires transitions when asked: step/1 fires one, run/2 fires until nothing can fire or a step count is reached, fire/2 fires a named transition. Nothing happens on its own, so a runner is idle between calls.

Guards and actions

A transition's guard receives the tokens it would consume, as a map of input place to the list of tokens taken from it, and returns a boolean — anything else is reported as {:error, {:invalid_guard, value}} rather than read as a refusal, which would disable a transition silently. Its action receives the same map and returns the tokens to produce, as a map of output place to list of tokens. The default action produces :token once per unit of arc weight.

An action must return exactly as many tokens as the arc weights say, for the places the transition actually feeds; otherwise the firing is refused with {:error, {:invalid_action, detail}} and the marking is unchanged. Analysis relies on those weights, and a runner that quietly produced a different number of tokens would be running a different net from the one that was checked.

Guards and actions run inside the runner process. One that raises takes the runner down with it, which is ordinary OTP behaviour and the reason a runner belongs under a supervisor. A slow action blocks the whole net. The pattern that keeps a net responsive is an action that hands the work to another process and returns immediately; that process later calls put/3 to inject the result.

Events

With a :subscriber pid, the runner sends {:petrex, ref, event} where ref identifies the runner (ref/1, or the :ref option):

  • {:fired, transition_id, consumed, produced} — after each firing
  • {:quiescent, marking} — nothing can fire, because every structurally enabled transition was refused by its guard
  • {:deadlock, marking} — nothing can fire, because no transition is structurally enabled; this is the deadlock Petrex.Analysis reports

There is no telemetry dependency; the subscriber message is the hook. A subscriber that has died is not an error: events to it are dropped and the net carries on.

Call timeouts

Every call runs inside the runner process, including run/2, so a long run is a long call. They therefore wait forever by default: a GenServer.call timeout would not stop the firing, it would only abandon the reply, reporting a failure to a caller whose net is still advancing. Each function takes a timeout as its last argument for callers that would rather not block, and run/2 with a step count is the way to bound the work itself.

Summary

Functions

Child specification for a supervisor: {Petrex.Runner, {net, opts}}, or {Petrex.Runner, net} for the defaults. The default restart is :transient, since a runner that stopped normally has finished its net.

The current token marking.

Adds tokens to a place: a count (each token is :token) or a list of arbitrary terms. This is how the world outside the net enters it.

The term identifying this runner in its events.

Fires until nothing can fire or max_steps firings have happened.

The runner's whole state, for restore/2.

Starts a runner for net.

Fires one transition chosen by the policy.

Types

policy()

@type policy() ::
  :first
  | ([Petrex.Transition.id()], Petrex.Marking.t() -> Petrex.Transition.id())

stop_reason()

@type stop_reason() :: :quiescent | :deadlock | :max_steps

Functions

child_spec(init_arg)

Child specification for a supervisor: {Petrex.Runner, {net, opts}}, or {Petrex.Runner, net} for the defaults. The default restart is :transient, since a runner that stopped normally has finished its net.

fire(runner, transition, timeout \\ :infinity)

@spec fire(GenServer.server(), Petrex.Transition.id(), timeout()) ::
  {:ok, Petrex.Transition.id()} | {:error, term()}

Fires a named transition.

Returns {:ok, transition_id}, or {:error, :not_enabled} when it is not enabled or its guard refuses it, {:error, {:unknown_transition, id}} for a transition the net does not have, or {:error, {:invalid_action, detail}} when its action breaks the arc weights.

marking(runner, timeout \\ :infinity)

@spec marking(GenServer.server(), timeout()) :: Petrex.Marking.t()

The current token marking.

put(runner, place, tokens, timeout \\ :infinity)

@spec put(
  GenServer.server(),
  Petrex.Place.id(),
  non_neg_integer() | [term()],
  timeout()
) ::
  :ok | {:error, term()}

Adds tokens to a place: a count (each token is :token) or a list of arbitrary terms. This is how the world outside the net enters it.

Returns {:error, {:unknown_place, id}} for a place the net does not have and {:error, {:invalid_tokens, value}} for anything that is neither a count nor a list.

ref(runner, timeout \\ :infinity)

@spec ref(GenServer.server(), timeout()) :: term()

The term identifying this runner in its events.

restore(runner, snapshot, timeout \\ :infinity)

@spec restore(GenServer.server(), map(), timeout()) :: :ok | {:error, term()}

Restores a state taken with snapshot/1.

The marking must belong to this net: {:error, {:unknown_places, ids}} names places the net does not have, and {:error, {:invalid_tokens, ids}} places whose tokens are neither a count nor a list. A marking from another net is a mistake worth reporting, not one to absorb.

run(runner, max_steps \\ :infinity, timeout \\ :infinity)

@spec run(GenServer.server(), pos_integer() | :infinity, timeout()) ::
  {:ok, non_neg_integer(), stop_reason()} | {:error, term()}

Fires until nothing can fire or max_steps firings have happened.

Returns {:ok, fired, reason} with the number of transitions fired and why it stopped: :quiescent, :deadlock or :max_steps. A firing that fails — an action breaking the arc weights, a policy naming a transition that is not enabled — stops the run and returns {:error, reason} with that failure, never as a reason the net came to rest.

:infinity runs until the net stops of its own accord, which a live net never does: a cyclic net keeps firing forever and the call never returns. Pass a step count unless the net is known to terminate — Petrex.Analysis can tell you whether it is.

snapshot(runner, timeout \\ :infinity)

@spec snapshot(GenServer.server(), timeout()) :: map()

The runner's whole state, for restore/2.

start_link(net, opts \\ [])

@spec start_link(Petrex.Net.t(), keyword()) :: GenServer.on_start()

Starts a runner for net.

Options:

  • :marking — token marking to start from, instead of the net's own
  • :policy:first (default), which picks the enabled transition that was defined first, or a function receiving the enabled transitions and the current marking and returning one of them
  • :subscriber — pid to send events to
  • :ref — term identifying this runner in events (default: a new reference)
  • :id — child id for child_spec/1; ignored by start_link/2 itself

Any other option is passed to GenServer.start_link/3, so :name works as usual.

step(runner, timeout \\ :infinity)

@spec step(GenServer.server(), timeout()) ::
  {:ok, Petrex.Transition.id()} | {:error, stop_reason() | term()}

Fires one transition chosen by the policy.

Returns {:ok, transition_id}, or {:error, :quiescent} when guards refuse every structurally enabled transition, or {:error, :deadlock} when none is structurally enabled. A firing that fails returns its own reason instead: {:error, {:invalid_action, detail}} or {:error, {:policy_chose_disabled_transition, id}}.