Docs · Begin

Getting started

What Vertep is, what you need on your machine, how to build it from source, and one small chart taken all the way from an SCXML file to a durable actor whose past you can query.

What Vertep is

Vertep is a Rust workspace for W3C SCXML statecharts. You write a chart in SCXML, in YAML or with a Rust macro. Vertep runs it as an actor: a long-lived process with an IRI address that handles one event at a time and writes every event it accepts to a journal before it acts on it. Because the journal is complete, the actor can be stopped, moved and replayed, and its state can be read back as it was at any earlier moment.

The same chart also projects to RDF. Its version is the hash of its canonical RDF form, so a journal always records exactly which chart produced it. A chart can mark a state as a choice point (vt:decide); there a guard, a person or a language model picks the next event, but only from the events the chart enables in that state. Actors run on one node, in a cluster, across trust boundaries with DIDs, or in the browser through WebAssembly. A Lean model of the semantics checks the Rust core trace by trace.

Most applications depend on one crate, the facade vertep, and turn on what they need with cargo features: runtime, tiramemsu and scxml are on by default; ecmascript, agent, cluster and federation are opt-in (see crates/vertep/Cargo.toml).

Prerequisites

With rustup installed you do not pick the Rust version yourself: the first cargo command inside the repository installs the toolchain named in rust-toolchain.toml, together with rustfmt, clippy and the wasm32-unknown-unknown and thumbv7em-none-eabihf targets. The embedded target is there because the core is no_std: CI runs cargo build -p vertep-core --no-default-features --target thumbv7em-none-eabihf to show it needs no standard library.

Installing

The crates are on crates.io and the JavaScript packages on npm. Most Rust programs depend on the facade crate vertep and turn on the layers they need with features; the API reference is on docs.rs.

[dependencies]
vertep = "0.1"

cargo install vertep-cli          # the vt command
npm install @vertep/web           # browsers and Node.js; add @vertep/dm-ecma for ECMAScript charts

Building from source

To work on Vertep itself, or to run the examples and the proofs, build from a checkout:

git clone https://github.com/Volland/vertep.git
cd vertep
cargo build --workspace          # every crate and the examples
cargo test --workspace           # what CI runs on every push
cargo build --release -p vertep-cli
./target/release/vt --help

The vt command line: typecheck, schema, validate, hash, convert and certify

Usage: vt <COMMAND>

Commands:
  typecheck  Type-check a chart and report every error with its location
  schema     Print a projection of the chart's types
  validate   Check well-formedness and SHACL conformance
  hash       Print the chart version IRI
  convert    Convert a chart to another surface, refusing lossy conversions
  certify    Run the Lean checker and print the certificate
  gen        Generate code from a chart
  cluster    Cluster operations
  help       Print this message or the help of the given subcommand(s)

Options:
  -h, --help     Print help
  -V, --version  Print version

The JavaScript packages and the Lean model build separately. See Browser and JavaScript for npm run build in bindings/js, and Verification for lean/vertep-lean/scripts/check.sh.

A first chart, end to end

The chart below is an order. It waits in open; the event pay moves it to paid and schedules a ship event 200 ms later; ship moves it to shipped. It comes from crates/vertep/examples/quickstart.rs, the facade's own example. Save it as order.scxml.

<scxml xmlns="http://www.w3.org/2005/07/scxml" version="1.0" initial="open">
  <state id="open">
    <transition event="pay" target="paid"><send event="ship" delay="200ms"/></transition>
  </state>
  <state id="paid"><transition event="ship" target="shipped"/></state>
  <state id="shipped"/>
</scxml>

1. Check it and name its version

vt validate reads the chart, checks that it is well formed and that its RDF projection conforms to the SHACL shapes, and prints the chart's version IRI. vt hash prints only the IRI.

vt validate order.scxml
vt hash order.scxml

order.scxml: ok: urn:vertep:chart:sha256:6b74f6c5d780053619e9d360bbd73331f41fd52709d0bb7f5310d175b1272b08
urn:vertep:chart:sha256:6b74f6c5d780053619e9d360bbd73331f41fd52709d0bb7f5310d175b1272b08

The IRI is the SHA-256 of the chart's canonical RDF (RDFC-1.0). It does not depend on whitespace, attribute order or which surface you wrote the chart in. RDF and versions explains how it is computed.

2. See it in another surface

Every surface lowers to the same IR, so vt convert can write the chart back out as YAML, or as Turtle, TriG or N-Quads. It refuses a conversion that would lose information.

vt convert order.scxml --to yaml

vertep: 1
name: null
datamodel:
  value: "null"
  implicit: true
initial: open
states:
  open:
    on:
      pay:
        target: paid
        actions:
          - send:
              event: ship
              delay: "200ms"
  paid:
    on:
      ship: shipped
  shipped: {}

The chart names no datamodel, so it gets the null datamodel, and the YAML records that this was implicit. That keeps the round trip exact, and keeps the version hash the same.

3. Run it as a durable actor

The quickstart program registers the chart as an actor type, sends pay to the actor with key 42, lets the node run for 400 ms, and then reads the actor's state, its journal, and its past. These are the central lines; the full file is crates/vertep/examples/quickstart.rs.

use vertep::prelude::*;

const ORDER_TYPE: &str = "https://example.org/charts/order";

let backend = Arc::new(TiramemsuBackend::open(&dir, 1)?);
let mut node = Node::builder(backend.clone(), Shell::tokio()).build();
let chart = vertep::scxml::read_str(ORDER).map_err(|e| format!("{e:?}"))?.chart;
let version = node.register_type(ORDER_TYPE, chart)?;
println!("chart version {}", version.as_str());

// A virtual actor exists for every key: no create call, the first message activates it.
let order = Address::virtual_actor(ORDER_TYPE, "42")?;
node.send(&order, Event::named("pay", EventType::External))?;

// ... run the node for 400 ms inside a tokio LocalSet, then shut it down ...

let now = node.state(&order)?;                 // the current configuration
for e in node.journal(&order)? { /* ... */ }   // every accepted input, in order
let then = node.state_at(&order, 1)?;          // the state after entry 1, by replay

// tiramemsu never deletes, so every past transaction can be queried with SPARQL:
let shard = backend.shard_for(order.node());
shard.view_as_of(t).query(&query)?;

cargo run -p vertep --example quickstart

chart version urn:vertep:chart:sha256:6b74f6c5d780053619e9d360bbd73331f41fd52709d0bb7f5310d175b1272b08
now: ["shipped"] after 2 entries
  entry 1: pay (timers scheduled: 1)
  entry 2: ship (timers scheduled: 0)
as of entry 1: ["paid"]
  tiramemsu tx 2: in ["paid"]
  tiramemsu tx 3: in ["paid"]
  tiramemsu tx 4: in ["paid"]
  tiramemsu tx 5: in ["shipped"]
  tiramemsu tx 6: in ["shipped"]

Read the output from the top:

• The runtime computes the same version IRI that vt hash printed. Every journal segment records it, so a replay always uses the chart that wrote the entries.
• Nothing created actor 42. It is a virtual actor: it exists for every key, and the first message activated it.
• The journal has two entries. Entry 1 is pay, and it recorded one timer: the delayed ship. That timer is durable. Had the process stopped within those 200 ms, the next activation would have found it in the journal and fired it.
• Entry 2 is ship. The timer came back as an ordinary input and was journaled like any other event.
• state_at(&order, 1) rebuilt the state after entry 1 by replaying the journal up to that point, without touching the live actor.
• The last lines ask tiramemsu, the default store, what its current-state graph said after each of its transactions. The store commits more transactions than there are journal entries, so one state shows up in several of them. This is time travel without replay.

4. Use it from your own crate

Until the crates are published, point a path dependency at your checkout. The quickstart needs tokio with a current-thread runtime, because a node runs all its actors on one thread (some datamodels are not Send).

[dependencies]
vertep = { path = "../vertep/crates/vertep" }   # default features: runtime, tiramemsu, scxml
tokio = { version = "1.54", features = ["rt", "macros", "time"] }

Add features = ["agent"], ["ecmascript"], ["cluster"] or ["federation"] to the vertep line as you need them.

Where to go next

The examples are complete programs you can run, each checked against its recorded output: a traffic light on the pure core, a chart written with the Rust macro, a durable actor, a decider agent and a typed order. The docs pages go in this order: