Formal Card-Game Systems
r1 qualified Selected asymmetric formal reference: 2,502 contracts across nine families; bounded evidence and three separate teaching models Read the evidence scope

TraversalTimingMC

Complete selected asymmetric reference profile. Definitions and supplied fixtures are distinct from the three teaching specializations; review and qualification are stated in the bound evidence and release.

Package reference-profile, input revision 2. Exact prepared source; CC0 1.0.

This is a definition inventory. Start with the learning chapters for the contract and its assumptions.

This model/fact module also contains 154 local fixture helpers outside the selected contract inventory. Their complete executable text remains in the exact module download and owning definition bodies. Listed dependencies include paths through those helpers. All selected contracts and frozen nested helpers retain their own entries.

ActualTraversalDestinationsT11 · operator

reference-profile · input revision 2 · CC0 1.0

ActualTraversalDestinationsT11(f,completed,drained) ==
 LET b==f.control ended==[b EXCEPT !.phaseEndedIds=@ \cup {b.traversal.phaseId}]
     c==IF BeginNormalTraversalPhaseEnd6(b,ended,f.layout,f.activated,f.encounter,f.movement,f.work,completed,{TraversalPhaseEndEvent6(b.traversal)}) THEN ended ELSE b
     end==[EndTraversalOutcome6(b,1001) EXCEPT !.traversal.withdrewTraversal=TRUE]
     done==[b EXCEPT !.traversal.complete=TRUE,!.phaseEndedIds=@ \cup {b.traversal.phaseId}]
     returned==[done EXCEPT !.returned=TRUE]
 IN {TraversalDestinationT11(a) : a \in {g \in TraversalCandidateControlsT11(c) : AdvanceNormalTraversalStep6(c,g,f.layout,f.activated,f.encounter,f.movement,f.work,g.traversal.phaseId,completed,drained,{})}} \cup
    (IF f.work.jackChoice="WithdrawTraversal" /\ MovementWithdrawTraversal6(b,end,f.movement,f.layout,f.layout,1001,TRUE,completed /\ drained,TRUE,EndTraversalEffectEvents6(b)) THEN {TraversalDestinationT11(end)} ELSE {}) \cup
    (IF CompleteTraversal6(b,done,completed,{[tag |-> "TraversalEnds",traversalId |-> b.traversal.id],TraversalPhaseEndEvent6(b.traversal)},{b.traversal.id}) /\ ReturnTraversalToCaller6(done,returned,drained,"AuditCaller") THEN {TraversalDestinationT11(returned)} ELSE {})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AdvanceNormalTraversalStep6, BeginNormalTraversalPhaseEnd6, CompleteTraversal6, EndTraversalEffectEvents6, EndTraversalOutcome6, MovementWithdrawTraversal6, ReturnTraversalToCaller6, TraversalPhaseEndEvent6, TraversalCandidateControlsT11, TraversalDestinationT11

ActualTraversalOptionT11 · operator

reference-profile · input revision 2 · CC0 1.0

ActualTraversalOptionT11(w,kind,actor,target) ==
 LET option==OptionT11(kind,actor,target) IN BeginPriorityOption9(<<w>>,<<StartPriorityOptionFrame9(w,option,200)>>,option,TraversalObjectsT11,LegalityT11(w,option),EmptyT11)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BeginPriorityOption9, StartPriorityOptionFrame9, EmptyT11, LegalityT11, OptionT11, TraversalObjectsT11

ExpectedTraversalDestinationT11 · operator

reference-profile · input revision 2 · CC0 1.0

ExpectedTraversalDestinationT11(edge) == IF edge.after="ReturnToCaller" THEN <<edge.after,"OutsideTraversal">> ELSE <<edge.after,TraversalOraclePhases11[edge.after]>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TraversalOraclePhases11

LegacyTraversalWindowT11 · operator

reference-profile · input revision 2 · CC0 1.0

LegacyTraversalWindowT11(w) == [open |-> w.open,kind |-> w.kind,phaseId |-> w.site.structure.id,step |-> w.site.step,priority |-> w.priority]

Exact module download · Source bundle and reproduction instructions

TraversalActivationReceiptMatchesT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalActivationReceiptMatchesT11(w,c,a,l,receipt) ==
 /\ w.stage="Resolving" /\ w.busy.kind="Activation" /\ w.busy.controller="SideA"
 /\ receipt.windowId=w.id /\ receipt.reception=w.reception /\ receipt.site=w.site /\ receipt.option=w.busy /\ receipt.transactionId=w.busyTransaction
 /\ receipt.view.open=w.open /\ receipt.view.kind=w.kind /\ receipt.view.phaseId=w.site.structure.id /\ receipt.view.step=w.site.step /\ receipt.view.priority=w.busy.controller
 /\ w.site.traversalId=c.traversal.id /\ w.site.structure.id=c.traversal.phaseId /\ w.site.step=c.traversal.step
 /\ w.busy.target=ApproachedBarrier6(a,l)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ApproachedBarrier6

TraversalActivationReceiptT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalActivationReceiptT11(w,option) == [windowId |-> w.id,reception |-> w.reception,site |-> w.site,option |-> option,transactionId |-> 200,view |-> LegacyTraversalWindowT11(w)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: LegacyTraversalWindowT11

TraversalAuditAdvanceT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalAuditAdvanceT11 ==
 /\ qT11.ready /\ qT11.drained /\ ~qT11.specialJump /\ ~qT11.control.traversal.complete /\ qT11.stack= <<>>
 /\ \E g \in TraversalTraceCandidatesT11(qT11.control) :
      /\ AdvanceNormalTraversalStep6(qT11.control,g,qT11.layout,TraversalItemActivatedT11(qT11.objects),qT11.encounter,qT11.movement,qT11.work,g.traversal.phaseId,qT11.ready,qT11.drained,{})
      /\ TraversalViewJoinT11(qT11.control,g,qT11.approach,qT11.encounter,qT11.movement,qT11.layout,TraversalItemActivatedT11(qT11.objects))
      /\ qT11'=TraversalRecordEdgeT11(qT11,[qT11 EXCEPT !.control=g,!.ready=FALSE,!.drained=FALSE,!.pendingEvents={},
           !.approach=IF g.traversal.phase="Approach" /\ g.traversal.phaseId#qT11.control.traversal.phaseId THEN OpenApproach6(g.traversal) ELSE @,
           !.encounter=IF g.traversal.phase="Encounter" /\ g.traversal.phaseId#qT11.control.traversal.phaseId THEN OpenEncounter6(g.traversal.phaseId,ApproachedBarrier6(qT11.approach,qT11.layout),g.traversal.id,FALSE,"AuditTraversal",qT11.order) ELSE @,
           !.movement=IF g.traversal.phase="Movement" /\ g.traversal.phaseId#qT11.control.traversal.phaseId THEN OpenMovement6(g.traversal,qT11.control.traversal.phase,IF qT11.control.traversal.phase="Encounter" THEN qT11.encounter.barrierCard ELSE IF qT11.control.traversal.phase="Approach" THEN ApproachedBarrier6(qT11.approach,qT11.layout) ELSE 0,IF qT11.control.traversal.phase="Encounter" THEN qT11.encounter.id ELSE 0,TRUE) ELSE @],g.traversal.step)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11, AdvanceNormalTraversalStep6, ApproachedBarrier6, OpenApproach6, OpenEncounter6, OpenMovement6, TraversalItemActivatedT11, TraversalRecordEdgeT11, TraversalTraceCandidatesT11, TraversalViewJoinT11

TraversalAuditAfterJackT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalAuditAfterJackT11 ==
 /\ qT11.ready /\ qT11.drained /\ qT11.specialJump
 /\ qT11'=[qT11 EXCEPT !.ready=FALSE,!.drained=FALSE,!.specialJump=FALSE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

TraversalAuditDoneT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalAuditDoneT11 == qT11.control.returned

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

TraversalAuditDrainT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalAuditDrainT11 ==
 /\ qT11.ready /\ ~qT11.drained /\ ~TraversalCanEndPhaseT11(qT11)
 /\ qT11'=[qT11 EXCEPT !.drained=TRUE,!.checkpoints=Append(@,[step |-> qT11.pendingStep,phaseId |-> qT11.pendingPhase,
     insidePhase |-> qT11.pendingPhase \notin qT11.control.phaseEndedIds,insideTraversal |-> DuringTraversal6(qT11.control.traversal)])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11, DuringTraversal6, TraversalCanEndPhaseT11

TraversalAuditEventuallyReturnsT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalAuditEventuallyReturnsT11 == <>TraversalAuditDoneT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TraversalAuditDoneT11

TraversalAuditInitT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalAuditInitT11 ==
 /\ guideCaseT11=8
 /\ \E n \in 0..2 : \E activationPlan \in SUBSET OccupiedBarrier6(TraversalLayoutT11(n)),order \in {<<>>,<<1,2>>},jack \in BOOLEAN,fund \in {0,1} :
      LET l==TraversalLayoutT11(n) r==TraversalInitialT11.traversal IN
      qT11=[control |-> TraversalInitialT11,layout |-> l,objects |-> [id \in 1..4 |-> IF id \in {3,4} \ OccupiedBarrier6(l) THEN [TraversalObjectsT11[id] EXCEPT !.deployed=FALSE,!.zone="SideAHand"] ELSE TraversalObjectsT11[id]],
        approach |-> OpenApproach6(r),encounter |-> OpenEncounter6(0,0,7,FALSE,"AuditTraversal",order),movement |-> OpenMovement6(r,"Initiation",0,0,TRUE),
        order |-> order,activationPlan |-> activationPlan,jack |-> jack,initialFund |-> fund,fund |-> fund,bank |-> 12,
        stack |-> <<>>,windows |-> <<>>,nextWindow |-> 1,usedWindows |-> {},optionDone |-> FALSE,activationReceipt |-> EmptyT11,pendingEvents |-> {},
        ready |-> FALSE,drained |-> FALSE,specialJump |-> FALSE,pendingStep |-> "NoValue",pendingPhase |-> 0,
        work |-> TraversalWorkT11("Continue",0),history |-> <<>>,edges |-> <<>>,events |-> <<>>,checkpoints |-> <<>>,expired |-> {}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyT11, guideCaseT11, qT11, OccupiedBarrier6, OpenApproach6, OpenEncounter6, OpenMovement6, TraversalInitialT11, TraversalLayoutT11, TraversalObjectsT11, TraversalWorkT11

TraversalAuditInvariantT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalAuditInvariantT11 ==
 /\ guideCaseT11=8 /\ TraversalFrameValid6(qT11.control.traversal) /\ SideBPositionValid6(qT11.control.traversal,qT11.layout)
 /\ qT11.bank+qT11.fund=12+qT11.initialFund /\ qT11.bank \in Nat /\ qT11.fund \in Nat
 /\ Len(qT11.edges)<=Len(qT11.history)
 /\ \A i \in 1..Len(qT11.edges) :
      /\ qT11.edges[i] \in {[before |-> e.before,after |-> e.after,decision |-> e.decision,phaseId |-> qT11.edges[i].phaseId] : e \in TraversalOracleEdges11}
      /\ qT11.edges[i].before=qT11.history[i].step
      /\ (qT11.edges[i].before="ProcedureCodef1914978bb8e" => (qT11.edges[i].decision="BarrierInstruction")=(qT11.history[i].selectedSub#0))
 /\ \A i \in 1..Len(qT11.history) :
      LET row==qT11.history[i] IN
      /\ row.kind=TraversalOracleKinds11[row.step]
      /\ TraversalFormalConditionsT11(row.events)=TraversalExpectedFormalT11(row,qT11.layout)
      /\ (row.step="ProcedureCode714dfe070fed" /\ row.barrierCard=0 => row.events={})
      /\ (row.step="ProcedureCode714dfe070fed" => \A event \in row.events : event.tag#"PassAllBarrier" \/ (row.barrierCard#0 /\ row.position="inner") \/ (row.barrierCard#0 /\ Len(qT11.layout.orders["SchemaAtom082"])=1))
 /\ \A i \in 1..Len(qT11.checkpoints) :
      LET row==qT11.checkpoints[i] IN
      /\ (row.step="ProcedureCode9606a4cd52b4" => ~row.insideTraversal /\ ~row.insidePhase)
      /\ (row.step \in {"ProcedureCode7e3f7e5033c8","ProcedureCode4d474d346807","ProcedureCode687f72772ab1","ProcedureCodea732fbc12ae0","ProcedureCodec7b41615d673"} => ~row.insidePhase)
 /\ {event.phaseId : event \in {e \in UNION SetupRange(qT11.events) : e.tag="PhaseEnds"}}=qT11.control.phaseEndedIds
 /\ (qT11.control.traversal.complete => qT11.expired={7} /\ ~DuringTraversal6(qT11.control.traversal) /\ qT11.fund=0)
 /\ (TraversalAuditDoneT11 => qT11.control.traversal.complete /\ qT11.drained /\ qT11.fund=0 /\ qT11.bank=12+qT11.initialFund /\ qT11.control.traversal.successful#qT11.control.traversal.unsuccessful /\ Len(qT11.edges)=Len(qT11.history))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: guideCaseT11, qT11, TraversalOracleEdges11, TraversalOracleKinds11, SetupRange, DuringTraversal6, SideBPositionValid6, TraversalFrameValid6, TraversalAuditDoneT11, TraversalExpectedFormalT11, TraversalFormalConditionsT11

TraversalAuditNextT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalAuditNextT11 == /\ UNCHANGED guideCaseT11
 /\ (TraversalAuditWorkT11 \/ TraversalAuditWindowOpenT11 \/ TraversalAuditWindowStepT11 \/ TraversalAuditPhaseEndT11 \/ TraversalAuditDrainT11 \/ TraversalAuditAdvanceT11 \/ TraversalAuditAfterJackT11 \/ TraversalAuditReturnT11 \/ (TraversalAuditDoneT11 /\ UNCHANGED qT11))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: guideCaseT11, qT11, TraversalAuditAdvanceT11, TraversalAuditAfterJackT11, TraversalAuditDoneT11, TraversalAuditDrainT11, TraversalAuditPhaseEndT11, TraversalAuditReturnT11, TraversalAuditWindowOpenT11, TraversalAuditWindowStepT11, TraversalAuditWorkT11

TraversalAuditPhaseEndT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalAuditPhaseEndT11 ==
 /\ qT11.ready /\ ~qT11.drained /\ TraversalCanEndPhaseT11(qT11)
 /\ qT11'=[qT11 EXCEPT !.control=TraversalPhaseEndCandidateT11(qT11.control),!.events=Append(@,{TraversalPhaseEndEvent6(qT11.control.traversal)})]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11, TraversalPhaseEndEvent6, TraversalCanEndPhaseT11, TraversalPhaseEndCandidateT11

TraversalAuditReturnT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalAuditReturnT11 ==
 /\ qT11.ready /\ qT11.drained /\ qT11.control.traversal.complete /\ ~TraversalAuditDoneT11
 /\ LET c==[qT11.control EXCEPT !.returned=TRUE] IN
      /\ ReturnTraversalToCaller6(qT11.control,c,qT11.drained,"AuditCaller")
      /\ qT11'=TraversalRecordEdgeT11(qT11,[qT11 EXCEPT !.control=c],"ReturnToCaller")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11, ReturnTraversalToCaller6, TraversalAuditDoneT11, TraversalRecordEdgeT11

TraversalAuditSpecT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalAuditSpecT11 == TraversalAuditInitT11 /\ [][TraversalAuditNextT11]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(TraversalAuditNextT11)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: guideCaseT11, qT11, TraversalAuditInitT11, TraversalAuditNextT11

TraversalAuditWindowOpenT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalAuditWindowOpenT11 ==
 /\ ~TraversalAuditDoneT11 /\ ~qT11.ready /\ qT11.stack= <<>> /\ TraversalStepInfo6(qT11.control.traversal.step).kind="PaidWindow"
 /\ LET c==qT11.control e==qT11.encounter
        paid==WithFullySuppressInstruction6([e EXCEPT !.stage="Paid",!.paidReached=TRUE])
        site==TraversalSiteT11("SideB",c,qT11.approach,qT11.layout) id==qT11.nextWindow w==TraversalWindowT11(id,site) IN
    /\ (c.traversal.phase#"Encounter" \/ BeginEncounterPaid6(e,paid,TRUE,NewFullySuppressInstructionEvents6(e,paid)))
    /\ OpenPriorityWindow9(<<>>,<<w>>,id,"Paid",site,EmptyT11,TraversalOpeningT11(id,site),qT11.usedWindows)
    /\ qT11'=[qT11 EXCEPT !.stack= <<w>>,!.control.paidOpen=TRUE,!.nextWindow=@+1,!.usedWindows=@ \cup {id},!.optionDone=FALSE,
         !.encounter=IF c.traversal.phase="Encounter" THEN paid ELSE @,!.pendingEvents=IF c.traversal.phase="Encounter" THEN NewFullySuppressInstructionEvents6(e,paid) ELSE {}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenPriorityWindow9, EmptyT11, qT11, BeginEncounterPaid6, NewFullySuppressInstructionEvents6, TraversalStepInfo6, WithFullySuppressInstruction6, TraversalAuditDoneT11, TraversalOpeningT11, TraversalSiteT11, TraversalWindowT11

TraversalAuditWindowStepT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalAuditWindowStepT11 ==
 /\ ~TraversalAuditDoneT11 /\ ~qT11.ready /\ Len(qT11.stack)=1
 /\ LET w==WindowTop9(qT11.stack) barrierCard==ApproachedBarrier6(qT11.approach,qT11.layout)
        wantActivation==w.site.step="ProcedureCode3a6daf593ad4" /\ w.priority="SideA" /\ barrierCard \in qT11.activationPlan /\ ~qT11.objects[barrierCard].activated IN
    \/ /\ w.stage="NeedCheckpoint" /\ CheckpointPriority9(qT11.stack,<<PriorityReadyT11(w)>>,PriorityCheckpointT11(w))
       /\ qT11'=[qT11 EXCEPT !.stack= <<PriorityReadyT11(w)>>]
    \/ /\ w.stage="Ready" /\ wantActivation
       /\ LET option==OptionT11("Activation","SideA",barrierCard) next==StartPriorityOptionFrame9(w,option,200) IN
          /\ BeginPriorityOption9(qT11.stack,<<next>>,option,qT11.objects,LegalityT11(w,option),EmptyT11)
          /\ qT11'=[qT11 EXCEPT !.stack= <<next>>,!.optionDone=FALSE,!.activationReceipt=TraversalActivationReceiptT11(w,option)]
    \/ /\ w.stage="Resolving" /\ ~qT11.optionDone
       /\ TraversalActivationReceiptMatchesT11(w,qT11.control,qT11.approach,qT11.layout,qT11.activationReceipt)
       /\ LET card==qT11.objects[w.busy.target] after==[card EXCEPT !.face="Up",!.activated=TRUE] IN
          /\ ApproachActivation6(qT11.control.traversal,qT11.approach,qT11.layout,qT11.activationReceipt.view,w.busy.target,card,after,TRUE,TRUE)
          /\ qT11'=[qT11 EXCEPT !.objects[w.busy.target]=after,!.optionDone=TRUE]
    \/ /\ w.stage="Resolving" /\ qT11.optionDone
       /\ CompletePriorityOption9(qT11.stack,<<CompletePriorityOptionFrame9(w)>>,TraversalOptionReturnT11(w,qT11.optionDone))
       /\ qT11'=[qT11 EXCEPT !.stack= <<CompletePriorityOptionFrame9(w)>>]
    \/ /\ w.stage="Ready" /\ ~wantActivation
       /\ PassPriority9(qT11.stack,<<PassPriorityFrame9(w)>>,w.priority,[id |-> 0])
       /\ qT11'=[qT11 EXCEPT !.stack= <<PassPriorityFrame9(w)>>]
    \/ /\ w.stage="Closed" /\ PopClosedPriorityWindow9(qT11.stack,<<>>)
       /\ LET e==qT11.encounter after==[e EXCEPT !.stage="BarrierInstructions"] IN
          /\ (w.site.step#"ProcedureCode8b3260c0010f" \/ CloseEncounterPaid6(e,after,TRUE))
          /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.stack= <<>>,!.control.paidOpen=FALSE,!.windows=Append(@,qT11.control.traversal.step),!.encounter=IF w.site.step="ProcedureCode8b3260c0010f" THEN after ELSE @],qT11.pendingEvents)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BeginPriorityOption9, CheckpointPriority9, CompletePriorityOption9, CompletePriorityOptionFrame9, PassPriority9, PassPriorityFrame9, PopClosedPriorityWindow9, StartPriorityOptionFrame9, WindowTop9, EmptyT11, LegalityT11, OptionT11, PriorityCheckpointT11, PriorityReadyT11, qT11, ApproachActivation6, ApproachedBarrier6, CloseEncounterPaid6, TraversalActivationReceiptMatchesT11, TraversalActivationReceiptT11, TraversalAuditDoneT11, TraversalOptionReturnT11, TraversalRecordWorkT11

TraversalAuditWorkT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalAuditWorkT11 ==
 /\ ~TraversalAuditDoneT11 /\ ~qT11.ready /\ qT11.stack= <<>>
 /\ LET c==qT11.control r==c.traversal kind==TraversalStepInfo6(r.step).kind IN
    CASE kind="AnnounceAndPay" ->
      LET g==[c EXCEPT !.traversal.attacked="SchemaAtom082",!.announced=TRUE,!.costsPaid=TRUE] ev=={[tag |-> "TraversalTargetSiteAnnounced",traversalId |-> r.id,targetSite |-> "SchemaAtom082"]} IN
      /\ AnnounceTraversalTargetSite6(c,g,"SchemaAtom082",[SchemaAtom082 |-> 1],TRUE,TRUE,ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g],ev)
    [] kind="LiabilityMarker" ->
      LET g==[c EXCEPT !.badPubAdded=TRUE] IN
      /\ AddInitiationLiabilityMarker6(c,g,qT11.fund,qT11.fund+2,2)
      /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g,!.fund=@+2,!.bank=@-2],{})
    [] kind="TraversalBegins" ->
      LET g==[c EXCEPT !.traversal.formalBegun=TRUE] ev=={TraversalBeginEvent6(r)} IN
      /\ FormalTraversalBegin6(c,g,ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g],ev)
    [] kind="InitialPosition" ->
      LET g==[r EXCEPT !.position=OutermostOccupiedPosition6(qT11.layout,r.attacked)] IN
      /\ SetInitialSideBPosition6(r,g,qT11.layout,r.step) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control.traversal=g],{})
    [] kind="ApproachBarrier" ->
      LET a==[qT11.approach EXCEPT !.begun=TRUE] ev=={[tag |-> "ApproachBarrier",barrierCard |-> ApproachedBarrier6(a,qT11.layout),phaseId |-> r.phaseId,traversalId |-> r.id]} IN
      /\ BeginApproach6(r,qT11.approach,a,qT11.layout,ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.approach=a],ev)
    [] kind="EncounterBarrier" ->
      LET e==[qT11.encounter EXCEPT !.stage="BeginReactions"] ev=={[tag |-> "EncounterBarrier",encounterId |-> e.id,barrierCard |-> e.barrierCard,traversalId |-> e.traversalId]} IN
      /\ BeginEncounter6(qT11.encounter,e,TRUE,ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.encounter=e],ev)
    [] kind="NextBarrierInstruction" ->
      LET sub==NextEncounterSub6(qT11.encounter) e==IF sub=0 THEN qT11.encounter ELSE [qT11.encounter EXCEPT !.resolved=@ \cup {sub}] IN
      /\ (sub=0 \/ ResolveEncounterSub6(qT11.encounter,e,sub,TRUE))
      /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.encounter=e,!.work.resolvedSub=sub],{})
    [] kind="PassBarrier" ->
      LET m==[qT11.movement EXCEPT !.begun=TRUE,!.passedBarrier=MovementBarrier6(r,qT11.layout),!.passedAll=MovementBarrier6(r,qT11.layout)#0 /\ NextInwardPosition6(qT11.layout,r.attacked,r.position)="NoValue"] ev==MovementPassEvents6(r,qT11.layout) IN
      /\ BeginMovement6(r,qT11.movement,m,qT11.layout,ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.movement=m],ev)
    [] kind="WithdrawTraversalDecision" ->
      IF qT11.jack THEN
        LET g==[EndTraversalOutcome6(c,r.phaseId+1) EXCEPT !.traversal.withdrewTraversal=TRUE] ev==EndTraversalEffectEvents6(c)
            before==[qT11 EXCEPT !.work.jackChoice="WithdrawTraversal"] next==[before EXCEPT !.control=g,!.specialJump=TRUE] IN
        /\ MovementWithdrawTraversal6(c,g,qT11.movement,qT11.layout,qT11.layout,r.phaseId+1,TRUE,TRUE,TRUE,ev)
        /\ qT11'=TraversalRecordEdgeT11(before,TraversalRecordWorkT11(before,next,ev),"ProcedureCode6ea937bb44ac")
      ELSE LET m==[qT11.movement EXCEPT !.declined=TRUE] IN
        /\ DeclineMovementWithdrawTraversal6(r,qT11.movement,m,TRUE)
        /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.movement=m,!.work.jackChoice="Continue"],{})
    [] kind="AdvancePosition" ->
      LET g==[r EXCEPT !.position=NextInwardPosition6(qT11.layout,r.attacked,r.position)] m==[qT11.movement EXCEPT !.advanced=TRUE,!.movedToNew=g.position#"NoValue"] IN
      /\ AdvanceMovement6(r,g,qT11.movement,m,qT11.layout,qT11.layout)
      /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control.traversal=g,!.movement=m],{})
    [] kind="ApproachTargetSite" ->
      LET m==[qT11.movement EXCEPT !.approachedTargetSite=TRUE] ev=={[tag |-> "ApproachTargetSite",traversalId |-> r.id,targetSite |-> r.attacked,phaseId |-> r.phaseId]} IN
      /\ ApproachTargetSite6(r,qT11.movement,m,ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.movement=m],ev)
    [] kind="DeclareSuccessful" ->
      LET g==[c EXCEPT !.declarationProcessed=TRUE,!.traversal.successful=TRUE] ev=={[tag |-> "SuccessfulTraversal",traversalId |-> r.id,targetSite |-> r.attacked]} IN
      /\ DeclareSuccessfulTraversal6(c,g,TRUE,ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g],ev)
    [] kind="RulesInspection" ->
      IF ~c.siteInspectionChosen THEN
        LET g==[c EXCEPT !.siteInspectionChosen=TRUE] directive==[kind |-> "Inspection",choice |-> "Inspection",traversalId |-> r.id,targetSite |-> r.attacked,origin |-> "RulesTraversalInspection"] IN
        /\ ChooseRulesInspection6(c,g,"Inspection",{"Inspection"},TRUE,directive) /\ qT11'=[qT11 EXCEPT !.control=g]
      ELSE LET g==[c EXCEPT !.siteInspectionFinished=TRUE] IN
        /\ FinishRulesInspectionInstruction6(c,g,TRUE) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g],{})
    [] kind="EndWindows" ->
      LET g==[c EXCEPT !.windowsDone=TRUE] IN
      /\ FinishTraversalEndWindows6(c,g) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g],{})
    [] kind="ReturnLiabilityMarker" ->
      LET g==[c EXCEPT !.fundReturned=TRUE] IN
      /\ ReturnLiabilityMarkerFund6(c,g,qT11.fund,0,qT11.bank,qT11.bank+qT11.fund)
      /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g,!.bank=@+qT11.fund,!.fund=0],{})
    [] kind="DeclareUnsuccessful" ->
      LET applies==ShouldDeclareUnsuccessful6(r,[SchemaAtom082 |-> 1]) g==[c EXCEPT !.resultDeclared=TRUE,!.traversal.unsuccessful=applies]
          ev==IF applies THEN {[tag |-> "UnsuccessfulTraversal",traversalId |-> r.id,targetSite |-> r.attacked]} ELSE {} IN
      /\ DeclareUnsuccessfulTraversal6(c,g,[SchemaAtom082 |-> 1],ev) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g],ev)
    [] kind="CompleteTraversal" ->
      LET g==[c EXCEPT !.traversal.complete=TRUE,!.phaseEndedIds=@ \cup {r.phaseId}] ev=={[tag |-> "TraversalEnds",traversalId |-> r.id],TraversalPhaseEndEvent6(r)} IN
      /\ CompleteTraversal6(c,g,TRUE,ev,{r.id}) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.control=g,!.expired={r.id}],ev)
    [] kind="CompletePhase" /\ r.phase="Encounter" ->
      LET e==[qT11.encounter EXCEPT !.stage="Complete"] IN
      /\ CompleteEncounter6(qT11.encounter,e,TRUE) /\ qT11'=TraversalRecordWorkT11(qT11,[qT11 EXCEPT !.encounter=e],{})
    [] kind \in {"CompletePhase","BarrierInstructionLoop","MovementBranch"} -> qT11'=TraversalRecordWorkT11(qT11,qT11,{})
    [] OTHER -> FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11, AddInitiationLiabilityMarker6, AdvanceMovement6, AnnounceTraversalTargetSite6, ApproachTargetSite6, ApproachedBarrier6, BeginApproach6, BeginEncounter6, BeginMovement6, ChooseRulesInspection6, CompleteEncounter6, CompleteTraversal6, DeclareSuccessfulTraversal6, DeclareUnsuccessfulTraversal6, DeclineMovementWithdrawTraversal6, EndTraversalEffectEvents6, EndTraversalOutcome6, FinishRulesInspectionInstruction6, FinishTraversalEndWindows6, FormalTraversalBegin6, MovementBarrier6, MovementPassEvents6, MovementWithdrawTraversal6, NextEncounterSub6, NextInwardPosition6, OutermostOccupiedPosition6, ResolveEncounterSub6, ReturnLiabilityMarkerFund6, SetInitialSideBPosition6, ShouldDeclareUnsuccessful6, TraversalBeginEvent6, TraversalPhaseEndEvent6, TraversalStepInfo6, TraversalAuditDoneT11, TraversalRecordEdgeT11, TraversalRecordWorkT11

TraversalCanEndPhaseT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalCanEndPhaseT11(s) == BeginNormalTraversalPhaseEnd6(s.control,TraversalPhaseEndCandidateT11(s.control),s.layout,TraversalItemActivatedT11(s.objects),s.encounter,s.movement,s.work,s.ready,{TraversalPhaseEndEvent6(s.control.traversal)})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BeginNormalTraversalPhaseEnd6, TraversalPhaseEndEvent6, TraversalItemActivatedT11, TraversalPhaseEndCandidateT11

TraversalCandidateControlsT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalCandidateControlsT11(c) ==
 {TraversalPostFrameT11(c,step,phase,pid) : step \in TraversalOracleStepSet11 \cup {"UnauthorizedStep"},phase \in {"Initiation","Approach","Encounter","Movement","Success","TraversalEnds"},pid \in {c.traversal.phaseId,c.traversal.phaseId+1}}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TraversalOracleStepSet11, TraversalPostFrameT11

TraversalCleanupAndAdapterChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalCleanupAndAdapterChecksT11 ==
 LET paid==[id |-> 1,kind |-> "Paid",open |-> TRUE,beginPhaseId |-> 0,pending |-> {},lostPending |-> {},priority |-> "SideB"]
     begin==[paid EXCEPT !.id=2,!.kind="Reaction",!.beginPhaseId=1000,!.pending={1,2}]
     other==[paid EXCEPT !.id=3,!.kind="Reaction",!.pending={3}]
     pc==[paid EXCEPT !.open=FALSE,!.priority="NoValue"] bc==[begin EXCEPT !.open=FALSE,!.pending={},!.lostPending={1,2},!.priority="NoValue"] oc==[other EXCEPT !.open=FALSE,!.pending={},!.priority="NoValue"]
     c==TraversalGraphFixtureT11("ProcedureCode3a6daf593ad4","Next").control a==[OpenApproach6(c.traversal) EXCEPT !.begun=TRUE] l==TraversalLayoutT11(2)
     w==PriorityReadyT11(PassPriorityFrame9(PriorityReadyT11(TraversalWindowT11(1,TraversalSiteT11("SideB",c,a,l))))) option==OptionT11("Activation","SideA",3)
     resolving==StartPriorityOptionFrame9(w,option,200) receipt==TraversalActivationReceiptT11(w,option)
     forced==[OpenEncounter6(900,3,7,TRUE,"ExactChildCaller",<<>>) EXCEPT !.stage="Complete"]
 IN /\ ProcessTraversalEndWindow6(<<paid>>,<<>>,pc,FALSE,{},{}) /\ ~ProcessTraversalEndWindow6(<<paid>>,<<>>,pc,TRUE,{1},{})
    /\ ProcessTraversalEndWindow6(<<begin>>,<<>>,bc,FALSE,{},{}) /\ ~ProcessTraversalEndWindow6(<<begin>>,<<>>,bc,TRUE,{1},{})
    /\ ProcessTraversalEndWindow6(<<other>>,<<>>,oc,TRUE,{3},{}) /\ ~ProcessTraversalEndWindow6(<<other>>,<<>>,oc,FALSE,{},{})
    /\ ~ProcessTraversalEndWindow6(<<other>>,<<>>,oc,TRUE,{3},{"NewStructure"})
    /\ BeginPriorityOption9(<<w>>,<<resolving>>,option,TraversalObjectsT11,LegalityT11(w,option),EmptyT11)
    /\ resolving.priority="NoValue" /\ receipt.view.priority="SideA"
    /\ TraversalActivationReceiptMatchesT11(resolving,c,a,l,receipt)
    /\ ~TraversalActivationReceiptMatchesT11(resolving,c,a,l,[receipt EXCEPT !.windowId=99])
    /\ ~TraversalActivationReceiptMatchesT11(resolving,c,a,l,[receipt EXCEPT !.reception=99])
    /\ ~TraversalActivationReceiptMatchesT11(resolving,c,a,l,[receipt EXCEPT !.site.turnId=99])
    /\ ~TraversalActivationReceiptMatchesT11(resolving,c,a,l,[receipt EXCEPT !.option.target=4])
    /\ ~TraversalActivationReceiptMatchesT11(resolving,c,a,l,[receipt EXCEPT !.transactionId=99])
    /\ ~TraversalActivationReceiptMatchesT11(resolving,[c EXCEPT !.traversal.id=99],a,l,receipt)
    /\ ~TraversalActivationReceiptMatchesT11(resolving,[c EXCEPT !.traversal.phaseId=99],a,l,receipt)
    /\ ~TraversalActivationReceiptMatchesT11(resolving,[c EXCEPT !.traversal.step="ProcedureCode4d474d346807"],a,l,receipt)
    /\ ~TraversalActivationReceiptMatchesT11([resolving EXCEPT !.busy.target=4],c,a,l,receipt)
    /\ ReturnForcedEncounter6(<<forced>>,<<>>,c.traversal,c.traversal,"ExactChildCaller",{},{900})
    /\ ~ReturnForcedEncounter6(<<forced>>,<<>>,c.traversal,c.traversal,"WrongChildCaller",{},{900})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BeginPriorityOption9, PassPriorityFrame9, StartPriorityOptionFrame9, EmptyT11, LegalityT11, OptionT11, PriorityReadyT11, OpenApproach6, OpenEncounter6, ProcessTraversalEndWindow6, ReturnForcedEncounter6, TraversalActivationReceiptMatchesT11, TraversalActivationReceiptT11, TraversalGraphFixtureT11, TraversalLayoutT11, TraversalObjectsT11, TraversalSiteT11, TraversalWindowT11

TraversalControlT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalControlT11(r) ==
 [traversal |-> r,encounter |-> IF r.phase="Encounter" THEN r.phaseId ELSE 0,siteInspections |-> EmptyT11,itemInspections |-> EmptyT11,
  abortedEncounters |-> {},abortedInspectiones |-> {},abortedItemInspectiones |-> {},paidOpen |-> FALSE,windows |-> <<>>,
  windowCleanupDue |-> FALSE,onlyWindowCleanup |-> FALSE,phaseEndedIds |-> {},phaseStepsSkipped |-> FALSE,
  redirect |-> NoTraversalRedirect6,redirectStage |-> "NoValue",redirectCheckpointDue |-> FALSE,
  announced |-> FALSE,costsPaid |-> FALSE,badPubAdded |-> FALSE,declarationProcessed |-> FALSE,
  siteInspectionChosen |-> FALSE,siteInspectionFinished |-> FALSE,windowsDone |-> FALSE,fundReturned |-> FALSE,resultDeclared |-> FALSE,returned |-> FALSE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyT11, NoTraversalRedirect6

TraversalDecisionT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalDecisionT11(s) ==
 CASE s.control.traversal.step="ProcedureCode7e3f7e5033c8" -> IF s.control.traversal.position \in DOMAIN s.layout.slots /\ s.layout.slots[s.control.traversal.position].barrierCard#0 THEN "Barrier" ELSE "NoBarrier"
 [] s.control.traversal.step="ProcedureCode4d474d346807" -> IF ApproachedBarrier6(s.approach,s.layout) \in TraversalItemActivatedT11(s.objects) THEN "ItemActivated" ELSE "NoEncounter"
 [] s.control.traversal.step="ProcedureCodef1914978bb8e" -> IF s.work.resolvedSub#0 THEN "BarrierInstruction" ELSE "NoBarrierInstruction"
 [] s.control.traversal.step="ProcedureCode9bca3a096549" -> s.work.jackChoice
 [] s.control.traversal.step="ProcedureCode6c5d14f545f7" -> IF s.movement.movedToNew THEN "NewPosition" ELSE "NoPosition"
 [] OTHER -> "Next"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ApproachedBarrier6, TraversalItemActivatedT11

TraversalDestinationT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalDestinationT11(c) == IF c.returned THEN <<"ReturnToCaller","OutsideTraversal">> ELSE <<c.traversal.step,c.traversal.phase>>

Exact module download · Source bundle and reproduction instructions

TraversalEncounterAndMovementChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalEncounterAndMovementChecksT11 ==
 LET r==[TraversalGraphFixtureT11("ProcedureCode714dfe070fed","Next").control.traversal EXCEPT !.position="outer"] l==TraversalLayoutT11(2)
     e0==OpenEncounter6(1000,3,7,FALSE,"AuditTraversal",<<1,2>>) eb==[e0 EXCEPT !.stage="BeginReactions"]
     ep==[eb EXCEPT !.stage="Paid",!.paidReached=TRUE] es==[ep EXCEPT !.stage="BarrierInstructions"]
     one==[es EXCEPT !.resolved={1}] both==[one EXCEPT !.resolved={1,2}] done==[both EXCEPT !.stage="Complete"]
     m0==OpenMovement6(r,"Encounter",3,1000,TRUE) m1==[m0 EXCEPT !.begun=TRUE,!.passedBarrier=3]
     decisionTraversal==[r EXCEPT !.step="ProcedureCode9bca3a096549"] declined==[m1 EXCEPT !.declined=TRUE]
     advanceTraversal==[r EXCEPT !.step="ProcedureCoded4ddeafb5f2f"] inward==[advanceTraversal EXCEPT !.position="inner"]
 IN /\ BeginEncounter6(e0,eb,TRUE,{[tag |-> "EncounterBarrier",encounterId |-> 1000,barrierCard |-> 3,traversalId |-> 7]})
    /\ BeginEncounterPaid6(eb,ep,TRUE,{}) /\ ~BeginEncounterPaid6(eb,ep,FALSE,{})
    /\ CloseEncounterPaid6(ep,es,TRUE) /\ ~CloseEncounterPaid6(ep,es,FALSE)
    /\ TraversalOracleSuppressInstructionSteps11={"ProcedureCode8b3260c0010f"}
    /\ LET c==TraversalGraphFixtureT11("ProcedureCode8b3260c0010f","Next").control a==[OpenApproach6(c.traversal) EXCEPT !.begun=TRUE]
            w==PriorityReadyT11(TraversalWindowT11(1,TraversalSiteT11("SideB",c,a,l)))
            barrierInstructionSuppressed==[ep EXCEPT !.barrierInstructionSuppressed={1},!.barrierInstructionSuppressedBy[1]=700] IN
         /\ PaidSuppressInstructionEncounterSubs6(ep,barrierInstructionSuppressed,LegacyTraversalWindowT11(w),{1},700,TRUE,TRUE,{})
         /\ ~PaidSuppressInstructionEncounterSubs6(ep,barrierInstructionSuppressed,[LegacyTraversalWindowT11(w) EXCEPT !.step="ProcedureCode4f60245a1dde"],{1},700,TRUE,TRUE,{})
         /\ ~PaidSuppressInstructionEncounterSubs6(ep,barrierInstructionSuppressed,[LegacyTraversalWindowT11(w) EXCEPT !.phaseId=99],{1},700,TRUE,TRUE,{})
         /\ ~PaidSuppressInstructionEncounterSubs6(ep,barrierInstructionSuppressed,[LegacyTraversalWindowT11(w) EXCEPT !.priority="SideA"],{1},700,TRUE,TRUE,{})
         /\ ~PaidSuppressInstructionEncounterSubs6(ep,barrierInstructionSuppressed,LegacyTraversalWindowT11(w),{1},700,FALSE,TRUE,{})
         /\ ~PaidSuppressInstructionEncounterSubs6(ep,barrierInstructionSuppressed,LegacyTraversalWindowT11(w),{1},700,TRUE,FALSE,{})
    /\ NextEncounterSub6(es)=1 /\ ResolveEncounterSub6(es,one,1,TRUE) /\ NextEncounterSub6(one)=2
    /\ ~ResolveEncounterSub6(es,[es EXCEPT !.resolved={2}],2,TRUE) /\ ~ResolveEncounterSub6(es,one,1,FALSE)
    /\ ~ResolveEncounterSub6(one,one,1,TRUE) /\ ResolveEncounterSub6(one,both,2,TRUE) /\ NextEncounterSub6(both)=0
    /\ CompleteEncounter6(both,done,TRUE) /\ ~CompleteEncounter6(one,[one EXCEPT !.stage="Complete"],TRUE)
    /\ ~CompleteEncounter6(both,done,FALSE)
    /\ MovementPassEvents6(r,l)={[tag |-> "PassBarrier",traversalId |-> 7,phaseId |-> 1000,barrierCard |-> 3]}
    /\ MovementPassEvents6([r EXCEPT !.position="NoValue"],l)={}
    /\ MovementPassEvents6(r,[l EXCEPT !.slots["outer"].barrierCard=0])={}
    /\ MovementPassEvents6([r EXCEPT !.position="inner"],l)={[tag |-> "PassBarrier",traversalId |-> 7,phaseId |-> 1000,barrierCard |-> 4],[tag |-> "PassAllBarrier",traversalId |-> 7,phaseId |-> 1000,barrierCard |-> 4]}
    /\ BeginMovement6(r,m0,m1,l,MovementPassEvents6(r,l))
    /\ DeclineMovementWithdrawTraversal6(decisionTraversal,m1,declined,TRUE) /\ ~DeclineMovementWithdrawTraversal6(decisionTraversal,m1,declined,FALSE)
    /\ AdvanceMovement6(advanceTraversal,inward,declined,[declined EXCEPT !.advanced=TRUE,!.movedToNew=TRUE],l,l)
    /\ NextInwardPosition6(l,"SchemaAtom082","inner")="NoValue" /\ NextInwardPosition6(l,"SchemaAtom082","outer")="inner"
    /\ ~AdvanceMovement6(advanceTraversal,inward,m1,[m1 EXCEPT !.advanced=TRUE,!.movedToNew=TRUE],l,l)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PriorityReadyT11, TraversalOracleSuppressInstructionSteps11, AdvanceMovement6, BeginEncounter6, BeginEncounterPaid6, BeginMovement6, CloseEncounterPaid6, CompleteEncounter6, DeclineMovementWithdrawTraversal6, MovementPassEvents6, NextEncounterSub6, NextInwardPosition6, OpenApproach6, OpenEncounter6, OpenMovement6, PaidSuppressInstructionEncounterSubs6, ResolveEncounterSub6, LegacyTraversalWindowT11, TraversalGraphFixtureT11, TraversalLayoutT11, TraversalSiteT11, TraversalWindowT11

TraversalEntryAndGraphChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalEntryAndGraphChecksT11 ==
 /\ TraversalInitialT11.traversal.step=TraversalOracleEntry11 /\ TraversalInitialT11.traversal.phase="Initiation" /\ ~TraversalInitialT11.traversal.formalBegun /\ ~DuringTraversal6(TraversalInitialT11.traversal)
 /\ TraversalSteps6=TraversalOracleStepSet11 /\ TraversalOracleHidden11={}
 /\ \A step \in TraversalOracleStepSet11 : TraversalStepInfo6(step).kind=TraversalOracleKinds11[step] /\ TraversalStepInfo6(step).phase=TraversalOraclePhases11[step]
 /\ \A edge \in TraversalOracleEdges11 :
      LET f==TraversalGraphFixtureT11(edge.before,edge.decision) IN
      /\ ActualTraversalDestinationsT11(f,TRUE,TRUE)={ExpectedTraversalDestinationT11(edge)}
      /\ ActualTraversalDestinationsT11(f,FALSE,TRUE)={} /\ ActualTraversalDestinationsT11(f,TRUE,FALSE)={}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TraversalOracleEdges11, TraversalOracleEntry11, TraversalOracleHidden11, TraversalOracleKinds11, TraversalOraclePhases11, TraversalOracleStepSet11, DuringTraversal6, TraversalStepInfo6, TraversalSteps6, ActualTraversalDestinationsT11, ExpectedTraversalDestinationT11, TraversalGraphFixtureT11, TraversalInitialT11

TraversalExpectedFormalT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalExpectedFormalT11(row,layout) ==
 IF row.step="ProcedureCode714dfe070fed" THEN IF row.barrierCard=0 THEN {} ELSE {"PassBarrier"} \cup (IF row.position=Head(layout.orders["SchemaAtom082"]) THEN {"PassAllProtectingBarrier"} ELSE {})
 ELSE IF row.step="ProcedureCode5e397645e65c" THEN IF ~row.reachedSuccess /\ row.targetSiteExists THEN {"UnsuccessfulTraversal"} ELSE {}
 ELSE IF row.step \in DOMAIN TraversalOracleFormalConditions11 THEN TraversalOracleFormalConditions11[row.step] ELSE {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TraversalOracleFormalConditions11

TraversalFormalConditionsT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalFormalConditionsT11(events) == UNION
 {CASE e.tag="TraversalBegins" -> {"TraversalBegins"} \cup (IF e.alsoInitiates THEN {"TraversalInitiated"} ELSE {})
  [] e.tag="ApproachBarrier" -> {"ApproachBarrierBegins"} [] e.tag="EncounterBarrier" -> {"EncounterBarrierBegins"}
  [] e.tag="PassBarrier" -> {"PassBarrier"} [] e.tag="PassAllBarrier" -> {"PassAllProtectingBarrier"}
  [] e.tag="ApproachTargetSite" -> {"ApproachTargetSite"} [] e.tag="SuccessfulTraversal" -> {"SuccessfulTraversal"}
  [] e.tag="UnsuccessfulTraversal" -> {"UnsuccessfulTraversal"} [] e.tag="TraversalEnds" -> {"TraversalEnds"} [] OTHER -> {} : e \in events}

Exact module download · Source bundle and reproduction instructions

TraversalGraphFixtureT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalGraphFixtureT11(step,decision) ==
 LET r==[OpenTraversal6(7,1000,"AuditCaller") EXCEPT !.step=step,!.phase=TraversalOraclePhases11[step],!.attacked="SchemaAtom082",
          !.formalBegun=step \notin {"ProcedureCode12371046a2e5","ProcedureCodeacc82dbcc545"},!.ending=TraversalOraclePhases11[step]="TraversalEnds",
          !.position=IF TraversalOraclePhases11[step] \in {"Success","TraversalEnds"} \/ step \in {"ProcedureCode7e82ab2b38b7","ProcedureCodea732fbc12ae0"} \/ decision \in {"NoBarrier","NoPosition"}
                     THEN "NoValue" ELSE IF decision="NewPosition" THEN "inner" ELSE "outer",
          !.reachedSuccess=TraversalOraclePhases11[step]="Success",!.successful=TraversalOraclePhases11[step]="Success"]
     c==[TraversalControlT11(r) EXCEPT !.announced=TRUE,!.costsPaid=TRUE,!.badPubAdded=TRUE,!.declarationProcessed=TRUE,
          !.siteInspectionChosen=TRUE,!.siteInspectionFinished=TRUE,!.windowsDone=TRUE,!.fundReturned=TRUE,!.resultDeclared=TRUE]
     e==[OpenEncounter6(1000,3,7,FALSE,"AuditTraversal",IF decision="NoBarrierInstruction" THEN <<1>> ELSE <<1,2>>) EXCEPT
          !.stage=IF step="ProcedureCodeda7bff1d9270" THEN "BeginReactions" ELSE IF step="ProcedureCode687f72772ab1" THEN "Complete" ELSE "BarrierInstructions",!.paidReached=TRUE,!.resolved={1}]
     m==[OpenMovement6(r,"Approach",3,0,TRUE) EXCEPT !.begun=TRUE,!.declined=decision#"WithdrawTraversal",!.advanced=TRUE,
          !.movedToNew=decision="NewPosition",!.approachedTargetSite=step="ProcedureCodea732fbc12ae0"]
 IN [control |-> c,encounter |-> e,movement |-> m,layout |-> TraversalLayoutT11(2),activated |-> IF decision="ItemActivated" THEN {3} ELSE {},
     work |-> TraversalWorkT11(IF decision="WithdrawTraversal" THEN "WithdrawTraversal" ELSE "Continue",IF decision="BarrierInstruction" THEN 1 ELSE 0)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TraversalOraclePhases11, OpenEncounter6, OpenMovement6, OpenTraversal6, TraversalControlT11, TraversalLayoutT11, TraversalWorkT11

TraversalInitialT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalInitialT11 == TraversalControlT11(OpenTraversal6(7,1000,"AuditCaller"))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenTraversal6, TraversalControlT11

TraversalInitiationAndPositionChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalInitiationAndPositionChecksT11 ==
 LET b==TraversalInitialT11 a==[b EXCEPT !.announced=TRUE,!.costsPaid=TRUE,!.traversal.attacked="SchemaAtom082"]
     bp==[a EXCEPT !.traversal.step="ProcedureCodeacc82dbcc545"] funded==[bp EXCEPT !.badPubAdded=TRUE]
     begin==[funded EXCEPT !.traversal.step="ProcedureCode4d6bd06d2c9f"] begun==[begin EXCEPT !.traversal.formalBegun=TRUE]
     pos==[begun.traversal EXCEPT !.step="ProcedureCode347de0bdd6b4"] placed==[pos EXCEPT !.position="outer"]
     approachTraversal==[placed EXCEPT !.phase="Approach",!.step="ProcedureCode453e949a114f"] approach==OpenApproach6(approachTraversal) approached==[approach EXCEPT !.begun=TRUE]
     paidTraversal==[approachTraversal EXCEPT !.step="ProcedureCode3a6daf593ad4"] w==[open |-> TRUE,kind |-> "Paid",phaseId |-> 1000,step |-> "ProcedureCode3a6daf593ad4",priority |-> "SideA"]
     barrierCard==TraversalObjectsT11[3] up==[barrierCard EXCEPT !.face="Up",!.activated=TRUE]
 IN /\ AnnounceTraversalTargetSite6(b,a,"SchemaAtom082",[SchemaAtom082 |-> 1],TRUE,TRUE,{[tag |-> "TraversalTargetSiteAnnounced",traversalId |-> 7,targetSite |-> "SchemaAtom082"]})
    /\ ~AnnounceTraversalTargetSite6(b,a,"SchemaAtom082",[SchemaAtom082 |-> 1],FALSE,TRUE,{[tag |-> "TraversalTargetSiteAnnounced",traversalId |-> 7,targetSite |-> "SchemaAtom082"]})
    /\ ~AnnounceTraversalTargetSite6(b,a,"SchemaAtom082",[SchemaAtom082 |-> 1],TRUE,FALSE,{[tag |-> "TraversalTargetSiteAnnounced",traversalId |-> 7,targetSite |-> "SchemaAtom082"]})
    /\ AddInitiationLiabilityMarker6(bp,funded,1,3,2) /\ ~AddInitiationLiabilityMarker6(bp,funded,1,2,2)
    /\ ~AddInitiationLiabilityMarker6([bp EXCEPT !.costsPaid=FALSE],[funded EXCEPT !.costsPaid=FALSE],1,3,2)
    /\ FormalTraversalBegin6(begin,begun,{TraversalBeginEvent6(begin.traversal)}) /\ DuringTraversal6(begun.traversal) /\ ~FormalTraversalBegin6(begin,begun,{})
    /\ ~FormalTraversalBegin6([begin EXCEPT !.badPubAdded=FALSE],[begun EXCEPT !.badPubAdded=FALSE],{TraversalBeginEvent6(begin.traversal)})
    /\ SetInitialSideBPosition6(pos,placed,TraversalLayoutT11(2),"ProcedureCode347de0bdd6b4") /\ SetInitialSideBPosition6(pos,[pos EXCEPT !.position="NoValue"],TraversalLayoutT11(0),"ProcedureCode347de0bdd6b4")
    /\ ~SetInitialSideBPosition6(pos,placed,TraversalLayoutT11(2),"ProcedureCode4d6bd06d2c9f")
    /\ BeginApproach6(approachTraversal,approach,approached,TraversalLayoutT11(2),{[tag |-> "ApproachBarrier",barrierCard |-> 3,phaseId |-> 1000,traversalId |-> 7]})
    /\ ApproachActivation6(paidTraversal,approached,TraversalLayoutT11(2),w,3,barrierCard,up,TRUE,TRUE)
    /\ ~ApproachActivation6(paidTraversal,approached,TraversalLayoutT11(2),w,3,barrierCard,up,FALSE,TRUE)
    /\ ~ApproachActivationPermission6(paidTraversal,approached,TraversalLayoutT11(2),w,4)
    /\ ~ApproachActivationPermission6(paidTraversal,approached,TraversalLayoutT11(2),[w EXCEPT !.phaseId=99],3)
    /\ ~ApproachActivationPermission6(paidTraversal,approached,TraversalLayoutT11(2),[w EXCEPT !.priority="SideB"],3)
    /\ InitiationDestination6([placed EXCEPT !.step="ProcedureCode7e3f7e5033c8"],[TraversalLayoutT11(2) EXCEPT !.slots["outer"].barrierCard=0])="Movement"
    /\ ApproachDestination6(approached,TraversalLayoutT11(2),{})="Movement"
    /\ ApproachDestination6(approached,[TraversalLayoutT11(2) EXCEPT !.slots["outer"].barrierCard=0],{3})="Movement"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AddInitiationLiabilityMarker6, AnnounceTraversalTargetSite6, ApproachActivation6, ApproachActivationPermission6, ApproachDestination6, BeginApproach6, DuringTraversal6, FormalTraversalBegin6, InitiationDestination6, OpenApproach6, SetInitialSideBPosition6, TraversalBeginEvent6, TraversalInitialT11, TraversalLayoutT11, TraversalObjectsT11

TraversalItemActivatedT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalItemActivatedT11(objects) == {id \in DOMAIN objects : objects[id].deployed /\ objects[id].kind="Barrier" /\ objects[id].activated}

Exact module download · Source bundle and reproduction instructions

TraversalLayoutT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalLayoutT11(n) ==
 [orders |-> [SchemaAtom082 |-> IF n=0 THEN <<>> ELSE IF n=1 THEN <<"outer">> ELSE <<"inner","outer">>],
  slots |-> [p \in IF n=0 THEN {} ELSE IF n=1 THEN {"outer"} ELSE {"inner","outer"} |->
    [targetSite |-> "SchemaAtom082",barrierCard |-> IF p="outer" THEN 3 ELSE 4,reservation |-> 0,retained |-> FALSE]],used |-> {"inner","outer"}]

Exact module download · Source bundle and reproduction instructions

TraversalObjectsT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalObjectsT11 == [id \in 1..4 |-> IF id=4 THEN TestObjectsT11[3] ELSE TestObjectsT11[id]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TestObjectsT11

TraversalOpeningT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalOpeningT11(id,site) == [tag |-> "PriorityWindowOpening",windowId |-> id,kind |-> "Paid",site |-> site,members |-> {},instances |-> EmptyT11,group |-> 0,beginning |-> NoTimingRef9,instruction |-> [id |-> 0],effectRevision |-> 0]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NoTimingRef9, EmptyT11

TraversalOptionReturnT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalOptionReturnT11(w,done) == [tag |-> "PriorityOptionReturn",windowId |-> w.id,option |-> w.busy,transactionId |-> w.busyTransaction,triggerPayment |-> TraversalPaymentT11(w),allCostsPaid |-> TRUE,optionComplete |-> done,childrenReturned |-> TRUE,reactionsDrained |-> TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TraversalPaymentT11

TraversalPaymentT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalPaymentT11(w) == [tag |-> "PriorityOptionPayment",windowId |-> w.id,option |-> w.busy,transactionId |-> w.busyTransaction,allTriggerCostsPaid |-> TRUE,costCheckpointAndReactionsDrained |-> TRUE]

Exact module download · Source bundle and reproduction instructions

TraversalPhaseAndLastSubChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalPhaseAndLastSubChecksT11 ==
 LET f==TraversalGraphFixtureT11("ProcedureCode7e3f7e5033c8","Barrier") b==f.control ended==TraversalPhaseEndCandidateT11(b)
     g==TraversalPostFrameT11(ended,"ProcedureCode453e949a114f","Approach",1001) missing==TraversalPostFrameT11(b,"ProcedureCode453e949a114f","Approach",1001)
     stale==TraversalPostFrameT11(ended,"ProcedureCode453e949a114f","Approach",1000)
     sub==[TraversalGraphFixtureT11("ProcedureCodef1914978bb8e","BarrierInstruction") EXCEPT !.encounter=[OpenEncounter6(1000,3,7,FALSE,"AuditTraversal",<<1>>) EXCEPT !.stage="BarrierInstructions",!.paidReached=TRUE,!.resolved={1}]]
 IN /\ BeginNormalTraversalPhaseEnd6(b,ended,f.layout,f.activated,f.encounter,f.movement,f.work,TRUE,{TraversalPhaseEndEvent6(b.traversal)})
    /\ ~BeginNormalTraversalPhaseEnd6(ended,ended,f.layout,f.activated,f.encounter,f.movement,f.work,TRUE,{TraversalPhaseEndEvent6(b.traversal)})
    /\ ~AdvanceNormalTraversalStep6(b,missing,f.layout,f.activated,f.encounter,f.movement,f.work,1001,TRUE,TRUE,{})
    /\ AdvanceNormalTraversalStep6(ended,g,f.layout,f.activated,f.encounter,f.movement,f.work,1001,TRUE,TRUE,{})
    /\ ~AdvanceNormalTraversalStep6(ended,stale,f.layout,f.activated,f.encounter,f.movement,f.work,1000,TRUE,TRUE,{})
    /\ ActualTraversalDestinationsT11(sub,TRUE,TRUE)={<<"ProcedureCodeaa0828fbf852","Encounter">>}
    /\ TraversalPhaseEndEvent6(b.traversal)=[tag |-> "PhaseEnds",phase |-> b.traversal.phase,phaseId |-> b.traversal.phaseId,traversalId |-> b.traversal.id]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AdvanceNormalTraversalStep6, BeginNormalTraversalPhaseEnd6, OpenEncounter6, TraversalPhaseEndEvent6, ActualTraversalDestinationsT11, TraversalGraphFixtureT11, TraversalPhaseEndCandidateT11, TraversalPostFrameT11

TraversalPhaseEndCandidateT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalPhaseEndCandidateT11(c) == [c EXCEPT !.phaseEndedIds=@ \cup {c.traversal.phaseId}]

Exact module download · Source bundle and reproduction instructions

TraversalPointwiseChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalPointwiseChecksT11 == CASE guideCaseT11=1 -> (TraversalEntryAndGraphChecksT11 /\ TraversalPhaseAndLastSubChecksT11) [] guideCaseT11=2 -> TraversalWindowChecksT11
 [] guideCaseT11=3 -> TraversalInitiationAndPositionChecksT11 [] guideCaseT11=4 -> TraversalEncounterAndMovementChecksT11 [] guideCaseT11=5 -> TraversalSuccessAndEndChecksT11 [] OTHER -> TraversalCleanupAndAdapterChecksT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: guideCaseT11, TraversalCleanupAndAdapterChecksT11, TraversalEncounterAndMovementChecksT11, TraversalEntryAndGraphChecksT11, TraversalInitiationAndPositionChecksT11, TraversalPhaseAndLastSubChecksT11, TraversalSuccessAndEndChecksT11, TraversalWindowChecksT11

TraversalPointwiseInitT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalPointwiseInitT11 == guideCaseT11 \in 1..6 /\ qT11=EmptyT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyT11, guideCaseT11, qT11

TraversalPointwiseSpecT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalPointwiseSpecT11 == TraversalPointwiseInitT11 /\ [][PointwiseNextT11]_<<guideCaseT11,qT11>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PointwiseNextT11, guideCaseT11, qT11, TraversalPointwiseInitT11

TraversalPostFrameT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalPostFrameT11(c,step,phase,pid) ==
 [c EXCEPT !.traversal.step=step,!.traversal.phase=phase,!.traversal.phaseId=pid,
    !.traversal.usedPhaseIds=IF phase#c.traversal.phase THEN @ \cup {pid} ELSE @,
    !.traversal.reachedSuccess=@ \/ phase="Success",!.traversal.ending=@ \/ phase="TraversalEnds",
    !.traversal.position=IF phase \in {"Success","TraversalEnds"} THEN "NoValue" ELSE @,
    !.encounter=IF phase="Encounter" THEN pid ELSE IF c.traversal.phase="Encounter" THEN 0 ELSE @,
    !.phaseStepsSkipped=FALSE,!.windowCleanupDue=IF phase="TraversalEnds" /\ phase#c.traversal.phase THEN TRUE ELSE IF c.traversal.step="ProcedureCode6ea937bb44ac" THEN FALSE ELSE @]

Exact module download · Source bundle and reproduction instructions

TraversalRecordEdgeT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalRecordEdgeT11(before,after,target) ==
 [after EXCEPT !.edges=Append(@,[before |-> before.control.traversal.step,after |-> target,decision |-> TraversalDecisionT11(before),phaseId |-> before.control.traversal.phaseId])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TraversalDecisionT11

TraversalRecordWorkT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalRecordWorkT11(before,after,events) ==
 [after EXCEPT !.ready=TRUE,!.drained=FALSE,!.pendingStep=before.control.traversal.step,!.pendingPhase=before.control.traversal.phaseId,
   !.history=Append(@,[step |-> before.control.traversal.step,kind |-> TraversalStepInfo6(before.control.traversal.step).kind,phaseId |-> before.control.traversal.phaseId,
     events |-> events,position |-> before.control.traversal.position,barrierCard |-> MovementBarrier6(before.control.traversal,before.layout),selectedSub |-> after.work.resolvedSub,reachedSuccess |-> before.control.traversal.reachedSuccess,targetSiteExists |-> before.control.traversal.attacked \in DOMAIN before.layout.orders]),
   !.events=Append(@,events)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MovementBarrier6, TraversalStepInfo6

TraversalSiteT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalSiteT11(player,c,a,l) == TraversalPrioritySite9(TraversalTurnT11(player),c.traversal,a,l,c)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TraversalPrioritySite9, TraversalTurnT11

TraversalSuccessAndEndChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalSuccessAndEndChecksT11 ==
 LET c==TraversalGraphFixtureT11("ProcedureCodebbb14496b09b","Next").control s==[c EXCEPT !.declarationProcessed=FALSE,!.traversal.successful=FALSE]
     declared==[s EXCEPT !.declarationProcessed=TRUE,!.traversal.successful=TRUE]
     prevented==[s EXCEPT !.declarationProcessed=TRUE] b==[declared EXCEPT !.traversal.step="ProcedureCoded75d879e00ff"] chosen==[b EXCEPT !.siteInspectionChosen=TRUE]
     bf==[b EXCEPT !.siteInspectionChosen=FALSE,!.siteInspectionFinished=FALSE] bc==[bf EXCEPT !.siteInspectionChosen=TRUE]
     directive==[kind |-> "Inspection",choice |-> "Inspection",traversalId |-> 7,targetSite |-> "SchemaAtom082",origin |-> "RulesTraversalInspection"]
     end==[TraversalGraphFixtureT11("ProcedureCode6ea937bb44ac","Next").control EXCEPT !.windowsDone=FALSE,!.fundReturned=FALSE,!.resultDeclared=FALSE]
     wd==[end EXCEPT !.windowsDone=TRUE] fund==[wd EXCEPT !.traversal.step="ProcedureCode84dea7dc8ecc"] fr==[fund EXCEPT !.fundReturned=TRUE]
     result==[fr EXCEPT !.traversal.step="ProcedureCode5e397645e65c"] aDrawPile==[result EXCEPT !.resultDeclared=TRUE,!.traversal.unsuccessful=TRUE]
     last==[aDrawPile EXCEPT !.traversal.step="ProcedureCode9606a4cd52b4"] completed==[last EXCEPT !.traversal.complete=TRUE,!.phaseEndedIds={1000}]
     events=={[tag |-> "TraversalEnds",traversalId |-> 7],TraversalPhaseEndEvent6(last.traversal)}
 IN /\ DeclareSuccessfulTraversal6(s,declared,TRUE,{[tag |-> "SuccessfulTraversal",traversalId |-> 7,targetSite |-> "SchemaAtom082"]})
    /\ DeclareSuccessfulTraversal6(s,prevented,FALSE,{}) /\ ~ShouldDeclareUnsuccessful6(prevented.traversal,[SchemaAtom082 |-> 1])
    /\ ChooseRulesInspection6(bf,bc,"Inspection",{"Inspection"},TRUE,directive) /\ ~ChooseRulesInspection6(bf,bc,"Inspection",{"Inspection"},FALSE,directive)
    /\ FinishRulesInspectionInstruction6(bc,[bc EXCEPT !.siteInspectionFinished=TRUE],TRUE)
    /\ ~FinishRulesInspectionInstruction6(bc,[bc EXCEPT !.siteInspectionFinished=TRUE],FALSE)
    /\ FinishTraversalEndWindows6(end,wd) /\ ReturnLiabilityMarkerFund6(fund,fr,3,0,10,13)
    /\ ~ReturnLiabilityMarkerFund6([fund EXCEPT !.windowsDone=FALSE],[fr EXCEPT !.windowsDone=FALSE],3,0,10,13)
    /\ ~ReturnLiabilityMarkerFund6(fund,fr,3,1,10,12)
    /\ DeclareUnsuccessfulTraversal6(result,aDrawPile,[SchemaAtom082 |-> 1],{[tag |-> "UnsuccessfulTraversal",traversalId |-> 7,targetSite |-> "SchemaAtom082"]})
    /\ ~ShouldDeclareUnsuccessful6(result.traversal,EmptyT11)
    /\ DuringTraversal6(last.traversal) /\ CompleteTraversal6(last,completed,TRUE,events,{7}) /\ ~DuringTraversal6(completed.traversal)
    /\ ~CompleteTraversal6(last,completed,FALSE,events,{7})
    /\ ReturnTraversalToCaller6(completed,[completed EXCEPT !.returned=TRUE],TRUE,"AuditCaller")
    /\ ~ReturnTraversalToCaller6(completed,[completed EXCEPT !.returned=TRUE],FALSE,"AuditCaller")
    /\ ~ReturnTraversalToCaller6(completed,[completed EXCEPT !.returned=TRUE],TRUE,"WrongCaller")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyT11, ChooseRulesInspection6, CompleteTraversal6, DeclareSuccessfulTraversal6, DeclareUnsuccessfulTraversal6, DuringTraversal6, FinishRulesInspectionInstruction6, FinishTraversalEndWindows6, ReturnLiabilityMarkerFund6, ReturnTraversalToCaller6, ShouldDeclareUnsuccessful6, TraversalPhaseEndEvent6, TraversalGraphFixtureT11

TraversalTraceCandidatesT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalTraceCandidatesT11(c) ==
 {TraversalPostFrameT11(c,step,TraversalStepInfo6(step).phase,IF TraversalStepInfo6(step).phase=c.traversal.phase THEN c.traversal.phaseId ELSE c.traversal.phaseId+1) : step \in TraversalSteps6}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TraversalStepInfo6, TraversalSteps6, TraversalPostFrameT11

TraversalTurnT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalTurnT11(player) == [OpenTurn5(player,2,[SideA |-> 1,SideB |-> 1]) EXCEPT !.phase="NeutralValue00001",!.formalBegun=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenTurn5

TraversalViewJoinT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalViewJoinT11(c,g,a,e,m,l,activated) ==
 CASE c.traversal.step="ProcedureCode7e3f7e5033c8" -> CompleteInitiationTraversalView6(c.traversal,g.traversal,l,g.traversal.phaseId,TRUE)
 [] c.traversal.step="ProcedureCode4d474d346807" -> CompleteApproachTraversalView6(c.traversal,g.traversal,a,l,activated,g.traversal.phaseId,TRUE)
 [] c.traversal.step="ProcedureCode687f72772ab1" -> CompleteOrdinaryEncounterTraversalView6(c.traversal,g.traversal,e,g.traversal.phaseId,TRUE)
 [] c.traversal.step="ProcedureCodea732fbc12ae0" \/ (c.traversal.step="ProcedureCode6c5d14f545f7" /\ m.movedToNew) -> CompleteMovementTraversalView6(c.traversal,g.traversal,m,g.traversal.phaseId,TRUE)
 [] c.traversal.step="ProcedureCodec7b41615d673" -> CompleteSuccessTraversalView6([traversal |-> c.traversal,siteInspectionFinished |-> c.siteInspectionFinished],[traversal |-> g.traversal,siteInspectionFinished |-> g.siteInspectionFinished],g.traversal.phaseId,TRUE)
 [] OTHER -> TRUE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CompleteApproachTraversalView6, CompleteInitiationTraversalView6, CompleteMovementTraversalView6, CompleteOrdinaryEncounterTraversalView6, CompleteSuccessTraversalView6

TraversalWindowChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalWindowChecksT11 ==
 /\ \A step \in TraversalOracleStepSet11 :
      LET expected==IF step \in DOMAIN TraversalOracleWindowOptions11 THEN TraversalOracleWindowOptions11[step] ELSE [paid |-> FALSE,nonBarrierActivation |-> FALSE,approachedBarrierActivation |-> FALSE,score |-> FALSE] IN
      /\ TraversalWindowOptions6(step)=expected
      /\ \A player \in SetupPlayers :
           LET c==TraversalGraphFixtureT11(step,"Next").control a==[OpenApproach6(c.traversal) EXCEPT !.begun=TRUE] l==TraversalLayoutT11(2) site==TraversalSiteT11(player,c,a,l) IN
           /\ WindowSiteAllowed9("Paid",site)=expected.paid
           /\ (expected.paid =>
                LET w==TraversalWindowT11(1,site) first==PriorityReadyT11(w) SchemaAtom187==PriorityReadyT11(PassPriorityFrame9(first))
                    sideA==IF player="SideA" THEN first ELSE SchemaAtom187 sideB==IF player="SideB" THEN first ELSE SchemaAtom187 IN
                /\ w.priority=player /\ OpenPriorityWindow9(<<>>,<<w>>,1,"Paid",site,EmptyT11,TraversalOpeningT11(1,site),{})
                /\ ActualTraversalOptionT11(sideA,"RegularPaid","SideA",0) /\ ActualTraversalOptionT11(sideB,"RegularPaid","SideB",0)
                /\ ActualTraversalOptionT11(sideA,"Activation","SideA",1)=expected.nonBarrierActivation /\ ActualTraversalOptionT11(sideA,"Activation","SideA",2)=expected.nonBarrierActivation
                /\ ActualTraversalOptionT11(sideA,"Activation","SideA",3)=expected.approachedBarrierActivation /\ ~ActualTraversalOptionT11(sideA,"Activation","SideA",4)
                /\ ~ActualTraversalOptionT11(sideB,"Activation","SideB",1) /\ ~ActualTraversalOptionT11(sideA,"ObjectiveCompletion","SideA",0) /\ ~ActualTraversalOptionT11(sideB,"ObjectiveCompletion","SideB",0)
                /\ ~ActualTraversalOptionT11(first,"RegularPaid",(IF player="SideA" THEN "SideB" ELSE "SideA"),0)
                /\ CheckpointPriority9(<<w>>,<<first>>,PriorityCheckpointT11(w))
                /\ ~CheckpointPriority9(<<w>>,<<first>>,[PriorityCheckpointT11(w) EXCEPT !.reactionsDrained=FALSE])
                /\ ~CheckpointPriority9(<<w>>,<<first>>,[PriorityCheckpointT11(w) EXCEPT !.reception=99])
                /\ ~WindowSiteAllowed9("Paid",[site EXCEPT !.timingLive=FALSE]))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointPriority9, OpenPriorityWindow9, PassPriorityFrame9, WindowSiteAllowed9, EmptyT11, PriorityCheckpointT11, PriorityReadyT11, TraversalOracleStepSet11, TraversalOracleWindowOptions11, SetupPlayers, OpenApproach6, TraversalWindowOptions6, ActualTraversalOptionT11, TraversalGraphFixtureT11, TraversalLayoutT11, TraversalOpeningT11, TraversalSiteT11, TraversalWindowT11

TraversalWindowT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalWindowT11(id,site) == NewPriorityWindow9(id,"Paid",site,EmptyT11,0,NoTimingRef9,[id |-> 0],0)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewPriorityWindow9, NoTimingRef9, EmptyT11

TraversalWorkT11 · operator

reference-profile · input revision 2 · CC0 1.0

TraversalWorkT11(jack,sub) == [jackChoice |-> jack,resolvedSub |-> sub]

Exact module download · Source bundle and reproduction instructions