State Machines

Wire formats alone are not enough to implement a protocol correctly. A parser can decode every individual packet perfectly and still allow illegal sequences — sending data on a closed connection, retransmitting after a handshake that never completed, or abandoning a path that was never active. wirespec makes state machines a first-class language primitive: they are declared in the same .wspec file as the wire formats they describe, compiled to verifiable C dispatch code, and subject to the same type-checking rules as the rest of the language.

Basic Structure

A state machine begins with state machine Name { ... }. Inside, you declare states, the initial state, and transitions.

state machine PathState {
    state Init       { path_id: VarInt }
    state Validating { path_id: VarInt, challenge: bytes[8] }
    state Active     { path_id: VarInt, rtt: u64 = 0, cwnd: u64 = 0 }
    state Standby    { path_id: VarInt }
    state Closing    { path_id: VarInt, error_code: VarInt }
    state Closed [terminal]

    initial Init
    ...
}

Each state carries associated data declared as typed fields in braces. Fields may have default values (rtt: u64 = 0). States with no associated data need no braces (state Idle).

The [terminal] marker means the state machine cannot leave that state. Sending an event to a terminal state (other than a wildcard transition defined to absorb it) returns WIRESPEC_ERR_INVALID_STATE.

initial Name designates which state the machine starts in.

Transitions

A transition moves the machine from one state to another in response to an event.

transition Validating -> Active {
    on recv_path_response(r: bytes[8])
    guard r == src.challenge
    action { dst.path_id = src.path_id; }
}

The three optional clauses inside a transition are:

Clause	Role
on event(params)	The event that triggers this transition (required)
guard expr	Boolean condition; transition is skipped if false (optional)
action { ... }	Assignments that initialize the destination state (optional)

src and dst

• src holds the current state's data — read-only
• dst holds the next state's data — write-only
• guard may only read src
• action reads src, writes dst

Assignments inside action are separated by semicolons:

action {
    dst.path_id = src.path_id;
    dst.error_code = code;
}

A trailing semicolon after the last assignment is allowed but not required.

Complete Initialization

The compiler enforces that every dst field without a default value is assigned somewhere in the action block. Leaving a field unassigned is a compile error — there is no zero-initialization or implicit copying.

transition Active -> Closing {
    on send_path_abandon(code: VarInt)
    action {
        dst.path_id = src.path_id;    # required: Closing has path_id (no default)
        dst.error_code = code;         # required: Closing has error_code (no default)
    }
}

Fields that have defaults (rtt: u64 = 0) do not need to be assigned; they receive their default value automatically if omitted.

Wildcard Transitions

transition * -> State matches from any source state. This is how you express "this event always terminates the connection regardless of where we are":

transition * -> Closed { on connection_closed }

Concrete transitions always take priority over wildcard transitions. If both a concrete A -> B { on ev } and * -> Closed { on ev } are defined, and the machine is in state A, the concrete one wins.

State Constructors

When you need to create a state value as a literal — for example, when initializing an array element — use the state constructor syntax:

PathState::Active(path_id, 0, 0)

Arguments are positional, in the order fields are declared. Fields with defaults may be omitted from the right end:

# Active has: path_id: VarInt, rtt: u64 = 0, cwnd: u64 = 0
PathState::Active(pid)          # equivalent to PathState::Active(pid, 0, 0)
PathState::Active(pid, 10)      # equivalent to PathState::Active(pid, 10, 0)

Terminal states with no fields require no parentheses:

PathState::Closed               # not PathState::Closed()

fill() for Arrays

State fields can be arrays of other state machines. To initialize every element of an array to the same value, use the built-in fill() expression:

dst.paths = fill(PathState::Closed, 4)   # set all 4 slots to Closed

fill(value, count) is a built-in — it is not a function call and cannot be passed as a value.

Array Subscript and +=

Individual array elements can be read and assigned:

action {
    dst.paths = src.paths;
    dst.paths[src.active_path_count] = PathState::Init(path_id);
    dst.active_path_count = src.active_path_count + 1;
}

The += shorthand is available for incrementing counters:

action {
    dst.paths = src.paths;
    dst.paths[src.active_path_count] = PathState::Init(path_id);
    dst.active_path_count += 1;
}

Putting It Together: PathState

Here is the complete PathState machine from examples/mpquic/path.wspec:

module mpquic.path

import quic.varint.VarInt

state machine PathState {
    state Init       { path_id: VarInt }
    state Validating { path_id: VarInt, challenge: bytes[8] }
    state Active     { path_id: VarInt, rtt: u64 = 0, cwnd: u64 = 0 }
    state Standby    { path_id: VarInt }
    state Closing    { path_id: VarInt, error_code: VarInt }
    state Closed [terminal]

    initial Init

    transition Init -> Validating {
        on send_path_challenge(c: bytes[8])
        action { dst.path_id = src.path_id; dst.challenge = c; }
    }
    transition Validating -> Active {
        on recv_path_response(r: bytes[8])
        guard r == src.challenge
        action { dst.path_id = src.path_id; }
    }
    transition Validating -> Closed { on validation_timeout }
    transition Active -> Standby {
        on recv_path_standby
        action { dst.path_id = src.path_id; }
    }
    transition Standby -> Active {
        on recv_path_available
        action { dst.path_id = src.path_id; }
    }
    transition Active -> Closing {
        on send_path_abandon(code: VarInt)
        action { dst.path_id = src.path_id; dst.error_code = code; }
    }
    transition Standby -> Closing {
        on send_path_abandon(code: VarInt)
        action { dst.path_id = src.path_id; dst.error_code = code; }
    }
    transition Closing -> Closed { on closing_complete }
    transition * -> Closed { on connection_closed }
}

The Active <-> Standby transitions demonstrate that the same event names can appear on multiple transitions from different source states. The * -> Closed at the bottom ensures connection_closed terminates the path cleanly from any state.

delegate for Hierarchical State Machines

A state machine can hold another state machine as a field. The parent forwards events to the child using delegate:

module mpquic.connection

state machine ChildProcess {
    state Running { value: u8 }
    state Stopped [terminal]
    initial Running
    transition Running -> Stopped { on halt }
    transition * -> Stopped { on force_stop }
}

state machine SimpleDelegateExample {
    state Active { child: ChildProcess, data: u64 }
    state Closed [terminal]

    initial Active

    transition Active -> Active {
        on child_event(ev: u8)
        delegate src.child <- ev
    }

    transition Active -> Closed { on disconnect }
    transition * -> Closed { on error }
}

The delegate src.child <- ev clause in SimpleDelegateExample forwards the ev event to src.child (the ChildProcess sub-machine).

Rules for delegate:

• Only valid on self-transitions (the source and destination state must be the same, here Active -> Active)
• A transition with delegate cannot also have an explicit action block
• The target of delegate must be a field whose type is another state machine

Automatic dst initialization

When a transition uses delegate, the compiler automatically copies src into dst before forwarding the event to the child. You do not need to write dst.data = src.data yourself. The child update then happens in-place on the already-copied dst.

child_state_changed

After a delegate transition forwards an event and the child's state actually changes, the runtime fires an internal event called child_state_changed back at the parent. The parent can define a transition to react:

transition Connected -> Draining {
    on child_state_changed
    guard all(src.paths[0..src.active_path_count], in_state(Closed))
}

child_state_changed is the one event that is silently discarded when no matching transition (or no matching guard) exists. Every other unhandled event returns WIRESPEC_ERR_INVALID_STATE. This makes child_state_changed safe to fire frequently — the parent only reacts when it has something meaningful to do.

child_state_changed is a reserved identifier; you cannot define a user event with that name.

all() Quantifier and in_state()

all(collection, predicate) checks that every element of a collection satisfies a predicate:

guard all(src.paths[0..src.active_path_count], in_state(Closed))

• The collection is a slice expression (see below)
• The predicate must be in_state(StateName) — this is the only supported predicate form in v1.0
• all() is a built-in special form, not a general higher-order function

in_state(S) checks that an element is currently in state S. It is only meaningful when applied to a field or array element whose type is a state machine.

Slice Expressions

A slice collection[start..end] selects elements from index start up to (but not including) index end — a half-open range, matching Rust's .. convention:

src.paths[0..src.active_path_count]   # first active_path_count elements
src.paths[1..4]                        # elements at indices 1, 2, 3

Slices appear in:

• all(slice, predicate) — check a subset of an array
• exists i in 0..N: ... — iterate over a range of indices (in verify properties)

verify Declarations

State machines may include verify declarations:

verify NoDeadlock
verify AllReachClosed
verify property AbandonIsFinal:
    in_state(Closing) -> [] not in_state(Active)

verify NoDeadlock and verify AllReachClosed are named built-in properties that the compiler knows how to check. verify property Name: formula attaches a named temporal-logic property using the same expression language as guards, extended with temporal operators ([] always, <> eventually, ~> leads-to).

TIP

See the Formal Verification guide for the full reference on verify declarations, TLA+ model checking, and the wirespec verify CLI command.

Generated C

The compiler generates a double-switch dispatch function for each state machine. Given a machine named FooState:

wirespec_result_t foo_state_dispatch(
    foo_state_t *sm,
    foo_state_event_t event,
    const void *event_data);

The generated body looks like:

switch (sm->tag) {
    case FOO_STATE_ACTIVE:
        switch (event) {
            case FOO_STATE_EVENT_TIMEOUT:
                /* evaluate guard, then action */
                ...
                return WIRESPEC_OK;
            default:
                return WIRESPEC_ERR_INVALID_STATE;
        }
    case FOO_STATE_CLOSED:
        return WIRESPEC_ERR_INVALID_STATE;   /* terminal */
    ...
}

The outer switch selects the current state; the inner switch dispatches the event. The compiler statically verifies that all non-wildcard transitions are covered and that no (state, event) pair has two conflicting concrete transitions.

State data is represented as a tagged union:

typedef struct {
    foo_state_tag_t tag;
    union {
        foo_state_active_t active;
        foo_state_validating_t validating;
        /* ... */
    } data;
} foo_state_t;

Verification

State machines can be verified at compile time and with TLA+ model checking (built-in, no Java required). See the Formal Verification guide for details.

Quick Example

@verify(bound = 3)
state machine PathState {
    ...
    verify NoDeadlock
    verify AllReachClosed
    verify property AbandonIsFinal:
        in_state(Closing) -> [] not in_state(Active)
}

wirespec verify path.wspec

Next Steps

• Modules & Imports — Split your protocol definitions across multiple .wspec files
• Language Tour — Wire format primitives, frames, capsules, and expressions
• C API Reference — Full reference for the generated parse/serialize/dispatch functions