A Karp–Miller coverability tree, as built by
Petrex.Analysis.coverability/3.
Each node holds an ω-marking: a count per place, where :omega stands for
"arbitrarily many". Node 0 is the root (the initial marking). nodes is a
tuple of {marking, parent, transition}, with parent and transition
nil for the root. A node whose marking already occurs earlier in the tree
is a leaf and is not expanded.
A place is unbounded exactly when :omega appears for it in some node, and
a transition can fire in some reachable marking exactly when it labels
some edge of a complete tree. complete? is false when construction
stopped at its node limit, in which case neither property is decided by
the tree.
Summary
Functions
Per-place bound over all nodes: the largest count, or :unbounded when
:omega occurs.
Transitions that label at least one edge, in definition order.
The ω-marking of a node, as a map over every place.
Distinct ω-markings in the tree, in node order.
A node as a map: its ω-marking, the node it was reached from (nil for
the root) and the transition that reached it (nil for the root).
Every node, in node order, as node/2 returns them.
The path from the root to a node, as the transitions fired to reach it.
Number of nodes.
Types
Functions
@spec bounds(t()) :: %{required(Petrex.Place.id()) => non_neg_integer() | :unbounded}
Per-place bound over all nodes: the largest count, or :unbounded when
:omega occurs.
@spec fired_transitions(t()) :: [Petrex.Transition.id()]
Transitions that label at least one edge, in definition order.
@spec marking(t(), node_id()) :: %{required(Petrex.Place.id()) => count()}
The ω-marking of a node, as a map over every place.
@spec markings(t()) :: [%{required(Petrex.Place.id()) => count()}]
Distinct ω-markings in the tree, in node order.
@spec node(t(), node_id()) :: %{ marking: %{required(Petrex.Place.id()) => count()}, parent: node_id() | nil, transition: Petrex.Transition.id() | nil }
A node as a map: its ω-marking, the node it was reached from (nil for
the root) and the transition that reached it (nil for the root).
Every node, in node order, as node/2 returns them.
@spec path_to(t(), node_id()) :: [Petrex.Transition.id()]
The path from the root to a node, as the transitions fired to reach it.
@spec size(t()) :: non_neg_integer()
Number of nodes.