Values and state¶
A model records distinctions that matter to its rules. A balance can be a number, a set can hold live object identities, and a record can collect an object’s properties. Choosing these values is part of specifying the mechanism: two states that look similar at a table may permit different next actions.
Read Reading a model first if pre-state and post-state notation are unfamiliar.
Numbers, truth values and membership¶
Nat contains zero and the positive integers. Int also contains negative integers. A spendable balance can belong to Nat even when a cost calculation uses a signed intermediate value from Int.
Expression |
Reading |
|---|---|
|
The balance is a nonnegative integer. |
|
The flag is either |
|
The actor is one of the two named seats. |
|
The balance is sufficient for this cost. |
|
The payment flag is false. |
Membership, written \in, checks a value against a collection. Quoted text such as "A" is a string. The particular spelling does not create a permission: the action’s conditions must say which seat may act.
Sets and sequences answer different questions¶
The set {2, 5} says that two identities are present. It does not order them. The sequence <<2, 5>> puts 2 first and 5 second. A discard collection may need membership; a draw order needs position. Neither representation should be inferred from the way a viewer happens to print the values.
An empty set is {} and an empty sequence is <<>>. Both contain no members, but operations on them can differ. A trace presentation must retain that distinction when the generating tool supplies it.
Records collect named fields¶
This notation example describes one object:
[identity |-> 7, controller |-> "A", zone |-> "table"]
The field identity has value 7; controller has value "A". If this record is named object, object.zone selects its zone. A record is a value, not a mutable container with an implied lifecycle. An action must describe its next value explicitly.
Functions provide a more general keyed mapping. For example, a function may associate each live identity with its current record. DOMAIN objects is the set of keys for which that mapping is defined. Looking up an identity outside that domain requires an explicit rule; a model should not rely on an accidental undefined lookup.
A state is more than one convenient record¶
The state variables chosen by a specification determine what its actions can observe and change. An example may use separate variables for balance, payment and completion. Another model may place those values in one record. These are representation choices, not automatic evidence that the models permit the same behaviors.
For each action, read its field changes together. The formula
/\ available' = available - cost
/\ paid' = TRUE
constrains the next balance and payment flag in the same step. It does not publish an intermediate state with the debit applied and the flag still false. Any additional state variables need their own next-value or UNCHANGED constraints.
State descriptions are not player observations¶
A model may record both participants’ concealed information so it can adjudicate a rule. That does not give either participant permission to read all of it. A seat’s observation needs a separate definition specifying which identities, values and history are available to that seat.
Likewise, displaying a complete referee state for an explanatory trace does not establish a safe player-facing observation interface. Keep the state needed to define a transition separate from the information a participant may use to choose it.
Continue with invariants and checking. It explains how claims about these values become questions for a checker.