Petrex (petrex v1.0.0)

Copy Markdown View Source

Place/transition Petri nets for the BEAM, with analysis as the primary product.

This module is the builder: nets are data (Petrex.Net), and these functions assemble one step at a time.

Petrex.new()
|> Petrex.place(:free, tokens: 2)
|> Petrex.place(:busy)
|> Petrex.transition(:acquire, in: [free: 1], out: [busy: 1])
|> Petrex.transition(:release, in: [busy: 1], out: [free: 1])
|> Petrex.transition(:panic, in: [busy: 1], inhibit: [:free], out: [busy: 1])

Arcs may name places that are added later. The builder raises ArgumentError only for input that cannot be represented in a Petrex.Net at all: a reused identifier, a malformed option, a negative token count. Everything else, such as a zero weight or an arc to a place that never gets defined, is reported by validate/1.

Summary

Functions

Returns an empty net.

Adds a transition and its arcs.

Checks a net's structure. See Petrex.Net.validate/1.

Functions

new()

@spec new() :: Petrex.Net.t()

Returns an empty net.

place(net, id, opts \\ [])

@spec place(Petrex.Net.t(), Petrex.Place.id(), keyword()) :: Petrex.Net.t()

Adds a place.

Options:

  • :tokens — initial tokens: a count (each token is :token) or a list of arbitrary terms. Default 0.
  • :name — a human-readable label.

transition(net, id, opts \\ [])

@spec transition(Petrex.Net.t(), Petrex.Transition.id(), keyword()) :: Petrex.Net.t()

Adds a transition and its arcs.

Arc lists accept place (weight 1) or {place, weight}, so keyword lists such as [free: 2] work for atom identifiers.

Options:

  • :in — input places, consumed on firing.
  • :out — output places, produced into on firing.
  • :inhibit — inhibitor places: the transition is enabled only while each holds fewer tokens than the arc weight.
  • :guard, :action — see Petrex.Transition.
  • :name — a human-readable label.

validate(net)

@spec validate(Petrex.Net.t()) :: :ok | {:error, [Petrex.Net.error()]}

Checks a net's structure. See Petrex.Net.validate/1.