The four-term DSL gives us primitives: cell, func, arrow, guard. With these we can build any Petri net. But not all Petri nets are alike. An order-processing workflow and an epidemiological simulation both use places, transitions, and arcs — yet their tokens mean fundamentally different things.
Net types give us kinds. They classify Petri nets by how their tokens behave, what invariants hold, and how the nets compose with other nets. This post introduces the pflow net type taxonomy and shows how these typed nets form a category — with typed links as morphisms — enabling compositional system design.
The pflow schema defines five concrete net types, each a specialization of the base PetriNet:
| Type | Token Semantics | Composition Role |
|---|---|---|
| WorkflowNet | Single control-flow token moving through states | Orchestration |
| ResourceNet | Countable inventory tokens consumed and produced | Resource management |
| GameNet | Turn-based tokens with player roles and alternating state | Interactive logic |
| ComputationNet | Continuous quantities evolving via ODE / mass-action rates | Continuous processes |
| ClassificationNet | Signal tokens with threshold activation and branching | Decision making |
WorkflowNet. A single token traces a path through states. Think of an order moving through pending → confirmed → shipped → delivered. The token is a cursor — it marks "where we are" in a sequential process. WorkflowNets are the Petri net equivalent of finite state machines, with the added benefit that parallelism (multiple concurrent tokens) is structurally expressible.
ResourceNet. Tokens represent countable, fungible things: inventory items, currency units, capacity slots. A warehouse model might have 100 tokens in available, consumed by reserve and produced into reserved. The key property is conservation — the total token count across related places stays constant (a P-invariant).
GameNet. Tokens encode both game state and turn structure. In tic-tac-toe, empty cells hold tokens that get consumed when a player moves, producing tokens in X-marked or O-marked places. A turn-control token alternates between players. GameNets combine WorkflowNet sequencing (turns) with ResourceNet accounting (board positions).
ComputationNet. Token quantities are continuous, not discrete. Transitions fire at rates proportional to their input concentrations — mass-action kinetics. The classic example is an SIR epidemiological model: Susceptible → Infected → Recovered, where the rate of infection depends on the product of S and I populations. DDM analysis operates natively on ComputationNets.
ClassificationNet. Tokens accumulate as evidence, and transitions fire when a threshold is reached. A spam filter might accumulate signal tokens from various heuristics — suspicious sender, keyword matches, link density — and fire a classify_spam transition when enough evidence accrues. ClassificationNets model decision processes where multiple weak signals combine into a strong conclusion.
At the structural level, all five net types are Petri nets — bipartite graphs with places, transitions, and arcs. We could ignore the type annotations and treat everything uniformly. So why bother with types?
Token semantics differ. A WorkflowNet token is a cursor; moving it twice is an error (the process already advanced). A ResourceNet token is a countable thing; having many in one place is normal. A ComputationNet token is a continuous quantity; fractional values are meaningful. The type tells us what operations make sense.
Invariants differ. ResourceNets have P-invariants (token conservation). WorkflowNets have mutual exclusion (the cursor is in exactly one state). GameNets combine both. ComputationNets have rate invariants (flow conservation in steady state). The type determines which safety properties we can verify.
Composition rules differ. When we connect two nets, the type annotations constrain what links are valid. An EventLink between two WorkflowNets cascades control flow. A DataLink from a ResourceNet to a WorkflowNet lets the workflow observe inventory levels. Without types, we'd have to manually reason about whether each connection makes sense.
Types make implicit semantics explicit. They're the difference between "a Petri net" and "a Petri net that models inventory with conservation guarantees."
Individual typed nets are useful. But real systems are compositions of multiple nets — an order system combines workflow logic with inventory management, payment processing, and notification delivery.
The CompositeNet type captures this composition:
CompositeNet = schemas[] + links[]
Each entry in schemas is a sealed, typed sub-net (a WorkflowNet, ResourceNet, etc.). Each entry in links is a typed connection between elements of different schemas.
This has a natural categorical interpretation:
The schemas carry their own verified properties via seals. The links describe how those properties interact. The CompositeNet is the coproduct — the "sum" of its parts with explicit boundary connections.
Not all connections between schemas are the same. The pflow schema defines four link types, each with distinct coupling semantics:
{
"@type": "EventLink",
"from": { "ref": "orders", "transition": "confirm" },
"to": { "ref": "inventory", "transition": "reserve" }
}
When the source transition fires, the target transition fires too — a cascade. EventLinks connect transitions to transitions. They express "when this happens, that happens too."
This is the strongest form of coupling. The target transition must be enabled (its input places must have sufficient tokens), or the source firing is blocked. Both schemas' states change atomically.
{
"@type": "DataLink",
"from": { "ref": "inventory", "place": "available" },
"to": { "ref": "dashboard", "place": "stock_display" }
}
The target place mirrors the token count of the source place — read-only observation. DataLinks connect places to places. They express "this value reflects that value."
This is weak coupling. The observer sees the state but cannot modify it. No tokens transfer. The source schema is unaffected by the link's existence.
{
"@type": "TokenLink",
"from": { "ref": "warehouse_a", "place": "stock" },
"to": { "ref": "warehouse_b", "place": "stock" }
}
Actual token transfer between schemas. When tokens leave the source place, they appear in the target place. The total is conserved across the boundary — a cross-schema P-invariant.
TokenLinks are the composition mechanism for ResourceNets. They model supply chains, fund transfers, and resource redistribution.
{
"@type": "GuardLink",
"from": { "ref": "compliance", "place": "approved" },
"to": { "ref": "orders", "transition": "ship" }
}
A place in one schema gates a transition in another — a cross-schema predicate. The target transition can only fire if the source place satisfies some condition (e.g., has at least one token).
GuardLinks express inter-schema constraints without data transfer. They model approval gates, regulatory checks, and dependency conditions.
Let's walk through a concrete CompositeNet that composes an order workflow with inventory management:
The system has two schemas:
Orders (WorkflowNet): A control-flow token moves through pending → confirmed → shipped. The confirm transition advances the order from pending to confirmed. The ship transition advances it from confirmed to shipped.
Inventory (ResourceNet): Multiple tokens represent available stock. The reserve transition moves tokens from available to reserved. The ship_out transition consumes reserved tokens.
Two EventLinks wire them together:
orders.confirm → inventory.reserve — Confirming an order automatically reserves inventoryorders.ship → inventory.ship_out — Shipping an order automatically removes reserved stockThe link types constrain valid composition. An EventLink between confirm and reserve makes sense: both are transitions, and the cascade semantics (fire one, fire the other) match the business logic. We couldn't accidentally link a place to a transition with an EventLink — the type system prevents it.
Each schema carries its own seal. The Orders WorkflowNet's seal verifies mutual exclusion (the order is in exactly one state). The Inventory ResourceNet's seal verifies token conservation (total stock = available + reserved). These properties hold independently of the composition — adding EventLinks doesn't invalidate either seal.
Why does this composition work reliably? Because the CompositeNet grammar has algebraic properties that make reasoning tractable.
Associative. Composing (A + B) + C gives the same result as A + (B + C). We can build systems incrementally without worrying about composition order.
Commutative. The order of schema declarations doesn't matter. schemas: [orders, inventory] is the same system as schemas: [inventory, orders].
Monotonic. Adding a new schema or link never invalidates existing ones. If the Orders-Inventory composite works, adding a Notifications schema with new links can only extend behavior — it can't break what's already there.
These three properties make the declaration space a free commutative monoid. In practical terms: development is additive. Teams can work on schemas independently, and composition is mechanical — list the schemas, declare the links, and the algebraic properties guarantee that the result is well-formed.
Seals enable assume-guarantee reasoning. Each sub-net's seal certifies its properties: conservation, boundedness, liveness, mutual exclusion. When composing sealed nets, we only need to verify that the links are compatible — we don't need to re-analyze the internal structure of each sub-net. The seal is the interface contract.
Development is a functor from the free commutative monoid of declarations to the category of executable systems. Collaboration is coproduct in the source category.
This is the Monotonic Source Theorem from the composable SDK vision. In practice it means: the build toolchain verifies seal compatibility at link boundaries, and composition never requires re-opening a sealed model.
The EventLink and DataLink types are implemented in pflow today. TokenLink and GuardLink are next — they'll enable resource transfer and cross-schema constraints, completing the four coupling modes.
Beyond that:
The categorical structure isn't decoration. It's what makes composition trustworthy: sealed objects, typed morphisms, and algebraic properties that guarantee the whole is consistent with its parts.