Formal Object-Centric Petri Net (OCPN) Specification and Soundness Engine.
Represents an OCPN as a tuple N = (P, T, F, V, l, type_p, type_t) where:
- P is a set of places typed by object types (type_p: P -> T_O)
- T is a set of transitions
- F is the flow relation with variable arc inscriptions
- Verifies Object Token Conservation and 1-Safe sub-net soundness per object type.
Summary
Functions
Adds a typed arc to the OCPN.
Adds a typed place to the OCPN.
Adds a transition to the OCPN.
Constructs a new Object-Centric Petri Net.
Projects the OCPN onto a single object type ot, yielding a standard Workflow Net. Verifies 1-safe soundness on the projection.
Verifies Object Token Conservation: Proves that for every transition t and every involved object type ot, the number of input tokens consumed matches the output tokens produced or explicitly transitions to terminal/consumed state.
Functions
Adds a typed arc to the OCPN.
Adds a typed place to the OCPN.
Adds a transition to the OCPN.
Constructs a new Object-Centric Petri Net.
Projects the OCPN onto a single object type ot, yielding a standard Workflow Net. Verifies 1-safe soundness on the projection.
Verifies Object Token Conservation: Proves that for every transition t and every involved object type ot, the number of input tokens consumed matches the output tokens produced or explicitly transitions to terminal/consumed state.