Docs · Begin

Concepts

The handful of ideas everything else in Vertep is built from, in the order they depend on each other: the chart, how it runs, how an actor wraps it, and the one rule that makes every run replayable.

Chart

A chart is a W3C SCXML statechart: a tree of states with transitions between them. A state is atomic (no children), compound (exactly one child active at a time), parallel (all children active together), final, or a history pseudo-state that remembers which children were active. Transitions fire on events, may have a condition, and carry executable content: raise, send, cancel, assign, log, script, if, foreach. A state can also run an <invoke>, a child process that lives exactly as long as the state is active.

Vertep implements the SCXML algorithm in full and treats it as the normative behaviour of every chart. Where it adds something, it does so through vt: attributes and elements in its own namespace, so a chart without them is plain SCXML.

IR

You can write a chart in SCXML, in YAML or with the statechart! macro (Writing charts). Each surface lowers to one typed intermediate representation, the Chart type in vertep-core (crates/vertep-core/src/ir.rs). The IR is the hub: conversion between surfaces, the RDF projection, hashing, type checking and execution all work on it and on nothing else.

The IR keeps document order as data, because SCXML resolves conflicts by document order. It keeps unknown vt: and foreign elements as extension nodes rather than dropping them. Before a chart can run it is validated, and every well-formedness error is reported at once: unknown targets, duplicate ids, a parallel state with an initial, history in the wrong place, and so on. Validation produces a CompiledChart, which holds derived tables (state indices, ancestors, transition domains). A compiled chart is always rebuilt from the IR and never stored.

Configuration

The configuration is the set of states that are active right now. If an atomic state is active, so are all its ancestors; a compound state has exactly one active child; a parallel state has all of them. In the traffic light from examples/traffic-light/traffic-light.scxml, the parallel state operating runs a light region and a crossing region side by side, so one configuration is:

operating light green crossing dont_walk

That a configuration is always legal in this sense is one of the theorems of the Lean model (Verification).

Macrostep and microstep

A chart takes one external event at a time and runs it to completion. That unit of work is a macrostep. Inside it, the interpreter takes microsteps: each one selects the set of enabled transitions, exits the states they leave, runs the transitions' content and enters the target states. After the transitions for the event itself, the macrostep keeps going while eventless transitions are enabled or events that the chart raised are waiting on the internal queue. When neither is left, the configuration is stable and the macrostep ends.

You can watch this in the traffic light. At start the crossing enters dont_walk, but its eventless transition cond="In('red')" is already enabled, so the same macrostep moves it on to walk. The first line of cargo run -p vertep-examples --bin traffic-light shows only the stable result:

[   0s] (start)  -> operating light red crossing walk
          schedule tick in 30s

A chart whose eventless transitions never settle would loop forever. To stop that, a macrostep has a microstep budget, 10,000 by default (DEFAULT_MICROSTEP_BUDGET in crates/vertep-core/src/session.rs); a macrostep that exceeds it is cut off and reported as an error.

step, a pure function

The interpreter is two functions in vertep_core::session. start runs the first macrostep; step runs every later one.

pub fn start(chart: &CompiledChart, input: StartInput, dm: &mut dyn Datamodel)
    -> Result<Outcome, StartError>;

pub fn step(chart: &CompiledChart, session: Session, input: Input, dm: &mut dyn Datamodel)
    -> Result<Outcome, StepError>;

pub struct Outcome {
    pub session: Session,        // the session after the macrostep
    pub effects: Vec<Effect>,    // in the order they were produced
    pub trace: MacrostepTrace,   // the macrostep record
}

pub struct Environment {
    pub now_ms: i64,             // current time, as recorded in the input
    pub seed: u64,               // seed for the datamodel's random numbers
}

The session (configuration, history, internal queue, active invocations) is a value that goes in and comes back out. The datamodel, which holds the chart's variables, is passed by mutable reference, because embedded engines such as the ECMAScript one are mutable objects. "Pure" therefore means: equal sessions, equal inputs and equal datamodel states give equal results. step does no I/O, never reads a clock and never draws a random number of its own. The current time and the random seed arrive inside the input, in its Environment.

Effects

Whatever a chart wants from the outside world, step returns as an effect instead of doing it. The host carries the effects out. The variants of vertep_core::session::Effect are:

Because every interaction is an effect, one kernel runs unchanged under three hosts: the small loop in the traffic-light example, the actor runtime, and the Lean oracle that replays its traces. Errors are not exceptions either: a failed expression becomes an error.execution event on the internal queue, and the chart can handle it like any other event.

Actor

An actor is anything that takes events one at a time and produces events. Its contract in vertep-runtime (crates/vertep-runtime/src/actor.rs) is small:

pub trait Actor {
    /// The actor's address.
    fn address(&self) -> &Address;
    /// Handles one input.
    fn turn(&mut self, input: ActorInput) -> Turn;
}

A running chart is the main kind of actor, and for a chart one turn is exactly one macrostep. Functions, tools and LLM adapters are actors too, which is why any of them can be the target of a <send>. A turn that fails leaves the journal unchanged and touches no other actor.

Mailbox

Events for an actor wait in a mailbox, a durable inbox that outlives any one activation of the actor. A mailbox can be an in-process queue, a queue kept in the store, or a DIDComm or TSP mediator for actors on the far side of a trust boundary. Vertep keeps three things apart: the identity of an actor (its IRI), its mailbox (where messages wait), and the transport (how a message travels to the mailbox). Swapping one does not change the others. Relays deliver at least once, so each message has an id, and the actor drops one it has already journaled.

Journal

Each durable actor has a journal: the ordered list of every input it accepted. The order of work in a turn is fixed:

1. Take the next message from the mailbox. If its id is already in the journal, acknowledge it and drop it.
2. Run step on it.
3. Append one entry to the journal: the input, the chart version, and the sends and timers the step produced. The append is a compare-and-set on the expected position, so if two activations of one actor ever race, the second append fails and that activation steps down.
4. Only after the append commits, dispatch the sends and arm the timers (the transactional outbox).

The append is the commit point. Before it nothing is visible; after it every recorded send is dispatched at least once, even across a crash, because a new activation re-reads the outbox. Delivery is at least once and processing is effectively once. The journal is the only source of truth: state is whatever replaying the journal produces, and snapshots only make activation faster.

Virtual actors and IRI addresses

Every actor has exactly one absolute IRI as its address. The IRI is also the RDF subject of its state and journal. Actors come in three lifecycle classes:

A virtual actor, in the style of Orleans, exists for every key. You never create one: Address::virtual_actor("https://example.org/charts/order", "42") names https://example.org/charts/order/42, and the first message to it activates it from its snapshot and journal. When it is idle it is deactivated, and a due timer activates it again. A virtual actor cannot be started by <invoke>, because no single state owns its lifetime; leaving a state must never kill an actor others share.

Chart versions

A chart version is an IRI of the form urn:vertep:chart:sha256:<hex>: the SHA-256 of the chart's RDF projection after RDFC-1.0 canonicalization. Two charts that differ only in layout, attribute order or surface have the same version; any change in behaviour gives a new one. Every journal segment records the version that wrote it, and an actor stays on its version until it reaches a final state. Moving a running actor to a new version is an explicit migration, itself written to the journal. Replaying an old journal against the latest chart would break determinism, so Vertep never does it. See RDF and versions and The actor runtime.

Deciders

A state marked vt:decide is a choice point. On entry, the core computes which events would be enabled there and offers them to a decider: guards, an LLM, a person, or another actor. The answer comes back as an event, vt.decision, is journaled like any other input, and is accepted only if it names one of the events offered. vt.decide.none is always a legal answer. A decider can choose among the chart's transitions; it can never add one. Because the decision is in the journal, a replay reproduces the run without calling the decider again. See Agents and deciders.

The determinism rule

Everything above rests on one rule:

Anything nondeterministic — time, randomness, model output, the network — enters the core only as a journaled input.

In practice:

• Time is the timestamp the shell records with the input. A chart that reads the time gets that value, both the first time and on replay. Timer due times are computed from it too.
• Randomness comes from the seed in the input's Environment. In the runtime the seed is derived from the journal entry's IRI, so a replay draws the same numbers.
• Model output, tool results and replies reach an actor only as input events journaled with their full content, so a replay never repeats the call.
• Guards may not change the datamodel; the datamodel enforces that.

Hold to the rule and the journal is the whole truth of an actor. Replay it and you get the same configurations, on a server, in a browser, or in the Lean model.

Glossary