Examples

Runnable Strata examples live under examples/.

Read them in this order:

1. hello.str for the minimum source-to-runtime program.
2. actor_ping.str for spawning, sending, and a single worker transition.
3. actor_sequence.str for multiple messages and message-keyed transitions.
4. actor_match.str for whole-body match authoring that checks into typed message-keyed transitions.
5. init_match.str for whole-body match authoring in init.
6. function_match.str for module functions, process-local helpers, and pattern matching outside actor dispatch.
7. function_payload_match.str for payload-bearing enum construction and matching in normal source helpers.
8. state_payload_enum.str for payload-bearing process state enum transitions.
9. state_payload_match.str for matching immutable current process state payloads.
10. actor_instances.str for multiple runtime instances of one process definition.
11. actor_payloads.str for typed message payloads and immutable payload bindings in actor step parameter patterns.
12. actor_payload_match.str for the same payload binding through a whole-body match msg.
13. actor_reply.str for transporting typed process references through message payloads.
14. actor_panic_no_replay.str for fail-closed actor failure and no replay after message dequeue.

Hello

examples/hello.str is the first source-to-runtime gate. It checks, builds, runs, emits hello from Strata, and records an observability trace.

cargo build
cargo run -p strata --bin strata -- check examples/hello.str
cargo run -p strata --bin strata -- build examples/hello.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/hello.mta

Key source ideas:

• Main is the entry process.
• MainMsg.Start is the entry message.
• emit is declared in the step effect list.
• Stop(state) terminates normally without changing state.

Actor Ping

examples/actor_ping.str is the first actor/runtime gate. It spawns a worker, sends a message, handles that message, updates state, terminates normally, and records the runtime trace.

cargo run -p strata --bin strata -- check examples/actor_ping.str
cargo run -p strata --bin strata -- build examples/actor_ping.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_ping.mta

Key source ideas:

• Main uses let worker: ProcessRef<Worker> = spawn Worker; before send worker Ping;.
• WorkerMsg.Ping is checked against Worker’s message type.
• Worker replaces Idle with Handled.
• Both processes stop normally.

Actor Sequence

examples/actor_sequence.str exercises message-keyed process transitions. The worker handles First, returns a whole replacement state with Continue(...), then handles Second through the wildcard clause and returns a whole replacement state with Stop(...).

cargo run -p strata --bin strata -- check examples/actor_sequence.str
cargo run -p strata --bin strata -- build examples/actor_sequence.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_sequence.mta

Key source ideas:

• WorkerMsg has two variants, and each variant resolves to exactly one step clause.
• The explicit First clause handles First; _ covers the remaining accepted message variants.
• Continue(SawFirst) keeps the worker alive for the next queued message.
• Stop(Done) terminates the worker normally.

The runtime trace records process, message, state, and output IDs alongside labels so that behavior can be checked without treating labels as executable bindings.

Actor Match

examples/actor_match.str exercises the whole-body match msg authoring form. The checker resolves each arm into the same typed transition table used by step parameter patterns.

cargo run -p strata --bin strata -- check examples/actor_match.str
cargo run -p strata --bin strata -- build examples/actor_match.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_match.mta

Key source ideas:

• fn step(state: WorkerState, msg: WorkerMsg) declares a typed message parameter.
• match msg must be the whole function body in this source slice.
• Each arm returns a whole replacement state through Continue(...) or Stop(...).
• The generated Mantle artifact still dispatches by typed message IDs.

Init Match

examples/init_match.str exercises a non-step whole-body match in init. The checker resolves the fieldless enum scrutinee, proves the arms are exhaustive, and selects the typed initial state before lowering.

cargo run -p strata --bin strata -- check examples/init_match.str
cargo run -p strata --bin strata -- build examples/init_match.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/init_match.mta

Key source ideas:

• match Warm is checked against StartupMode.
• Both Cold and Warm arms return immutable whole MainState record values.
• The Mantle trace starts Main in MainState{readiness:WarmReady}, proving the selected initial state reached runtime admission.

Function Match

examples/function_match.str exercises normal source functions outside actor dispatch. It uses module-level functions and process-local helpers, including signature-pattern dispatch and a whole-body match helper.

cargo run -p strata --bin strata -- check examples/function_match.str
cargo run -p strata --bin strata -- build examples/function_match.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/function_match.mta

Key source ideas:

• readiness_sig(Cold) and readiness_sig(Warm) are module-level function clauses selected by typed signature patterns.
• readiness_body(mode: StartupMode) uses a whole-body match mode outside an actor step.
• Main and Worker declare process-local helper functions for state construction.
• send worker Assign(ready_job(Ready)) proves helper calls are expanded for message payload discovery and lowering.
• Mantle sees typed state IDs, message IDs, and payload templates, not source helper dispatch names.

Function Payload Match

examples/function_payload_match.str extends normal source helpers to payload-bearing enum values. It constructs source-visible enum payload values, matches them through signature patterns and whole-body helper matches, and lowers a received actor payload through a process-local helper into an enum payload state template.

cargo run -p strata --bin strata -- check examples/function_payload_match.str
cargo run -p strata --bin strata -- build examples/function_payload_match.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/function_payload_match.mta

Key source ideas:

• Assigned(Job { phase: Ready }) is resolved as a typed enum value, not a helper call.
• status_sig(Assigned(job: Job)) binds the enum payload immutably in a normal source helper signature pattern.
• status_body(work: Work) matches the typed helper parameter and binds the payload inside the selected arm.
• state_for(Assigned(job)) proves a process-local helper can wrap a received immutable payload into a source enum value before lowering.

State Payload Enum

examples/state_payload_enum.str admits payload-bearing process state enum values. It starts a worker in fieldless Idle, receives an immutable Job payload, and transitions to Working(Job { phase: Ready }).

cargo run -p strata --bin strata -- check examples/state_payload_enum.str
cargo run -p strata --bin strata -- build examples/state_payload_enum.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/state_payload_enum.mta

Key source ideas:

• enum WorkerState { Idle, Working(Job) } declares a payload-bearing state variant.
• return Stop(Working(job)); constructs a whole replacement state from an immutable received payload.
• Mantle receives a next-state value template and admits the resulting Working(Job{phase:Ready}) only because it is present in the typed state table.

State Payload Match

examples/state_payload_match.str matches the current process state as typed immutable data. The worker first enters Working(Job { phase: Ready }); a later Complete message dispatches over the current state and binds job inside the selected state arm.

cargo run -p strata --bin strata -- check examples/state_payload_match.str
cargo run -p strata --bin strata -- build examples/state_payload_match.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/state_payload_match.mta

Key source ideas:

• fn step(state: WorkerState, Complete) can use a whole-body match state.
• Working(job: Job) binds the state enum payload immutably for that transition arm only.
• return Stop(Done(job)); returns a whole replacement state; it does not mutate the current state in place.
• The Mantle artifact carries state-specific transitions keyed by admitted message ID plus admitted current state ID, and the payload-derived next state uses a typed current-state payload template.

Actor Instances

examples/actor_instances.str proves process references and instance-aware sends. Main spawns the Worker process definition twice, binds each runtime instance to a different process reference, and sends Ping through both references.

cargo run -p strata --bin strata -- check examples/actor_instances.str
cargo run -p strata --bin strata -- build examples/actor_instances.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_instances.mta

Key source ideas:

• let first: ProcessRef<Worker> = spawn Worker; and let second: ProcessRef<Worker> = spawn Worker; create two runtime worker instances.
• send first Ping; and send second Ping; dispatch by reference, not by process definition label.
• The runtime trace records two different pid values with the same process_id for Worker.

Actor Payloads

examples/actor_payloads.str sends a typed payload from Main to Worker. Worker binds that payload with a step parameter pattern and returns a whole replacement state containing the immutable payload value.

cargo run -p strata --bin strata -- check examples/actor_payloads.str
cargo run -p strata --bin strata -- build examples/actor_payloads.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_payloads.mta

Key source ideas:

• enum WorkerMsg { Assign(Job) } declares a payload-bearing message variant.
• send worker Assign(Job { phase: Ready }); sends one checked payload value.
• Assign(job: Job) binds the received payload as an immutable step-local value.
• WorkerState { job: job } constructs the next state as a whole value.

Actor Payload Match

examples/actor_payload_match.str proves the same immutable payload binding works from a whole-body match msg arm, not only from a step signature.

cargo run -p strata --bin strata -- check examples/actor_payload_match.str
cargo run -p strata --bin strata -- build examples/actor_payload_match.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_payload_match.mta

Key source ideas:

• fn step(state: WorkerState, msg: WorkerMsg) binds the message parameter.
• match msg dispatches through the same typed pattern validation used by signature patterns.
• Assign(job: Job) binds the received payload immutably inside the match arm.
• Runtime still dispatches by admitted message IDs and payload type IDs.

Actor Reply References

examples/actor_reply.str passes a ProcessRef<Sink> as a typed immutable message payload. Worker receives that reference and sends Done through it.

cargo run -p strata --bin strata -- check examples/actor_reply.str
cargo run -p strata --bin strata -- build examples/actor_reply.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_reply.mta

Key source ideas:

• enum WorkerMsg { Work(ProcessRef<Sink>) } declares a typed reference payload.
• send worker Work(sink); transports the spawned Sink reference to Worker.
• Work(reply_to: ProcessRef<Sink>) binds the received reference immutably.
• send reply_to Done; routes by the transported runtime process ID and admitted target process ID, not by source labels.

Actor Panic No Replay

examples/actor_panic_no_replay.str admits an explicit abnormal transition. Main queues two Ping messages to Worker; Worker dequeues one message, returns Panic(Failed), records failure evidence, and the consumed message is not replayed.

cargo run -p strata --bin strata -- check examples/actor_panic_no_replay.str
cargo run -p strata --bin strata -- build examples/actor_panic_no_replay.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_panic_no_replay.mta

The final command is expected to return non-zero. The runtime trace should show two accepted Ping messages, one message_dequeued for Worker, one process_stepped event with result:"Panic", and one process_failed event.