Appendix B: Token Language Grammar

This appendix documents the S-expression DSL for defining token model schemas, the syntax introduced in Chapter 4: The Token Language. The implementation is go-pflow’s tokenmodel/dsl package: lexer.go, parser.go, ast.go and interpret.go, with tests in dsl_test.go. The rules below were read from that code; the tests were not re-run for this appendix. The DSL is easier to read than JSON, but it expresses less: the JSON model format of Appendix C has fields the DSL has no syntax for (see Equivalence with JSON).

Lexical Elements

The lexer recognizes these token types:

Whitespace (spaces, tabs, newlines) separates tokens but is otherwise ignored.

Top-Level Structure

A schema definition has the form:

(schema <name>
  (version <version>)
  (states ...)
  (actions ...)
  (arcs ...)
  (constraints ...))

The <name> and <version> are symbols, so v1.0.0 is written without quotes; a quoted string in either position is a parse error. The parser requires none of the clauses: (schema Test (version v1.0.0)) is a complete schema in TestParser_MinimalSchema. Clauses may appear in any order, and a repeated clause replaces the earlier one. The conventional order is version, states, actions, arcs, constraints.

States

The states clause defines places in the Petri net:

(states
  (state <id> :type <type> :kind <kind> :initial <value> :exported))

State Keywords

All keywords are optional. A minimal state definition is just (state <id>), which is a data state. The default kind differs from the JSON model format, where a place with no kind is a token place; a token-counting place in the DSL needs :kind token.

Examples

; Token-counting place with initial tokens
(state pending :kind token :initial 1)

; Data place holding a map
(state balances :type map[string]int64 :exported)

; Simple data place with initial value
(state total_supply :type int64 :initial 0 :exported)

Actions

The actions clause defines transitions:

(actions
  (action <id> :guard {<expression>}))

Action Keywords

Examples

; Action with no guard (always enabled when inputs are available)
(action ship)

; Action with guard expression
(action transfer :guard {balances[from] >= amount && amount > 0})

; Action with simple guard
(action mint :guard {amount > 0})

Arcs

The arcs clause defines connections between states and actions:

(arcs
  (arc <source> -> <target> :keys (<key1> <key2> ...) :value <binding>))

The -> arrow separates source from target. The parser accepts any two symbols here; the check that an arc joins a state to an action (input arc) or an action to a state (output arc) comes afterwards, when Interpret calls Schema.Validate (tokenmodel/validate.go), which also rejects an end that names no declared state or action.

Arc Keywords

The DSL has no syntax for arc weight or for inhibitor and read arcs. go-pflow’s tokenmodel.Arc has Weight and Type fields, but the DSL parser, the builder and the struct-tag dialect never set them, so every arc written in the DSL is a normal arc of weight 1. The contextual arcs of Appendix E have to be written in JSON or Go.

Examples

; Simple token arc (no keywords needed)
(arc pending -> ship)
(arc ship -> shipped)

; Data arc with keys and value
(arc balances -> transfer :keys (from) :value amount)
(arc transfer -> balances :keys (to) :value amount)

; Arc with multiple keys
(arc ledger -> settle :keys (from to) :value amount)

Constraints

The constraints clause defines invariants:

(constraints
  (constraint <id> {<expression>}))

The expression is enclosed in {...} braces, like guard expressions. Schema.Validate does not look at constraints. go-pflow’s tokenmodel.Runtime (runtime.go) evaluates them against the token counts after each action it executes, provided CheckConstraints is true (the default) and a guard evaluator has been supplied; with no evaluator, constraints are skipped. A constraint is a runtime assertion about the markings a run actually visits. It does not prove the property over every reachable marking.

Examples

; Conservation law
(constraint conservation {sum(balances) == total_supply})

; Mutual exclusion
(constraint mutex {pending + shipped + delivered == 1})

Guard Expression Syntax

Guard expressions (used in both :guard and constraint) support:

The DSL parser does not read guard expressions. The lexer captures everything between { and the matching } as a single token, and the parser stores it as a string. Evaluation happens later, through whatever guard evaluator the runtime is given, and the expression language has two implementations whose operators agree but whose aggregate functions do not:

• go-pflow’s tokenmodel/guard provides sum, count, tokens, min and max. Each takes a place ID or ID prefix as a string: sum("balances_") adds the token counts of every place whose ID starts with balances_ (guard_test.go checks it equals 600 on its test marking).
• petri-pilot’s pkg/dsl names the last two minOf and maxOf, and its sum, count, minOf and maxOf also accept a data state’s map, so sum(balances) totals the values in the balances map.

The constraint sum(balances) == total_supply used in this appendix is written for petri-pilot’s evaluator. Under go-pflow’s it fails to evaluate, because balances is a bare name rather than a string and is not a token place.

Complete Examples

Neither example below is in go-pflow’s test suite, and neither was run for this appendix. The nearest tested schema is erc020DSL in dsl_test.go, a fuller ERC-20 with allowances and burn: TestInterpret_ERC020 parses and interprets it and checks for 3 states, 5 actions, 10 arcs and 1 constraint, and TestRoundTrip_ParseAndValidate passes it through Schema.Validate.

ERC-20 Token

(schema erc20-token
  (version v1.0.0)

  (states
    (state balances :type map[string]int64 :exported)
    (state total_supply :type int64 :initial 0 :exported))

  (actions
    (action transfer :guard {balances[from] >= amount && amount > 0})
    (action mint :guard {amount > 0}))

  (arcs
    (arc balances -> transfer :keys (from) :value amount)
    (arc transfer -> balances :keys (to) :value amount)
    (arc mint -> balances :keys (to) :value amount)
    (arc mint -> total_supply :value amount))

  (constraints
    (constraint conservation {sum(balances) == total_supply})))

Order Workflow

(schema order-processing
  (version v1.0.0)

  (states
    (state received :kind token :initial 1)
    (state validated :kind token)
    (state shipped :kind token)
    (state completed :kind token))

  (actions
    (action validate)
    (action ship)
    (action deliver))

  (arcs
    (arc received -> validate)
    (arc validate -> validated)
    (arc validated -> ship)
    (arc ship -> shipped)
    (arc shipped -> deliver)
    (arc deliver -> completed))

  (constraints
    (constraint conservation {received + validated + shipped + completed == 1})))

The conservation constraint holds by construction. Each action has one input arc and one output arc of weight 1, so every firing moves the single token one place along the chain and the four counts always sum to the initial 1. That follows from the arcs by hand; it was not checked by a run.

AST Representation

The parser produces an abstract syntax tree with these node types:

The S-expression DSL is one of three front ends that build a SchemaNode. The others are the fluent builder (builder.go, dsl.Build(...)) and the Go struct-tag dialect (tags.go in the same package, dsl.ASTFromStruct). Interpret turns any SchemaNode into a tokenmodel.Schema and validates it. The three front ends do not produce identical trees for the same model: the builder and struct-tag paths default the version to v1.0.0 and give token states the type int, where the parser leaves both empty unless the source sets them.

Equivalence with JSON

A parsed DSL schema has two JSON forms. The first is tokenmodel.Schema itself, whose JSON field names come from the struct tags in tokenmodel/schema.go; its top-level keys are states, actions, arcs and constraints. The second is the model format of Appendix C: JSON Schema Reference, which calls the same things places, transitions, arcs and constraints. go-pflow’s metamodel.FromTokenModel (metamodel/convert.go) converts the first into the second:

petri-pilot accepts DSL input by this route. Its parseModelV2 (pkg/mcp/server.go) treats input that begins with ( as DSL, calls ParseSchema and then FromTokenModel, and copies each data state’s :initial into the place’s initial_value, because FromTokenModel drops it.

The two formats are not equally expressive. Arc weights and types, transition rates, roles, views and the other sections of Appendix C have no DSL syntax, so every DSL schema has a JSON model but a JSON model cannot in general be written as DSL without losing fields.