The Token Language

At the heart of go-pflow is an interpreted language for defining and executing token models. This language gives us a declarative way to specify Petri nets with rich data semantics—going beyond simple integer counters to structured state, guard predicates, and conservation invariants.

The Four-Term DSL

The language distills to four primitives:

This minimal vocabulary captures the essential structure of executable schemas. Every token model—from ERC-20 tokens to game boards to workflow engines—can be expressed with these four terms.

S-Expression Syntax

The DSL uses an S-expression syntax familiar to Lisp programmers:

(schema ERC-20
  (version v1.0.0)

  (state totalSupply :type uint256)
  (state balances :type map[address]uint256 :exported)
  (state allowances :type map[address]map[address]uint256)

  (action transfer :guard {balances[from] >= amount && to != address(0)})
  (action approve)
  (action mint :guard {to != address(0)})
  (action burn :guard {balances[from] >= amount})

  (arc balances -> transfer :keys (from))
  (arc transfer -> balances :keys (to))
  (arc mint -> totalSupply)
  (arc totalSupply -> burn)

  (constraint conservation {sum(balances) == totalSupply}))

Each form declares structure: states hold data, actions perform operations, arcs define flow, and constraints enforce invariants.

Memory Model: Tokens vs Data

The language distinguishes two kinds of state:

TokenState

Integer counters representing discrete token quantities. This is classic Petri net semantics:

• Firing consumes and produces: An action removes tokens from input places and adds them to output places
• Enabling condition: An action can fire only when all input places have sufficient tokens
• No identity: Tokens are fungible; we track counts, not individuals

type Snapshot struct {
    Tokens map[string]int  // TokenState
    Data   map[string]any  // DataState
}

DataState

Typed containers holding structured data—maps, records, or scalar values. This extends Petri nets to handle real-world state:

• Arc keys specify access paths: (arc balances -> transfer :keys (from)) binds from to the map key
• No automatic consumption: Data arcs read and write; they don't consume
• Type-aware: Schemas specify types like map[address]uint256

The combination enables modeling systems where both control flow (tokens) and data transformations (balances, permissions, state) matter.

Guard Evaluation

Guards are boolean expressions that gate action execution. An action fires only when its guard evaluates to true.

Expression Syntax

Guards support a familiar expression language:

Comparison:  balances[from] >= amount
             to != address(0)
             count > 0

Logical:     condition1 && condition2
             condition1 || condition2
             !condition

Indexing:    balances[key]
             allowances[owner][spender]

Field:       schedule.revocable
             data.timestamp

Function:    sum(balances)
             count(owners)
             address(0)

Evaluation Context

Guards evaluate against a context containing:

1. Bindings: Variable values from action parameters (from, to, amount)
2. Functions: Built-in aggregates and custom functions (sum, count)
3. State: Current snapshot for data access

The evaluator uses short-circuit evaluation—&& stops on first false, || stops on first true—making guards efficient even with complex conditions.

Execution Pipeline

From source text to running model, the language follows a classic interpreter pipeline:

Compilation

1. Lexer: Tokenizes source into LPAREN, SYMBOL, GUARD, etc.
2. Parser: Builds an AST with SchemaNode, StateNode, ActionNode, ArcNode
3. Interpreter: Converts AST to executable Schema with validated references

Runtime

Each action execution follows:

1. Guard Check: Evaluate guard expression with current bindings
2. Input Processing: Read from input arcs (consume tokens, bind data)
3. Output Processing: Write to output arcs (produce tokens, update data)
4. Invariant Check: Verify all constraints still hold
5. Snapshot Update: Commit new state with incremented sequence

If the guard fails, the action is blocked. If an invariant fails, the action is rolled back.

Invariants

Invariants are constraints that must hold across all state transitions. They catch bugs at runtime and document system properties.

Conservation Laws (P-Invariants)

The most common invariant type: quantities that must be preserved:

(constraint conservation {sum(balances) == totalSupply})

This declares that the total of all balances must always equal totalSupply. The sum() aggregate function computes across all map entries.

Other aggregate functions:

• sum(place) — sum all values
• count(place) — count non-zero entries
• tokens(place) — token count at place

Guard vs Invariant

Guards are "can we do this?" checks. Invariants are "did we break anything?" checks.

Example: Token Transfer

Consider a simple token transfer:

(action transfer :guard {balances[from] >= amount && to != address(0)})
(arc balances -> transfer :keys (from))
(arc transfer -> balances :keys (to))

Execution trace:

1. Guard: Check balances[0x1a2b] >= 100 and 0x3c4d != address(0)
2. Input arc: Read balances[from], bind to action
3. Action: Compute new balances
4. Output arc: Write balances[to] += amount, balances[from] -= amount
5. Invariant: Verify sum(balances) == totalSupply
6. Commit: Update snapshot, increment sequence

The guard prevents overdrafts. The invariant catches any implementation bug that would create or destroy tokens.

Why an Interpreted Language?

We could define models in Go structs or JSON. Why a dedicated language?

Declarative clarity: The DSL makes structure visible. (arc balances -> transfer :keys (from)) is clearer than wiring up method calls.

Executable specification: The same text that documents the model also runs it. No translation gap between spec and implementation.

Analysis-friendly: Parseable structure enables static analysis—checking guard completeness, invariant coverage, reachability.

Composable: Schemas can import states and actions from other schemas. The DSL makes composition explicit.

Little language philosophy: A small, focused language does one thing well. The four-term vocabulary keeps models comprehensible.

Try It

The language is implemented in go-pflow:

import "github.com/pflow-xyz/go-pflow/tokenmodel/dsl"

schema, err := dsl.ParseSchema(`
  (schema Counter
    (state count :kind token :initial 10)
    (action decrement :guard {tokens(count) > 0})
    (arc count -> decrement)
    (arc decrement -> done))
`)

For visual exploration, pflow.xyz provides a browser-based editor with ODE analysis.

Key Takeaways

1. Four terms suffice: cell, func, arrow, guard capture token model structure
2. Two memory modes: TokenState for counts, DataState for structured values
3. Guards gate actions: Boolean predicates with indexing, comparison, and logic operators
4. Invariants enforce properties: Conservation laws checked after every state change
5. Interpreted for clarity: Declarative syntax makes models readable and analyzable