The petri_net library

The Petri net library provides a matrix representation of dimensioned Petri nets. In a dimensioned Petri net a unit of measurement is associated with the net's places.

A Petri net is a tuple (P, T, F, B) with

P a set of places,
T a set of transitions,
F a matrix of the form P × T → ℕ called the pre or forward matrix.
B a matrix of the form P × T → ℕ called the post or backward, and

A Petri net's state is defined by its marking. A marking m is a vector P → ℕ .

For any place p ∈ P value m(p) is the number of tokens in that place.

A Petri net changes state by firing transitions. In a matrix setting it is natural to define firing of transitions in parallel.

Given a transition vector x of type T → ℕ where x(t) is number of times transition t ∈ T fires, the new marking m' is given by

m' = m + Gx under the condition that Fx ≥ m

where flow matrix G is defined as G = B - F

Synopsis

fire_petri_net :: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!), T!) -> PetriNet(a, P!u, T!)
make_petri_net :: for_unit a, P!u: for_index P, T: (a*P!u per T!, a*P!u per T!, a*P!u) -> PetriNet(a, P!u, T!)
make_zero_net :: for_unit a, P!u: for_index P, T: (a*P!u per T!, a*P!u per T!) -> PetriNet(a, P!u, T!)
petri_net_enabled :: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!), T!) -> Boole
petri_net_flow :: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> a*P!u per T!
petri_net_marking :: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> a*P!u
petri_net_places :: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> List(P)
petri_net_post :: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> a*P!u per T!
petri_net_pre :: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> a*P!u per T!
petri_net_transitions :: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> List(T)
petri_net_unit :: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> a*P!u per T!
petri_subnet :: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!), T!) -> PetriNet(a, P!u, T!)
place_unit :: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> a*P!u
semi_flows :: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> List(T!)
transition_unit :: for_unit a, mon, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> T!

Types

PetriNet

for_index P, T: for_unit a, P!u: PetriNet(a, P!u, T!)

A dimensioned Petri nets. In a dimensioned Petri net a unit of measurement is associated with the net's places.

Functions

fire_petri_net

:: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!), T!) -> PetriNet(a, P!u, T!)

Fires the Petri net. Results in a Petri net with the new marking.

make_petri_net

:: for_unit a, P!u: for_index P, T: (a*P!u per T!, a*P!u per T!, a*P!u) -> PetriNet(a, P!u, T!)

Constructor for record PetriNet(a, P!u, T!)

make_zero_net

:: for_unit a, P!u: for_index P, T: (a*P!u per T!, a*P!u per T!) -> PetriNet(a, P!u, T!)

Creates a Petri net from incidence matrices with a zero marking.

petri_net_enabled

:: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!), T!) -> Boole

Is firing the Petri net enabled for the given transition count?

petri_net_flow

:: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> a*P!u per T!

The Petri net's flow matrix. Defined as the difference between the net's post matrix and the net's pre matrix.

petri_net_marking

:: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> a*P!u

Getter for record PetriNet(a, P!u, T!)

petri_net_places

:: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> List(P)

The places in a petri net.

Equals the row domain of the incidence matrices.

petri_net_post

:: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> a*P!u per T!

Getter for record PetriNet(a, P!u, T!)

petri_net_pre

:: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> a*P!u per T!

Getter for record PetriNet(a, P!u, T!)

petri_net_transitions

:: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> List(T)

The transitions in a petri net.

Equals the column domain of the incidence matrices.

petri_net_unit

:: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> a*P!u per T!

The units of measurement of the Petri net's pre and post matrices.

petri_subnet

:: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!), T!) -> PetriNet(a, P!u, T!)

Filters the net's transitions.

place_unit

:: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> a*P!u

Unit vector for the net's places.

semi_flows

:: for_unit a, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> List(T!)

All transition vector that leaves the net's marking unchanged when fired.

transition_unit

:: for_unit a, mon, P!u: for_index P, T: (PetriNet(a, P!u, T!)) -> T!

Unit vector for the net's transitions.

Version v0.6.0, 2026-03-05T15:49:25.025069793+01:00[Europe/Amsterdam]