Petri nets

A NET consumes and produces several tokens in one semantic operation. One firing transforms one immutable marking; a definition does not run, and a query for enabled transitions reserves nothing.

assembly = NET
  PLACE parts INITIAL 12 CAPACITY 20
  PLACE machine INITIAL 1 CAPACITY 1
  PLACE completed INITIAL 0 CAPACITY 20

  TRANSITION assemble
    CONSUME parts: 2, machine: 1
    PRODUCE completed: 1, machine: 1
  END
END

initial = assembly.INITIAL()
attempt = assembly.FIRE(initial, :assemble)

After one successful firing, parts is 10, machine is 1 and completed is 1. Six consecutive firings succeed; the seventh is disabled for lack of parts and leaves the marking untouched. The machine token must be present before firing even though the same firing returns it.

NET assembly … END is the equivalent declaration spelling. A parameterized net, name = NET(tools) … END, evaluates its initial counts and capacities against the arguments of INITIAL. The definition binds INITIAL, FIRE, ENABLED, TOKENS and REPORT members: no clock, scheduler or implicit chooser.

Imported ordinary PT nets

A static IMPORT pnml"…" clause may replace the authored body. It compiles through the same native count NET owner; all existing operations below keep their semantics. The imported definition cannot mix parameters or authored clauses. The bounded import contract records accepted IDs, references, counts and refusal boundaries. See the imported delivery example.

Imported BPMN control flow

The explicit BPMN importer maps one bounded acyclic process with plain tasks and parallel gateways to ordinary NET places and transitions. It adds source-linked task begin/complete steps and explicit instance cancellation. It creates no task worker, scheduler or external action; wider BPMN event, condition and subprocess semantics remain separate profiles.

A separate DMN routing profile admits one exclusive split/merge pair with a frozen decision receipt and bounded position encoding.

Places and transitions

Declaration	Meaning
PLACE name INITIAL expression [CAPACITY expression]	Count place; exact nonnegative integer initial count and optional capacity
TRANSITION name … END	One atomic consume/read/guard/produce contract
CONSUME place: count, …	Tokens removed by the firing; duplicate entries add
READ place: count, …	Availability thresholds that are not consumed; the strongest threshold applies
WHEN boolean	Guard evaluated once after availability; an error is an error, not false
PRODUCE place: count, …	Tokens added by the firing

Count expressions may use the definition parameters and marking.<place> counts from the pre-marking. Counts are exact integers in the safe numeric range; fractional, negative or nonfinite values are errors (NET_INVALID_MULTIPLICITY). Missing CAPACITY means no modeled bound.

Firing

FIRE(marking, :transition) evaluates, in order: multiplicities, availability (count >= MAX(consumed, read)), the guard, outputs, then post-capacity. It returns OK({next, transition, firing_id}) with the complete proposed marking, or ERR(reason) where reason.kind is :disabled (shortage, false guard, capacity) or :error (invalid multiplicity, failed expression, overflow, wrong definition, unknown transition). reason.phase names the step. No partial consumption or production survives rejection, and a same-firing output never satisfies an input shortage. A marking from another definition is refused (NET_DEFINITION_MISMATCH). Restored or edited markings are validated before any transition expression: record shapes, exact nonnegative counts, parameter names, declared capacities, occupancy and the firing counter must agree. Copying a definition ID does not validate a marking. Invalid contents return NET_INVALID_MARKING; exhausting the exact firing-counter range returns NET_COUNT_OVERFLOW.

ENABLED(marking, options) tries every transition against the same marking and returns OK({bindings, examined, complete, reason, cursor}); an optional {transition: :name} narrows the search. An expression error in any transition is reported, never hidden as deadlock. REPORT(marking, :transition) performs one firing evaluation and returns grid.net.report.v1 with status :fired, :disabled or :error and the same outcome FIRE would return. checks lists only the checks attempted, in execution order, with passed/failed status. proposed_changes contains validated partial consumption/production counts, labeled :proposed; a failed firing returns no committed marking. The changes list describes a successful proposed next marking. Neither list commits shared state.

A marking is ordinary immutable data. Committing its effects to shared state is the job of an existing owner (a STATE cell, a rule, a durable table); FIRE itself has no network, storage or clock.

Typed occurrences and selection

A typed place retains distinct token occurrences, even when their payloads are equal. TOKENS(marking, :place) returns occurrence references containing the payload and its identity. Use those references to select exactly which job and part a firing consumes:

repair = NET(jobs, parts)
  PLACE waiting OF {id: string, sku: string} INITIAL jobs
  PLACE stock OF {id: string, sku: string} INITIAL parts
  PLACE active OF {job_id: string, part_id: string} INITIAL VECTOR()
  PLACE benches INITIAL 1 CAPACITY 1

  TRANSITION start
    TAKE job FROM waiting
    TAKE part FROM stock
    CONSUME benches: 1
    WHEN job.sku = part.sku
    PRODUCE active: {job_id: job.id, part_id: part.id}
  END
END

FIRE(marking, :start, {job: job_reference, part: part_reference}) checks all references against that marking before evaluating the guard. A copied payload is not an occurrence reference. Consumed references cannot be selected again; a stale selection or a reference to a different place/definition is refused. The payload names job and part are available only inside the transition.

TAKE items COUNT expression FROM place [MATCH pattern] selects a collection of distinct occurrences. The count may depend on an earlier binding, such as TAKE order FROM waiting followed by TAKE parts COUNT order.quantity FROM stock. READ items [COUNT expression] FROM place [MATCH pattern] binds without consuming; reads may share occurrences. Separate TAKE bindings may not consume the same occurrence. PRODUCE place: EACH values produces one occurrence per value; without EACH it produces one typed payload. Outputs must satisfy the place type and post-capacity before any change succeeds.

ENABLED returns proposed, snapshot-bound selections. limit bounds returned selections; work bounds candidate exploration. Pass its returned cursor to continue the same search on the same marking and transition scope. A bounded page with complete: FALSE is not proof of deadlock. Equal payloads still give different occurrence choices. Expression errors remain errors rather than being silently discarded as disabled candidates.

Subnets and live ownership

A subnet declares PORT INPUT, PORT OUTPUT or PORT SHARED places, with OF type for typed ports. INPUT allows consumption/read, OUTPUT allows production, and SHARED permits both. Instantiate it inside a parent with:

USE first = worker(1) PLACES {pool: benches, waiting: waiting, done: completed}

The mappings alias the parent's places; they do not copy inventories. Private places and transitions are qualified by the instance name. For example, FIRE(marking, "first.start", selection) selects the child's transition. A template with unmapped ports cannot be initialized as a standalone net.

Live applications explicitly select the Host NET owner. It freezes the compiled definition and initial arguments, then commits one proposed firing and its operation receipt in the existing model database transaction. A stale expected revision fails without consumption; an identical operation retry returns its committed result. Reopening reuses the committed marking. Changed definitions or admission arguments cannot silently reinterpret that state. Formula calls remain pure and never select this owner.

The repair-shop example selects one compatible job, part and bench. The kitting schedule uses an imported decision and maps accepted packed payloads to explicit simulation arrivals. Rejected firings produce no arrival, and the simulation owns its resource pool separately. Durable Frame publication remains an explicit owner operation.

Scope

Count and typed places share atomic firing, bounded search and reports. REPORT retains the actual attempt's checks and per-place deltas without evaluating the firing a second time. It retains at most 4,096 checks and 8,192 occurrence IDs; omission sets explanation_complete to false while preserving the complete firing outcome. Explanation materialization has an 8 MiB bound. Timing, stochastic firing, reachability proofs and automatic selection policies are separate contracts; they are not implied by a NET reference or a complete enabled-search page.