Appendix B: Token Language Grammar

This appendix documents the S-expression DSL for defining token model schemas. The DSL is an alternative to JSON for defining Petri net models — more readable for humans, equivalent in expressiveness.

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-string>)       ; optional
  (states ...)                     ; required
  (actions ...)                    ; required
  (arcs ...)                       ; required
  (constraints ...))               ; optional

The <name> is a symbol identifying the schema. Clauses may appear in any order, but 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>).

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. Arcs are bipartite: they connect a state to an action (input arc) or an action to a state (output arc).

Arc Keywords

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. Constraints are checked at validation time and should hold for all reachable markings.

Examples

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

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

Guard Expression Syntax

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

Guard expressions are opaque to the DSL parser — the lexer captures everything between { and } as a single token. The guard DSL parser in petri-pilot evaluates these expressions at runtime against the current state.

Complete Examples

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})))

AST Representation

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

The AST is the same regardless of whether the schema was defined via the S-expression DSL, the Go struct tag syntax, or the fluent builder API. All three produce identical SchemaNode trees, which are then compiled to Petri nets.

Equivalence with JSON

Every DSL schema has an equivalent JSON representation. The mapping is direct:

The DSL is syntactic sugar. The JSON schema (Appendix C) is the canonical format.