@spec bound(Petrex.Net.t(), Petrex.Marking.skeleton() | keyword() | nil, keyword()) ::
  result(bounds())

Computes the bound of every place: the largest number of tokens it holds in any reachable marking, or :unbounded.

Without inhibitor arcs the answer comes from the coverability tree. With inhibitor arcs it comes from explicit reachability and is exact only if the exploration completes.

A partial result maps each place to a bound that is certainly reached (a lower bound) or to :unbounded, which is always certain.

iex> net =
...>   Petrex.new()
...>   |> Petrex.place(:p, tokens: 1)
...>   |> Petrex.place(:q)
...>   |> Petrex.transition(:grow, in: [:p], out: [:p, :q])
iex> Petrex.Analysis.bound(net)
{:ok, %{p: 1, q: :unbounded}}

@spec bounded?(Petrex.Net.t(), Petrex.Marking.skeleton() | keyword() | nil, keyword()) ::
  boolean()

Whether every place is bounded. Raises Petrex.InconclusiveError when the limit was reached before an unbounded place was found.

@spec coverability(
  Petrex.Net.t(),
  Petrex.Marking.skeleton() | keyword() | nil,
  keyword()
) ::
  result(Petrex.Analysis.CoverabilityTree.t()) | {:error, :inhibitor_arcs}

Builds the Karp–Miller coverability tree.

The construction terminates for every net without inhibitor arcs, bounded or not, but the tree can be very large; {:partial, tree} is returned when the :limit is reached. Nets with inhibitor arcs return {:error, :inhibitor_arcs}. See Petrex.Analysis.CoverabilityTree.

@spec dead_transitions(
  Petrex.Net.t(),
  Petrex.Marking.skeleton() | keyword() | nil,
  keyword()
) ::
  result([Petrex.Transition.id()])

Lists the transitions that are not enabled in any reachable marking (dead in the sense of liveness level L0), in definition order.

Without inhibitor arcs the answer comes from the coverability tree, which decides it exactly even for unbounded nets. With inhibitor arcs it comes from explicit reachability. A partial result lists the candidates: every transition not seen enabled before the limit. Transitions absent from a partial result are certainly not dead.

@spec deadlocks(
  Petrex.Net.t(),
  Petrex.Marking.skeleton() | keyword() | nil,
  keyword()
) ::
  result([Petrex.Marking.skeleton()])

Lists the reachable markings in which no transition is enabled, in breadth-first order.

Computed on the reachability graph. A partial result lists the deadlocks found before the limit; others may exist. For an unbounded net the result is always partial.

iex> net =
...>   Petrex.new()
...>   |> Petrex.place(:p, tokens: 1)
...>   |> Petrex.place(:q)
...>   |> Petrex.transition(:t, in: [:p], out: [:q])
iex> Petrex.Analysis.deadlocks(net)
{:ok, [%{p: 0, q: 1}]}

@spec enabled(Petrex.Net.t(), Petrex.Marking.skeleton() | nil) :: [
  Petrex.Transition.id()
]

Lists the transitions enabled in a marking, in definition order.

iex> net =
...>   Petrex.new()
...>   |> Petrex.place(:free, tokens: 1)
...>   |> Petrex.place(:busy)
...>   |> Petrex.transition(:acquire, in: [:free], out: [:busy])
...>   |> Petrex.transition(:release, in: [:busy], out: [:free])
iex> Petrex.Analysis.enabled(net)
[:acquire]
iex> Petrex.Analysis.enabled(net, %{busy: 1})
[:release]

@spec fire(Petrex.Net.t(), Petrex.Marking.skeleton() | nil, Petrex.Transition.id()) ::
  {:ok, Petrex.Marking.skeleton()} | {:error, :not_enabled}

Fires a transition on a skeleton marking.

Returns {:ok, marking} or {:error, :not_enabled}. Raises ArgumentError for an unknown transition or place.

iex> net =
...>   Petrex.new()
...>   |> Petrex.place(:free, tokens: 2)
...>   |> Petrex.place(:busy)
...>   |> Petrex.transition(:acquire, in: [:free], out: [:busy])
iex> Petrex.Analysis.fire(net, %{free: 2}, :acquire)
{:ok, %{free: 1, busy: 1}}
iex> Petrex.Analysis.fire(net, %{busy: 2}, :acquire)
{:error, :not_enabled}

@spec invariants(Petrex.Net.t()) :: %{
  p_invariants: [%{required(Petrex.Place.id()) => pos_integer()}],
  t_invariants: [%{required(Petrex.Transition.id()) => pos_integer()}]
}

Computes the minimal-support semi-positive P- and T-invariants.

A P-invariant y ≥ 0 satisfies yᵀC = 0 for the incidence matrix C: the weighted token sum Σ y(p)·M(p) is the same in every reachable marking. A T-invariant x ≥ 0 satisfies Cx = 0: firing every transition t exactly x(t) times returns to the starting marking. Every semi-positive invariant is a non-negative rational combination of the returned ones.

Each invariant is a map from identifier to positive integer coefficient, with the coefficients' greatest common divisor equal to 1. Inhibitor arcs do not move tokens and are not part of the incidence matrix. Self-loops cancel out in it for the same reason.

iex> net =
...>   Petrex.new()
...>   |> Petrex.place(:free, tokens: 2)
...>   |> Petrex.place(:busy)
...>   |> Petrex.transition(:acquire, in: [:free], out: [:busy])
...>   |> Petrex.transition(:release, in: [:busy], out: [:free])
iex> Petrex.Analysis.invariants(net)
%{p_invariants: [%{free: 1, busy: 1}], t_invariants: [%{acquire: 1, release: 1}]}

@spec reachability(
  Petrex.Net.t(),
  Petrex.Marking.skeleton() | keyword() | nil,
  keyword()
) ::
  result(Petrex.Analysis.ReachabilityGraph.t())

Builds the explicit reachability graph by breadth-first search.

Returns {:ok, graph} when every reachable marking was found, or {:partial, graph} when the :limit was reached first. See Petrex.Analysis.ReachabilityGraph.

iex> net =
...>   Petrex.new()
...>   |> Petrex.place(:free, tokens: 2)
...>   |> Petrex.place(:busy)
...>   |> Petrex.transition(:acquire, in: [:free], out: [:busy])
...>   |> Petrex.transition(:release, in: [:busy], out: [:free])
iex> {:ok, graph} = Petrex.Analysis.reachability(net)
iex> Petrex.Analysis.ReachabilityGraph.size(graph)
3

@spec safe?(Petrex.Net.t(), Petrex.Marking.skeleton() | keyword() | nil, keyword()) ::
  boolean()

Whether every place is 1-bounded. Raises Petrex.InconclusiveError when the limit was reached before a place with more than one token was found.

@spec short_circuit(Petrex.Net.t(), keyword()) ::
  {:ok, Petrex.Net.t()} | {:error, term()}

Adds a transition from the sink back to the source, the short-circuited net of van der Aalst's soundness proof.

Returns {:error, reason} for a net that is not a workflow net, or {:error, {:id_taken, id}} when the identifier is already used. The transition is named by the :id option, :short_circuit by default.

@spec sound?(Petrex.Net.t(), keyword()) ::
  {:ok, :sound} | {:error, term()} | {:partial, :limit_reached}

Checks classical soundness of a workflow net (van der Aalst 1997), starting from one token in the source place. The net's own initial marking is ignored.

Weaker variants exist in the literature (relaxed, weak and lazy soundness); this is the classical notion and the only one Petrex checks.

A workflow net is sound when every marking reachable from the initial one can still reach the final marking (one token in the sink, nothing elsewhere), when no reachable marking other than the final one covers it, and when no transition is dead. Equivalently, the short-circuited net is live and bounded.

Returns {:ok, :sound} or {:error, reason} with a witness:

• {:not_a_workflow_net, reason} — see workflow_net/1
• {:unbounded, place}
• {:improper_completion, marking} — reachable, covers the final marking
• {:no_option_to_complete, marking} — reachable, cannot reach the final marking
• {:dead_transition, id}
• {:partial, :limit_reached} — the state space exceeded :limit, so no verdict was reached

Examples

iex> sound =
...>   Petrex.new()
...>   |> Petrex.place(:in)
...>   |> Petrex.place(:out)
...>   |> Petrex.transition(:work, in: [:in], out: [:out])
iex> Petrex.Analysis.sound?(sound)
{:ok, :sound}

iex> mismatch =
...>   Petrex.new()
...>   |> Petrex.place(:in)
...>   |> Petrex.place(:left)
...>   |> Petrex.place(:right)
...>   |> Petrex.place(:out)
...>   |> Petrex.transition(:split, in: [:in], out: [:left, :right])
...>   |> Petrex.transition(:finish_left, in: [:left], out: [:out])
...>   |> Petrex.transition(:finish_right, in: [:right], out: [:out])
iex> Petrex.Analysis.sound?(mismatch)
{:error, {:improper_completion, %{in: 0, left: 0, right: 1, out: 1}}}

@spec workflow_net(Petrex.Net.t()) ::
  {:ok, %{source: Petrex.Place.id(), sink: Petrex.Place.id()}}
  | {:error, term()}

Like workflow_net?/1, but returns {:ok, %{source: id, sink: id}} or {:error, reason} naming what disqualifies the net: {:source, places} or {:sink, places} when there is not exactly one, {:source_is_sink, place}, or {:disconnected, nodes} for nodes off every path from the source to the sink.

@spec workflow_net?(Petrex.Net.t()) :: boolean()

Whether the net is a workflow net: one source place, one sink place, and every node on a path from the source to the sink.

Only normal arcs form that flow relation; inhibitor arcs are ignored when looking for sources, sinks and paths.

iex> net =
...>   Petrex.new()
...>   |> Petrex.place(:in, tokens: 1)
...>   |> Petrex.place(:out)
...>   |> Petrex.transition(:work, in: [:in], out: [:out])
iex> Petrex.Analysis.workflow_net?(net)
true