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 classify Petri nets by how their tokens behave, what invariants hold, and how they compose. This post introduces the five pflow net types, the typed links that connect them, and why the resulting structure forms a category with useful algebraic properties.
The pflow schema defines five concrete net types, each a specialization of the base PetriNet:
| Type | Token Semantics | Invariant |
|---|---|---|
| WorkflowNet | Single control-flow token (cursor) | Mutual exclusion — cursor in exactly one state |
| ResourceNet | Countable inventory tokens | Conservation — total tokens constant |
| GameNet | Turn-based tokens with player roles | Both mutual exclusion and conservation |
| ComputationNet | Continuous quantities via ODE rates | Rate conservation at steady state |
| ClassificationNet | Signal tokens with threshold activation | Threshold firing conditions |
WorkflowNet. A single token traces a path through states. An order moves through pending → confirmed → shipped → delivered. The token is a cursor — it marks where we are in a sequential process. WorkflowNets are finite state machines with the structural advantage that parallelism (multiple concurrent tokens) is expressible.
ResourceNet. Tokens represent countable, fungible things: inventory items, currency, capacity slots. A warehouse has 100 tokens in available, consumed by reserve and produced into reserved. The total is conserved — the P-invariant guarantees that nothing is created or destroyed.
GameNet. Tokens encode both game state and turn structure. In tic-tac-toe, empty cells hold tokens consumed when a player moves. A turn-control token alternates between players. GameNets combine WorkflowNet sequencing (turns) with ResourceNet accounting (board positions).
ComputationNet. Tokens are continuous, not discrete. Transitions fire at rates — mass-action kinetics. An SIR epidemic model is a ComputationNet: the infection rate depends on the product of susceptible and infected populations. DDM analysis operates natively on ComputationNets.
ClassificationNet. Tokens accumulate as evidence. Transitions fire when enough tokens accrue — a threshold. A spam filter accumulates signal tokens from heuristics (suspicious sender, keyword matches, link density) and fires classify_spam when the threshold is met.
At the structural level, all five types are Petri nets. The type annotations matter because they constrain composition. When we connect two nets, the types determine what connections are valid:
Types make the composition rules explicit. We can't accidentally link a workflow cursor to an inventory counter. The type system prevents semantic nonsense at the structural level — 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? The CompositeNet grammar has algebraic properties that make reasoning tractable:
These 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.
Each component is verified in isolation, and composition only needs to check the boundaries. Adding a new schema or link can only extend behavior, never break what's already working.
This topic is covered in depth in Chapter 4: The Token Language of Petri Nets as a Universal Abstraction.