Traversal and inspection¶
A traversal coordinates movement through a protected location and the procedures it starts along the way. Reaching a destination, encountering a barrier, inspecting a group of cards and inspecting one selected object are separate pieces of work. Each needs an identity, a current stage and a caller that can resume after it returns.
Read object operations for movement and lifetime, and priority and completion for nested work. This chapter describes the asymmetric two-seat reference profile: SideB performs the ordinary traversal, while SideA controls the relevant protected locations and objects.
Give the traversal a frame before starting its events¶
The frame records a traversal identifier, phase identifier, used phase identifiers, caller, target location, current position and completion/result flags. Locations and positions come from their own admitted registries. Object metadata and the participant allowed to act are additional inputs; the frame is not an authorization certificate.
The actor, object controller and effect executor remain distinct. An encounter can concern a SideA object during SideB’s traversal, and an instruction can be executed by a specified participant. Visibility is also separate: announcing the location being approached does not reveal every concealed object there.
reference-profile · input revision 2 · CC0 1.0
OpenTraversal6(traversalId,phaseId,callerId) ==
[id |-> traversalId,phaseId |-> phaseId,usedPhaseIds |-> {phaseId},caller |-> callerId,
phase |-> "Initiation",step |-> "ProcedureCode12371046a2e5",attacked |-> "NoValue",position |-> "NoValue",
formalBegun |-> FALSE,complete |-> FALSE,ending |-> FALSE,
reachedSuccess |-> FALSE,successful |-> FALSE,unsuccessful |-> FALSE,withdrewTraversal |-> FALSE]Definition and resolved references · Exact module download · Source bundle and reproduction instructions
The new frame has not formally begun. FormalTraversalBegin6 requires the initiation work recorded by its enclosing procedure before marking the formal beginning and producing its event. Creating the record early does not count as that event.
A record update frames the components it contains. The composed state must still relate its layout, objects, windows and child procedures to that frame and constrain unrelated state.
Preserve phase and position identity¶
Approach, encounter, movement, success and ending phases describe different opportunities. A phase occurrence gets its own identifier; returning to a phase name does not mean returning to the same occurrence. The recorded used identifiers prevent an ordinary transition from reusing one where a fresh phase is required.
A position in the layout is also different from the barrier object occupying it. If a barrier moves, disappears or is exchanged, the position relationship must be updated under the appropriate layout contract. A stale object reference should not silently select whichever object later occupies that slot.
An authored example is a traversal at position 21, initially occupied by object 11. A permitted layout change can remove object 11 while the position still exists. The next approach decision must inspect the current occupancy. It cannot infer an encounter with 11 from the earlier frame. This example explains the representation; it is not a retained execution.
A requested redirection still owes completion work¶
A redirect can identify a new target and phase while the old window or checkpoint remains unfinished. The request records that pending change. The commit relation applies it only after the redirect’s required window and checkpoint work has drained.
Follow CommitTraversalRedirect6 for that boundary. It should not be replaced by an arbitrary assignment of a new phase label. A supplied authorization fact permits a particular redirection; it is not a general interpreter for every effect that mentions movement.
Similarly, an instruction ending traversal can abort subordinate encounters or inspections and create window-cleanup obligations. Completion and return still have to account for those obligations.
Select an object without leaking the candidate identities¶
An inspection procedure determines its current candidates, limits, selection method and any required preparation. Different location categories have different candidate rules. A specific-object choice and a validated random choice are not interchangeable sources of authority.
The internal candidate set can contain identities that should not be displayed as a menu. A random-choice offer can be visible while the actual identities remain concealed. Randomness, exceptional selection permission and current candidate derivation are explicit inputs or relations, rather than facts inferred from a convenient user-interface list.
Selecting an object also differs from actually beginning its individual inspection. The child binds the current object and its captured location, and it has its own begin, intermediate work, end and return boundaries.
Grant a look for the bound inspection¶
The individual look grant applies while that child is active, incomplete and still attached to its current target at the captured location:
reference-profile · input revision 2 · CC0 1.0
ItemInspectionLookGrant7(a,objects,player) ==
StillItemInspectioning7(a,objects) /\ (player = "SideB" \/ (player = "SideA" /\ a.sourceZone # "SideADeck"))Definition and resolved references · Exact module download · Source bundle and reproduction instructions
The two seats have different permissions in this profile. In particular, the default individual inspection grant does not give SideA a look at its own concealed deck card merely because SideB is inspecting it. Other lawful viewers and an actual reveal-to-both instruction are combined separately.
For an authored example, let inspection 31 bind object 11. If a valid operation removes 11 and creates successor 12, the old inspection does not acquire 12 automatically. Its presence guard fails for the old reference. The containing procedure must apply the appropriate movement-ending outcome; it cannot keep a look grant alive by matching a physical name.
Finish children, then return to the exact caller¶
An individual inspection can own an option, a cost checkpoint or another instruction. Its parent waits for that child instruction and return, rather than merely for the selection to be recorded. The overall inspection then finishes its own ending windows and checkpoint before returning to the traversal.
The traversal return has a final matching-caller guard:
reference-profile · input revision 2 · CC0 1.0
ReturnTraversalToCaller6(before,after,actualTraversalEndReactionsAndCheckpointComplete,caller) ==
/\ before.traversal.complete /\ before.traversal.id # 0 /\ ~before.returned
/\ actualTraversalEndReactionsAndCheckpointComplete /\ caller = before.traversal.caller
/\ after = [before EXCEPT !.returned = TRUE]Definition and resolved references · Exact module download · Source bundle and reproduction instructions
A successful traversal result is not permission to resume the caller before ending work finishes. Conversely, ending unsuccessfully is a result of the relevant procedure, not a reason to invent a missing return receipt.
The traversal and inspection evidence records the selected assertions, finite transition drivers, provider assumptions and bounds. A checked frame relationship does not establish every possible effect, random provider or player observation. Continue with the inspection reference, or abilities and use for the work initiated by these events.