Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Several regions and guards

A program can declare more than one state. The specification calls each one a region. One event can update several regions at once.

intent "a cart and its statistics, updated by the same events"
    example AddItem(name: "tea"), AddItem(name: "jam"), RemoveItem(name: "tea") -> items == ["jam"] and adds == 2
    example AddItem(name: "a"), AddItem(name: "b"), AddItem(name: "c"), AddItem(name: "d") -> refused: CartFull

state Cart
    items: List[text] = []

state Stats
    adds: u64 = 0
    removes: u64 = 0

event AddItem(name: text)
event RemoveItem(name: text)

error CartFull

step Cart on AddItem(name: _) if items.len() >= 3
    fail CartFull
step Cart on AddItem(name: n) -> items.with(n)
step Stats on AddItem(name: _)
    adds += 1
step Cart on RemoveItem(name: n)
    items = [copy(i) for i in items if i != n]
step Stats on RemoveItem(name: _)
    removes += 1

AddItem has steps in both Cart and Stats. When it arrives, the step of each region runs. Each step sees the state as it was before the event, so the order in which regions are listed does not change the result.

All or nothing

The cart holds at most three items. The guarded step refuses a fourth:

$ rce run cart.rce "AddItem(name: \"a\"), AddItem(name: \"b\"), AddItem(name: \"c\"), AddItem(name: \"d\")"
0 (initial) Cart { items = [] }; Stats { adds = 0, removes = 0 }
1 AddItem(name: "a") Cart { items = ["a"] }; Stats { adds = 1, removes = 0 }
2 AddItem(name: "b") Cart { items = ["a", "b"] }; Stats { adds = 2, removes = 0 }
3 AddItem(name: "c") Cart { items = ["a", "b", "c"] }; Stats { adds = 3, removes = 0 }
4 AddItem(name: "d") refused: CartFull
exit status: 1

Look at the last line. Stats would have counted the fourth add, but because Cart refused the event, neither region changed. An event applies to every region or to none. This is what makes a refused event safe to ignore: nothing half-happened.

Examples over several fields

With more than one field in the program, an example's expected outcome is a condition on the final state, such as items == ["jam"] and adds == 2 in the intent above.

What you learned

  • Several state regions can react to the same event.
  • Every step reads the state from before the event.
  • An event is applied to all regions or refused for all of them.