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

SchedulerChecksMC¶

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

ActualOptionT11 · operator

reference-profile · input revision 2 · CC0 1.0

ActualOptionT11(w,kind,actor,target) ==
 LET option==OptionT11(kind,actor,target) IN BeginPriorityOption9(<<w>>,<<StartPriorityOptionFrame9(w,option,200)>>,option,TestObjectsT11,LegalityT11(w,option),[id |-> 0])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BeginPriorityOption9, StartPriorityOptionFrame9, LegalityT11, OptionT11, TestObjectsT11

ActualSideADestinationsT11 · operator

reference-profile · input revision 2 · CC0 1.0

ActualSideADestinationsT11(f,workComplete) ==
 {DestinationT11(after) : after \in {g \in SideACandidateFramesT11(f) : SideAStepAdvance5(f,g,workComplete)}}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DestinationT11, SideACandidateFramesT11, SideAStepAdvance5

ActualSideBDestinationsT11 · operator

reference-profile · input revision 2 · CC0 1.0

ActualSideBDestinationsT11(f,workComplete) ==
 {SideBDestinationT11(after) : after \in {g \in SideBCandidateFramesT11(f) : SideBStepAdvance5(f,g,workComplete)}}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBCandidateFramesT11, SideBDestinationT11, SideBStepAdvance5

ChildNameT11 · operator

reference-profile · input revision 2 · CC0 1.0

ChildNameT11(id) == CASE id=1 -> "Child1" [] id=2 -> "Child2" [] OTHER -> "Child3"

Exact module download · Source bundle and reproduction instructions

DestinationT11 · operator

reference-profile · input revision 2 · CC0 1.0

DestinationT11(f) == IF f.turn.owner="SideB" THEN <<"HandoffToSideB","DeferredSideBPhase">> ELSE <<f.step,f.turn.phase>>

Exact module download · Source bundle and reproduction instructions

EmptyT11 · operator

reference-profile · input revision 2 · CC0 1.0

EmptyT11 == [id \in {} |-> id]

Exact module download · Source bundle and reproduction instructions

ExpectedSideADestinationsT11 · operator

reference-profile · input revision 2 · CC0 1.0

ExpectedSideADestinationsT11(step,decision) ==
 {IF e.after="HandoffToSideB" THEN <<e.after,"DeferredSideBPhase">> ELSE <<e.after,SideAOraclePhases11[e.after]>> :
   e \in {e \in SideAOracleEdges11 : e.before=step /\ e.decision=decision}}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAOracleEdges11, SideAOraclePhases11

ExpectedSideBDestinationsT11 · operator

reference-profile · input revision 2 · CC0 1.0

ExpectedSideBDestinationsT11(step,decision) ==
 {IF e.after="HandoffToSideA" THEN <<e.after,"DeferredSideAPhase">> ELSE <<e.after,SideBOraclePhases11[e.after]>> :
   e \in {e \in SideBOracleEdges11 : e.before=step /\ e.decision=decision}}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBOracleEdges11, SideBOraclePhases11

IdleActionT11 · operator

reference-profile · input revision 2 · CC0 1.0

IdleActionT11 == [NewAction5(0,"SideA",BasicActionKey5("SideA","GainResourceUnit")) EXCEPT !.status="Idle"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasicActionKey5, NewAction5

LegalityT11 · operator

reference-profile · input revision 2 · CC0 1.0

LegalityT11(w,option) == [tag |-> "PriorityOptionLegality",windowId |-> w.id,reception |-> w.reception,option |-> option,legal |-> TRUE,active |-> TRUE,transactionId |-> 200,costsPayable |-> TRUE]

Exact module download · Source bundle and reproduction instructions

OpeningT11 · operator

reference-profile · input revision 2 · CC0 1.0

OpeningT11(f,id) ==
 [tag |-> "PriorityWindowOpening",windowId |-> id,kind |-> "Paid",site |-> SideASiteT11(f,1),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, SideASiteT11

OptionT11 · operator

reference-profile · input revision 2 · CC0 1.0

OptionT11(kind,actor,target) == PriorityOption9(20,kind,actor,0,0,RuleAbilitySource9("AuditOption"),target,{})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PriorityOption9, RuleAbilitySource9

PointwiseChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

PointwiseChecksT11 == CASE guideCaseT11=1 -> SideAEntryAndGraphChecksT11
                       [] guideCaseT11=2 -> SideAWindowChecksT11
                       [] guideCaseT11=3 -> SideAEffectAndBarrierChecksT11
                       [] guideCaseT11=4 -> SideBEntryAndGraphChecksT11
                       [] guideCaseT11=5 -> SideBWindowChecksT11
                       [] OTHER -> SideBEffectAndBarrierChecksT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAEffectAndBarrierChecksT11, SideAEntryAndGraphChecksT11, SideAWindowChecksT11, SideBEffectAndBarrierChecksT11, SideBEntryAndGraphChecksT11, SideBWindowChecksT11, guideCaseT11

PointwiseInitT11 · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyT11, guideCaseT11, qT11

PointwiseNextT11 · operator

reference-profile · input revision 2 · CC0 1.0

PointwiseNextT11 == UNCHANGED <<guideCaseT11,qT11>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: guideCaseT11, qT11

PointwiseSpecT11 · operator

reference-profile · input revision 2 · CC0 1.0

PointwiseSpecT11 == PointwiseInitT11 /\ [][PointwiseNextT11]_<<guideCaseT11,qT11>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PointwiseInitT11, PointwiseNextT11, guideCaseT11, qT11

PreparedSideAT11 · operator

reference-profile · input revision 2 · CC0 1.0

PreparedSideAT11(step,decision) ==
 [SideAInitialT11 EXCEPT !.step=step,!.turn.phase=SideAOraclePhases11[step],!.decision=decision,
   !.turn.formalBegun=SourcePositionT11(step)>=SourcePositionT11("ProcedureCode824821d07be7"),
   !.turn.begunCounts["SideA"]=IF SourcePositionT11(step)>=SourcePositionT11("ProcedureCode824821d07be7") THEN 1 ELSE 0,
   !.turn.formalEnded=step \in {"ProcedureCodea107cee5c079","ProcedureCode72a65676fb11"},!.phaseEndMet=SourcePositionT11(step)>=SourcePositionT11("ProcedureCode042aa78ff256")]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAInitialT11, SourcePositionT11, SideAOraclePhases11

PreparedSideBT11 · operator

reference-profile · input revision 2 · CC0 1.0

PreparedSideBT11(step,decision) ==
 [SideBInitialT11 EXCEPT !.step=step,!.turn.phase=SideBOraclePhases11[step],!.decision=decision,
   !.turn.formalBegun=SideBPositionT11(step)>=SideBPositionT11("ProcedureCodebb587f61a951"),
   !.turn.begunCounts["SideB"]=IF SideBPositionT11(step)>=SideBPositionT11("ProcedureCodebb587f61a951") THEN 1 ELSE 0,
   !.turn.formalEnded=step \in {"ProcedureCode8f113080e47f","ProcedureCode49c3ccade13b"},!.phaseEndMet=SideBPositionT11(step)>=SideBPositionT11("ProcedureCodeb6952d25a4da")]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBInitialT11, SideBPositionT11, SideBOraclePhases11

PriorityCheckpointT11 · operator

reference-profile · input revision 2 · CC0 1.0

PriorityCheckpointT11(w) ==
 [tag |-> "NormalPriorityCheckpoint",id |-> 10000+w.id*10+w.reception,windowId |-> w.id,reception |-> w.reception,player |-> w.priority,complete |-> TRUE,reactionsDrained |-> TRUE]

Exact module download · Source bundle and reproduction instructions

PriorityReadyT11 · operator

reference-profile · input revision 2 · CC0 1.0

PriorityReadyT11(w) == [w EXCEPT !.stage="Ready",!.checkpoint=PriorityCheckpointT11(w).id]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PriorityCheckpointT11

RecordWorkT11 · operator

reference-profile · input revision 2 · CC0 1.0

RecordWorkT11(before,after,events) ==
 [after EXCEPT !.ready=TRUE,!.history=Append(@,[step |-> before.flow.step,kind |-> SideAStepInfo5(before.flow.step).kind,
    visible |-> SideAOracleVisible11[before.flow.step],events |-> events,decision |-> after.flow.decision,decisionActionPoints |-> after.decisionActionPoints])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAOracleVisible11, SideAStepInfo5

SideAAuditActionBodyT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAAuditActionBodyT11 ==
 /\ ~SideAAuditDoneT11 /\ ~qT11.ready /\ qT11.flow.step="ProcedureCode0e20572a4bab" /\ qT11.flow.decision="NeutralValue00001"
 /\ LET a==qT11.action child==ChildNameT11(a.id) IN
    \/ /\ a.status="CostReactions" /\ ActionEffectsBegin5(a,[a EXCEPT !.status="Effects"],TRUE)
       /\ qT11'=[qT11 EXCEPT !.action.status="Effects"]
    \/ /\ a.status="Effects" /\ a.id \in qT11.nestedPlan /\ ~qT11.nestedUsed /\ ~qT11.tailDone
       /\ ActionNestedBegin5(a,[a EXCEPT !.status="Nested",!.nested=child],child)
       /\ qT11'=[qT11 EXCEPT !.action.status="Nested",!.action.nested=child,!.nestedUsed=TRUE]
    \/ /\ a.status="Nested" /\ ~qT11.childDone
       /\ qT11'=[qT11 EXCEPT !.childDone=TRUE]
    \/ /\ a.status="Nested" /\ qT11.childDone
       /\ ActionNestedReturn5(a,[a EXCEPT !.status="Effects",!.nested="NoValue"],child,qT11.childDone)
       /\ qT11'=[qT11 EXCEPT !.action.status="Effects",!.action.nested="NoValue"]
    \/ /\ a.status="Effects" /\ ~qT11.tailDone /\ (a.id \notin qT11.nestedPlan \/ qT11.nestedUsed)
       /\ LET added==[id \in {3000+a.id} |-> [form |-> "Counter",card |-> "none",virtual |-> FALSE,kind |-> "ResourceUnit",zone |-> "SideAResourceUnits",host |-> 0]]
              after==[id \in DOMAIN qT11.bank \cup DOMAIN added |-> IF id \in DOMAIN added THEN added[id] ELSE qT11.bank[id]]
          IN /\ BankMintProjection4(qT11.bank,after,added,1,"ResourceUnit",qT11.usedBank,[kind |-> "Zone",zone |-> "Bank"],BasicAction5("SideA","GainResourceUnit").effect="GainResourceUnit",TRUE)
             /\ qT11'=[qT11 EXCEPT !.bank=after,!.usedBank=@ \cup DOMAIN added,!.tailDone=TRUE]
    \/ /\ a.status="Effects" /\ qT11.tailDone
       /\ ActionComplete5(a,[a EXCEPT !.status="Complete"],qT11.tailDone)
       /\ qT11'=RecordWorkT11(qT11,[qT11 EXCEPT !.action.status="Complete"],{})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BankMintProjection4, ChildNameT11, RecordWorkT11, SideAAuditDoneT11, qT11, ActionComplete5, ActionEffectsBegin5, ActionNestedBegin5, ActionNestedReturn5, BasicAction5

SideAAuditActionStartT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAAuditActionStartT11 ==
 /\ ~SideAAuditDoneT11 /\ ~qT11.ready /\ qT11.flow.step="ProcedureCode0e20572a4bab" /\ qT11.flow.decision="NeutralValue00001"
 /\ qT11.action.status \in {"Idle","Complete"} /\ qT11.actionPoints["SideA"]>0
 /\ LET a==NewAction5(qT11.actions+1,"SideA",BasicActionKey5("SideA","GainResourceUnit")) IN
    /\ ActionStart5(qT11.flow.turn,"SideA",TRUE,<<[kind |-> "SpendActionPoints",amount |-> 1]>>,WindowSiteAllowed9("NeutralValue00001",SideASiteT11(qT11.flow,qT11.actionPoints["SideA"])),TRUE,TRUE,a.id,a.key,a)
    /\ qT11'=[qT11 EXCEPT !.actionPoints["SideA"]=@-1,!.action=a,!.actions=@+1,!.tailDone=FALSE,!.nestedUsed=FALSE,!.childDone=FALSE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowSiteAllowed9, SideAAuditDoneT11, SideASiteT11, qT11, ActionStart5, BasicActionKey5, NewAction5

SideAAuditAdvanceT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAAuditAdvanceT11 ==
 /\ ~SideAAuditDoneT11 /\ qT11.ready /\ qT11.stack= <<>>
 /\ \E g \in SideACandidateFramesT11(qT11.flow) :
    /\ SideAStepAdvance5(qT11.flow,g,IF qT11.flow.step="ProcedureCode0e20572a4bab" /\ qT11.flow.decision="NeutralValue00001" THEN ActionReadyToContinue5(qT11.action) ELSE qT11.ready)
    /\ qT11'=[qT11 EXCEPT !.flow=g,!.ready=FALSE,!.edges=Append(@,[before |-> qT11.flow.step,after |-> IF g.turn.owner="SideB" THEN "HandoffToSideB" ELSE g.step,phase |-> g.turn.phase,decision |-> qT11.flow.decision])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAAuditDoneT11, SideACandidateFramesT11, qT11, ActionReadyToContinue5, SideAStepAdvance5

SideAAuditDoneT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAAuditDoneT11 == qT11.flow.turn.owner="SideB"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

SideAAuditEventuallyHandoffT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAAuditEventuallyHandoffT11 == <>SideAAuditDoneT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAAuditDoneT11

SideAAuditInitT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAAuditInitT11 ==
 /\ guideCaseT11=4
 /\ \E nestedPlan \in SUBSET {1,2,3}, recurring \in {0,3} :
      qT11=[flow |-> SideAInitialT11,ready |-> FALSE,actionPoints |-> ZeroCountsT11,recurring |-> recurring,
        draw |-> [deck |-> <<1,2>>,hand |-> {11,12,13,14,15,16}],discard |-> {},faces |-> [id \in 1..20 |-> "Up"],
        windows |-> <<>>,stack |-> <<>>,nextWindow |-> 1,usedWindows |-> {},actionWindowReady |-> FALSE,
        action |-> IdleActionT11,actions |-> 0,nestedPlan |-> nestedPlan,nestedUsed |-> FALSE,childDone |-> FALSE,tailDone |-> FALSE,
        bank |-> EmptyT11,usedBank |-> {},decisionActionPoints |-> 0,history |-> <<>>,edges |-> <<>>]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyT11, IdleActionT11, SideAInitialT11, ZeroCountsT11, guideCaseT11, qT11

SideAAuditInvariantT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAAuditInvariantT11 ==
 /\ guideCaseT11=4 /\ qT11.actionPoints \in [SetupPlayers -> 0..3] /\ qT11.actions \in 0..3 /\ Cardinality(DOMAIN qT11.bank) \in 0..3
 /\ IF SideAAuditDoneT11 THEN TurnFrameValid5(qT11.flow.turn) ELSE SideAProcedureValid5(qT11.flow)
 /\ \A i \in 1..Len(qT11.edges) :
      LET row==qT11.edges[i] IN
      /\ \E e \in SideAOracleEdges11 : row.before=e.before /\ row.after=e.after /\ row.decision=e.decision
      /\ (row.after#"HandoffToSideB" => row.phase=SideAOraclePhases11[row.after])
 /\ \A i \in 1..Len(qT11.history) :
      LET row==qT11.history[i] IN
      /\ row.kind=SideAOracleKinds11[row.step]
      /\ SideAFormalConditionsT11(row.events)=IF row.step \in DOMAIN SideAOracleFormalConditions11 THEN SideAOracleFormalConditions11[row.step] ELSE {}
      /\ (row.step="ProcedureCode0e20572a4bab" => ((row.decision="NeutralValue00001")=(row.decisionActionPoints>0)))
 /\ (qT11.action.status \in {"CostReactions","Effects","Nested"} => qT11.flow.step="ProcedureCode0e20572a4bab" /\ qT11.flow.decision="NeutralValue00001" /\ ~qT11.ready)
 /\ (qT11.ready /\ qT11.flow.step="ProcedureCode0e20572a4bab" /\ qT11.flow.decision="NeutralValue00001" => qT11.action.status="Complete" /\ qT11.tailDone)
 /\ (SideAAuditDoneT11 =>
       /\ qT11.flow.turn.id=2 /\ qT11.flow.turn.begunCounts=[SideA |-> 1,SideB |-> 0] /\ ~qT11.flow.turn.formalBegun /\ ~qT11.flow.turn.formalEnded
       /\ qT11.actions=3 /\ Cardinality(DOMAIN qT11.bank)=3 /\ qT11.actionPoints=ZeroCountsT11 /\ Cardinality(qT11.draw.hand)=5 /\ qT11.draw.deck= <<2>>
       /\ Len(qT11.windows)=6 /\ Cardinality({i \in 1..Len(qT11.windows) : qT11.windows[i]="ProcedureCoded6fbcb09dd4f"})=4
       /\ Len(qT11.history)=24 /\ Cardinality({i \in 1..Len(qT11.history) : qT11.history[i].visible#"Hidden"})=22
       /\ \A id \in qT11.discard : qT11.faces[id]="Down")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAAuditDoneT11, SideAFormalConditionsT11, ZeroCountsT11, guideCaseT11, qT11, SideAOracleEdges11, SideAOracleFormalConditions11, SideAOracleKinds11, SideAOraclePhases11, SetupPlayers, SideAProcedureValid5, TurnFrameValid5

SideAAuditLatchT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAAuditLatchT11 ==
 /\ ~SideAAuditDoneT11 /\ ~qT11.ready /\ qT11.flow.step="ProcedureCode0e20572a4bab" /\ qT11.flow.decision="NoValue" /\ qT11.actionWindowReady
 /\ LET g==[qT11.flow EXCEPT !.decision=IF qT11.actionPoints["SideA"]>0 THEN "NeutralValue00001" ELSE "End"]
        next==[qT11 EXCEPT !.flow=g,!.decisionActionPoints=qT11.actionPoints["SideA"],!.actionWindowReady=FALSE] IN
    /\ SideALatchDecision5(qT11.flow,g,qT11.actionPoints["SideA"],TRUE)
    /\ qT11'=IF g.decision="End" THEN RecordWorkT11(qT11,next,{}) ELSE next

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RecordWorkT11, SideAAuditDoneT11, qT11, SideALatchDecision5

SideAAuditNextT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAAuditNextT11 == /\ UNCHANGED guideCaseT11
 /\ (SideAAuditWorkT11 \/ SideAAuditWindowOpenT11 \/ SideAAuditWindowStepT11 \/ SideAAuditLatchT11 \/ SideAAuditActionStartT11 \/ SideAAuditActionBodyT11 \/ SideAAuditAdvanceT11 \/ (SideAAuditDoneT11 /\ UNCHANGED qT11))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAAuditActionBodyT11, SideAAuditActionStartT11, SideAAuditAdvanceT11, SideAAuditDoneT11, SideAAuditLatchT11, SideAAuditWindowOpenT11, SideAAuditWindowStepT11, SideAAuditWorkT11, guideCaseT11, qT11

SideAAuditSpecT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAAuditSpecT11 == SideAAuditInitT11 /\ [][SideAAuditNextT11]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(SideAAuditNextT11)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAAuditInitT11, SideAAuditNextT11, guideCaseT11, qT11

SideAAuditWindowOpenT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAAuditWindowOpenT11 ==
 /\ ~SideAAuditDoneT11 /\ ~qT11.ready /\ qT11.stack= <<>> /\ SideAStepInfo5(qT11.flow.step).kind="PaidWindow"
 /\ LET f==qT11.flow id==qT11.nextWindow site==SideASiteT11(f,qT11.actionPoints["SideA"])
        opening==[OpeningT11(f,id) EXCEPT !.site=site]
        w==NewPriorityWindow9(id,"Paid",site,EmptyT11,0,NoTimingRef9,[id |-> 0],0)
    IN /\ OpenPriorityWindow9(<<>>,<<w>>,id,"Paid",site,EmptyT11,opening,qT11.usedWindows)
       /\ qT11'=[qT11 EXCEPT !.stack= <<w>>,!.nextWindow=@+1,!.usedWindows=@ \cup {id}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewPriorityWindow9, NoTimingRef9, OpenPriorityWindow9, EmptyT11, OpeningT11, SideAAuditDoneT11, SideASiteT11, qT11, SideAStepInfo5

SideAAuditWindowStepT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAAuditWindowStepT11 ==
 /\ ~SideAAuditDoneT11 /\ ~qT11.ready /\ Len(qT11.stack)=1
 /\ LET w==WindowTop9(qT11.stack) IN
    \/ /\ w.stage="NeedCheckpoint"
       /\ CheckpointPriority9(qT11.stack,<<PriorityReadyT11(w)>>,PriorityCheckpointT11(w))
       /\ qT11'=[qT11 EXCEPT !.stack= <<PriorityReadyT11(w)>>]
    \/ /\ w.stage="Ready"
       /\ PassPriority9(qT11.stack,<<PassPriorityFrame9(w)>>,w.priority,[id |-> 0])
       /\ qT11'=[qT11 EXCEPT !.stack= <<PassPriorityFrame9(w)>>]
    \/ /\ w.stage="Closed" /\ PopClosedPriorityWindow9(qT11.stack,<<>>)
       /\ qT11'=RecordWorkT11(qT11,[qT11 EXCEPT !.stack= <<>>,!.windows=Append(@,qT11.flow.step),!.actionWindowReady=qT11.flow.step="ProcedureCoded6fbcb09dd4f"],{})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointPriority9, PassPriority9, PassPriorityFrame9, PopClosedPriorityWindow9, WindowTop9, PriorityCheckpointT11, PriorityReadyT11, RecordWorkT11, SideAAuditDoneT11, qT11

SideAAuditWorkT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAAuditWorkT11 ==
 /\ ~SideAAuditDoneT11 /\ ~qT11.ready /\ qT11.stack= <<>>
 /\ LET f==qT11.flow kind==SideAStepInfo5(f.step).kind IN
    CASE kind="AllotActionPoints" ->
       LET c==[qT11.actionPoints EXCEPT !.SideA=@+SideADefaultAllotment5] IN
       /\ SideAAllotmentAtStep5(f,qT11.actionPoints,c,SideADefaultAllotment5)
       /\ qT11'=RecordWorkT11(qT11,[qT11 EXCEPT !.actionPoints=c],{})
    [] kind="Refill" ->
       /\ SideARefillAtStep5(f,qT11.recurring,MaxOf(qT11.recurring,2),2,TRUE)
       /\ qT11'=RecordWorkT11(qT11,[qT11 EXCEPT !.recurring=MaxOf(@,2)],{})
    [] kind="TurnBegins" ->
       LET g==[f EXCEPT !.turn.formalBegun=TRUE,!.turn.begunCounts["SideA"]=@+1] events=={TurnBeginEvent5(f.turn)} IN
       /\ SideAFormalBeginAtStep5(f,g,events) /\ qT11'=RecordWorkT11(qT11,[qT11 EXCEPT !.flow=g],events)
    [] kind="MandatoryDraw" ->
       LET d==[qT11.draw EXCEPT !.deck=Tail(@),!.hand=@ \cup {qT11.draw.deck[1]}] IN
       /\ SideAMandatoryDrawAtStep5(f,qT11.draw,d,TRUE,"NoValue",{MandatoryDrawEvent5})
       /\ qT11'=RecordWorkT11(qT11,[qT11 EXCEPT !.draw=d],{MandatoryDrawEvent5})
    [] kind="ActionPhaseEnds" ->
       LET g==[f EXCEPT !.phaseEndMet=TRUE] events=={ActionPhaseEndEvent5(f.turn)} IN
       /\ SideAActionPhaseEndAtStep5(f,g,events) /\ qT11'=RecordWorkT11(qT11,[qT11 EXCEPT !.flow=g],events)
    [] kind="DiscardStep" ->
       \E selected \in SUBSET qT11.draw.hand :
        LET before==[hand |-> qT11.draw.hand,discard |-> qT11.discard,faces |-> qT11.faces]
            after==[before EXCEPT !.hand=@ \ selected,!.discard=@ \cup selected,!.faces=[id \in DOMAIN @ |-> IF id \in selected THEN "Down" ELSE @[id]]]
            events==IF selected={} THEN {} ELSE {DiscardBatchEvent5("SideA",selected)}
        IN /\ SideADiscardAtStep5(f,before,after,FALSE,5,selected,TRUE,"NoValue",events)
           /\ qT11'=RecordWorkT11(qT11,[qT11 EXCEPT !.draw.hand=after.hand,!.discard=after.discard,!.faces=after.faces],events)
    [] kind="LoseUnspentActionPoints" ->
       LET c==[qT11.actionPoints EXCEPT !.SideA=IF @>0 THEN 0 ELSE @] IN
       /\ SideALoseActionPointsAtStep5(f,qT11.actionPoints,c) /\ qT11'=RecordWorkT11(qT11,[qT11 EXCEPT !.actionPoints=c],{})
    [] kind="TurnEnds" ->
       LET g==[f EXCEPT !.turn.formalEnded=TRUE] events==TurnEndEvents5(f.turn) IN
       /\ SideAFormalEndAtStep5(f,g,events) /\ qT11'=RecordWorkT11(qT11,[qT11 EXCEPT !.flow=g],events)
    [] kind \in {"PhaseComplete","Loop","Handoff"} -> qT11'=RecordWorkT11(qT11,qT11,{})
    [] OTHER -> FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MaxOf, RecordWorkT11, SideAAuditDoneT11, qT11, ActionPhaseEndEvent5, DiscardBatchEvent5, MandatoryDrawEvent5, SideAActionPhaseEndAtStep5, SideAAllotmentAtStep5, SideADefaultAllotment5, SideADiscardAtStep5, SideAFormalBeginAtStep5, SideAFormalEndAtStep5, SideALoseActionPointsAtStep5, SideAMandatoryDrawAtStep5, SideARefillAtStep5, SideAStepInfo5, TurnBeginEvent5, TurnEndEvents5

SideACandidateFramesT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideACandidateFramesT11(f) ==
 {[f EXCEPT !.step=step,!.turn.phase=phase,!.decision="NoValue"] : step \in SideAOracleStepSet11 \cup {"UnauthorizedStep"},phase \in {"Draw","NeutralValue00001","Discard"}} \cup
 {[f EXCEPT !.turn=OpenTurn5("SideB",f.turn.id+1,f.turn.begunCounts),!.step=OpenSideBProcedure5(OpenTurn5("SideB",f.turn.id+1,f.turn.begunCounts)).step,!.decision="NoValue",!.phaseEndMet=FALSE]}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAOracleStepSet11, OpenSideBProcedure5, OpenTurn5

SideAEffectAndBarrierChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAEffectAndBarrierChecksT11 ==
 LET actionPoints==[SideA |-> 1,SideB |-> 2] allotted==[actionPoints EXCEPT !.SideA=4]
     d0==[PreparedSideAT11("ProcedureCode824821d07be7","NoValue") EXCEPT !.turn.formalBegun=FALSE,!.turn.begunCounts["SideA"]=0]
     d1==[d0 EXCEPT !.turn.formalBegun=TRUE,!.turn.begunCounts["SideA"]=1]
     draw==[deck |-> <<1,2>>,hand |-> {3},actionPoints |-> 4] drawn==[draw EXCEPT !.deck= <<2>>,!.hand={1,3}]
     phase0==[PreparedSideAT11("ProcedureCode042aa78ff256","NoValue") EXCEPT !.phaseEndMet=FALSE] phase1==[phase0 EXCEPT !.phaseEndMet=TRUE]
     end0==[PreparedSideAT11("ProcedureCodea107cee5c079","NoValue") EXCEPT !.turn.formalEnded=FALSE] end1==[end0 EXCEPT !.turn.formalEnded=TRUE]
     hand==[hand |-> {1,2,3,4,5,6},discard |-> {},faces |-> [id \in 1..6 |-> "Up"]]
     discarded==[hand EXCEPT !.hand={1,2,3,4,5},!.discard={6},!.faces[6]="Down"]
     action==PreparedSideAT11("ProcedureCode0e20572a4bab","NoValue") latched==[action EXCEPT !.decision="NeutralValue00001"]
     effects==[NewAction5(1,"SideA",BasicActionKey5("SideA","GainResourceUnit")) EXCEPT !.status="Effects"] nested==[effects EXCEPT !.status="Nested",!.nested="AuditChild"]
 IN /\ SideAAllotmentAtStep5(SideAInitialT11,actionPoints,allotted,SideAOracleDefaultAllotment11)
    /\ \A step \in SideAOracleStepSet11 \ {"ProcedureCode3557d050aec7"} : ~SideAAllotmentAtStep5(PreparedSideAT11(step,"NoValue"),actionPoints,allotted,3)
    /\ \A before \in {0,1,2,3} : SideARefillAtStep5(PreparedSideAT11("ProcedureCode599a3c2d7264","NoValue"),before,MaxOf(before,2),2,TRUE)
    /\ ~SideARefillAtStep5(PreparedSideAT11("ProcedureCode599a3c2d7264","NoValue"),0,2,2,FALSE)
    /\ SideAFormalBeginAtStep5(d0,d1,{TurnBeginEvent5(d0.turn)}) /\ ~SideAFormalBeginAtStep5(d0,d1,{})
    /\ ActualSideADestinationsT11(d0,TRUE)={} /\ ActualSideADestinationsT11(d1,TRUE)={<<"ProcedureCode59141ee1a13b","Draw">>}
    /\ SideAMandatoryDrawAtStep5(PreparedSideAT11("ProcedureCode59141ee1a13b","NoValue"),draw,drawn,TRUE,"NoValue",{MandatoryDrawEvent5})
    /\ ~SideAMandatoryDrawAtStep5(PreparedSideAT11("ProcedureCode59141ee1a13b","NoValue"),draw,drawn,FALSE,"NoValue",{MandatoryDrawEvent5})
    /\ \A n \in {-1,0,1,3} : SideALatchDecision5(action,[action EXCEPT !.decision=IF n>0 THEN "NeutralValue00001" ELSE "End"],n,TRUE)
    /\ ~SideALatchDecision5(action,latched,1,FALSE) /\ ~SideALatchDecision5(latched,latched,1,TRUE)
    /\ SideAActionPhaseEndAtStep5(phase0,phase1,{ActionPhaseEndEvent5(phase0.turn)}) /\ ~SideAActionPhaseEndAtStep5(phase0,phase1,{})
    /\ ActualSideADestinationsT11(phase0,TRUE)={}
    /\ SideADiscardAtStep5(PreparedSideAT11("ProcedureCode93af477f9d95","NoValue"),hand,discarded,FALSE,5,{6},TRUE,"NoValue",{DiscardBatchEvent5("SideA",{6})})
    /\ ~SideADiscardAtStep5(PreparedSideAT11("ProcedureCode438597bede05","NoValue"),hand,discarded,FALSE,5,{6},TRUE,"NoValue",{DiscardBatchEvent5("SideA",{6})})
    /\ SideALoseActionPointsAtStep5(PreparedSideAT11("ProcedureCode4e363e6bb7cf","NoValue"),actionPoints,[actionPoints EXCEPT !.SideA=0])
    /\ SideAFormalEndAtStep5(end0,end1,TurnEndEvents5(end0.turn)) /\ ~SideAFormalEndAtStep5(end0,end1,{}) /\ ActualSideADestinationsT11(end0,TRUE)={}
    /\ ActualSideADestinationsT11([PreparedSideAT11("ProcedureCode72a65676fb11","NoValue") EXCEPT !.turn.formalEnded=FALSE],TRUE)={}
    /\ ~ActionNestedReturn5(nested,effects,"WrongChild",TRUE) /\ ~ActionNestedReturn5(nested,effects,"AuditChild",FALSE) /\ ActionNestedReturn5(nested,effects,"AuditChild",TRUE)
    /\ ~ActionEffectsBegin5(NewAction5(1,"SideA",effects.key),effects,FALSE)
    /\ ~ActionStart5(action.turn,"SideA",TRUE,<<[kind |-> "SpendActionPoints",amount |-> 1]>>,TRUE,FALSE,TRUE,1,effects.key,NewAction5(1,"SideA",effects.key))
    /\ ~ActionStart5(action.turn,"SideA",TRUE,<<[kind |-> "SpendActionPoints",amount |-> 1]>>,TRUE,TRUE,FALSE,1,effects.key,NewAction5(1,"SideA",effects.key))
    /\ ~ActionComplete5(effects,[effects EXCEPT !.status="Complete"],FALSE) /\ ~ActionComplete5(nested,[effects EXCEPT !.status="Complete"],TRUE)
    /\ ActualSideADestinationsT11(latched,ActionReadyToContinue5(nested))={} /\ ~ActionReadyToContinue5(effects)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MaxOf, ActualSideADestinationsT11, PreparedSideAT11, SideAInitialT11, SideAOracleDefaultAllotment11, SideAOracleStepSet11, ActionComplete5, ActionEffectsBegin5, ActionNestedReturn5, ActionPhaseEndEvent5, ActionReadyToContinue5, ActionStart5, BasicActionKey5, DiscardBatchEvent5, MandatoryDrawEvent5, NewAction5, SideAActionPhaseEndAtStep5, SideAAllotmentAtStep5, SideADiscardAtStep5, SideAFormalBeginAtStep5, SideAFormalEndAtStep5, SideALatchDecision5, SideALoseActionPointsAtStep5, SideAMandatoryDrawAtStep5, SideARefillAtStep5, TurnBeginEvent5, TurnEndEvents5

SideAEntryAndGraphChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAEntryAndGraphChecksT11 ==
 /\ SideAInitialT11.step=SideAOracleEntry11 /\ SideAInitialT11.turn.phase="Draw" /\ ~SideAInitialT11.turn.formalBegun /\ ~SideAInitialT11.turn.formalEnded
 /\ SideADefaultAllotment5=SideAOracleDefaultAllotment11
 /\ SetupRange(SideASteps5)=SideAOracleStepSet11
 /\ \A step \in SideAOracleStepSet11 :
      /\ SideAStepInfo5(step).kind=SideAOracleKinds11[step] /\ SideAStepInfo5(step).phase=SideAOraclePhases11[step]
      /\ \A decision \in IF step="ProcedureCode0e20572a4bab" THEN {"NeutralValue00001","End"} ELSE {"NoValue"} :
           ActualSideADestinationsT11(PreparedSideAT11(step,decision),TRUE)=ExpectedSideADestinationsT11(step,decision)
 /\ \A step \in SideAOracleStepSet11 : ActualSideADestinationsT11(PreparedSideAT11(step,"NoValue"),FALSE)={}
 /\ ActualSideADestinationsT11(PreparedSideAT11("ProcedureCode0e20572a4bab","NoValue"),TRUE)={}
 /\ \A index \in 1..Len(SideAOracleVisibleEdges11) :
      LET edge==SideAOracleVisibleEdges11[index] path== <<edge.before>> \o edge.via \o <<edge.after>> IN
      /\ \A i \in 1..(Len(path)-1) :
           LET d==IF i=1 THEN edge.decision ELSE "NoValue" target==path[i+1]
           IN (IF target="HandoffToSideB" THEN <<target,"DeferredSideBPhase">> ELSE <<target,SideAOraclePhases11[target]>>) \in ActualSideADestinationsT11(PreparedSideAT11(path[i],d),TRUE)
      /\ \A i \in 1..Len(edge.via) : edge.via[i] \in SideAOracleHidden11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualSideADestinationsT11, ExpectedSideADestinationsT11, PreparedSideAT11, SideAInitialT11, SideAOracleDefaultAllotment11, SideAOracleEntry11, SideAOracleHidden11, SideAOracleKinds11, SideAOraclePhases11, SideAOracleStepSet11, SideAOracleVisibleEdges11, SetupRange, SideADefaultAllotment5, SideAStepInfo5, SideASteps5

SideAFormalConditionsT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAFormalConditionsT11(events) ==
 {CASE e.tag="TurnBegins" -> "SideATurnBegins" [] e.tag="ActionPhaseEnds" -> "SideAActionPhaseEnds" [] e.tag="TurnEnds" -> "SideATurnEnds" [] OTHER -> "SideADiscardPhaseEnds" : e \in {e \in events : e.tag \in {"TurnBegins","ActionPhaseEnds","TurnEnds","DiscardPhaseEnds"} /\ e.actor="SideA"}}

Exact module download · Source bundle and reproduction instructions

SideAInitialT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAInitialT11 == OpenSideAProcedure5(OpenTurn5("SideA",1,ZeroCountsT11))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ZeroCountsT11, OpenSideAProcedure5, OpenTurn5

SideASiteT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideASiteT11(f,actionPoints) == TurnPrioritySite9(f.turn,f.step,100,actionPoints,f)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TurnPrioritySite9

SideAWindowChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideAWindowChecksT11 ==
 /\ \A step \in SideAOracleStepSet11 :
      LET f==PreparedSideAT11(step,"NoValue") info==SideAStepInfo5(step) expected==IF step \in DOMAIN SideAOracleWindowOptions11 THEN SideAOracleWindowOptions11[step] ELSE {} IN
      /\ info.options=expected
      /\ WindowSiteAllowed9("Paid",SideASiteT11(f,1))=(step \in DOMAIN SideAOracleWindowOptions11)
      /\ (step \in DOMAIN SideAOracleWindowOptions11 =>
           LET w==WindowT11(f,1) ready==PriorityReadyT11(w) passed==PassPriorityFrame9(ready) sideB==PriorityReadyT11(passed) IN
           /\ info.activationNonBarrierOnly /\ OpenPriorityWindow9(<<>>,<<w>>,1,"Paid",w.site,EmptyT11,OpeningT11(f,1),{})
           /\ CheckpointPriority9(<<w>>,<<ready>>,PriorityCheckpointT11(w))
           /\ ActualOptionT11(ready,"RegularPaid","SideA",0) /\ ActualOptionT11(sideB,"RegularPaid","SideB",0)
           /\ ActualOptionT11(ready,"Activation","SideA",1) /\ ActualOptionT11(ready,"Activation","SideA",2) /\ ~ActualOptionT11(ready,"Activation","SideA",3)
           /\ ~ActualOptionT11(sideB,"Activation","SideB",1) /\ ~ActualOptionT11(sideB,"ObjectiveCompletion","SideB",0)
           /\ ActualOptionT11(ready,"ObjectiveCompletion","SideA",0)=("ObjectiveCompletion" \in expected)
           /\ ~ActualOptionT11(ready,"RegularPaid","SideB",0)
           /\ ~CheckpointPriority9(<<w>>,<<ready>>,[PriorityCheckpointT11(w) EXCEPT !.reactionsDrained=FALSE])
           /\ ~CheckpointPriority9(<<w>>,<<ready>>,[PriorityCheckpointT11(w) EXCEPT !.windowId=99])
           /\ PassPriority9(<<ready>>,<<passed>>,"SideA",[id |-> 0]) /\ CheckpointPriority9(<<passed>>,<<sideB>>,PriorityCheckpointT11(passed))
           /\ PassPriority9(<<sideB>>,<<PassPriorityFrame9(sideB)>>,"SideB",[id |-> 0])
           /\ ~WindowSiteAllowed9("Paid",[w.site EXCEPT !.timingLive=FALSE]))
 /\ ~WindowSiteAllowed9("NeutralValue00001",SideASiteT11(PreparedSideAT11("ProcedureCode0e20572a4bab","NoValue"),0))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointPriority9, OpenPriorityWindow9, PassPriority9, PassPriorityFrame9, WindowSiteAllowed9, ActualOptionT11, EmptyT11, OpeningT11, PreparedSideAT11, PriorityCheckpointT11, PriorityReadyT11, SideASiteT11, WindowT11, SideAOracleStepSet11, SideAOracleWindowOptions11, SideAStepInfo5

SideBAuditActionBodyT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBAuditActionBodyT11 ==
 /\ ~SideBAuditDoneT11 /\ ~qT11.ready /\ qT11.flow.step="ProcedureCode989abc27e0c6" /\ qT11.flow.decision="NeutralValue00001"
 /\ LET a==qT11.action child==SideBChildNameT11(a.id) IN
    \/ /\ a.status="CostReactions" /\ ActionEffectsBegin5(a,[a EXCEPT !.status="Effects"],TRUE)
       /\ qT11'=[qT11 EXCEPT !.action.status="Effects"]
    \/ /\ a.status="Effects" /\ a.id \in qT11.nestedPlan /\ ~qT11.nestedUsed /\ ~qT11.tailDone
       /\ ActionNestedBegin5(a,[a EXCEPT !.status="Nested",!.nested=child],child)
       /\ qT11'=[qT11 EXCEPT !.action.status="Nested",!.action.nested=child,!.nestedUsed=TRUE]
    \/ /\ a.status="Nested" /\ ~qT11.childDone
       /\ qT11'=[qT11 EXCEPT !.childDone=TRUE]
    \/ /\ a.status="Nested" /\ qT11.childDone
       /\ ActionNestedReturn5(a,[a EXCEPT !.status="Effects",!.nested="NoValue"],child,qT11.childDone)
       /\ qT11'=[qT11 EXCEPT !.action.status="Effects",!.action.nested="NoValue"]
    \/ /\ a.status="Effects" /\ ~qT11.tailDone /\ (a.id \notin qT11.nestedPlan \/ qT11.nestedUsed)
       /\ LET added==[id \in {3000+a.id} |-> [form |-> "Counter",card |-> "none",virtual |-> FALSE,kind |-> "ResourceUnit",zone |-> "SideBResourceUnits",host |-> 0]]
              after==[id \in DOMAIN qT11.bank \cup DOMAIN added |-> IF id \in DOMAIN added THEN added[id] ELSE qT11.bank[id]]
          IN /\ BankMintProjection4(qT11.bank,after,added,1,"ResourceUnit",qT11.usedBank,[kind |-> "Zone",zone |-> "Bank"],BasicAction5("SideB","GainResourceUnit").effect="GainResourceUnit",TRUE)
             /\ qT11'=[qT11 EXCEPT !.bank=after,!.usedBank=@ \cup DOMAIN added,!.tailDone=TRUE]
    \/ /\ a.status="Effects" /\ qT11.tailDone
       /\ ActionComplete5(a,[a EXCEPT !.status="Complete"],qT11.tailDone)
       /\ qT11'=SideBRecordWorkT11(qT11,[qT11 EXCEPT !.action.status="Complete"],{})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BankMintProjection4, SideBAuditDoneT11, SideBChildNameT11, SideBRecordWorkT11, qT11, ActionComplete5, ActionEffectsBegin5, ActionNestedBegin5, ActionNestedReturn5, BasicAction5

SideBAuditActionStartT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBAuditActionStartT11 ==
 /\ ~SideBAuditDoneT11 /\ ~qT11.ready /\ qT11.flow.step="ProcedureCode989abc27e0c6" /\ qT11.flow.decision="NeutralValue00001"
 /\ qT11.action.status \in {"Idle","Complete"} /\ qT11.actionPoints["SideB"]>0
 /\ LET a==NewAction5(qT11.actions+1,"SideB",BasicActionKey5("SideB","GainResourceUnit")) IN
    /\ ActionStart5(qT11.flow.turn,"SideB",TRUE,<<[kind |-> "SpendActionPoints",amount |-> 1]>>,WindowSiteAllowed9("NeutralValue00001",SideBSiteT11(qT11.flow,qT11.actionPoints["SideB"])),TRUE,TRUE,a.id,a.key,a)
    /\ qT11'=[qT11 EXCEPT !.actionPoints["SideB"]=@-1,!.action=a,!.actions=@+1,!.tailDone=FALSE,!.nestedUsed=FALSE,!.childDone=FALSE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: WindowSiteAllowed9, SideBAuditDoneT11, SideBSiteT11, qT11, ActionStart5, BasicActionKey5, NewAction5

SideBAuditAdvanceT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBAuditAdvanceT11 ==
 /\ ~SideBAuditDoneT11 /\ qT11.ready /\ qT11.stack= <<>>
 /\ \E g \in SideBCandidateFramesT11(qT11.flow) :
    /\ SideBStepAdvance5(qT11.flow,g,IF qT11.flow.step="ProcedureCode989abc27e0c6" /\ qT11.flow.decision="NeutralValue00001" THEN ActionReadyToContinue5(qT11.action) ELSE qT11.ready)
    /\ qT11'=[qT11 EXCEPT !.flow=g,!.ready=FALSE,!.edges=Append(@,[before |-> qT11.flow.step,after |-> IF g.turn.owner="SideA" THEN "HandoffToSideA" ELSE g.step,phase |-> g.turn.phase,decision |-> qT11.flow.decision])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBAuditDoneT11, SideBCandidateFramesT11, qT11, ActionReadyToContinue5, SideBStepAdvance5

SideBAuditDoneT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBAuditDoneT11 == qT11.flow.turn.owner="SideA"

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

SideBAuditEventuallyHandoffT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBAuditEventuallyHandoffT11 == <>SideBAuditDoneT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBAuditDoneT11

SideBAuditInitT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBAuditInitT11 ==
 /\ guideCaseT11=7
 /\ \E nestedPlan \in SUBSET {1,2,3,4}, recurring \in {0,3} :
      qT11=[flow |-> SideBInitialT11,ready |-> FALSE,actionPoints |-> ZeroCountsT11,recurring |-> recurring,
        draw |-> [deck |-> <<1,2>>,hand |-> {11,12,13,14,15,16,17}],discard |-> {9},faces |-> [id \in 1..20 |-> IF id=9 THEN "Up" ELSE "Down"],
        windows |-> <<>>,stack |-> <<>>,nextWindow |-> 1,usedWindows |-> {},actionWindowReady |-> FALSE,
        action |-> SideBIdleActionT11,actions |-> 0,nestedPlan |-> nestedPlan,nestedUsed |-> FALSE,childDone |-> FALSE,tailDone |-> FALSE,
        bank |-> EmptyT11,usedBank |-> {},decisionActionPoints |-> 0,history |-> <<>>,edges |-> <<>>]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyT11, SideBIdleActionT11, SideBInitialT11, ZeroCountsT11, guideCaseT11, qT11

SideBAuditInvariantT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBAuditInvariantT11 ==
 /\ guideCaseT11=7 /\ qT11.actionPoints \in [SetupPlayers -> 0..4] /\ qT11.actions \in 0..4 /\ Cardinality(DOMAIN qT11.bank) \in 0..4
 /\ IF SideBAuditDoneT11 THEN TurnFrameValid5(qT11.flow.turn) ELSE SideBProcedureValid5(qT11.flow)
 /\ \A i \in 1..Len(qT11.edges) :
      LET row==qT11.edges[i] IN
      /\ \E e \in SideBOracleEdges11 : row.before=e.before /\ row.after=e.after /\ row.decision=e.decision
      /\ (row.after#"HandoffToSideA" => row.phase=SideBOraclePhases11[row.after])
 /\ \A i \in 1..Len(qT11.history) :
      LET row==qT11.history[i] IN
      /\ row.kind=SideBOracleKinds11[row.step]
      /\ SideBFormalConditionsT11(row.events)=IF row.step \in DOMAIN SideBOracleFormalConditions11 THEN SideBOracleFormalConditions11[row.step] ELSE {}
      /\ (row.step="ProcedureCode989abc27e0c6" => ((row.decision="NeutralValue00001")=(row.decisionActionPoints>0)))
 /\ (qT11.action.status \in {"CostReactions","Effects","Nested"} => qT11.flow.step="ProcedureCode989abc27e0c6" /\ qT11.flow.decision="NeutralValue00001" /\ ~qT11.ready)
 /\ (qT11.ready /\ qT11.flow.step="ProcedureCode989abc27e0c6" /\ qT11.flow.decision="NeutralValue00001" => qT11.action.status="Complete" /\ qT11.tailDone)
 /\ (SideBAuditDoneT11 =>
       /\ qT11.flow.turn.id=3 /\ qT11.flow.turn.begunCounts=[SideA |-> 1,SideB |-> 1] /\ ~qT11.flow.turn.formalBegun /\ ~qT11.flow.turn.formalEnded
       /\ qT11.actions=4 /\ Cardinality(DOMAIN qT11.bank)=4 /\ qT11.actionPoints=ZeroCountsT11 /\ Cardinality(qT11.draw.hand)=5 /\ qT11.draw.deck= <<1,2>>
       /\ Len(qT11.windows)=7 /\ Cardinality({i \in 1..Len(qT11.windows) : qT11.windows[i]="ProcedureCode484be3e50aa9"})=5
       /\ Len(qT11.history)=25 /\ Cardinality({i \in 1..Len(qT11.history) : qT11.history[i].visible#"Hidden"})=24
       /\ \A id \in qT11.discard : qT11.faces[id]="Up")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBAuditDoneT11, SideBFormalConditionsT11, ZeroCountsT11, guideCaseT11, qT11, SideBOracleEdges11, SideBOracleFormalConditions11, SideBOracleKinds11, SideBOraclePhases11, SetupPlayers, SideBProcedureValid5, TurnFrameValid5

SideBAuditLatchT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBAuditLatchT11 ==
 /\ ~SideBAuditDoneT11 /\ ~qT11.ready /\ qT11.flow.step="ProcedureCode989abc27e0c6" /\ qT11.flow.decision="NoValue" /\ qT11.actionWindowReady
 /\ LET g==[qT11.flow EXCEPT !.decision=IF qT11.actionPoints["SideB"]>0 THEN "NeutralValue00001" ELSE "End"]
        next==[qT11 EXCEPT !.flow=g,!.decisionActionPoints=qT11.actionPoints["SideB"],!.actionWindowReady=FALSE] IN
    /\ SideBLatchDecision5(qT11.flow,g,qT11.actionPoints["SideB"],TRUE)
    /\ qT11'=IF g.decision="End" THEN SideBRecordWorkT11(qT11,next,{}) ELSE next

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBAuditDoneT11, SideBRecordWorkT11, qT11, SideBLatchDecision5

SideBAuditNextT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBAuditNextT11 == /\ UNCHANGED guideCaseT11
 /\ (SideBAuditWorkT11 \/ SideBAuditWindowOpenT11 \/ SideBAuditWindowStepT11 \/ SideBAuditLatchT11 \/ SideBAuditActionStartT11 \/ SideBAuditActionBodyT11 \/ SideBAuditAdvanceT11 \/ (SideBAuditDoneT11 /\ UNCHANGED qT11))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBAuditActionBodyT11, SideBAuditActionStartT11, SideBAuditAdvanceT11, SideBAuditDoneT11, SideBAuditLatchT11, SideBAuditWindowOpenT11, SideBAuditWindowStepT11, SideBAuditWorkT11, guideCaseT11, qT11

SideBAuditSpecT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBAuditSpecT11 == SideBAuditInitT11 /\ [][SideBAuditNextT11]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(SideBAuditNextT11)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBAuditInitT11, SideBAuditNextT11, guideCaseT11, qT11

SideBAuditWindowOpenT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBAuditWindowOpenT11 ==
 /\ ~SideBAuditDoneT11 /\ ~qT11.ready /\ qT11.stack= <<>> /\ SideBStepInfo5(qT11.flow.step).kind="PaidWindow"
 /\ LET f==qT11.flow id==qT11.nextWindow site==SideBSiteT11(f,qT11.actionPoints["SideB"])
        opening==[SideBOpeningT11(f,id) EXCEPT !.site=site]
        w==NewPriorityWindow9(id,"Paid",site,EmptyT11,0,NoTimingRef9,[id |-> 0],0)
    IN /\ OpenPriorityWindow9(<<>>,<<w>>,id,"Paid",site,EmptyT11,opening,qT11.usedWindows)
       /\ qT11'=[qT11 EXCEPT !.stack= <<w>>,!.nextWindow=@+1,!.usedWindows=@ \cup {id}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewPriorityWindow9, NoTimingRef9, OpenPriorityWindow9, EmptyT11, SideBAuditDoneT11, SideBOpeningT11, SideBSiteT11, qT11, SideBStepInfo5

SideBAuditWindowStepT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBAuditWindowStepT11 ==
 /\ ~SideBAuditDoneT11 /\ ~qT11.ready /\ Len(qT11.stack)=1
 /\ LET w==WindowTop9(qT11.stack) IN
    \/ /\ w.stage="NeedCheckpoint"
       /\ CheckpointPriority9(qT11.stack,<<PriorityReadyT11(w)>>,PriorityCheckpointT11(w))
       /\ qT11'=[qT11 EXCEPT !.stack= <<PriorityReadyT11(w)>>]
    \/ /\ w.stage="Ready"
       /\ PassPriority9(qT11.stack,<<PassPriorityFrame9(w)>>,w.priority,[id |-> 0])
       /\ qT11'=[qT11 EXCEPT !.stack= <<PassPriorityFrame9(w)>>]
    \/ /\ w.stage="Closed" /\ PopClosedPriorityWindow9(qT11.stack,<<>>)
       /\ qT11'=SideBRecordWorkT11(qT11,[qT11 EXCEPT !.stack= <<>>,!.windows=Append(@,qT11.flow.step),!.actionWindowReady=qT11.flow.step="ProcedureCode484be3e50aa9"],{})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointPriority9, PassPriority9, PassPriorityFrame9, PopClosedPriorityWindow9, WindowTop9, PriorityCheckpointT11, PriorityReadyT11, SideBAuditDoneT11, SideBRecordWorkT11, qT11

SideBAuditWorkT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBAuditWorkT11 ==
 /\ ~SideBAuditDoneT11 /\ ~qT11.ready /\ qT11.stack= <<>>
 /\ LET f==qT11.flow kind==SideBStepInfo5(f.step).kind IN
    CASE kind="AllotActionPoints" ->
       LET c==[qT11.actionPoints EXCEPT !.SideB=@+SideBDefaultAllotment5] IN
       /\ SideBAllotmentAtStep5(f,qT11.actionPoints,c,SideBDefaultAllotment5)
       /\ qT11'=SideBRecordWorkT11(qT11,[qT11 EXCEPT !.actionPoints=c],{})
    [] kind="Refill" ->
       /\ SideBRefillAtStep5(f,qT11.recurring,MaxOf(qT11.recurring,2),2,TRUE)
       /\ qT11'=SideBRecordWorkT11(qT11,[qT11 EXCEPT !.recurring=MaxOf(@,2)],{})
    [] kind="TurnBegins" ->
       LET g==[f EXCEPT !.turn.formalBegun=TRUE,!.turn.begunCounts["SideB"]=@+1] events=={TurnBeginEvent5(f.turn)} IN
       /\ SideBFormalBeginAtStep5(f,g,events) /\ qT11'=SideBRecordWorkT11(qT11,[qT11 EXCEPT !.flow=g],events)
    [] kind="ActionPhaseEnds" ->
       LET g==[f EXCEPT !.phaseEndMet=TRUE] events=={ActionPhaseEndEvent5(f.turn)} IN
       /\ SideBActionPhaseEndAtStep5(f,g,events) /\ qT11'=SideBRecordWorkT11(qT11,[qT11 EXCEPT !.flow=g],events)
    [] kind="DiscardStep" ->
       \E selected \in SUBSET qT11.draw.hand :
        LET before==[hand |-> qT11.draw.hand,discard |-> qT11.discard,faces |-> qT11.faces]
            after==[before EXCEPT !.hand=@ \ selected,!.discard=@ \cup selected,!.faces=[id \in DOMAIN @ |-> IF id \in selected THEN "Up" ELSE @[id]]]
            events==IF selected={} THEN {} ELSE {DiscardBatchEvent5("SideB",selected)}
        IN /\ SideBDiscardAtStep5(f,before,after,FALSE,5,selected,TRUE,"NoValue",events)
           /\ qT11'=SideBRecordWorkT11(qT11,[qT11 EXCEPT !.draw.hand=after.hand,!.discard=after.discard,!.faces=after.faces],events)
    [] kind="LoseUnspentActionPoints" ->
       LET c==[qT11.actionPoints EXCEPT !.SideB=IF @>0 THEN 0 ELSE @] IN
       /\ SideBLoseActionPointsAtStep5(f,qT11.actionPoints,c) /\ qT11'=SideBRecordWorkT11(qT11,[qT11 EXCEPT !.actionPoints=c],{})
    [] kind="TurnEnds" ->
       LET g==[f EXCEPT !.turn.formalEnded=TRUE] events==TurnEndEvents5(f.turn) IN
       /\ SideBFormalEndAtStep5(f,g,events) /\ qT11'=SideBRecordWorkT11(qT11,[qT11 EXCEPT !.flow=g],events)
    [] kind \in {"PhaseComplete","Loop","Handoff"} -> qT11'=SideBRecordWorkT11(qT11,qT11,{})
    [] OTHER -> FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MaxOf, SideBAuditDoneT11, SideBRecordWorkT11, qT11, ActionPhaseEndEvent5, DiscardBatchEvent5, SideBActionPhaseEndAtStep5, SideBAllotmentAtStep5, SideBDefaultAllotment5, SideBDiscardAtStep5, SideBFormalBeginAtStep5, SideBFormalEndAtStep5, SideBLoseActionPointsAtStep5, SideBRefillAtStep5, SideBStepInfo5, TurnBeginEvent5, TurnEndEvents5

SideBCandidateFramesT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBCandidateFramesT11(f) ==
 {[f EXCEPT !.step=step,!.turn.phase=phase,!.decision="NoValue"] : step \in SideBOracleStepSet11 \cup {"UnauthorizedStep"},phase \in {"Draw","NeutralValue00001","Discard"}} \cup
 {[f EXCEPT !.turn=OpenTurn5("SideA",f.turn.id+1,f.turn.begunCounts),!.step=OpenSideAProcedure5(OpenTurn5("SideA",f.turn.id+1,f.turn.begunCounts)).step,!.decision="NoValue",!.phaseEndMet=FALSE]}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBOracleStepSet11, OpenSideAProcedure5, OpenTurn5

SideBChildNameT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBChildNameT11(id) == CASE id=1 -> "Child1" [] id=2 -> "Child2" [] id=3 -> "Child3" [] OTHER -> "Child4"

Exact module download · Source bundle and reproduction instructions

SideBDestinationT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBDestinationT11(f) == IF f.turn.owner="SideA" THEN <<"HandoffToSideA","DeferredSideAPhase">> ELSE <<f.step,f.turn.phase>>

Exact module download · Source bundle and reproduction instructions

SideBEffectAndBarrierChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBEffectAndBarrierChecksT11 ==
 LET actionPoints==[SideA |-> 2,SideB |-> 1] allotted==[actionPoints EXCEPT !.SideB=5]
     d0==[PreparedSideBT11("ProcedureCodebb587f61a951","NoValue") EXCEPT !.turn.formalBegun=FALSE,!.turn.begunCounts["SideB"]=0] d1==[d0 EXCEPT !.turn.formalBegun=TRUE,!.turn.begunCounts["SideB"]=1]
     phase0==[PreparedSideBT11("ProcedureCodeb6952d25a4da","NoValue") EXCEPT !.phaseEndMet=FALSE] phase1==[phase0 EXCEPT !.phaseEndMet=TRUE]
     end0==[PreparedSideBT11("ProcedureCode8f113080e47f","NoValue") EXCEPT !.turn.formalEnded=FALSE] end1==[end0 EXCEPT !.turn.formalEnded=TRUE]
     hand==[hand |-> {1,2,3,4,5,6},discard |-> {9},faces |-> [id \in 1..9 |-> IF id=9 THEN "Up" ELSE "Down"]]
     discarded==[hand EXCEPT !.hand={1,2,3,4,5},!.discard={6,9},!.faces[6]="Up"]
     action==PreparedSideBT11("ProcedureCode989abc27e0c6","NoValue") latched==[action EXCEPT !.decision="NeutralValue00001"]
     effects==[NewAction5(1,"SideB",BasicActionKey5("SideB","GainResourceUnit")) EXCEPT !.status="Effects"] nested==[effects EXCEPT !.status="Nested",!.nested="SideBChild"]
 IN /\ SideBAllotmentAtStep5(SideBInitialT11,actionPoints,allotted,SideBOracleDefaultAllotment11) /\ allotted["SideA"]=actionPoints["SideA"]
    /\ \A step \in SideBOracleStepSet11 \ {"ProcedureCode81ed7b3ac00d"} : ~SideBAllotmentAtStep5(PreparedSideBT11(step,"NoValue"),actionPoints,allotted,4)
    /\ \A before \in {0,1,2,3} : SideBRefillAtStep5(PreparedSideBT11("ProcedureCoded05d55b14bf9","NoValue"),before,MaxOf(before,2),2,TRUE)
    /\ ~SideBRefillAtStep5(PreparedSideBT11("ProcedureCoded05d55b14bf9","NoValue"),0,2,2,FALSE)
    /\ SideBFormalBeginAtStep5(d0,d1,{TurnBeginEvent5(d0.turn)}) /\ d1.turn.begunCounts["SideA"]=1 /\ ~SideBFormalBeginAtStep5(d0,d1,{})
    /\ ActualSideBDestinationsT11(d0,TRUE)={} /\ ActualSideBDestinationsT11(d1,TRUE)={<<"ProcedureCode484be3e50aa9","NeutralValue00001">>}
    /\ \A step \in SideBOracleStepSet11 : ~MandatoryDrawContext5(PreparedSideBT11(step,"NoValue").turn,TRUE)
    /\ \A n \in {-1,0,1,4} : SideBLatchDecision5(action,[action EXCEPT !.decision=IF n>0 THEN "NeutralValue00001" ELSE "End"],n,TRUE)
    /\ ~SideBLatchDecision5(action,latched,1,FALSE) /\ ~SideBLatchDecision5(latched,latched,1,TRUE)
    /\ SideBActionPhaseEndAtStep5(phase0,phase1,{ActionPhaseEndEvent5(phase0.turn)}) /\ ~SideBActionPhaseEndAtStep5(phase0,phase1,{}) /\ ActualSideBDestinationsT11(phase0,TRUE)={}
    /\ SideBDiscardAtStep5(PreparedSideBT11("ProcedureCode593c4a6fb4f5","NoValue"),hand,discarded,FALSE,5,{6},TRUE,"NoValue",{DiscardBatchEvent5("SideB",{6})})
    /\ ~SideBDiscardAtStep5(PreparedSideBT11("ProcedureCode13c5f7239eb2","NoValue"),hand,discarded,FALSE,5,{6},TRUE,"NoValue",{DiscardBatchEvent5("SideB",{6})})
    /\ SideBLoseActionPointsAtStep5(PreparedSideBT11("ProcedureCodede325c329e93","NoValue"),actionPoints,[actionPoints EXCEPT !.SideB=0])
    /\ SideBFormalEndAtStep5(end0,end1,TurnEndEvents5(end0.turn)) /\ ~SideBFormalEndAtStep5(end0,end1,{}) /\ ActualSideBDestinationsT11(end0,TRUE)={}
    /\ ActualSideBDestinationsT11([PreparedSideBT11("ProcedureCode49c3ccade13b","NoValue") EXCEPT !.turn.formalEnded=FALSE],TRUE)={}
    /\ ~ActionNestedReturn5(nested,effects,"WrongChild",TRUE) /\ ~ActionNestedReturn5(nested,effects,"SideBChild",FALSE) /\ ActionNestedReturn5(nested,effects,"SideBChild",TRUE)
    /\ ~ActionEffectsBegin5(NewAction5(1,"SideB",effects.key),effects,FALSE)
    /\ ~ActionStart5(action.turn,"SideB",TRUE,<<[kind |-> "SpendActionPoints",amount |-> 1]>>,TRUE,FALSE,TRUE,1,effects.key,NewAction5(1,"SideB",effects.key))
    /\ ~ActionComplete5(effects,[effects EXCEPT !.status="Complete"],FALSE) /\ ~ActionComplete5(nested,[effects EXCEPT !.status="Complete"],TRUE)
    /\ ActualSideBDestinationsT11(latched,ActionReadyToContinue5(nested))={}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MaxOf, ActualSideBDestinationsT11, PreparedSideBT11, SideBInitialT11, SideBOracleDefaultAllotment11, SideBOracleStepSet11, ActionComplete5, ActionEffectsBegin5, ActionNestedReturn5, ActionPhaseEndEvent5, ActionReadyToContinue5, ActionStart5, BasicActionKey5, DiscardBatchEvent5, MandatoryDrawContext5, NewAction5, SideBActionPhaseEndAtStep5, SideBAllotmentAtStep5, SideBDiscardAtStep5, SideBFormalBeginAtStep5, SideBFormalEndAtStep5, SideBLatchDecision5, SideBLoseActionPointsAtStep5, SideBRefillAtStep5, TurnBeginEvent5, TurnEndEvents5

SideBEntryAndGraphChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBEntryAndGraphChecksT11 ==
 /\ SideBInitialT11.step=SideBOracleEntry11 /\ SideBInitialT11.turn.phase="NeutralValue00001" /\ ~SideBInitialT11.turn.formalBegun /\ ~SideBInitialT11.turn.formalEnded
 /\ SideBDefaultAllotment5=SideBOracleDefaultAllotment11 /\ ~HasDrawPhase5("SideB") /\ ~TurnFrameValid5([SideBInitialT11.turn EXCEPT !.phase="Draw"])
 /\ SetupRange(SideBSteps5)=SideBOracleStepSet11
 /\ \A step \in SideBOracleStepSet11 :
      /\ SideBStepInfo5(step).kind=SideBOracleKinds11[step] /\ SideBStepInfo5(step).phase=SideBOraclePhases11[step] /\ SideBStepInfo5(step).kind#"MandatoryDraw"
      /\ \A decision \in IF step="ProcedureCode989abc27e0c6" THEN {"NeutralValue00001","End"} ELSE {"NoValue"} :
           ActualSideBDestinationsT11(PreparedSideBT11(step,decision),TRUE)=ExpectedSideBDestinationsT11(step,decision)
 /\ \A step \in SideBOracleStepSet11 : ActualSideBDestinationsT11(PreparedSideBT11(step,"NoValue"),FALSE)={}
 /\ ActualSideBDestinationsT11(PreparedSideBT11("ProcedureCode989abc27e0c6","NoValue"),TRUE)={}
 /\ \A index \in 1..Len(SideBOracleVisibleEdges11) :
      LET edge==SideBOracleVisibleEdges11[index] path== <<edge.before>> \o edge.via \o <<edge.after>> IN
      /\ \A i \in 1..(Len(path)-1) :
           LET d==IF i=1 THEN edge.decision ELSE "NoValue" target==path[i+1]
           IN (IF target="HandoffToSideA" THEN <<target,"DeferredSideAPhase">> ELSE <<target,SideBOraclePhases11[target]>>) \in ActualSideBDestinationsT11(PreparedSideBT11(path[i],d),TRUE)
      /\ \A i \in 1..Len(edge.via) : edge.via[i] \in SideBOracleHidden11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualSideBDestinationsT11, ExpectedSideBDestinationsT11, PreparedSideBT11, SideBInitialT11, SideBOracleDefaultAllotment11, SideBOracleEntry11, SideBOracleHidden11, SideBOracleKinds11, SideBOraclePhases11, SideBOracleStepSet11, SideBOracleVisibleEdges11, SetupRange, HasDrawPhase5, SideBDefaultAllotment5, SideBStepInfo5, SideBSteps5, TurnFrameValid5

SideBFormalConditionsT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBFormalConditionsT11(events) ==
 {CASE e.tag="TurnBegins" -> "SideBTurnBegins" [] e.tag="ActionPhaseEnds" -> "SideBActionPhaseEnds" [] e.tag="TurnEnds" -> "SideBTurnEnds" [] OTHER -> "SideBDiscardPhaseEnds" : e \in {e \in events : e.tag \in {"TurnBegins","ActionPhaseEnds","TurnEnds","DiscardPhaseEnds"} /\ e.actor="SideB"}}

Exact module download · Source bundle and reproduction instructions

SideBIdleActionT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBIdleActionT11 == [NewAction5(0,"SideB",BasicActionKey5("SideB","GainResourceUnit")) EXCEPT !.status="Idle"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasicActionKey5, NewAction5

SideBInitialT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBInitialT11 == OpenSideBProcedure5(OpenTurn5("SideB",2,[SideA |-> 1,SideB |-> 0]))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenSideBProcedure5, OpenTurn5

SideBOpeningT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBOpeningT11(f,id) ==
 [tag |-> "PriorityWindowOpening",windowId |-> id,kind |-> "Paid",site |-> SideBSiteT11(f,1),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, SideBSiteT11

SideBPositionT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBPositionT11(step) == CHOOSE i \in 1..Len(SideBOracleSteps11) : SideBOracleSteps11[i]=step

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBOracleSteps11

SideBRecordWorkT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBRecordWorkT11(before,after,events) ==
 [after EXCEPT !.ready=TRUE,!.history=Append(@,[step |-> before.flow.step,kind |-> SideBStepInfo5(before.flow.step).kind,
    visible |-> SideBOracleVisible11[before.flow.step],events |-> events,decision |-> after.flow.decision,decisionActionPoints |-> after.decisionActionPoints])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideBOracleVisible11, SideBStepInfo5

SideBSiteT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBSiteT11(f,actionPoints) == TurnPrioritySite9(f.turn,f.step,200,actionPoints,f)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TurnPrioritySite9

SideBWindowChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBWindowChecksT11 ==
 /\ \A step \in SideBOracleStepSet11 :
      LET f==PreparedSideBT11(step,"NoValue") info==SideBStepInfo5(step) expected==IF step \in DOMAIN SideBOracleWindowOptions11 THEN SideBOracleWindowOptions11[step] ELSE {} IN
      /\ info.options=expected /\ "ObjectiveCompletion" \notin info.options
      /\ WindowSiteAllowed9("Paid",SideBSiteT11(f,1))=(step \in DOMAIN SideBOracleWindowOptions11)
      /\ (step \in DOMAIN SideBOracleWindowOptions11 =>
           LET w==SideBWindowT11(f,1) sideB==PriorityReadyT11(w) passed==PassPriorityFrame9(sideB) sideA==PriorityReadyT11(passed) IN
           /\ info.activationNonBarrierOnly /\ w.active="SideB" /\ w.priority="SideB"
           /\ OpenPriorityWindow9(<<>>,<<w>>,1,"Paid",w.site,EmptyT11,SideBOpeningT11(f,1),{}) /\ CheckpointPriority9(<<w>>,<<sideB>>,PriorityCheckpointT11(w))
           /\ ActualOptionT11(sideB,"RegularPaid","SideB",0) /\ ActualOptionT11(sideA,"RegularPaid","SideA",0)
           /\ ActualOptionT11(sideA,"Activation","SideA",1) /\ ActualOptionT11(sideA,"Activation","SideA",2) /\ ~ActualOptionT11(sideA,"Activation","SideA",3)
           /\ ~ActualOptionT11(sideB,"Activation","SideB",1) /\ ~ActualOptionT11(sideB,"ObjectiveCompletion","SideB",0) /\ ~ActualOptionT11(sideA,"ObjectiveCompletion","SideA",0)
           /\ ~ActualOptionT11(sideB,"RegularPaid","SideA",0)
           /\ ~CheckpointPriority9(<<w>>,<<sideB>>,[PriorityCheckpointT11(w) EXCEPT !.player="SideA"])
           /\ ~CheckpointPriority9(<<w>>,<<sideB>>,[PriorityCheckpointT11(w) EXCEPT !.reception=99])
           /\ ~CheckpointPriority9(<<w>>,<<sideB>>,[PriorityCheckpointT11(w) EXCEPT !.windowId=99])
           /\ ~CheckpointPriority9(<<w>>,<<sideB>>,[PriorityCheckpointT11(w) EXCEPT !.complete=FALSE])
           /\ ~CheckpointPriority9(<<w>>,<<sideB>>,[PriorityCheckpointT11(w) EXCEPT !.reactionsDrained=FALSE])
           /\ PassPriority9(<<sideB>>,<<passed>>,"SideB",[id |-> 0]) /\ CheckpointPriority9(<<passed>>,<<sideA>>,PriorityCheckpointT11(passed))
           /\ PassPriority9(<<sideA>>,<<PassPriorityFrame9(sideA)>>,"SideA",[id |-> 0]) /\ ~WindowSiteAllowed9("Paid",[w.site EXCEPT !.timingLive=FALSE]))
 /\ ~WindowSiteAllowed9("NeutralValue00001",SideBSiteT11(PreparedSideBT11("ProcedureCode989abc27e0c6","NoValue"),0))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointPriority9, OpenPriorityWindow9, PassPriority9, PassPriorityFrame9, WindowSiteAllowed9, ActualOptionT11, EmptyT11, PreparedSideBT11, PriorityCheckpointT11, PriorityReadyT11, SideBOpeningT11, SideBSiteT11, SideBWindowT11, SideBOracleStepSet11, SideBOracleWindowOptions11, SideBStepInfo5

SideBWindowT11 · operator

reference-profile · input revision 2 · CC0 1.0

SideBWindowT11(f,id) == NewPriorityWindow9(id,"Paid",SideBSiteT11(f,1),EmptyT11,0,NoTimingRef9,[id |-> 0],0)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewPriorityWindow9, NoTimingRef9, EmptyT11, SideBSiteT11

SourcePositionT11 · operator

reference-profile · input revision 2 · CC0 1.0

SourcePositionT11(step) == CHOOSE i \in 1..Len(SideAOracleSteps11) : SideAOracleSteps11[i]=step

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAOracleSteps11

TestObjectsT11 · operator

reference-profile · input revision 2 · CC0 1.0

TestObjectsT11 == [id \in {1,2,3} |-> [form |-> "Card",side |-> "SideA",kind |-> CASE id=1 -> "Facility" [] id=2 -> "Attachment" [] OTHER -> "Barrier",zone |-> "Play",deployed |-> TRUE,face |-> "Down",activated |-> FALSE]]

Exact module download · Source bundle and reproduction instructions

WindowT11 · operator

reference-profile · input revision 2 · CC0 1.0

WindowT11(f,id) == NewPriorityWindow9(id,"Paid",SideASiteT11(f,1),EmptyT11,0,NoTimingRef9,[id |-> 0],0)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewPriorityWindow9, NoTimingRef9, EmptyT11, SideASiteT11

ZeroCountsT11 · operator

reference-profile · input revision 2 · CC0 1.0

ZeroCountsT11 == [p \in SetupPlayers |-> 0]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers

guideCaseT11 · variable

reference-profile · input revision 2 · CC0 1.0

guideCaseT11

Exact module download · Source bundle and reproduction instructions

qT11 · variable

reference-profile · input revision 2 · CC0 1.0

qT11

Exact module download · Source bundle and reproduction instructions