Typed states and events

Typed events and state witnesses that constrain transitions.

Typed events and state payloads¶

A typed machine owns its State and Event enums. Transition patterns bind event and state payloads only within that transition. Initial payloads run once per instance. send returns false if no transition applies; can_send checks patterns without executing guards or actions.

Practice in By Example · Source program

// Typed catalogs make states and events ordinary nominal enum values.
machine Loader {
    state Idle, Ready(value: int)
    event Loaded(value: int), Reset
    initial Idle

    Idle -> Ready(value) on Loaded(value) if value > 0
    Ready(previous) -> Idle on Reset
}

let loader = Loader.new()
print(loader.can_send(Loader::Event::Loaded(-1))) // true: structural applicability only
print(loader.send(Loader::Event::Loaded(-1)))     // false: the guard is checked by send
print(loader.send(Loader::Event::Loaded(7)))      // true
if let Loader::State::Ready(value) = loader.state { print(value) } // 7
print(loader.send(Loader::Event::Loaded(8)))      // false: no transition from Ready
print(loader.send(Loader::Event::Reset))         // true
print(match loader.state { Loader::State::Idle => true, Loader::State::Ready(_) => false })       // true

State-indexed machines¶

new_static creates an owned machine with a state witness. send consumes it and returns the destination state type; a guarded failure returns the original machine and event. Functions can require Order<.Paid>. erase_state returns a dynamic machine when static checking is no longer needed.

Practice in By Example · Source program

machine Order {
    state Draft, Paid, Shipped
    event Pay, Ship
    initial Draft
    Draft -> Paid on Pay
    Paid -> Shipped on Ship
}

fn ship(sink order: Order<.Paid>) -> Order<.Shipped> =
    order.send(Order.Event.Ship)

let paid = Order.new_static().send(Order.Event.Pay)
let shipped = ship(sink paid)
let ordinary = shipped.erase_state()
match ordinary.state {
    .Shipped => print("shipped"),
    _ => assert(false)
}

// A guarded transition returns the original machine and event on failure.
machine Door {
    state Closed, Open
    event Unlock
    initial Closed
    Closed -> Open on Unlock if false
}
match Door.new_static().send(Door.Event.Unlock) {
    .Ok(open) => { let ordinary = open.erase_state(); assert(false) },
    .Err({ machine: closed, event: retry }) => {
        let ordinary = closed.erase_state()
        match retry { .Unlock => print("closed") }
    }
}

Continue learning¶

Documentation · Practice in By Example

Typed states and events

Typed events and state payloads¶

State-indexed machines¶

Continue learning¶

Did this page leave a question?

Find your way through Zolo

Start here