Appendix C: JSON Schema Reference

This appendix documents the JSON model format used by petri-pilot for code generation. The schema defines what a valid Petri net model looks like — places, transitions, arcs, and the higher-level structures (roles, views, navigation, admin, event sourcing, simulation) that drive application generation.

The full JSON Schema is schema/petri-model.schema.json in petri-pilot.

The schema file describes the format, but the code that reads a model decides what is accepted. petri-pilot’s CLI decodes a model into go-pflow’s metamodel.Model (metamodel/schema.go, at v0.33.0, the version petri-pilot’s go.mod pins), plus the extension fields of modelWithExtensions in cmd/petri-pilot/main.go: admin, navigation, roles, access, views, debug and graphql. Where the schema file and that loader disagree, this appendix follows the loader and says so. The disagreements are transition bindings and rate, arc type and kinetic, and eventSourcing. They were found by reading the Go types against the schema file. No model was run through the CLI to confirm them.

Top-Level Structure

A model is a JSON object with four required fields and several optional ones:

{
  "name": "order-processing",
  "version": "1.0.0",
  "description": "Order fulfillment workflow",
  "places": [...],
  "transitions": [...],
  "arcs": [...],
  "constraints": [...],
  "roles": [...],
  "access": [...],
  "views": [...],
  "navigation": {...},
  "admin": {...},
  "eventSourcing": {...},
  "simulation": {...}
}

Places

A place holds state — either token counts (classic Petri net) or structured data.

{
  "id": "order_received",
  "description": "Order has been received but not yet validated",
  "initial": 1,
  "kind": "token",
  "type": "string",
  "initial_value": null,
  "exported": false,
  "persisted": false
}

Data Types

For kind: "data" places, the type field specifies the data type:

Transitions

A transition is an action that fires when enabled. Each transition becomes an HTTP endpoint in the generated application.

{
  "id": "validate_order",
  "description": "Validate the order details",
  "guard": "amount > 0",
  "event_type": "OrderValidated",
  "http_method": "POST",
  "http_path": "/api/validate",
  "bindings": [
    {"name": "amount", "type": "number", "value": true}
  ]
}

The schema file is stale on bindings: it describes the field as an object mapping names to strings. The loader’s Transition.Bindings is an array of Binding objects with fields name, type, keys (map access path), value (true for the transferred amount) and place. Go’s JSON decoder does not turn an object into an array, so by the types an object-form bindings fails to parse. The old map form survives as the separate field legacy_bindings. The binding in the example above is copied from pflow-xyz’s extend-operations.json fixture.

Guard Syntax

Guards are boolean expressions evaluated against the current state. The lexer is petri-pilot’s pkg/dsl/lexer.go; strings may use single or double quotes.

Arcs

An arc connects a place to a transition (input) or a transition to a place (output).

{
  "from": "balances",
  "to": "transfer",
  "weight": 1,
  "keys": ["from"],
  "value": "amount"
}

The schema file has no type field, but go-pflow’s Arc does, and petri-pilot’s own services/vet-clinic.json uses both kinds, for example {"from": "wait_emergency", "to": "start_wellness", "type": "inhibitor"}. Neither kind moves tokens. An inhibitor arc blocks the transition while its place holds at least weight tokens. A read arc allows the transition only while its place holds at least weight tokens. These are the contextual arcs of Appendix E, outside the incidence matrix. Setting kinetic: false keeps an input arc’s enabling and consumption but removes its place from the rate product. go-pflow’s metamodel/validation.go rejects three things here: an unknown type, which is not quietly run as a normal arc; a read arc that does not run place → transition; and kinetic: false on any arc other than a consuming place → transition arc.

Constraints

An invariant that must always hold.

{
  "id": "conservation",
  "expr": "received + validated + shipped + completed == 1"
}

Roles

Named roles for access control, with inheritance.

{
  "id": "admin",
  "name": "Administrator",
  "description": "Full access to all operations",
  "inherits": ["manager"]
}

Access Rules

Maps transitions to allowed roles.

{
  "transition": "approve_order",
  "roles": ["manager", "admin"],
  "guard": "user.department == 'finance'"
}

Views

UI view definitions for forms, tables, and detail pages.

{
  "id": "order_detail",
  "name": "Order Details",
  "kind": "detail",
  "description": "Shows order information",
  "groups": [...],
  "actions": ["approve", "reject"]
}

View Groups

{
  "id": "customer_info",
  "name": "Customer Information",
  "fields": [...]
}

View Fields

{
  "binding": "customer_email",
  "label": "Email Address",
  "type": "email",
  "required": true,
  "readonly": false,
  "placeholder": "customer@example.com"
}

Field types: text, number, email, date, datetime, select, checkbox, textarea, password, hidden.

Navigation

Navigation menu configuration. Generates /api/navigation endpoint.

{
  "brand": "Order Tracker",
  "items": [
    {
      "label": "Orders",
      "path": "/orders",
      "icon": "box",
      "roles": []
    },
    {
      "label": "Admin",
      "path": "/admin",
      "icon": "gear",
      "roles": ["admin"]
    }
  ]
}

Admin

Admin dashboard configuration. Generates /admin/* endpoints.

{
  "enabled": true,
  "path": "/admin",
  "roles": ["admin"],
  "features": ["list", "detail", "history", "transitions"]
}

Features: list (instance listing), detail (instance detail page), history (event history), transitions (manual transition firing).

Event Sourcing

Snapshot and retention configuration.

{
  "snapshots": {
    "enabled": true,
    "frequency": 100
  },
  "retention": {
    "events": "90d",
    "snapshots": "1y"
  }
}

Retention durations use the pattern ^\d+[dwmy]$ — number followed by d (days), w (weeks), m (months), or y (years).

The schema file defines this block, but the loader does not read it: neither go-pflow’s Model nor modelWithExtensions has an eventSourcing field, so Go’s decoder drops it when a model file is read. In the Go generator, buildEventSourcingContext in pkg/codegen/golang/context.go is defined but has no caller. Treat the block as a declared format, not yet a working feature.

Simulation

ODE simulation configuration for AI move evaluation.

{
  "objective": "win_x - win_o",
  "players": {
    "x": {
      "maximizes": true,
      "turnPlace": "turn_x",
      "transitions": ["move_x_0", "move_x_1"]
    },
    "o": {
      "maximizes": false,
      "turnPlace": "turn_o",
      "transitions": ["move_o_0", "move_o_1"]
    }
  },
  "solver": {
    "tspan": [0, 10],
    "dt": 0.01,
    "rates": {
      "move_x_0": 1.0,
      "move_o_0": 1.0
    }
  }
}

Objective Functions

The objective field is a numeric guard-DSL expression, using arithmetic and the aggregate functions below. The same functions are available to guards and constraints. Except for tokens, each function takes a place-ID prefix: over token places it ranges over every place whose ID starts with the argument, and over a map data place of that name it ranges over the map’s values. The definitions are MakeAggregates and MakeAggregatesWithData in pkg/dsl/guard.go.

Solver Configuration

Minimal Example

A small model that satisfies the schema:

{
  "name": "toggle",
  "places": [
    {"id": "off", "initial": 1},
    {"id": "on"}
  ],
  "transitions": [
    {"id": "switch"}
  ],
  "arcs": [
    {"from": "off", "to": "switch"},
    {"from": "switch", "to": "on"}
  ]
}

This defines a one-shot toggle: a token starts in off, the switch transition fires, and the token moves to on, where it stays because nothing consumes from on. The model uses only the four required fields. on takes the default initial of 0, and both arcs take the default weight of 1. The schema’s minimums are one place, one transition and one arc, so a model with a single place and a single arc would also validate. This one was checked by reading it against the schema file, not by running it through petri-pilot’s validator.