Skip to content

PetriNets.kt

src/jvmMain/kotlin/afield/simulation/petri/PetriNets.kt · 1362 lines

@file:Suppress("MemberVisibilityCanBePrivate", "unused")
@file:afield.runtime.completion.CompletionCategory("Visualization")

package afield.simulation.petri

import afield.audio.synth.PatArc
import afield.audio.synth.PatQ
import afield.audio.synth.splitmix64
import afield.audio.synth.toUnitDouble

Petri nets: places hold tokens, transitions move them, and the whole thing is a clock. This file is the model and the engine, and the types the rest of the layer is a view onto.

It knows nothing about music. The one thing it takes from afield.audio.synth is PatQ, the exact rational Field uses for time everywhere. PetriMusic.kt turns a net into a PatPattern, PetriVisual.kt draws one, PetriNotation.kt parses the #petri text form, and PetriStateSpace.kt and PetriAnalysis.kt answer questions about one.

Read the surface from the outside in. Build a net: places are auto-declared on first mention, so a two-transition loop is three calls.

val net = petri {
    place("kick", tokens = 1)
    t("hit",  dur = cyc(1, 16), emit = "bd") { from("kick"); to("hats") }
    t("back", dur = cyc(1, 16), emit = "sd") { from("hats"); to("kick") }
}

Run it. A PetriRun is a memoised, append-only trajectory: ask it for any instant and it replays deterministically up to there.

net.run().stepsUntil(PatQ.of(4)).flatMap { it.firings }.forEach(::println)

Tokens carry colour, and a colour can be anything: a note number, a sample name, a whole PatPattern. That is what makes a net a song structure rather than a drum machine. Colours are carried through a firing by default, so the pattern held in verse below is the colour of the token that reaches chorus, with no lambda anywhere.

place("verse", pat("bd*4"))          // one token whose colour is a pattern
t("build", dur = cyc(4)) { from("verse"); from("hats"); to("chorus") }

Three timings, and why

  • PetriTiming.STEP — maximal step. Every transition that is enabled at a grid tick fires, all against the marking as it stood at the start of the tick, and produced tokens do not become available until the tick is over. This is the drum-machine semantics, and the same synchronous step BooleanNetworkSequencing.kt sequences. Conflicts (two transitions wanting the same token) are resolved greedily in PetriConflict order.

  • PetriTiming.EVENT — one transition per tick, the first in conflict order. Interleaving semantics; useful when you want a net to walk rather than pulse.

  • PetriTiming.TIMED — firing takes time. A transition consumes its inputs at the instant it starts and produces its outputs duration later, so a token can be in flight, and a transition with dur = cyc(4) holds a four-cycle section open. Time advances to the next instant at which something happens, not on a grid.

In STEP and EVENT, duration does not affect token flow at all; it only sets how long the emitted event lasts. In all three, delay shifts the emitted event and nothing else, so you can nudge a hit late without perturbing the net's logic.

Why the trajectory is reproducible

PetriMusic.kt presents a net as a PatPattern, and a PatPattern has to be a pure function of time: the scheduler queries it cycle by cycle and every combinator in the language is free to query it again, out of order. That only works if the trajectory is reproducible, so

  • tokens are consumed FIFO, oldest first, never "some matching token";
  • PetriConflict.RANDOM hashes (seed, step index, transition name) rather than pulling from a stateful RNG, so the answer does not depend on how many times anything was asked;
  • PetriRun memoises, so replay is not merely reproducible but literally the same objects.

A net whose conflict policy is genuinely non-deterministic cannot be presented as a pattern at all. PetriLive performs one directly instead, rebuilding the run from the current marking whenever you interfere with it.

time

fun cyc(n: Int, d: Int = 1): PatQ = PatQ.of(n, d)

An exact rational number of cycles — cyc(1, 16) is a sixteenth. The time unit of every net.

tokens and markings

data class PetriToken(val colour: Any? = null, val born: PatQ = PatQ.ZERO)

One token. colour is the token's value and may be anything at all — null for the classical black token, a String sample name, an Int note, or a whole PatPattern when the net is being used as a song structure.

born is the instant the token was produced, which is what makes FIFO consumption meaningful and lets the visualizer age a token as it sits in a place.

data class PetriToken(val colour: Any? = null, val born: PatQ = PatQ.ZERO) {

val isBlack: Boolean get() = colour == null

True for the classical indistinguishable token.

inline fun <reified T> colourAs(): T? = colour as? T

The colour cast to T, or null if it is absent or another type.

override fun toString(): String = if (colour == null) "•" else "•($colour)"

fun blackToken(at: PatQ = PatQ.ZERO): PetriToken = PetriToken(null, at)

Shorthand for a black token born at at.

internal class SharedTokenList private constructor

The tokens in one place: an immutable list that shares its storage with the list it was appended to.

A marking is immutable and every PetriStep keeps one, so copying the target place's tokens on each PetriMarking.add made a net with an unbounded place cost O(n²) in the step count — copying a list that is one longer every time. Four thousand steps of a net that merely leaks one token per step was enough to exhaust a default heap, and a leaking net is precisely the one you want the analysis to survive long enough to name.

So appends share. Every list is the window 0 until size onto an array that only ever grows at its end, and appending writes past the end of the previous list instead of copying it. Three rules make that safe with no lock and no volatile on the read path:

  • a list only reads elements[0 until size], and every one of those slots was written before it was constructed, so elements being final is what publishes them (JLS 17.5, the final-field freeze) to any thread that can see the list at all;
  • appending happens under the buffer's own monitor, and only ever writes past every existing list's end, so no slot any list can already see is written twice;
  • appending to a list that is not the buffer's tip starts a fresh buffer, because two branches cannot both own the next slot. That is what a search branching from an older marking does, and it copies exactly as the old code did.

Growing the buffer replaces its array rather than resizing one in place, and each list keeps the array it was built in, so an older list is never made to read an array published after its own freeze. The arrays a run leaves behind are then the doubling sequence, which sums to O(n) — which is the whole point.

internal class SharedTokenList private constructor(
    private val buffer: Buffer,
    private val elements: Array<PetriToken?>,
    override val size: Int,
) : AbstractList<PetriToken>() {

The array behind one chain of appends, and how much of it is already spoken for.

    private class Buffer(var elements: Array<PetriToken?>, var fill: Int)

override fun get(index: Int): PetriToken

    override fun get(index: Int): PetriToken {
        if (index < 0 || index >= size) throw IndexOutOfBoundsException("index $index, size $size")
        return elements[index]!!
    }

fun append(tokens: List<PetriToken>): SharedTokenList

This list with tokens on the end, sharing this list's storage when it can.

    fun append(tokens: List<PetriToken>): SharedTokenList {
        if (tokens.isEmpty()) return this
        val length = size + tokens.size
        synchronized(buffer) {
            if (buffer.fill == size) {
                var array = buffer.elements
                if (length > array.size) {
                    array = array.copyOf(maxOf(MIN_CAPACITY, length * 2))
                    buffer.elements = array
                }
                for ((offset, token) in tokens.withIndex()) array[size + offset] = token
                buffer.fill = length
                return SharedTokenList(buffer, array, length)
            }
        }
        // Not the tip: another list already owns the next slot, so this branch needs its own array.
        // Sized exactly, with no slack — a branch is usually a search's leaf and never appended to
        // again, and there are a great many of them. The slack arrives on the first append that
        // wants it, which is what keeps a *chain* of appends amortised.
        val array = arrayOfNulls<PetriToken>(length)
        for (index in 0 until size) array[index] = elements[index]
        for ((offset, token) in tokens.withIndex()) array[size + offset] = token
        return SharedTokenList(Buffer(array, length), array, length)
    }

companion object

    companion object {
        private const val MIN_CAPACITY = 8

fun of(tokens: List<PetriToken>): SharedTokenList

tokens as a list that can be appended to cheaply; already one, and it is its own answer.

        fun of(tokens: List<PetriToken>): SharedTokenList {
            if (tokens is SharedTokenList) return tokens
            val array = arrayOfNulls<PetriToken>(tokens.size)
            for ((index, token) in tokens.withIndex()) array[index] = token
            return SharedTokenList(Buffer(array, tokens.size), array, tokens.size)
        }
    }
}

class PetriMarking private constructor(private val byPlace: Map<String, SharedTokenList>)

A marking: which tokens are in which place, in arrival order.

Empty places are not stored, so two markings compare equal exactly when they hold the same tokens in the same order — which is what the reachability search in PetriAnalysis.kt needs.

class PetriMarking private constructor(private val byPlace: Map<String, SharedTokenList>) {

companion object

val EMPTY = PetriMarking(emptyMap())

fun of(tokens: Map<String, List<PetriToken>>): PetriMarking

A marking from place name to tokens; empty entries are dropped.

        fun of(tokens: Map<String, List<PetriToken>>): PetriMarking =
            PetriMarking(tokens.filterValues { it.isNotEmpty() }.mapValues { SharedTokenList.of(it.value) })

fun counts(vararg counts: Pair<String, Int>, at: PatQ = PatQ.ZERO): PetriMarking

A marking of black tokens only — counts("kick" to 1, "hats" to 0).

        fun counts(vararg counts: Pair<String, Int>, at: PatQ = PatQ.ZERO): PetriMarking =
            of(counts.associate { (name, n) -> name to List(maxOf(0, n)) { blackToken(at) } })
    }

operator fun get(place: String): List<PetriToken> = byPlace[place] ?: emptyList()

The tokens in place, oldest first; empty if the place holds none.

fun count(place: String): Int = byPlace[place]?.size ?: 0

How many tokens are in place.

val occupied: Set<String> get() = byPlace.keys

Every place that currently holds at least one token.

val size: Int get() = byPlace.values.sumOf { it.size }

Total tokens across the whole net.

fun colours(place: String): List<Any?> = this[place].map { it.colour }

The colours in place, in arrival order — null entries are black tokens.

fun add(place: String, tokens: List<PetriToken>): PetriMarking

A copy with tokens appended to the back of place.

The one operation a running net does over and over, and the one that used to make an unbounded place quadratic — see SharedTokenList for what it shares and when it cannot.

    fun add(place: String, tokens: List<PetriToken>): PetriMarking {
        if (tokens.isEmpty()) return this
        val grown = byPlace[place]?.append(tokens) ?: SharedTokenList.of(tokens)
        return PetriMarking(byPlace + (place to grown))
    }

internal fun removeAt(place: String, indices: Set<Int>): PetriMarking

A copy with exactly tokens removed from place, matched by identity of position.

    internal fun removeAt(place: String, indices: Set<Int>): PetriMarking {
        if (indices.isEmpty()) return this
        val remaining = this[place].filterIndexed { index, _ -> index !in indices }
        return if (remaining.isEmpty()) PetriMarking(byPlace - place)
        else PetriMarking(byPlace + (place to SharedTokenList.of(remaining)))
    }

fun withPlace(place: String, tokens: List<PetriToken>): PetriMarking

A copy with place set to exactly tokens.

    fun withPlace(place: String, tokens: List<PetriToken>): PetriMarking =
        if (tokens.isEmpty()) PetriMarking(byPlace - place)
        else PetriMarking(byPlace + (place to SharedTokenList.of(tokens)))

fun toMap(): Map<String, List<PetriToken>> = LinkedHashMap(byPlace)

The whole marking as a plain map — a defensive copy, safe to keep.

fun toCounts(): Map<String, Int> = byPlace.mapValues { (_, tokens) -> tokens.size }

The marking as counts only, which is what the analysis layer works in.

fun signature(): String

A stable identity for recurrence detection: places, and the colours in them, but not the instants those tokens were born.

Birth times are what make two otherwise identical markings unequal, and a net whose markings are never equal has no detectable period — every bar would look brand new. Colours are compared by equality, so a section swap that substitutes one pattern for another is a change, and the same pattern object coming round again is a recurrence.

    fun signature(): String = byPlace.entries
        .sortedBy { it.key }
        .joinToString(";") { (place, tokens) ->
            "$place=" + tokens.map { colourKey(it) }.sorted().joinToString(",")
        }

fun signatureHash(): Long

signature as a 64-bit number.

Recurrence detection asks "have I been here before?" once per step, and answering it with the signature string means keeping a string as long as the marking for every step — the same O(n²), now measured in characters. So the hash is what PetriRun keeps, and the string is built only to confirm a hit, of which there is at most one.

Terms are mixed and then summed rather than hashed in sequence, because signature sorts the colours within a place and the places by name, and a sum does not care what order it is given its terms in. Equal signatures therefore always hash equally, which is the direction that has to hold; unequal ones almost always differ, and the caller checks rather than trusts.

    fun signatureHash(): Long {
        var total = 0L
        for ((place, tokens) in byPlace) {
            var here = 1L
            for (token in tokens) here += splitmix64(colourKey(token).hashCode().toLong())
            total += splitmix64(splitmix64(place.hashCode().toLong()) xor here)
        }
        return total
    }

How signature and signatureHash both see a token: its colour by equality (its hashCode, with the rendering for reading), birth time dropped. Two different patterns that both print as PatPattern(...) are two different colours; the same pattern object fired again is one.

    private fun colourKey(token: PetriToken): String =
        token.colour?.let { "${it.hashCode().toString(16)}:$it" } ?: "•"

override fun equals(other: Any?): Boolean = other is PetriMarking && other.byPlace == byPlace

override fun hashCode(): Int = byPlace.hashCode()

override fun toString(): String

    override fun toString(): String =
        if (byPlace.isEmpty()) "∅"
        else byPlace.entries.sortedBy { it.key }.joinToString(", ") { (place, tokens) ->
            "$place:${tokens.size}" + if (tokens.any { !it.isBlack }) tokens.joinToString(prefix = "[", postfix = "]") { "${it.colour}" } else ""
        }
}

the net

data class PetriPlace(val name: String, val capacity: Int? = null)

A place. capacity of null is unbounded; a bounded place disables any transition that would overfill it.

init

    init {
        require(name.isNotBlank()) { "A place needs a name" }
        require(capacity == null || capacity > 0) { "Place '$name' capacity must be > 0 or null (unbounded)" }
    }
}

enum class PetriArcKind

What an input arc does to the tokens it looks at.

enum class PetriArcKind {

Requires and consumes weight tokens. The ordinary arc.

    NORMAL,

Requires weight tokens but consumes none — a test arc. Written &p in the notation.

    READ,

Requires fewer than weight tokens. Written ~p. "Not while that is armed."

    INHIBIT,
}

class PetriInput

An input arc: what a transition needs from a place, and which tokens count.

guard filters by colour — from("notes", guard = { (it.colour as? Int ?: 0) > 60 }) consumes only high notes. Guards apply to all three PetriArcKinds: an inhibitor arc with a guard means "not while that place holds a token of this kind".

class PetriInput(
    val place: String,
    val weight: Int = 1,
    val kind: PetriArcKind = PetriArcKind.NORMAL,
    val guard: ((PetriToken) -> Boolean)? = null,
) {

init { require(weight >= 1) { "Arc weight must be >= 1 (place '$place')" } }

internal fun accepts(token: PetriToken): Boolean = guard?.invoke(token) ?: true

override fun toString(): String

    override fun toString(): String = buildString {
        when (kind) {
            PetriArcKind.NORMAL -> {}
            PetriArcKind.READ -> append('&')
            PetriArcKind.INHIBIT -> append('~')
        }
        if (weight != 1) append("$weight*")
        append(place)
    }
}

class PetriOutput

An output arc: how many tokens a transition puts into a place, and what colour they are.

When produce is null the transition's PetriColourFlow decides. That default is the reason pattern-valued tokens work without ceremony: CARRY threads the consumed colours through, so a PatPattern that enters a net comes out the other side unless something deliberately changes it.

class PetriOutput(
    val place: String,
    val weight: Int = 1,
    val produce: ((PetriBinding) -> List<PetriToken>)? = null,
) {

init { require(weight >= 1) { "Arc weight must be >= 1 (place '$place')" } }

override fun toString(): String = if (weight == 1) place else "$weight*$place"

enum class PetriColourFlow

What colour a transition's output tokens take when an output arc has no explicit produce.

enum class PetriColourFlow {

Always produce black tokens. The classical place/transition net.

    BLACK,

Thread the consumed colours through: output token i takes consumed colour i, cycling if the counts differ, and black if nothing was consumed. Degenerates to BLACK for a black net, so it is the default.

    CARRY,
}

class PetriTransition

A transition.

duration and delay are both in cycles. delay shifts the emitted event only — it never changes when tokens move — so it is how you humanise or swing a hit. duration sets the emitted event's length in every timing, and additionally holds the tokens in flight under PetriTiming.TIMED.

emit is what the firing sounds; emitOf computes it from the binding when the answer depends on which tokens were consumed, and wins over emit when both are set.

class PetriTransition(
    val name: String,
    val inputs: List<PetriInput> = emptyList(),
    val outputs: List<PetriOutput> = emptyList(),
    val duration: PatQ = PatQ.ZERO,
    val delay: PatQ = PatQ.ZERO,
    /** Higher fires first under [PetriConflict.PRIORITY]. */
    val priority: Int = 0,
    /** Relative likelihood under [PetriConflict.RANDOM]. Must be > 0. */
    val weight: Double = 1.0,
    val emit: Any? = null,
    val emitOf: ((PetriBinding) -> Any?)? = null,
    /** A final veto once the tokens are chosen — the place for cross-place conditions. */
    val enabledIf: ((PetriBinding) -> Boolean)? = null,
    val colourFlow: PetriColourFlow = PetriColourFlow.CARRY,
) {

init

    init {
        require(name.isNotBlank()) { "A transition needs a name" }
        require(duration >= PatQ.ZERO) { "Transition '$name' duration must be >= 0" }
        require(weight > 0.0 && weight.isFinite()) { "Transition '$name' weight must be finite and > 0" }
    }

val consumes: List<PetriInput> get() = inputs.filter { it.kind == PetriArcKind.NORMAL }

The places this transition consumes from — PetriArcKind.NORMAL inputs only.

override fun toString(): String

    override fun toString(): String {
        val pre = inputs.joinToString(" + ").ifEmpty { "∅" }
        val post = outputs.joinToString(" + ").ifEmpty { "∅" }
        return "$pre -[ $name${if (duration > PatQ.ZERO) " @$duration" else ""}${emit?.let { " : $it" } ?: ""} ]-> $post"
    }
}

enum class PetriConflict

How a maximal step picks between transitions competing for the same tokens.

enum class PetriConflict {

Declaration order. Predictable and boring, which is often what you want.

    ORDER,

Highest PetriTransition.priority first, declaration order breaking ties. The default.

    PRIORITY,

Rotate the declaration order by the step index, so nobody starves.

    ROUND_ROBIN,

A deterministic shuffle hashed from (seed, step index), biased by PetriTransition.weight.

    RANDOM,
}

enum class PetriTiming { STEP, EVENT, TIMED }

See the file header: STEP is a drum machine, EVENT walks, TIMED holds sections open.

class PetriNet

A net: places, transitions, an initial marking, and the semantics under which it runs.

Nets are immutable. withMarking and withTiming give you a variant, which is what live coding does between evaluations.

class PetriNet(
    val places: List<PetriPlace>,
    val transitions: List<PetriTransition>,
    val initial: PetriMarking = PetriMarking.EMPTY,
    val timing: PetriTiming = PetriTiming.STEP,
    /** The tick for [PetriTiming.STEP] and [PetriTiming.EVENT], and the idle advance for TIMED. */
    val grid: PatQ = PatQ.of(1, 16),
    val conflict: PetriConflict = PetriConflict.PRIORITY,
    val seed: Int = 0,
) {

init

    init {
        require(grid > PatQ.ZERO) { "grid must be > 0" }
        val duplicatePlace = places.groupBy { it.name }.entries.firstOrNull { it.value.size > 1 }
        require(duplicatePlace == null) { "Duplicate place '${duplicatePlace?.key}'" }
        val duplicateTransition = transitions.groupBy { it.name }.entries.firstOrNull { it.value.size > 1 }
        require(duplicateTransition == null) { "Duplicate transition '${duplicateTransition?.key}'" }
        val known = places.map { it.name }.toSet()
        for (transition in transitions) {
            for (arc in transition.inputs) require(arc.place in known) {
                "Transition '${transition.name}' reads undeclared place '${arc.place}'"
            }
            for (arc in transition.outputs) require(arc.place in known) {
                "Transition '${transition.name}' writes undeclared place '${arc.place}'"
            }
        }
    }

    private val placeIndex: Map<String, PetriPlace> = places.associateBy { it.name }
    private val transitionIndex: Map<String, PetriTransition> = transitions.associateBy { it.name }

fun place(name: String): PetriPlace? = placeIndex[name]

The place called name, or null.

fun transition(name: String): PetriTransition? = transitionIndex[name]

The transition called name, or null.

val placeNames: List<String> get() = places.map { it.name }

The names of every place, in declaration order.

val transitionNames: List<String> get() = transitions.map { it.name }

The names of every transition, in declaration order.

fun withMarking(marking: PetriMarking): PetriNet

    fun withMarking(marking: PetriMarking): PetriNet =
        PetriNet(places, transitions, marking, timing, grid, conflict, seed)

fun withTiming(timing: PetriTiming = this.timing, grid: PatQ = this.grid): PetriNet

    fun withTiming(timing: PetriTiming = this.timing, grid: PatQ = this.grid): PetriNet =
        PetriNet(places, transitions, initial, timing, grid, conflict, seed)

fun withConflict(conflict: PetriConflict = this.conflict, seed: Int = this.seed): PetriNet

    fun withConflict(conflict: PetriConflict = this.conflict, seed: Int = this.seed): PetriNet =
        PetriNet(places, transitions, initial, timing, grid, conflict, seed)

fun run

A fresh memoised trajectory from from (the net's own initial marking by default).

Runs are cheap to make and expensive to keep filling, so hold one for as long as you want the same performance and make a new one when the marking should reset.

    fun run(
        from: PetriMarking = initial,
        startAt: PatQ = PatQ.ZERO,
        maxUnroll: Int = DEFAULT_MAX_UNROLL,
        maxTokens: Int = DEFAULT_MAX_TOKENS,
    ): PetriRun = PetriRun(this, from, startAt, maxUnroll, maxTokens)

override fun toString(): String

    override fun toString(): String = buildString {
        append("PetriNet(${places.size} places, ${transitions.size} transitions, $timing @$grid)\n")
        append("  marking $initial\n")
        transitions.forEach { append("  $it\n") }
    }

companion object

    companion object {

const val DEFAULT_MAX_UNROLL: Int = 200_000

How many steps a run will replay before it refuses. See the file header on purity.

const val DEFAULT_MAX_TOKENS: Int = 4_096

How many tokens one place may hold before a run stops with PetriHalt.FLOODED.

Generous enough that no net anyone writes on purpose meets it — a place holding four thousand tokens is leaking, not counting — and small enough that the run stops while its markings are still cheap to hash, which is what keeps a runaway net from turning maxUnroll steps into quadratic work. Raise it per-run if you really are counting.

firing

class PetriBinding

The tokens a transition is about to consume, and where they came from.

Passed to guards, to emitOf, and to every output arc's produce, so a transition's output can depend on its input — which is how a net does pattern algebra rather than mere token counting.

class PetriBinding(
    val transition: String,
    /** The instant the transition fires. */
    val at: PatQ,
    /** The 0-based cycle containing [at]. */
    val cycle: Long,
    /** Tokens about to be consumed, in input-arc declaration order. READ arcs are not included. */
    val consumed: List<PetriToken>,
    /** Every token this binding looked at, keyed by place — including the ones READ arcs only tested. */
    val byPlace: Map<String, List<PetriToken>>,
) {

operator fun get(place: String): List<PetriToken> = byPlace[place] ?: emptyList()

Tokens taken from place (empty if none).

fun colour(index: Int = 0): Any? = consumed.getOrNull(index)?.colour

The index-th consumed colour, or null.

inline fun <reified T> colourAs(index: Int = 0): T? = colour(index) as? T

The index-th consumed colour cast to T, or null.

inline fun <reified T> colours(): List<T> = consumed.mapNotNull { it.colour as? T }

Every consumed colour that is a T, in order — the usual way to reach pattern-valued tokens.

fun token(colour: Any?): PetriToken = PetriToken(colour, at)

One token of colour, born now. Sugar for output arcs.

override fun toString(): String = "PetriBinding($transition@$at, consumed=$consumed)"

data class PetriFiring

One transition firing: when it happened, what it moved, and what it sounds.

arc already has delay and duration applied, so it is the span the event occupies and can be handed straight to the pattern layer. at is when the net's logic actually fired, which is not the same instant if delay is non-zero.

data class PetriFiring(
    val transition: String,
    val at: PatQ,
    val arc: PatArc,
    val cycle: Long,
    val consumed: List<PetriToken>,
    val produced: List<PetriToken>,
    val emit: Any? = null,
    /** Monotone across a whole run — a firing's identity. */
    val index: Long = 0,
) {

override fun toString(): String

    override fun toString(): String =
        "PetriFiring($transition @$at${emit?.let { " : $it" } ?: ""}, ${consumed.size}→${produced.size})"
}

data class PetriStep

One instant of a run: everything that happened at at, and the marking either side of it.

A STEP tick with nothing enabled does not produce a step — it produces a deadlock, because in step semantics a marking that enables nothing now will never enable anything.

data class PetriStep(
    val index: Long,
    val at: PatQ,
    val before: PetriMarking,
    val after: PetriMarking,
    val firings: List<PetriFiring>,
) {

val quiet: Boolean get() = firings.isEmpty()

True when the marking is unchanged — only possible for a TIMED step that merely completed.

override fun toString(): String

    override fun toString(): String =
        "PetriStep(#$index @$at, ${firings.joinToString { it.transition }.ifEmpty { "—" }}, $after)"
}

enum class PetriHalt

Why a run stopped, when it did.

enum class PetriHalt {

Still going.

    RUNNING,

Nothing is enabled and nothing is in flight. The net is stuck for good.

    DEADLOCK,

The run hit its maxUnroll ceiling. Not a property of the net — a property of the query.

    EXHAUSTED,

A place passed the run's maxTokens ceiling, and PetriRun.floodedPlace says which.

Not a proof that the place is unbounded — that is a coverability question and this is a measurement. But a place holding thousands of tokens is leaking rather than accumulating, and a run that carries on pays for a marking that size on every step it has left, so stopping and naming the place is worth more than continuing.

    FLOODED,
}

data class PetriLasso

A trajectory that has started repeating: a run-in of tailSteps, then a loop of loopSteps lasting duration.

duration is the answer to "how long is this net's bar?" — measured from the trajectory rather than assumed from the grid, which is why a net built out of a five-step ring and a three-step ring reports fifteen rather than either.

data class PetriLasso(
    /** How many steps happen once, before the loop. */
    val tailSteps: Int,
    /** How many steps the loop is. */
    val loopSteps: Int,
    /** The instant the loop's first step happens at. */
    val startsAt: PatQ,
    /** How long one turn of the loop takes, in cycles. The net's own bar length. */
    val duration: PatQ,
    /** How many times each transition fires per turn — a realised T-invariant. */
    val firingCounts: Map<String, Int>,
) {

override fun toString(): String =

        "PetriLasso(tail=$tailSteps steps, loop=$loopSteps steps = $duration cycles, $firingCounts)"
}

A run's state after one step, compressed enough to be worth keeping one of per step: the marking hashed, and whatever is still in flight written out in full because there is never much of it.

See PetriRun.lasso for where the hash gets checked against the marking it came from.

private class PetriStateKey(val markingHash: Long, val inFlight: String)

A transition's outputs waiting to land, under PetriTiming.TIMED.

private class PetriPending(
    val due: PatQ,
    val place: String,
    val tokens: List<PetriToken>,
    val order: Long,
)

class PetriRun internal constructor

A deterministic, memoised, append-only trajectory through a net.

This is the object the pattern layer sits on. Every query extends the trajectory as far as it needs and never rewinds, so asking about cycle 3, then cycle 1, then cycle 3 again returns the same steps all three times. That is what lets net.pattern() satisfy PatPattern's contract — see the file header.

Not thread-safe by accident: every extension is under a lock, because the pattern scheduler and the visualizer will query the same run from different threads.

class PetriRun internal constructor(
    val net: PetriNet,
    val from: PetriMarking,
    val startAt: PatQ = PatQ.ZERO,
    val maxUnroll: Int = PetriNet.DEFAULT_MAX_UNROLL,
    val maxTokens: Int = PetriNet.DEFAULT_MAX_TOKENS,
) {
    private val lock = Any()
    private val steps = mutableListOf<PetriStep>()
    private val pending = mutableListOf<PetriPending>()

One key per materialised step, index for index with steps: the marking, plus whatever is still in flight expressed as an offset from the instant the run has reached.

Recorded as the run advances because it cannot be reconstructed afterwards — pending is mutable state, not part of a PetriStep, and a TIMED net with a token in flight has a different future from the same marking with nothing in flight.

The marking is hashed rather than spelled out so that a step costs a constant amount of retained memory whatever the marking's size. See PetriMarking.signatureHash.

    private val stepKeys = mutableListOf<PetriStateKey>()

    private var cursor: PatQ = startAt
    private var marking: PetriMarking = from
    private var firingCounter: Long = 0
    private var pendingCounter: Long = 0
    private var halted: PetriHalt = PetriHalt.RUNNING
    private var flooded: String? = null

val halt: PetriHalt get() = synchronized(lock) { halted }

Why the run stopped, or PetriHalt.RUNNING if it has not. Only meaningful after a query.

val floodedPlace: String? get() = synchronized(lock) { flooded }

The place that passed maxTokens, when that is why the run stopped, and null otherwise.

The name of the leak, which is usually the whole answer: a place that only fills is a missing output arc.

val materialised: Int get() = synchronized(lock) { steps.size }

How many steps have been materialised so far.

val reach: PatQ get() = synchronized(lock) { cursor }

The instant the trajectory currently reaches.

fun steps(count: Int): List<PetriStep>

The first count steps, extending the trajectory if needed. Shorter if the net halts.

    fun steps(count: Int): List<PetriStep> = synchronized(lock) {
        while (steps.size < count && halted == PetriHalt.RUNNING) advanceLocked()
        steps.take(count)
    }

fun stepsUntil(instant: PatQ): List<PetriStep>

Every step strictly before instant.

    fun stepsUntil(instant: PatQ): List<PetriStep> = synchronized(lock) {
        extendToLocked(instant)
        steps.filter { it.at < instant }
    }

fun stepsIn(from: PatQ, until: PatQ): List<PetriStep>

Every step whose instant lies in [from, until).

    fun stepsIn(from: PatQ, until: PatQ): List<PetriStep> = synchronized(lock) {
        extendToLocked(until)
        steps.filter { it.at >= from && it.at < until }
    }

fun firingsOver(arc: PatArc): List<PetriFiring>

Every firing whose event arc intersects arc.

Not the same question as "every firing that happened in this window": a transition with a long duration is still sounding after it fired, and the pattern layer needs it back. The trajectory is extended past arc.end by the longest transition duration in the net so a firing that started earlier and reaches into the window is not missed.

    fun firingsOver(arc: PatArc): List<PetriFiring> = synchronized(lock) {
        extendToLocked(arc.end)
        steps.asSequence()
            .flatMap { it.firings }
            .filter { it.arc.intersect(arc) != null }
            .toList()
    }

fun markingAt(instant: PatQ): PetriMarking

The marking as it stood immediately before instant.

Binary search, not a scan: the signal layer asks this question once per query per place, and a run that has been playing for a while has a lot of steps behind it.

    fun markingAt(instant: PatQ): PetriMarking = synchronized(lock) {
        extendToLocked(instant)
        lastStepBeforeLocked(instant)?.after ?: from
    }

fun countAt(place: String, instant: PatQ): Int = markingAt(instant).count(place)

How many tokens were in place at instant. The raw material for a control signal.

fun changes(place: String, until: PatQ): List<Pair<PatQ, Int>>

Every instant at which place's token count changed, up to until, with the count it changed to. The first entry is always startAt and the initial count, so the list is total.

This is what an interpolated control signal reads: the raw marking is a step function and the interpolators need to know where the steps are.

    fun changes(place: String, until: PatQ): List<Pair<PatQ, Int>> = synchronized(lock) {
        extendToLocked(until)
        val out = mutableListOf(startAt to from.count(place))
        for (step in steps) {
            if (step.at >= until) break
            val count = step.after.count(place)
            if (count != out.last().second) out += step.at to count
        }
        out
    }

The state the run is in after the step just appended: the marking, plus everything still in flight written as an offset from the instant the run has now reached, so the key is about shape rather than absolute position.

    private fun stateKeyLocked(): PetriStateKey {
        val flight = pending
            .map { "${(it.due - cursor)}@${it.place}x${it.tokens.size}" }
            .sorted()
            .joinToString(",")
        return PetriStateKey(marking.signatureHash(), flight)
    }

The last materialised step strictly before instant, by binary search over at.

    private fun lastStepBeforeLocked(instant: PatQ): PetriStep? {
        var low = 0
        var high = steps.size - 1
        var found: PetriStep? = null
        while (low <= high) {
            val mid = (low + high) ushr 1
            if (steps[mid].at < instant) {
                found = steps[mid]
                low = mid + 1
            } else {
                high = mid - 1
            }
        }
        return found
    }

fun lasso(maxSteps: Int = 4_096): PetriLasso?

Where the run settles: how long before it starts repeating, and how long the repeat is.

With a deterministic conflict policy a net has exactly one future, so its trajectory is a lasso — a run-in followed by a loop, or a run-in followed by a wall. That makes the musically interesting question cheap to answer: the loop's duration is the net's own bar length, discovered rather than declared.

Returns null if the run neither repeats nor stops within maxSteps — which for a net that keeps minting fresh colours it never will, since a marking it has never held before cannot be one it is returning to.

A PetriStateKey holds the marking as a hash, so a match is a candidate: it is confirmed against the real signatures before it is believed. There is at most one signature pair to build, because a confirmed match returns and an unconfirmed one is a hash collision, which over a 64-bit mix is not something that happens.

    fun lasso(maxSteps: Int = 4_096): PetriLasso? = synchronized(lock) {
        val limit = minOf(maxSteps, maxUnroll)
        while (steps.size < limit && halted == PetriHalt.RUNNING) advanceLocked()
        check(steps.size == stepKeys.size) { "a step was materialised without its recurrence key" }

        val seen = HashMap<Long, MutableList<Int>>()
        for ((index, key) in stepKeys.withIndex()) {
            val candidates = seen.getOrPut(key.markingHash) { mutableListOf() }
            val earlier = if (candidates.isEmpty()) null else {
                val signature = steps[index].after.signature()
                candidates.firstOrNull { other ->
                    stepKeys[other].inFlight == key.inFlight && steps[other].after.signature() == signature
                }
            }
            if (earlier == null) {
                candidates += index
                continue
            }
            return PetriLasso(
                tailSteps = earlier + 1,
                loopSteps = index - earlier,
                startsAt = steps[earlier + 1].at,
                duration = steps[index].at - steps[earlier].at,
                firingCounts = steps.subList(earlier + 1, index + 1)
                    .flatMap { it.firings }
                    .groupingBy { it.transition }
                    .eachCount(),
            )
        }
        null
    }

fun reset()

Drop every materialised step and start again from the initial marking.

    fun reset() = synchronized(lock) {
        steps.clear()
        stepKeys.clear()
        pending.clear()
        cursor = startAt
        marking = from
        firingCounter = 0
        pendingCounter = 0
        halted = PetriHalt.RUNNING
        flooded = null
    }

override fun toString(): String

    override fun toString(): String =
        "PetriRun(${net.transitions.size} transitions, ${materialised} steps to $reach, $halt)"

the engine

The longest transition duration — how far past a query we must look for still-sounding firings.

    private val lookahead: PatQ =
        net.transitions.fold(PatQ.ZERO) { acc, t -> if (t.duration + t.delay > acc) t.duration + t.delay else acc }

    private fun extendToLocked(instant: PatQ) {
        val target = instant + lookahead
        while (halted == PetriHalt.RUNNING && cursor < target) advanceLocked()
    }

    private fun advanceLocked() {
        if (steps.size >= maxUnroll) {
            halted = PetriHalt.EXHAUSTED
            return
        }
        when (net.timing) {
            PetriTiming.STEP -> advanceGridLocked(maximal = true)
            PetriTiming.EVENT -> advanceGridLocked(maximal = false)
            PetriTiming.TIMED -> advanceTimedLocked()
        }
        // Checked after the step rather than before it, so that the marking which overflowed is the
        // one you get to look at — that being the point of knowing.
        if (halted == PetriHalt.RUNNING) {
            flooded = marking.occupied.firstOrNull { marking.count(it) > maxTokens }
            if (flooded != null) halted = PetriHalt.FLOODED
        }
    }

STEP and EVENT. Everything fires against the marking as it stood at the tick's start and the produced tokens land only once the tick is over, so a chain of transitions takes a tick each rather than collapsing into one instant.

    private fun advanceGridLocked(maximal: Boolean) {
        val at = cursor
        val before = marking
        var working = marking
        val firings = mutableListOf<PetriFiring>()
        val produced = mutableListOf<Pair<String, List<PetriToken>>>()

        for (transition in orderedTransitions(steps.size.toLong())) {
            val bound = bind(transition, working, before, at) ?: continue
            val out = producedTokens(transition, bound.binding)
            if (!capacityAllows(working, produced + out)) continue
            working = bound.consumeFrom(working)
            produced += out
            firings += firing(transition, bound.binding, out.flatMap { it.second })
            if (!maximal) break
        }

        if (firings.isEmpty()) {
            halted = PetriHalt.DEADLOCK
            return
        }

        for ((place, tokens) in produced) working = working.add(place, tokens)
        marking = working
        steps += PetriStep(steps.size.toLong(), at, before, working, firings)
        cursor = at + net.grid
        stepKeys += stateKeyLocked()
    }

TIMED. An instant is interesting if something completes there or something can start there; time jumps to the next such instant rather than walking a grid.

source — 82 lines, from line 978 
    private fun advanceTimedLocked() {
        var guard = 0
        while (true) {
            val at = cursor
            val before = marking
            var working = marking

            val due = pending.filter { it.due <= at }.sortedBy { it.order }
            if (due.isNotEmpty()) {
                pending.removeAll(due.toSet())
                for (entry in due) working = working.add(entry.place, entry.tokens)
            }

            // Tests (read and inhibitor arcs) are answered against the marking as it stands at the
            // *start* of this instant, after completions have landed but before anything fires.
            val atInstant = working

            val firings = mutableListOf<PetriFiring>()
            for (transition in orderedTransitions(steps.size.toLong())) {
                val bound = bind(transition, working, atInstant, at) ?: continue
                val out = producedTokens(transition, bound.binding)
                // Only immediate production can overfill a place right now; a delayed production
                // is checked again when it lands, because the marking will have moved on by then.
                if (transition.duration <= PatQ.ZERO && !capacityAllows(working, out)) continue
                working = bound.consumeFrom(working)
                val landing = at + transition.duration
                if (transition.duration <= PatQ.ZERO) {
                    for ((place, tokens) in out) working = working.add(place, tokens)
                } else {
                    for ((place, tokens) in out) pending += PetriPending(landing, place, tokens, pendingCounter++)
                }
                firings += firing(transition, bound.binding, out.flatMap { it.second })
            }

            if (firings.isNotEmpty() || due.isNotEmpty()) {
                marking = working
                steps += PetriStep(steps.size.toLong(), at, before, working, firings)
                cursor = pending.minOfOrNull { it.due }?.takeIf { it > at } ?: (at + net.grid)
                stepKeys += stateKeyLocked()
                return
            }

            // Nothing at this instant. Jump to the next thing in flight, or admit defeat.
            val next = pending.minOfOrNull { it.due }
            if (next == null || next <= at) {
                halted = PetriHalt.DEADLOCK
                return
            }
            cursor = next
            if (++guard > MAX_IDLE_JUMPS) {
                halted = PetriHalt.EXHAUSTED
                return
            }
        }
    }

    private fun firing(transition: PetriTransition, binding: PetriBinding, produced: List<PetriToken>): PetriFiring {
        val start = binding.at + transition.delay
        val length = if (transition.duration > PatQ.ZERO) transition.duration else net.grid
        return PetriFiring(
            transition = transition.name,
            at = binding.at,
            arc = PatArc(start, start + length),
            cycle = qFloorLong(binding.at),
            consumed = binding.consumed,
            produced = produced,
            emit = transition.emitOf?.invoke(binding) ?: transition.emit,
            index = firingCounter++,
        )
    }

    private fun bind(
        transition: PetriTransition,
        available: PetriMarking,
        tested: PetriMarking,
        at: PatQ,
    ): PetriBound? = petriBind(transition, available, tested, at)

    private fun producedTokens(
        transition: PetriTransition,
        binding: PetriBinding,
    ): List<Pair<String, List<PetriToken>>> = petriProduce(transition, binding)

Would landing adding on top of marking overfill a bounded place?

The caller passes everything the step has promised so far, not just this transition's share, because in a maximal step two transitions can each fit and still overflow together.

    private fun capacityAllows(marking: PetriMarking, adding: List<Pair<String, List<PetriToken>>>): Boolean {
        val extra = HashMap<String, Int>()
        for ((place, tokens) in adding) extra[place] = (extra[place] ?: 0) + tokens.size
        for ((place, count) in extra) {
            val capacity = net.place(place)?.capacity ?: continue
            if (marking.count(place) + count > capacity) return false
        }
        return true
    }

The order conflicts are resolved in for the step numbered step.

    private fun orderedTransitions(step: Long): List<PetriTransition> = when (net.conflict) {
        PetriConflict.ORDER -> net.transitions
        PetriConflict.PRIORITY -> net.transitions.sortedByDescending { it.priority }
        PetriConflict.ROUND_ROBIN -> {
            val all = net.transitions
            if (all.isEmpty()) all
            else {
                val offset = (step.mod(all.size.toLong())).toInt()
                all.drop(offset) + all.take(offset)
            }
        }
        PetriConflict.RANDOM -> net.transitions.sortedBy { transition ->
            // A weighted deterministic shuffle: exponential race, hashed rather than sampled, so
            // the order depends only on (seed, step, name) and never on call history.
            val hash = splitmix64(
                net.seed.toLong() * 0x9E3779B97F4A7C15uL.toLong() xor
                    (step * 0x2545F4914F6CDD1DuL.toLong()) xor
                    transition.name.hashCode().toLong()
            )
            -Math.log(1.0 - toUnitDouble(hash).coerceIn(1e-12, 1.0 - 1e-12)) / transition.weight
        }
    }

    private companion object {
        /** How many empty instants a TIMED run will skip before it calls the query exhausted. */
        const val MAX_IDLE_JUMPS = 1024
    }
}

enabling, shared by the engine, the live runtime and the visualizer

internal class PetriBound(val binding: PetriBinding, private val claimed: Map<String, Set<Int>>)

A binding plus the exact token positions it claimed, so consumption is unambiguous.

fun consumeFrom(marking: PetriMarking): PetriMarking

    fun consumeFrom(marking: PetriMarking): PetriMarking {
        var working = marking
        for ((place, indices) in claimed) working = working.removeAt(place, indices)
        return working
    }
}

internal fun petriBind

Chooses the tokens transition would consume from available, or null if it is not enabled.

Tokens are taken oldest first from each place; guards filter which ones count. READ arcs are tested but their tokens are not consumed, and inhibitor arcs are satisfied by scarcity.

The two markings are not the same question. Consumption reads available, which shrinks as earlier transitions in the same step claim tokens — that is how conflict is resolved. Tests read tested, the marking as it stood at the start of the instant, so that disarming a place and acting on it being disarmed cannot happen in one tick. Without that split, an inhibitor arc turns a step boundary back into a cascade.

Claims are tracked as positions, not values, so two arcs reading the same place with different guards cannot both claim the same token and identical tokens are never confused.

body — 41 lines, from line 1133 
internal fun petriBind(
    transition: PetriTransition,
    available: PetriMarking,
    tested: PetriMarking,
    at: PatQ,
): PetriBound? {
    val consumed = mutableListOf<PetriToken>()
    val looked = LinkedHashMap<String, List<PetriToken>>()
    val claimed = HashMap<String, MutableSet<Int>>()

    for (arc in transition.inputs) {
        when (arc.kind) {
            PetriArcKind.INHIBIT -> {
                if (tested[arc.place].count { arc.accepts(it) } >= arc.weight) return null
            }
            PetriArcKind.READ -> {
                // A read arc only tests, so it neither claims positions nor respects claims: a
                // token can be read and consumed in the same firing, which is what "test" means.
                // It does not join `consumed`.
                val matching = tested[arc.place].filter { arc.accepts(it) }
                if (matching.size < arc.weight) return null
                looked[arc.place] = (looked[arc.place] ?: emptyList()) + matching.take(arc.weight)
            }
            PetriArcKind.NORMAL -> {
                val here = available[arc.place]
                val taken = claimed.getOrPut(arc.place) { linkedSetOf() }
                val free = here.indices.filter { it !in taken && arc.accepts(here[it]) }
                if (free.size < arc.weight) return null
                val take = free.take(arc.weight)
                taken += take
                val tokens = take.map { here[it] }
                consumed += tokens
                looked[arc.place] = (looked[arc.place] ?: emptyList()) + tokens
            }
        }
    }

    val binding = PetriBinding(transition.name, at, qFloorLong(at), consumed, looked)
    if (transition.enabledIf?.invoke(binding) == false) return null
    return PetriBound(binding, claimed)
}

internal fun petriProduce

The tokens each output arc contributes, before they are placed.

internal fun petriProduce(
    transition: PetriTransition,
    binding: PetriBinding,
): List<Pair<String, List<PetriToken>>> = transition.outputs.map { arc ->
    val tokens = arc.produce?.invoke(binding) ?: petriDefaultProduction(transition, binding, arc)
    arc.place to tokens
}

private fun petriDefaultProduction(
    transition: PetriTransition,
    binding: PetriBinding,
    arc: PetriOutput,
): List<PetriToken> = when (transition.colourFlow) {
    PetriColourFlow.BLACK -> List(arc.weight) { PetriToken(null, binding.at) }
    PetriColourFlow.CARRY ->
        if (binding.consumed.isEmpty()) List(arc.weight) { PetriToken(null, binding.at) }
        else List(arc.weight) { index ->
            PetriToken(binding.consumed[index % binding.consumed.size].colour, binding.at)
        }
}

fun PetriNet.enabled(marking: PetriMarking = initial, at: PatQ = PatQ.ZERO): List<String>

Which transitions could fire against marking, ignoring conflict — two transitions can both be listed here and still not both fire, because they may want the same token.

This is what the visualizer highlights and what a live runtime offers as the set of things you could force. Capacity is not checked, because a transition blocked only by a full output place is still enabled in the usual sense of the word.

fun PetriNet.enabled(marking: PetriMarking = initial, at: PatQ = PatQ.ZERO): List<String> =
    transitions.filter { petriBind(it, marking, marking, at) != null }.map { it.name }

internal fun qFloorLong(q: PatQ): Long

floor(q) as a Long — the cycle a rational instant falls in.

internal fun qFloorLong(q: PatQ): Long {
    val (quotient, remainder) = q.n.divideAndRemainder(q.d)
    val floored = if (remainder.signum() < 0) quotient.subtract(java.math.BigInteger.ONE) else quotient
    return floored.toLong()
}

the builder

class PetriBuilder internal constructor()

Builds a net. Places are auto-declared the first time a transition mentions them, so you only write place when you want an initial marking, a capacity, or coloured tokens.

val net = petri {
    timing = PetriTiming.STEP
    grid = cyc(1, 16)
    place("kick", tokens = 1)
    t("hit",  dur = cyc(1, 16), emit = "bd") { from("kick"); to("hats") }
    t("back", dur = cyc(1, 16), emit = "sd") { from("hats"); to("kick") }
}

var timing: PetriTiming = PetriTiming.STEP

var grid: PatQ = PatQ.of(1, 16)

var conflict: PetriConflict = PetriConflict.PRIORITY

var seed: Int = 0

    private val declared = LinkedHashMap<String, PetriPlace>()
    private val marking = LinkedHashMap<String, MutableList<PetriToken>>()
    private val builtTransitions = mutableListOf<PetriTransition>()

fun place

Declares a place.

tokens black tokens and one token per entry of colours are placed in it, black ones first. Returns the name so it composes into an arc call.

    fun place(
        name: String,
        tokens: Int = 0,
        capacity: Int? = null,
        colours: List<Any?> = emptyList(),
        at: PatQ = PatQ.ZERO,
    ): String {
        declared[name] = PetriPlace(name, capacity)
        val bucket = marking.getOrPut(name) { mutableListOf() }
        repeat(maxOf(0, tokens)) { bucket += PetriToken(null, at) }
        colours.forEach { bucket += PetriToken(it, at) }
        return name
    }

fun place(name: String, vararg colours: Any?): String = place(name, colours = colours.toList())

Declares a place holding exactly these coloured tokens — place("verse", pat("bd*4")).

fun t

Declares a transition. The block wires its arcs.

dur sets how long the emitted event lasts (and, under PetriTiming.TIMED, how long the firing holds its tokens); delay shifts the event without touching the net's logic.

    fun t(
        name: String,
        dur: PatQ = PatQ.ZERO,
        delay: PatQ = PatQ.ZERO,
        priority: Int = 0,
        weight: Double = 1.0,
        emit: Any? = null,
        colourFlow: PetriColourFlow = PetriColourFlow.CARRY,
        build: PetriTransitionBuilder.() -> Unit = {},
    ): String {
        val spec = PetriTransitionBuilder(name).apply(build)
        spec.mentioned.forEach { declared.getOrPut(it) { PetriPlace(it) } }
        builtTransitions += PetriTransition(
            name = name,
            inputs = spec.inputs.toList(),
            outputs = spec.outputs.toList(),
            duration = dur,
            delay = delay,
            priority = priority,
            weight = weight,
            emit = emit,
            emitOf = spec.emitOf,
            enabledIf = spec.enabledIf,
            colourFlow = colourFlow,
        )
        return name
    }

internal fun build(): PetriNet

    internal fun build(): PetriNet = PetriNet(
        places = declared.values.toList(),
        transitions = builtTransitions.toList(),
        initial = PetriMarking.of(marking),
        timing = timing,
        grid = grid,
        conflict = conflict,
        seed = seed,
    )
}

class PetriTransitionBuilder internal constructor(private val name: String)

Wires one transition's arcs. See PetriBuilder.t.

internal val inputs = mutableListOf<PetriInput>()

internal val outputs = mutableListOf<PetriOutput>()

internal val mentioned = LinkedHashSet<String>()

internal var emitOf: ((PetriBinding) -> Any?)? = null

internal var enabledIf: ((PetriBinding) -> Boolean)? = null

fun from(place: String, weight: Int = 1, guard: ((PetriToken) -> Boolean)?

Consume weight tokens from place, optionally only those matching guard.

    fun from(place: String, weight: Int = 1, guard: ((PetriToken) -> Boolean)? = null) {
        mentioned += place
        inputs += PetriInput(place, weight, PetriArcKind.NORMAL, guard)
    }

fun read(place: String, weight: Int = 1, guard: ((PetriToken) -> Boolean)?

Require weight tokens in place but consume none — a test arc, &p in the notation.

    fun read(place: String, weight: Int = 1, guard: ((PetriToken) -> Boolean)? = null) {
        mentioned += place
        inputs += PetriInput(place, weight, PetriArcKind.READ, guard)
    }

fun inhibit(place: String, weight: Int = 1, guard: ((PetriToken) -> Boolean)?

Require fewer than weight tokens in place — an inhibitor arc, ~p in the notation.

    fun inhibit(place: String, weight: Int = 1, guard: ((PetriToken) -> Boolean)? = null) {
        mentioned += place
        inputs += PetriInput(place, weight, PetriArcKind.INHIBIT, guard)
    }

fun to(place: String, weight: Int = 1, produce: ((PetriBinding) -> List<PetriToken>)?

Produce weight tokens into place. Without produce the transition's PetriColourFlow decides their colour — by default the consumed colours are carried through.

    fun to(place: String, weight: Int = 1, produce: ((PetriBinding) -> List<PetriToken>)? = null) {
        mentioned += place
        outputs += PetriOutput(place, weight, produce)
    }

fun toColoured(place: String, colour: (PetriBinding) -> Any?) {

Produce one token into place whose colour is computed from the binding.

    fun toColoured(place: String, colour: (PetriBinding) -> Any?) {
        to(place) { binding -> listOf(PetriToken(colour(binding), binding.at)) }
    }

fun emit(of: (PetriBinding) -> Any?) {

What this firing sounds, when it depends on which tokens were consumed.

    fun emit(of: (PetriBinding) -> Any?) {
        emitOf = of
    }

fun onlyIf(predicate: (PetriBinding) -> Boolean) {

A final veto once the tokens are chosen.

    fun onlyIf(predicate: (PetriBinding) -> Boolean) {
        enabledIf = predicate
    }

override fun toString(): String = "PetriTransitionBuilder($name)"

fun petri(build: PetriBuilder.() -> Unit): PetriNet = PetriBuilder().apply(build).build()

Builds a net with the Kotlin DSL. See PetriBuilder.