The shape of behaviour

Most programs that live for a long time are waiting. An order waits for payment, a support ticket waits for an answer, a door waits to be opened, an agent waits for a model. While they wait, they are in a state, and what they do next depends on that state and on what happens to them. That sentence is the whole idea of a state machine. The trouble starts when we try to write it down.

Booleans pretending to be states

The usual way to write state is not to write it. A record grows fields: paid, shipped, cancelled, awaiting_review. Each handler checks some of them. Nobody wrote down which combinations are possible, so every handler has to guess. Can an order be both cancelled and shipped? The schema allows it. Four booleans make sixteen combinations, and in practice perhaps five of them are real. The other eleven are bugs waiting for a path that reaches them.

A state machine names the five and forbids the rest. It says which events each state answers and where each answer leads. Anything not written is not possible. That is a stronger promise than any number of if statements can make, because it is a promise about the whole program, not about one handler.

Flat state machines have a well-known weakness, though: they explode. Two independent concerns, each with two states, need four combined states. Three need eight. Add a "cancel from anywhere" rule and you draw the same arrow from every state. Engineers who tried flat machines on real systems often went back to booleans, because the diagram became harder to read than the code.

Harel's three additions

In 1987 David Harel published Statecharts: A Visual Formalism for Complex Systems, written while he was working on avionics. He kept the state machine and added three things.

Hierarchy. A state may contain states. Being in payment means also being in checkout, so a transition drawn once on checkout, such as cancel, applies to every state inside it. The repeated arrows disappear.

Orthogonality. A parallel state has regions that are all active at once, each with its own current state. Independent concerns stay independent. The product of their states is never drawn, and never has to be.

History. A history state remembers where a compound state was when it was left, so that coming back resumes there instead of at the start. Pausing and resuming, interrupting for an alarm, stepping out to ask a human: all of these are history.

With these three additions, a diagram of a real system fits on a page and still says everything the program may do.

One chart, written down

Here is a small order flow in SCXML, the W3C's XML notation for statecharts. checkout is a compound state, so its cancel transition covers cart, payment and review at once. Two transitions answer authorized. The first whose condition holds wins, in document order.

<scxml xmlns="http://www.w3.org/2005/07/scxml" version="1.0"
       datamodel="ecmascript" initial="idle" name="order">
  <datamodel><data id="total" expr="0"/></datamodel>

  <state id="idle">
    <transition event="start" target="checkout"/>
  </state>

  <state id="checkout" initial="cart">
    <transition event="cancel" target="cancelled"/>
    <state id="cart">
      <transition event="pay" cond="_event.data.amount &gt; 0" target="payment">
        <assign location="total" expr="_event.data.amount"/>
      </transition>
    </state>
    <state id="payment">
      <transition event="authorized" cond="total &gt; 100" target="review"/>
      <transition event="authorized" target="paid"/>
    </state>
    <state id="review">
      <transition event="approve" target="paid"/>
    </state>
  </state>

  <final id="paid"/>
  <final id="cancelled"/>
</scxml>

$ vt validate order.scxml
order.scxml: ok: urn:vertep:chart:sha256:23ede432a69736bd8c523baf5547828af92211b2cb5e9c1f99d1ac084d730327

The last line of the output deserves a word. Vertep names every chart by the hash of its canonical RDF form. Change one transition and the name changes. Every journal entry records the version it ran under, so you can always tell which rules an actor was following when it did what it did.

The algorithm is the specification

A diagram is not yet a program. Many statechart libraries agree on the pictures and disagree on the details. What happens when two transitions in different regions fire on one event and both leave a shared ancestor? Which runs first, exit actions or transition actions? Does an event raised inside an action interrupt the current step?

SCXML, a W3C Recommendation since 2015, answers all of these with an algorithm, given in pseudo-code in its Appendix D. One external event starts a macrostep. The interpreter selects the enabled transitions, resolves conflicts between them by document order, and fires them as one microstep: exit the states being left, run the transitions' actions, enter the new states. Then it takes eventless transitions and internal events, microstep after microstep, until nothing more is enabled. Only then does it look at the next external event. This is called run to completion, and it is what makes a chart's behaviour predictable.

Vertep implements that algorithm in full, as the normative behaviour of every chart, and runs the W3C conformance suite against it. Where the Recommendation leaves room for reading, Vertep writes its reading down as a decision, and the Lean model has to make the same choice.

Step as a pure function

Inside Vertep, the algorithm is two functions in vertep-core: start opens a session, and step takes the session and one input and returns what happened.

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

It does no I/O. It has no clock, no randomness and no network. When a chart wants to send a message, start a timer or ask a model, step does not do it. It returns an effect that says so, and the runtime shell around it carries the effect out. The result comes back later as another event.

This one restriction pays for most of what Vertep does:

• Journals. If step is pure, an actor's state is fully determined by the events it accepted. Store those events in order, before processing them, and you have stored the actor.
• Replay. Feed the same events to step again, on another machine, a year later, or in a browser, and you get the same states.
• Time travel. The state at any past moment is the replay up to that moment.
• Portability. The core needs nothing from its host, so the same crate runs on servers and in WebAssembly.
• Checking. A pure function can be compared with another pure function. That is where Lean comes in.

What the proof found

Vertep has a second implementation of the semantics, written in Lean 4. The Rust core records every step as a trace, and the Lean model replays the same inputs and must produce the same trace. That is differential testing, and it catches disagreements. A proof goes further. It says something about every chart, not just the ones a test generator happens to build.

One of the properties a statechart must never violate is simple to state. In every configuration, an active compound state has exactly one active child, and an active parallel state has all of its children active. The Lean package now proves it. Every session reachable by start and step from a well-formed chart has a legal configuration.

Writing that proof turned up five charts that passed validation and broke the property, all in the Rust runtime as well. Two became validation rules: a history target listed next to its own sibling, and an initial that names a history state with no default. The other three were in the entry algorithm, and they share a cause. The algorithm as Appendix D writes it recomputes a transition's domain from the history it has just recorded, and its addAncestorStatesToEnter climbs up to a history state's parent even when the transition's domain lies below that parent. On the right chart, with deep history and a parallel state in the right place, entry re-entered states that were still active. The result was a compound state with two active children, or a parallel state left inactive under its active region.

The fix is a one-line rule, now in both cores: entry never enters a state that is not a proper descendant of the transition's domain. Each case has a regression test in Rust and a matching check in Lean. None of these charts is exotic, and no test suite in the project had built one. The proof found them because a proof cannot skip a case.

A chart says what may happen. The algorithm says what does happen. The proof says the two agree, for every chart.

Why this matters beyond charts

A long-lived process is a promise to behave a certain way over time, often with money, people or other machines depending on it. Statecharts make that promise legible: you can point at a diagram and say "it cannot ship a cancelled order", and be right. A precise algorithm makes the promise executable. A pure step function makes it replayable. A proof makes it trustworthy.

The same structure also tells us where to put things that are not predictable, such as a person's judgement or a language model's answer. They go at the choice points, as events, under the chart's rules. That is the subject of the next article.