Petrex.Net (petrex v1.0.0)

A place/transition net with an initial token marking.

Nets are plain data. They are normally assembled with the builder in Petrex and checked with validate/1, which every analysis function also relies on.

Places and transitions share one identifier namespace, and identifiers are atoms (other than nil) or strings. place_order and transition_order record definition order: place order fixes the position of each place in internal count vectors, and transition order is the deterministic order in which enabled transitions are reported and conflicts are resolved by default.

Summary

Types

error()

path()

A path locating the offending element, e.g. [:arcs, 3] for the fourth arc or [:transitions, :acquire].

t()

Functions

validate(net)

Checks the structural well-formedness of a net.

Types

error()

@type error() :: {path(), reason :: term()}

path()

@type path() :: [term()]

A path locating the offending element, e.g. [:arcs, 3] for the fourth arc or [:transitions, :acquire].

t()

@type t() :: %Petrex.Net{
  arcs: [Petrex.Arc.t()],
  extra: Petrex.Place.extra(),
  initial: Petrex.Marking.t(),
  place_order: [Petrex.Place.id()],
  places: %{required(Petrex.Place.id()) => Petrex.Place.t()},
  transition_order: [Petrex.Transition.id()],
  transitions: %{required(Petrex.Transition.id()) => Petrex.Transition.t()}
}

Functions

validate(net)

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

Checks the structural well-formedness of a net.

Returns :ok, or {:error, errors} listing every problem found as {path, reason}. Detected problems:

identifiers that are not atoms or strings, or that differ from their map key ({:invalid_id, id}, {:id_mismatch, id})
an identifier used by both a place and a transition ({:duplicate_id, id})
order lists that are not exactly the keys of the maps (:order_mismatch)
guards or actions that are neither nil nor 1-arity functions
arcs whose endpoints do not exist ({:unknown_node, id}), that connect two places or two transitions, inhibitor arcs leaving a transition (:inhibitor_from_transition), weights that are not positive integers ({:invalid_weight, w}), and repeated arcs (:duplicate_arc)
initial markings naming unknown places ({:unknown_place, id}) or holding anything other than a token list ({:invalid_tokens, value})