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
stateregions 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.