Turns and ending¶
A turn is a piece of state with an owner and an ordered procedure. It is not just the moment when one participant happens to act. An opponent may receive a permitted opportunity during another seat’s turn, and a turn can own work that has not finished when its main action is over.
Read priority and completion for passing and returns, and zones and setup for the initial active seat. This chapter follows the asymmetric SideA/SideB reference profile.
Track the turn independently of individual actions¶
The turn record contains its owner, phase, positive identifier, formal-begin flag, formal-end flag and a begun-turn count for each seat. The phase must belong to that owner’s phase sequence. SideA has an opening draw phase; SideB starts with its action phase. Both eventually reach discard and handoff.
The owner is the active seat and receives the turn’s first priority. That does not make the owner the controller or executor of every effect during the turn. Those roles come from the relevant ability and instruction. Likewise, being active grants no general access to an opponent’s hidden information.
The surrounding procedure supplies permission to perform each actual step and evidence that its preceding work has drained. Phase and completion guards decide whether a relation may advance. A record update describes its own frame condition; variables outside that record still need constraints in the containing model.
Opening a turn deliberately leaves both formal event flags clear:
reference-profile · input revision 2 · CC0 1.0
OpenTurn5(player, turnId, begunCounts) ==
[owner |-> player,phase |-> TurnPhases5(player)[1],id |-> turnId,
formalBegun |-> FALSE,formalEnded |-> FALSE,begunCounts |-> begunCounts]Definition and resolved references · Exact module download · Source bundle and reproduction instructions
This makes room for opening procedure work before the formal turn-begin event. The count of turns begun changes at the formal-begin step, rather than merely because a new turn record was allocated.
Complete an action before advancing its caller¶
An action frame distinguishes cost reactions, effects, nested work and completion. Paying the action’s costs does not immediately authorize its effects: the cost checkpoint and reactions must finish first. Nested work records the particular structure to which the action has delegated control.
ActionNestedReturn5 requires a completed return from that recorded structure. A return from another child cannot clear the obligation. ActionComplete5 then requires the remaining effects to have resolved and no recorded nested structure to remain.
A supplied completion flag is a boundary of this contract. The small action relation checks it; it does not independently interpret every child ability that might justify it. This is the same distinction between a completion receipt and the work behind that receipt introduced in priority and completion.
End and hand off at distinct boundaries¶
Entering the discard phase, marking the formal end, finishing end reactions and opening the next turn are separate obligations. The handoff relation requires both the formal-end flag and completion of the old turn procedure:
reference-profile · input revision 2 · CC0 1.0
TurnHandoff5(before, after, oldTurnProcedureComplete, events) ==
/\ TurnFrameValid5(before) /\ before.phase = "Discard" /\ before.formalEnded
/\ oldTurnProcedureComplete /\ events = {}
/\ after = OpenTurn5(TurnOtherPlayer5(before.owner),before.id+1,before.begunCounts)Definition and resolved references · Exact module download · Source bundle and reproduction instructions
As an authored example, consider a completed SideA turn with identifier 7 and begun counts SideA 4, SideB 3. Handoff opens SideB turn 8 with those same counts and both formal flags false. At SideB’s later formal-begin step, its count becomes 4. The handoff itself emits no formal-begin event. This example reads the contracts; it is not a retained model trace.
If the old procedure has not completed, changing the active seat early does not satisfy this handoff. A phase label alone is insufficient evidence that its checkpoints and reactions have finished.
Test an ending condition at its specified boundary¶
A point total and a recorded game outcome are different state components. In the object kernel, a scoring change can make a checkpoint due; the checkpoint then evaluates objective winners with any supplied simultaneous winners. Other ending procedures, such as a required draw failure, have their own context guards.
The result of a correctly typed winner set is explicit:
reference-profile · input revision 2 · CC0 1.0
Result(winners) == CASE winners = {} -> "Playing"
[] winners = Players -> "Draw"
[] OTHER -> CHOOSE p \in winners : TRUEDefinition and resolved references · Exact module download · Source bundle and reproduction instructions
An empty set means play continues. Both seats together produce a draw. A singleton selects its seat. Those statements assume the winner set is a subset of the two admitted seats; the operator is not a validator for arbitrary sets of TLA+ values.
For an authored example, a permitted objective transition can raise SideA’s total from six to seven while the state still records play in progress and a checkpoint due. A ready checkpoint with no other winner records SideA’s result. If the winner set at that boundary contains both seats, Result yields a draw. The example does not assert that a complete application supplies every relevant simultaneous condition.
Keep terminal safety and eventual progress separate¶
The object kernel’s Next admits ordinary dispatched transitions only while its outcome is playing. Its behavior specification still allows stuttering. A recorded terminal result can therefore stop ordinary transitions without providing a proof that every permitted play must eventually reach such a result.
Permission providers, phase-step completion, effective hand-size inputs and simultaneous-ending inputs remain explicit assumptions. The turns and objectives evidence states the actual checks and bounds. Prepared assertions about a turn relation, explored finite procedures and a theorem about every possible game are different evidence claims.
Use the turn reference for formal-event and ending contracts, or continue with object operations to follow the procedures carried by an action.