Docs · Charts

Datamodels and types

A chart's datamodel decides what its conditions, assignments and data look like. Its types say what each event carries and what the context holds. This page covers the four datamodels, the type language, the type checker and the projections of types to Rust, TypeScript, JSON Schema, SHACL and CEL.

Four datamodels

All executable content goes through one Datamodel trait in vertep-core: initialize data, evaluate a condition, evaluate a value, assign, run a script, iterate, snapshot and restore. A chart names its datamodel, and the host creates it from a registry by that name. A chart whose datamodel is not registered is refused.

Which one to use

• No data at all: null. examples/traffic-light/traffic-light.scxml runs a two-region traffic light on it, with In() conditions only.
• An existing SCXML chart, or one that must also run in another SCXML engine: ecmascript.
• A chart written in YAML, or written by anyone you do not fully trust, including a language model: cel. It cannot cause side effects, always terminates, and is type-checked before the chart runs.
• A chart compiled into a Rust program, where guards and actions are Rust functions: rust.

null

The null datamodel (W3C SCXML B.1) holds no data. In() is the only condition it accepts. Any other condition, any <assign>, any <script> and any value expression is an evaluation error and queues error.execution. Its snapshot is the empty value.

ecmascript

vertep-dm-ecma implements W3C SCXML B.2 on the boa engine, behind the cargo feature ecmascript (on by default). Without the feature the crate registers no datamodel, and charts that need it are refused. Data items are variables of one global scope per session. Inline content that JSON.parse accepts becomes that value; anything else becomes a string. Conditions run against a read-only view of the session scope, so a condition that tries to assign fails. System variables are frozen. Math.random() is seeded from the input, and the current date is the timestamp journaled with the event, never the wall clock.

In the browser the same datamodel ships as a separate package, @vertep/dm-ecma; see Browser and JavaScript.

cel

vertep-dm-cel is Vertep's own CEL interpreter. No existing Rust CEL implementation had exact decimals, evaluation limits and a defined map order together with no_std, so it was written for this. It is no_std with alloc and uses integer arithmetic for decimals, timestamps and durations.

Expressions see:

There is no now() and no random function, so an expression that calls one fails type checking. The only state change a CEL datamodel makes is an <assign> of an expression's value to a location; a failed assignment leaves the location unchanged and raises error.execution. Every evaluation is bounded by limits, and exceeding one raises error.execution naming the limit. The defaults, from Limits::default() in crates/vertep-dm-cel/src/error.rs:

For charts from untrusted authors, load with Policy::CelOnly (vertep_dm_cel::Policy). It rejects a chart that names another datamodel, that contains <script>, or that references a registered Rust guard or action (vt:guard/…, vt:action/…). Plan charts, on Agents and deciders, type-check their CEL expressions under this policy.

rust

On the rust datamodel the context is a Rust struct (the generated Ctx), and guards and actions are Rust functions registered by IRI. A guard is fn(&Ctx, &P) -> bool: no mutable context and no emitter. An action is fn(&mut Ctx, &P, &mut Emit), fn(&mut Ctx, &P) or fn(&mut Ctx, &P) -> Vec<E>. Its only effects are context changes and emitted events, which become <raise> and <send> in the step. The registry rejects duplicate IRIs, and a chart whose IRIs are not all registered cannot start. Because the registry works by IRI, a chart loaded from RDF at run time can bind to compiled functions too. How the IRIs appear in the IR is shown on Writing charts.

Rules every datamodel follows

• System variables _event, _sessionid, _name and _ioprocessors are read-only. Assigning to one is an error.
• Guards are pure. A condition that tries to change data is an error, is treated as false, and queues error.execution.
• Errors are events. A failed expression becomes error.execution on the internal queue; it never panics.
• Binding follows SCXML 5.3. Under early binding (the default) all data is initialized at session start. Under late binding a state's data gets its initial value when the state is first entered.
• Determinism. The same datamodel state and the same input give the same result. Time and randomness come only from the input the host supplies, which the runtime journals.
• Snapshots. Every datamodel serializes its full state to a datamodel-independent value and restores from it, and restoring then continuing gives the same results as never stopping.

The type language

One algebraic type language describes event payloads and context in every surface. Typing is opt-in per chart. A chart without type declarations is untyped: every payload and context value has the dynamic type value, the checker reports nothing, and the chart runs as plain SCXML would.

The textual syntax, used in vt:type attributes, the vt:types block and YAML strings, from crates/vertep-core/src/types/syntax.rs:

//! type      := '|' variant ('|' variant)*          a union, leading bar allowed
//!            | variant ('|' variant)+              a union
//!            | tag atom                            a one-variant union with payload
//!            | atom
//! variant   := tag atom?                           tag is an identifier or a "quoted string"
//! atom      := bool | int | decimal | string | datetime | iri | value
//!            | list '<' type '>' | optional '<' type '>'
//!            | '{' (name ':' type (',' name ':' type)* ','?)? '}'
//!            | '(' type ')'
//!            | Name                                a named type
//! decls     := (('type' Name '=' type | 'event' event-name (':' type)?) ';')*

A few rules worth knowing:

• Named types are content-addressed. A named type's IRI is a hash of its canonical definition, such as urn:vertep:type:sha256:…. Identical definitions share an IRI; field order does not matter; any change gives a new IRI. The chart version covers its types, so changing a payload type is a new chart version.
• Recursion must go through a list or an optional. An unguarded self-reference is an error.
• Records are closed. A missing required field and an unknown extra field are both errors. An absent optional field reads as absent, not as an empty value.
• The dynamic boundary. A typed value can always go where value is expected. A value goes where a static type is expected only through a checked conversion, which raises error.execution on a mismatch.
• System events are typed. error.* carries { kind: string, message: string }; done.state.* and done.invoke.* carry value. A descriptor that matches several typed events sees the union of their payload types.

Writing types in a chart

Here is one small typed chart, a counter, on CEL in YAML. types names record and union types, events gives each event its payload type (null for none), and context gives each data item a type and an initial value:

vertep: 1
name: counter
datamodel: cel
types:
  Add: { by: int }
events: { add: Add, reset: null }
context:
  count: { type: int, init: "0" }
initial: counting
states:
  counting:
    on:
      add:
        - cond: "ev.data.by > 0"
          actions: [ { assign: { location: ctx.count, expr: "ctx.count + ev.data.by" } } ]
      reset:
        - actions: [ { assign: { location: ctx.count, expr: "0" } } ]

In SCXML the same declarations go in a vt:types element, and vt:type annotates a <data> item (or a <send> payload, or a <param>). This version uses the ecmascript datamodel, so its expressions read _event.data instead of ev.data:

<scxml xmlns="http://www.w3.org/2005/07/scxml" xmlns:vt="https://w3id.org/vertep/vt#"
       version="1.0" name="counter" datamodel="ecmascript" initial="counting">
  <vt:types>
    type Add = { by: int };
    event add: Add;
    event reset;
  </vt:types>
  <datamodel>
    <data id="count" expr="0" vt:type="int"/>
  </datamodel>
  <state id="counting">
    <transition event="add" cond="_event.data.by &gt; 0">
      <assign location="count" expr="count + _event.data.by"/>
    </transition>
    <transition event="reset">
      <assign location="count" expr="0"/>
    </transition>
  </state>
</scxml>

An SCXML processor that ignores the vt: namespace runs this document untyped. The two files differ in datamodel, so they are two charts with two versions:

$ vt hash counter.yaml
urn:vertep:chart:sha256:4ee7f3aad3f8bf39adb28adb68271c58a9460efbe090d6549a0e1eca8f954076
$ vt hash counter.scxml
urn:vertep:chart:sha256:6e1b433eed539ee7ff42ee23c1ee4e96592232e12e4688c248b2a0538464c2d2

In statechart!, types go in types { … }, context { name: type = literal } and events { name: Type }; see the macro. The type annotations survive every surface: converting a typed chart from YAML to SCXML to RDF and back gives the same types and the same version IRI.

Type checking

One checker in vertep-core (check_chart) serves the macros, the loaders, vt and the runtime. Before a typed chart can be instantiated, it checks event payloads, context declarations, <data> initializers, <send> payloads, parameters, guards and assignments against the declared types. A chart with type errors is not instantiated. For cel and rust charts the checker knows the ctx and ev roots and types expressions over them; for other datamodels it types literals only.

$ vt typecheck counter.yaml
counter.yaml: ok: 1 named types, 2 typed events, 1 context fields

If the reset transition assigns true to the int field ctx.count, the error names the line, the column and the path in the document, and the command exits 1:

$ vt typecheck assign-bool.yaml; echo "exit $?"
assign-bool.yaml:17:22: states.counting.on.reset[0].actions[0]: state "counting", transition 1 (on reset), action 0: the value assigned to `ctx.count` has type bool, expected int
exit 1

The CEL expressions themselves are checked against the chart's CEL type environment. A guard must have type bool, and a field must exist on the record it is read from:

$ vt typecheck guard-int.yaml
guard-int.yaml: state `counting` › transition 1 › cond: a guard must have type bool, but `ctx.count + 1` has type int
guard-int.yaml: 1 type error
$ vt typecheck no-field.yaml
no-field.yaml: state `counting` › transition 1 › cond: no field `amount` in Add in `ev.data.amount > 0`
no-field.yaml: 1 type error

An unknown type name gets a suggestion:

$ vt typecheck counter-typo.scxml
counter-typo.scxml:9:5: vt:type on <data id="count">: unknown type `Add2`; did you mean `Add`?

A larger example is examples/typed-order/: order.yaml is well typed, and order-ill-typed.yaml assigns a string to a decimal on purpose.

$ vt typecheck order-ill-typed.yaml
order-ill-typed.yaml:44:19: states.shopping.states.cart.on.add[0].actions[1]: state "cart", transition 0 (on add), action 1: the value assigned to `ctx.total` has type string, expected decimal
$ vt typecheck order.yaml
order.yaml: ok: 3 named types, 6 typed events, 3 context fields

In the macro the checker runs at compile time, and the generated Rust types catch the rest: Event::Pay { amount: "ten" } does not compile, because amount is a Decimal (crates/vertep-dm-rust/tests/ui/wrong_payload.stderr).

Projections

Each type projects to the forms the rest of the system needs. JSON Schema describes LLM structured output and tool arguments; SHACL validates journal values in RDF; the CEL environment type-checks CEL expressions; Rust and TypeScript give typed APIs.

All of them agree on one canonical encoding of values (crates/vertep-core/src/types/check.rs): a decimal is a string such as "12.50" (a number is accepted on input); a datetime is an RFC 3339 string, encoded in UTC with a Z; a record has exactly its declared fields, absent optional fields omitted; a tagged union is {"tag": …, "value": …}, without value for a variant with no payload.

vt schema

vt schema --format jsonschema|shacl|cel|rust <chart> prints a projection. The CEL environment of the counter:

$ vt schema --format cel counter.yaml
ctx.count: int
ev.data[add]: Add
ev.data[reset]: null_type

JSON Schema: one document for the context and one per event payload.

$ vt schema --format jsonschema counter.yaml
{
  "context": {
    "$schema": "https://json-schema.org/draft/2020-12/schema",
    "additionalProperties": false,
    "properties": {
      "count": {
        "exclusiveMaximum": 9223372036854775808,
        "minimum": -9223372036854775808,
        "type": "integer"
      }
    },
    "required": [
      "count"
    ],
    "type": "object"
  },
  "events": {
    "add": {
      "$defs": {
        "Add": {
          "additionalProperties": false,
          "properties": {
            "by": {
              "exclusiveMaximum": 9223372036854775808,
              "minimum": -9223372036854775808,
              "type": "integer"
            }
          },
          "required": [
            "by"
          ],
          "title": "Add",
          "type": "object"
        }
      },
      "$ref": "#/$defs/Add",
      "$schema": "https://json-schema.org/draft/2020-12/schema"
    },
    "reset": {
      "$schema": "https://json-schema.org/draft/2020-12/schema",
      "type": "null"
    }
  }
}

SHACL, in Turtle. Shapes for named types sit under the type's own IRI, so any graph can find them by type. Shapes for the context and events sit under the chart version:

$ vt schema --format shacl counter.yaml
@prefix c: <urn:vertep:chart:sha256:4ee7f3aad3f8bf39adb28adb68271c58a9460efbe090d6549a0e1eca8f954076#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix xsd: <http://www.w3.org/2001/XMLSchema#> .
@prefix sh: <http://www.w3.org/ns/shacl#> .
@prefix vt: <https://w3id.org/vertep/vt#> .
c:context.f.count.t a sh:NodeShape ;
	sh:datatype xsd:long .
c:context.f.count a sh:PropertyShape ;
	sh:maxCount 1 ;
	sh:minCount 1 ;
	sh:node c:context.f.count.t ;
	sh:path <https://w3id.org/vertep/field#count> .
c:context a sh:NodeShape ;
	sh:closed true ;
	sh:nodeKind sh:BlankNode ;
	sh:property c:context.f.count .
c:event.add a sh:NodeShape ;
	sh:node <urn:vertep:type:sha256:04cc38e2c0e46abd032d0b88badf9887bc3bc9e04fda108ed58c2729bb422411> .
<urn:vertep:type:sha256:04cc38e2c0e46abd032d0b88badf9887bc3bc9e04fda108ed58c2729bb422411#s.f.by.t> a sh:NodeShape ;
	sh:datatype xsd:long .
<urn:vertep:type:sha256:04cc38e2c0e46abd032d0b88badf9887bc3bc9e04fda108ed58c2729bb422411#s.f.by> a sh:PropertyShape ;
	sh:maxCount 1 ;
	sh:minCount 1 ;
	sh:node <urn:vertep:type:sha256:04cc38e2c0e46abd032d0b88badf9887bc3bc9e04fda108ed58c2729bb422411#s.f.by.t> ;
	sh:path <https://w3id.org/vertep/field#by> .
<urn:vertep:type:sha256:04cc38e2c0e46abd032d0b88badf9887bc3bc9e04fda108ed58c2729bb422411#t.f.by> a vt:TypeField ;
	vt:fieldName "by" ;
	vt:fieldType vt:IntType .
<urn:vertep:type:sha256:04cc38e2c0e46abd032d0b88badf9887bc3bc9e04fda108ed58c2729bb422411#t> a vt:RecordType ;
	vt:typeField <urn:vertep:type:sha256:04cc38e2c0e46abd032d0b88badf9887bc3bc9e04fda108ed58c2729bb422411#t.f.by> .
<urn:vertep:type:sha256:04cc38e2c0e46abd032d0b88badf9887bc3bc9e04fda108ed58c2729bb422411> a sh:NodeShape , vt:NamedType ;
	sh:closed true ;
	sh:nodeKind sh:BlankNode ;
	sh:property <urn:vertep:type:sha256:04cc38e2c0e46abd032d0b88badf9887bc3bc9e04fda108ed58c2729bb422411#s.f.by> ;
	vt:definition <urn:vertep:type:sha256:04cc38e2c0e46abd032d0b88badf9887bc3bc9e04fda108ed58c2729bb422411#t> ;
	vt:typeName "Add" .

The Rust projection is not printed. It is generated at compile time by the macros:

$ vt schema --format rust counter.yaml
counter.yaml: the Rust projection is generated at compile time by the statechart! and include_chart! macros (vertep-macros); use include_chart!("counter.yaml") to get the typed Rust API

The test union_projects_to_an_enum in crates/vertep-dm-rust/tests/rust_projection.rs shows the Rust side: a union becomes an enum you can match exhaustively, records become structs, recursion through an optional is boxed.

statechart! {
    #[allow(unhandled_events, unreachable_states)]
    name: types_demo,
    types {
        Payment = Card { last4: string } | Cash,
        Line = { sku: string, qty: int, price: decimal, note: optional<string> },
        Order = {
            id: iri,
            at: datetime,
            lines: list<Line>,
            payment: Payment,
            paid: bool,
            extra: value,
            parent: optional<Order>,
            "unit price": optional<Money>,
            type: optional<string>,
        },
        Tree = Leaf | Node { children: list<Tree> } | Labeled string,
        Money = decimal,
    }
    events { place: Order }
    initial open;
    state open { on place => open; }
}

fn label(p: &Payment) -> String {
    // Exhaustive: the enum has exactly these two variants.
    match p {
        Payment::Card { last4 } => format!("card {last4}"),
        Payment::Cash => "cash".to_string(),
    }
}

vt gen ts

vt gen ts <chart> [--name N] prints a TypeScript module for @vertep/web: the event union, the context interface, the union of state ids, the chart spec with its source and version, and a typed constructor for the chart's virtual actor. Scalar rules TypeScript cannot state (the integer range, the decimal, date-time and IRI patterns) are checked when the event reaches the chart.

$ vt gen ts counter.yaml
// Generated by `vt gen ts` from chart urn:vertep:chart:sha256:4ee7f3aad3f8bf39adb28adb68271c58a9460efbe090d6549a0e1eca8f954076. Do not edit.
import type { ActorRef, ActorSystem, ChartSpec, JsonValue } from "@vertep/web";

export type Add = { by: number };

export type CounterEvent =
  | { type: "add" } & Add
  | { type: "reset" };
export interface CounterContext {
  count: number;
}
export type CounterStateId = "counting";

/** The chart, typed: pass it to `spawn` or `virtual`. */
export const counterChart: ChartSpec<CounterEvent, CounterContext, CounterStateId> = {
  source: "vertep: 1\nname: counter\ndatamodel: cel\ntypes:\n  Add: { by: int }\nevents: { add: Add, reset: null }\ncontext:\n  count: { type: int, init: \"0\" }\ninitial: counting\nstates:\n  counting:\n    on:\n      add:\n        - cond: \"ev.data.by > 0\"\n          actions: [ { assign: { location: ctx.count, expr: \"ctx.count + ev.data.by\" } } ]\n      reset:\n        - actions: [ { assign: { location: ctx.count, expr: \"0\" } } ]\n",
  format: "yaml",
  type: "urn:vertep:chart:sha256:4ee7f3aad3f8bf39adb28adb68271c58a9460efbe090d6549a0e1eca8f954076",
};

/** The virtual actor of this chart with `key`, typed. */
export function createCounterActor(system: ActorSystem, key: string): ActorRef<CounterEvent, CounterContext, CounterStateId> {
  return system.virtual(counterChart, key);
}

How to use the generated module is on Browser and JavaScript.

How far the projections are checked

For a projection P, the property is check(T, v) = P.accepts(P(T), encode(v)): the checker accepts a value exactly when the projection accepts its canonical encoding.

• JSON Schema: tested on generated values and near misses (the property test checker_json_schema_and_shacl_agree in crates/vertep-rdf/tests/types.rs), and proven in Lean as JsonSchema.jsonSchema_agrees, for JSON values and for type blocks whose unions have distinct tags. The pattern keyword is read as the lexical rule its regular expression encodes; that the regular expression and the rule agree is not proven.
• SHACL: tested by the same property test, and proven in Lean (Types.Shacl.shacl_agrees) for the intended shapes. List members carry a vt:listMember predicate, so every shape path is a plain predicate path that standard SHACL engines check.
• Type soundness of step (a well-typed chart only ever writes well-typed values) is proven in Lean, relative to the checker's typing and a datamodel that answers each expression with a value of its static type. vt certify accepts typed charts, and the SHACL projection of types is proven to agree with the checker.

The open items are tracked in openspec/changes/verification-backlog/tasks.md and described on Verification.