An explicit reachability graph, as built by Petrex.Analysis.reachability/3.
States are numbered from 0 in breadth-first discovery order; state 0 is the
initial marking. Markings are held internally as tuples of counts in
places order; marking/2 and markings/1 return them as maps.
edges lists {from, transition_id, to} for every firing between known
states. It is the largest part of the graph — a million markings usually
come with several million edges — so Petrex.Analysis.reachability/3 can
be asked not to keep it (edges: false), in which case edges is empty
and edges? is false. edge_count/1, dead_states/1 and
fired_transitions/1 are collected during the search and stay available
either way.
When complete? is false the exploration stopped at its limit: only
states numbered below expanded have all their successors recorded, and
markings beyond the limit are missing altogether.
inhibitor_arcs? records that the net has inhibitor arcs. A completed
exploration is exact for those nets too; what inhibitor arcs remove is the
guarantee that it completes.
Summary
Functions
States with no enabled transition among the fully expanded ones: the reachable deadlocks found.
Number of edges, whether or not the edge list was kept.
The edges as {from_state, transition_id, to_state}, in discovery order.
Transitions enabled in at least one expanded state, in definition order.
The marking of a state, as a map over every place.
All markings, in state order.
Number of states.
The edges leaving a state, as {transition_id, to_state}. Needs a graph
that kept its edges.
Types
@type state() :: non_neg_integer()
@type t() :: %Petrex.Analysis.ReachabilityGraph{ complete?: boolean(), dead_states: [state()], edge_count: non_neg_integer(), edges: [{state(), Petrex.Transition.id(), state()}], edges?: boolean(), expanded: non_neg_integer(), fired: MapSet.t(Petrex.Transition.id()), inhibitor_arcs?: boolean(), markings: tuple(), places: tuple(), transitions: tuple() }
Functions
States with no enabled transition among the fully expanded ones: the reachable deadlocks found.
@spec edge_count(t()) :: non_neg_integer()
Number of edges, whether or not the edge list was kept.
@spec edges(t()) :: {:ok, [{state(), Petrex.Transition.id(), state()}]} | {:error, :edges_not_kept}
The edges as {from_state, transition_id, to_state}, in discovery order.
Returns {:ok, edges}, or {:error, :edges_not_kept} for a graph built
with edges: false, which has the count but not the list.
@spec fired_transitions(t()) :: [Petrex.Transition.id()]
Transitions enabled in at least one expanded state, in definition order.
@spec marking(t(), state()) :: Petrex.Marking.skeleton()
The marking of a state, as a map over every place.
@spec markings(t()) :: [Petrex.Marking.skeleton()]
All markings, in state order.
@spec size(t()) :: non_neg_integer()
Number of states.
@spec successors(t(), state()) :: {:ok, [{Petrex.Transition.id(), state()}]} | {:error, :edges_not_kept}
The edges leaving a state, as {transition_id, to_state}. Needs a graph
that kept its edges.