----------------------------- MODULE TurnContracts -----------------------------
EXTENDS LocationContracts

                                                                            
                                                                              
                                                                             
                                                                   

                                                                            
                                                                            
                                                                              
TurnOtherPlayer5(player) == IF player = "SideA" THEN "SideB" ELSE "SideA"
TurnPhases5(player) ==
    IF player = "SideA" THEN <<"Draw","NeutralValue00001","Discard">> ELSE <<"NeutralValue00001","Discard">>
OpenTurn5(player, turnId, begunCounts) ==
    [owner |-> player,phase |-> TurnPhases5(player)[1],id |-> turnId,
     formalBegun |-> FALSE,formalEnded |-> FALSE,begunCounts |-> begunCounts]
TurnFrameValid5(t) ==
    /\ t.owner \in SetupPlayers /\ t.phase \in SetupRange(TurnPhases5(t.owner))
    /\ t.id \in Nat \ {0} /\ t.formalBegun \in BOOLEAN /\ t.formalEnded \in BOOLEAN
    /\ t.begunCounts \in [SetupPlayers -> Nat]
TurnActivePlayer5(t) == t.owner
TurnFirstPriority5(t) == t.owner
DuringPlayersTurn5(t, player) == t.owner = player
TurnBeginEvent5(t) ==
    [tag |-> "TurnBegins",actor |-> t.owner,turnId |-> t.id,
     sideATurn |-> t.begunCounts["SideA"] + IF t.owner = "SideA" THEN 1 ELSE 0]
TurnFormalBegin5(before, after, atActualFormalBeginStep, events) ==
    /\ TurnFrameValid5(before) /\ ~before.formalBegun /\ ~before.formalEnded
    /\ atActualFormalBeginStep /\ events = {TurnBeginEvent5(before)}
    /\ after = [before EXCEPT !.formalBegun = TRUE,!.begunCounts[before.owner] = @+1]
TurnEndEvents5(t) ==
    {[tag |-> tag,actor |-> t.owner,turnId |-> t.id,
      sideATurn |-> t.begunCounts["SideA"]] : tag \in {"TurnEnds","DiscardPhaseEnds"}}
TurnFormalEnd5(before, after, atActualFormalEndStep, events) ==
    /\ TurnFrameValid5(before) /\ before.phase = "Discard" /\ ~before.formalEnded
    /\ atActualFormalEndStep /\ events = TurnEndEvents5(before)
    /\ after = [before EXCEPT !.formalEnded = TRUE]
NextTurnPhase5(owner, phase) ==
    CASE owner = "SideA" /\ phase = "Draw" -> "NeutralValue00001"
      [] phase = "NeutralValue00001" -> "Discard" [] OTHER -> "NoValue"
TurnPhaseAdvance5(before, after, actualPhaseProcedureComplete) ==
    /\ TurnFrameValid5(before) /\ ~before.formalEnded /\ actualPhaseProcedureComplete
    /\ NextTurnPhase5(before.owner,before.phase) # "NoValue"
    /\ after = [before EXCEPT !.phase = NextTurnPhase5(before.owner,before.phase)]
TurnHandoff5(before, after, oldTurnProcedureComplete, events) ==
    /\ TurnFrameValid5(before) /\ before.phase = "Discard" /\ before.formalEnded
    /\ oldTurnProcedureComplete /\ events = {}
    /\ after = OpenTurn5(TurnOtherPlayer5(before.owner),before.id+1,before.begunCounts)
NoBetweenTurns5(gameStarted, turn) == gameStarted => TurnFrameValid5(turn)
                                                                         
                                                                        
IsAction5(paidAbility, triggerCost) ==
    paidAbility /\ Len(triggerCost) > 0 /\ triggerCost[1].kind = "SpendActionPoints"
OwnActionPhase5(turn, player) ==
    TurnFrameValid5(turn) /\ turn.owner = player /\ turn.phase = "NeutralValue00001" /\ ~turn.formalEnded
BasicActionIds5(player) ==
    IF player = "SideA" THEN
       {"GainResourceUnit","Draw","Deploy","Play","AddProgress","RetireResource","Purge"}
    ELSE {"GainResourceUnit","Draw","Deploy","Play","SchemaAtom138","RemoveExposureMarker"}
BasicAction5(player, id) ==
    [actionPoints |-> IF id = "Purge" THEN 3 ELSE 1,
     resourceUnits |-> CASE id = "AddProgress" -> 1
                   [] id \in {"RetireResource","RemoveExposureMarker"} -> 2 [] OTHER -> 0,
     effect |-> CASE id = "GainResourceUnit" -> "GainResourceUnit" [] id = "Draw" -> "Draw"
                  [] id = "Deploy" -> "Deploy" [] id = "Play" -> "Play"
                  [] id = "AddProgress" -> "AddProgress" [] id = "RetireResource" -> "Retire"
                  [] id = "Purge" -> "PurgeCluster" [] id = "SchemaAtom138" -> "SchemaAtom138"
                  [] OTHER -> "RemoveExposureMarker",
     quantity |-> IF id = "Purge" THEN "AllClusterCounters" ELSE 1,
     sourceZone |-> IF id \in {"Deploy","Play"} THEN
                       IF player = "SideA" THEN "SchemaAtom082" ELSE "BHand"
                    ELSE "NoValue",
     types |-> CASE id = "Deploy" /\ player = "SideA" -> {"Objective","Facility","Attachment","Barrier"}
                 [] id = "Deploy" -> {"Technique","Support","Equipment"}
                 [] id = "Play" -> IF player = "SideA" THEN {"Plan"} ELSE {"Action"}
                 [] id = "RetireResource" -> {"Support"} [] OTHER -> {},
     deployedTarget |-> id \in {"AddProgress","RetireResource"},
     needsHasExposureMarkers |-> id \in {"RetireResource","RemoveExposureMarker"}]
BasicActionLocalGate5(player,id,sideBHasExposureMarkers) ==
    /\ player \in SetupPlayers /\ id \in BasicActionIds5(player)
    /\ (BasicAction5(player,id).needsHasExposureMarkers => sideBHasExposureMarkers)
BasicCardTarget5(player,id,cardType,zone,deployed) ==
    /\ id \in BasicActionIds5(player)
    /\ (BasicAction5(player,id).types # {} => cardType \in BasicAction5(player,id).types)
    /\ (BasicAction5(player,id).sourceZone # "NoValue" =>
          zone = BasicAction5(player,id).sourceZone)
    /\ (BasicAction5(player,id).deployedTarget => deployed)
BasicActionKey5(player,id) == <<"Basic",player,id>>
CardActionKey5(sourceObject,abilityNode) == <<"Card",sourceObject,abilityNode>>
AllSameActions5(keys) == Len(keys) > 0 /\ \A i \in 1..Len(keys): keys[i] = keys[1]
AllDifferentActions5(keys) ==
    \A i,j \in 1..Len(keys): i # j => keys[i] # keys[j]
                                                                           
                                                                                 
WithBasicEffect5(actionKind,actionId,occurrenceActionId,actualEffect,queriedEffect) ==
    actionKind = "Basic" /\ actionId = occurrenceActionId /\ actualEffect = queriedEffect

NewAction5(actionId,player,key) ==
    [id |-> actionId,owner |-> player,key |-> key,status |-> "CostReactions",nested |-> "NoValue"]
ActionStart5(turn,player,paidAbility,cost,actualActionWindow,allCostsPaid,
             noResolvingAction,actionId,key,after) ==
    /\ OwnActionPhase5(turn,player) /\ IsAction5(paidAbility,cost)
    /\ actualActionWindow /\ allCostsPaid /\ noResolvingAction
    /\ after = NewAction5(actionId,player,key)
ActionEffectsBegin5(before,after,costCheckpointAndReactionsDrained) ==
    /\ before.status = "CostReactions" /\ costCheckpointAndReactionsDrained
    /\ after = [before EXCEPT !.status = "Effects"]
ActionNestedBegin5(before,after,actualNestedStructureId) ==
    /\ before.status = "Effects" /\ before.nested = "NoValue"
    /\ actualNestedStructureId # "NoValue"
    /\ after = [before EXCEPT !.status = "Nested",!.nested = actualNestedStructureId]
ActionNestedReturn5(before,after,completedStructureId,actualStructureComplete) ==
    /\ before.status = "Nested" /\ actualStructureComplete
    /\ completedStructureId = before.nested
    /\ after = [before EXCEPT !.status = "Effects",!.nested = "NoValue"]
ActionComplete5(before,after,allRemainingActionEffectsResolved) ==
    /\ before.status = "Effects" /\ before.nested = "NoValue"
    /\ allRemainingActionEffectsResolved
    /\ after = [before EXCEPT !.status = "Complete"]
ActionReadyToContinue5(action) == action.status = "Complete"
ActionVoluntaryOption5(action,option,actualNestedPriorityOptions) ==
    /\ action.status = "Nested" /\ action.nested # "NoValue"
    /\ option \in {"PaidAbility","Activation","ObjectiveCompletion"} /\ option \in actualNestedPriorityOptions
ActionCompletionReactionStep5(player) ==
    IF player = "SideA" THEN "After5.6.2b" ELSE "After5.7.1f"
DirectedActionOutsidePhase5(turn,player,before,after) ==
    ~OwnActionPhase5(turn,player) /\ after = before
                                                                             
                                                                                   
HasDrawPhase5(player) == player = "SideA"
MandatoryDrawContext5(turn,atActualMandatoryDrawStep) ==
    TurnFrameValid5(turn) /\ turn.owner = "SideA" /\ turn.phase = "Draw"
    /\ ~turn.formalEnded /\ atActualMandatoryDrawStep
MandatoryDrawEvent5 ==
    [tag |-> "Draw",actor |-> "SideA",mandatory |-> TRUE,action |-> FALSE,amount |-> 1]
UnmodifiedMandatoryDraw5(turn,before,after,atActualMandatoryDrawStep,
                        normalDrawProcedureApplies,winner,events) ==
    /\ MandatoryDrawContext5(turn,atActualMandatoryDrawStep)
    /\ normalDrawProcedureApplies /\ DeckSequenceValid4(before.deck)
    /\ SetupRange(before.deck) \intersect before.hand = {}
    /\ IF before.deck = <<>> THEN
          /\ winner = RequiredEmptyDeckWinner4("SideA",before.deck,TRUE,TRUE)
          /\ after = before /\ events = {}
       ELSE
          /\ winner = "NoValue" /\ events = {MandatoryDrawEvent5}
          /\ after = [before EXCEPT !.deck = Tail(@),!.hand = @ \cup {before.deck[1]}]
                                                                            
                                                                                
ActionPhaseMayTakeAction5(turn,ending,player) == OwnActionPhase5(turn,player) /\ ~ending
ActionPhaseDecision5(turn,ending,actionPoints,actualDecisionStep,precedingProceduresDrained) ==
    IF ActionPhaseMayTakeAction5(turn,ending,turn.owner) /\ actualDecisionStep
       /\ precedingProceduresDrained
    THEN IF actionPoints > 0 THEN "MustTakeAction" ELSE "ProceedToFormalEnd"
    ELSE "Unavailable"
ActionPhaseEndEvent5(turn) ==
    [tag |-> "ActionPhaseEnds",actor |-> turn.owner,turnId |-> turn.id]
ForceActionPhaseEnd5(before,after,player,actualAuthorizedEndInstruction,events) ==
    /\ actualAuthorizedEndInstruction
    /\ OwnActionPhase5(before.turn,player) /\ ~before.ending
    /\ events = {ActionPhaseEndEvent5(before.turn)}
    /\ after = [before EXCEPT
         !.ending = TRUE,!.step = "EndingCheckpoint",!.remainingSteps = <<>>,
         !.openWindows = {},!.priority = "none",
         !.pending = {a \in @: before.pendingWindow[a] \notin before.openWindows},
         !.completedActions = @ \cup before.resolvingActions,
         !.completedAbilities = @ \cup before.resolvingAbilities,
         !.resolvingActions = {},!.resolvingAbilities = {},!.checkpointDue = TRUE]
ActionPhaseEndOutsidePhase5(before,after,player,events) ==
    ~OwnActionPhase5(before.turn,player) /\ after = before /\ events = {}
ActionPhaseEndCheckpoint5(before,after,actualNormalCheckpointCompleted) ==
    /\ before.ending /\ before.step = "EndingCheckpoint" /\ before.checkpointDue
    /\ actualNormalCheckpointCompleted
    /\ after = [before EXCEPT !.step = "EndingReactions",!.checkpointDue = FALSE]
ActionPhaseEndDrain5(before,after,allEndingReactionWindowsDrained) ==
    /\ before.ending /\ before.step = "EndingReactions" /\ ~before.checkpointDue
    /\ allEndingReactionWindowsDrained
    /\ after = [before EXCEPT !.turn.phase = "Discard",!.ending = FALSE,!.step = "DiscardStep"]
                                                                           
                                                                               
MaximumHandSize5(player,persistentCapacityLoss,effectiveOtherAdjustment) ==
    StandardMaximumHandSize4 + effectiveOtherAdjustment -
      IF player = "SideB" THEN persistentCapacityLoss ELSE 0
PersistentCapacityLossAccrual5(before,after,suffered) ==
    before \in Nat /\ suffered \in Nat /\ after = before+suffered
DiscardStepId5(player) == IF player = "SideA" THEN "ProcedureCode93af477f9d95" ELSE "ProcedureCode593c4a6fb4f5"
DiscardBatchEvent5(player,selected) ==
    [tag |-> "Discard",actor |-> player,cards |-> selected,simultaneous |-> TRUE]
DiscardStep5(turn,before,after,atActualDiscardBoundary,skipDiscardStep,
             effectiveMaximum,selected,handChecked,winCondition,events) ==
    /\ TurnFrameValid5(turn) /\ turn.phase = "Discard" /\ ~turn.formalEnded
    /\ atActualDiscardBoundary
    /\ IF skipDiscardStep THEN
          /\ after = before /\ selected = {} /\ ~handChecked
          /\ winCondition = "NoValue" /\ events = {}
       ELSE
          /\ handChecked
          /\ IF SideBHandHarmElimination4(turn.owner,effectiveMaximum,TRUE) THEN
                /\ after = before /\ selected = {} /\ winCondition = "SideA"
                /\ events = {}
             ELSE
                /\ winCondition = "NoValue" /\ selected \subseteq before.hand
                                                                              
                                                                                
                /\ Cardinality(selected) =
                     MinOf(Cardinality(before.hand),
                           HandDiscardDemand4(before.hand,effectiveMaximum,TRUE))
                /\ selected \subseteq DOMAIN before.faces
                /\ after = [before EXCEPT !.hand = @ \ selected,
                     !.discard = @ \cup selected,
                     !.faces = [c \in DOMAIN @ |-> IF c \in selected
                                  THEN DiscardArrivalFace4(turn.owner,
                                         IF turn.owner = "SideA" THEN "SideAHand" ELSE "SideBHand",
                                         "Discard",FALSE)
                                  ELSE before.faces[c]]]
                /\ events = IF selected = {} THEN {} ELSE {DiscardBatchEvent5(turn.owner,selected)}
                                                                               
                                                                             
TurnStepDescriptor5(kind,phase,objectiveCompletionWindow) ==
    [kind |-> kind,phase |-> phase,
     options |-> IF kind = "PaidWindow" THEN
                   IF objectiveCompletionWindow THEN {"PaidAbility","Activation","ObjectiveCompletion"} ELSE {"PaidAbility","Activation"}
                 ELSE {},
     activationNonBarrierOnly |-> kind = "PaidWindow"]
SideASteps5 ==
    <<"ProcedureCode3557d050aec7","ProcedureCode36065334a34a","ProcedureCode599a3c2d7264","ProcedureCode824821d07be7","ProcedureCode59141ee1a13b","ProcedureCodedab8b83ddbcc",
      "ProcedureCoded6fbcb09dd4f","ProcedureCode0e20572a4bab","ProcedureCodeb6035cb98279","ProcedureCode042aa78ff256","ProcedureCode79efdf0ee977",
      "ProcedureCode93af477f9d95","ProcedureCode438597bede05","ProcedureCode4e363e6bb7cf","ProcedureCodea107cee5c079","ProcedureCode72a65676fb11">>
SideAStepInfo5(step) ==
 LET phase == CASE step \in SetupRange(SubSeq(SideASteps5,1,6)) -> "Draw"
                [] step \in SetupRange(SubSeq(SideASteps5,7,11)) -> "NeutralValue00001"
                [] OTHER -> "Discard"
     kind == CASE step = "ProcedureCode3557d050aec7" -> "AllotActionPoints"
               [] step \in {"ProcedureCode36065334a34a","ProcedureCoded6fbcb09dd4f","ProcedureCode438597bede05"} -> "PaidWindow"
               [] step = "ProcedureCode599a3c2d7264" -> "Refill"
               [] step = "ProcedureCode824821d07be7" -> "TurnBegins"
               [] step = "ProcedureCode59141ee1a13b" -> "MandatoryDraw"
               [] step = "ProcedureCode0e20572a4bab" -> "NeutralValue00001"
               [] step = "ProcedureCodeb6035cb98279" -> "Loop"
               [] step = "ProcedureCode042aa78ff256" -> "ActionPhaseEnds"
               [] step = "ProcedureCode93af477f9d95" -> "DiscardStep"
               [] step = "ProcedureCode4e363e6bb7cf" -> "LoseUnspentActionPoints"
               [] step = "ProcedureCodea107cee5c079" -> "TurnEnds"
               [] step = "ProcedureCode72a65676fb11" -> "Handoff" [] OTHER -> "PhaseComplete"
 IN TurnStepDescriptor5(kind,phase,step \in {"ProcedureCode36065334a34a","ProcedureCoded6fbcb09dd4f"})
OpenSideAProcedure5(turn) ==
    [turn |-> turn,step |-> "ProcedureCode3557d050aec7",decision |-> "NoValue",phaseEndMet |-> FALSE]
SideAProcedureValid5(f) ==
    TurnFrameValid5(f.turn) /\ f.turn.owner = "SideA" /\ f.step \in SetupRange(SideASteps5)
    /\ f.turn.phase = SideAStepInfo5(f.step).phase
    /\ f.decision \in {"NoValue","NeutralValue00001","End"} /\ f.phaseEndMet \in BOOLEAN
SideANextStep5(step,decision) ==
    CASE step = "ProcedureCode0e20572a4bab" -> IF decision = "NeutralValue00001" THEN "ProcedureCodeb6035cb98279" ELSE "ProcedureCode042aa78ff256"
      [] step = "ProcedureCodeb6035cb98279" -> "ProcedureCoded6fbcb09dd4f"
      [] step = "ProcedureCode72a65676fb11" -> "ProcedureCode81ed7b3ac00d"
      [] OTHER -> SideASteps5[(CHOOSE i \in 1..Len(SideASteps5): SideASteps5[i] = step)+1]
SideALatchDecision5(before,after,actualUnspentActionPoints,precedingWindowAndReactionsDrained) ==
    /\ SideAProcedureValid5(before) /\ before.step = "ProcedureCode0e20572a4bab"
    /\ before.decision = "NoValue" /\ ~before.phaseEndMet
    /\ ActionPhaseDecision5(before.turn,FALSE,actualUnspentActionPoints,TRUE,
                          precedingWindowAndReactionsDrained) # "Unavailable"
    /\ after = [before EXCEPT !.decision = IF actualUnspentActionPoints > 0 THEN "NeutralValue00001" ELSE "End"]
SideAStepAdvance5(before,after,actualStepIncludingReactionsComplete) ==
    /\ SideAProcedureValid5(before) /\ actualStepIncludingReactionsComplete
    /\ (before.step = "ProcedureCode0e20572a4bab" => before.decision \in {"NeutralValue00001","End"})
    /\ (before.step = "ProcedureCode824821d07be7" => before.turn.formalBegun)
    /\ (before.step = "ProcedureCode042aa78ff256" => before.phaseEndMet)
    /\ (before.step = "ProcedureCodea107cee5c079" => before.turn.formalEnded)
    /\ IF before.step = "ProcedureCode72a65676fb11" THEN
          /\ TurnHandoff5(before.turn,after.turn,TRUE,{})
          /\ after = [before EXCEPT !.turn = OpenTurn5("SideB",before.turn.id+1,before.turn.begunCounts),
                       !.step = "ProcedureCode81ed7b3ac00d",!.decision = "NoValue",!.phaseEndMet = FALSE]
       ELSE
          LET next == SideANextStep5(before.step,before.decision)
          IN after = [before EXCEPT !.step = next,!.turn.phase = SideAStepInfo5(next).phase,!.decision = "NoValue"]
SideADefaultAllotment5 == 3
GainAllottedActionPoints5(before,after,player,effectiveAllotment) ==
    /\ player \in SetupPlayers /\ effectiveAllotment \in Int
    /\ after = [before EXCEPT ![player] = @+effectiveAllotment]
LoseUnspentActionPoints5(before,after,player) ==
    player \in SetupPlayers /\ after = [before EXCEPT ![player] = IF @ > 0 THEN 0 ELSE @]
RecurringRefill5(beforeCount,afterCount,effectiveRecurring,activeControlledByTurnPlayer) ==
    /\ activeControlledByTurnPlayer /\ beforeCount \in Nat /\ effectiveRecurring \in Int
    /\ afterCount = beforeCount+MaxOf(0,effectiveRecurring-beforeCount)
SideAAllotmentAtStep5(f,before,after,effectiveAllotment) ==
    SideAProcedureValid5(f) /\ f.step = "ProcedureCode3557d050aec7" /\
    GainAllottedActionPoints5(before,after,"SideA",effectiveAllotment)
SideARefillAtStep5(f,before,after,effectiveRecurring,activeControlledBySideA) ==
    SideAProcedureValid5(f) /\ f.step = "ProcedureCode599a3c2d7264" /\
    RecurringRefill5(before,after,effectiveRecurring,activeControlledBySideA)
SideAFormalBeginAtStep5(before,after,events) ==
    /\ SideAProcedureValid5(before) /\ before.step = "ProcedureCode824821d07be7"
    /\ TurnFormalBegin5(before.turn,after.turn,TRUE,events)
    /\ after = [before EXCEPT !.turn = after.turn]
SideAMandatoryDrawAtStep5(f,before,after,normalDrawApplies,winCondition,events) ==
    SideAProcedureValid5(f) /\ f.step = "ProcedureCode59141ee1a13b" /\
    UnmodifiedMandatoryDraw5(f.turn,before,after,TRUE,normalDrawApplies,winCondition,events)
SideAActionPhaseEndAtStep5(before,after,events) ==
    /\ SideAProcedureValid5(before) /\ before.step = "ProcedureCode042aa78ff256" /\ ~before.phaseEndMet
    /\ events = {ActionPhaseEndEvent5(before.turn)}
    /\ after = [before EXCEPT !.phaseEndMet = TRUE]
SideADiscardAtStep5(f,before,after,skip,maximum,selected,checked,winCondition,events) ==
    SideAProcedureValid5(f) /\ f.step = "ProcedureCode93af477f9d95" /\
    DiscardStep5(f.turn,before,after,TRUE,skip,maximum,selected,checked,winCondition,events)
SideALoseActionPointsAtStep5(f,before,after) ==
    SideAProcedureValid5(f) /\ f.step = "ProcedureCode4e363e6bb7cf" /\ LoseUnspentActionPoints5(before,after,"SideA")
SideAFormalEndAtStep5(before,after,events) ==
    /\ SideAProcedureValid5(before) /\ before.step = "ProcedureCodea107cee5c079"
    /\ TurnFormalEnd5(before.turn,after.turn,TRUE,events)
    /\ after = [before EXCEPT !.turn = after.turn]
                                                                             
                                                             
SideBSteps5 ==
    <<"ProcedureCode81ed7b3ac00d","ProcedureCodef53fc09e15ad","ProcedureCoded05d55b14bf9","ProcedureCodebb587f61a951","ProcedureCode484be3e50aa9","ProcedureCode989abc27e0c6","ProcedureCodea439ce381bba","ProcedureCodeb6952d25a4da","ProcedureCoded3bf6d016bb1",
      "ProcedureCode593c4a6fb4f5","ProcedureCode13c5f7239eb2","ProcedureCodede325c329e93","ProcedureCode8f113080e47f","ProcedureCode49c3ccade13b">>
SideBStepInfo5(step) ==
 LET phase == IF step \in SetupRange(SubSeq(SideBSteps5,1,9)) THEN "NeutralValue00001" ELSE "Discard"
     kind == CASE step = "ProcedureCode81ed7b3ac00d" -> "AllotActionPoints"
               [] step \in {"ProcedureCodef53fc09e15ad","ProcedureCode484be3e50aa9","ProcedureCode13c5f7239eb2"} -> "PaidWindow"
               [] step = "ProcedureCoded05d55b14bf9" -> "Refill"
               [] step = "ProcedureCodebb587f61a951" -> "TurnBegins"
               [] step = "ProcedureCode989abc27e0c6" -> "NeutralValue00001"
               [] step = "ProcedureCodea439ce381bba" -> "Loop"
               [] step = "ProcedureCodeb6952d25a4da" -> "ActionPhaseEnds"
               [] step = "ProcedureCode593c4a6fb4f5" -> "DiscardStep"
               [] step = "ProcedureCodede325c329e93" -> "LoseUnspentActionPoints"
               [] step = "ProcedureCode8f113080e47f" -> "TurnEnds"
               [] step = "ProcedureCode49c3ccade13b" -> "Handoff" [] OTHER -> "PhaseComplete"
 IN TurnStepDescriptor5(kind,phase,FALSE)
OpenSideBProcedure5(turn) ==
    [turn |-> turn,step |-> "ProcedureCode81ed7b3ac00d",decision |-> "NoValue",phaseEndMet |-> FALSE]
SideBProcedureValid5(f) ==
    TurnFrameValid5(f.turn) /\ f.turn.owner = "SideB" /\ f.step \in SetupRange(SideBSteps5)
    /\ f.turn.phase = SideBStepInfo5(f.step).phase
    /\ f.decision \in {"NoValue","NeutralValue00001","End"} /\ f.phaseEndMet \in BOOLEAN
SideBNextStep5(step,decision) ==
    CASE step = "ProcedureCode989abc27e0c6" -> IF decision = "NeutralValue00001" THEN "ProcedureCodea439ce381bba" ELSE "ProcedureCodeb6952d25a4da"
      [] step = "ProcedureCodea439ce381bba" -> "ProcedureCode484be3e50aa9"
      [] step = "ProcedureCode49c3ccade13b" -> "ProcedureCode3557d050aec7"
      [] OTHER -> SideBSteps5[(CHOOSE i \in 1..Len(SideBSteps5): SideBSteps5[i] = step)+1]
SideBLatchDecision5(before,after,actualUnspentActionPoints,precedingWindowAndReactionsDrained) ==
    /\ SideBProcedureValid5(before) /\ before.step = "ProcedureCode989abc27e0c6"
    /\ before.decision = "NoValue" /\ ~before.phaseEndMet
    /\ ActionPhaseDecision5(before.turn,FALSE,actualUnspentActionPoints,TRUE,
                          precedingWindowAndReactionsDrained) # "Unavailable"
    /\ after = [before EXCEPT !.decision = IF actualUnspentActionPoints > 0 THEN "NeutralValue00001" ELSE "End"]
SideBStepAdvance5(before,after,actualStepIncludingReactionsComplete) ==
    /\ SideBProcedureValid5(before) /\ actualStepIncludingReactionsComplete
    /\ (before.step = "ProcedureCode989abc27e0c6" => before.decision \in {"NeutralValue00001","End"})
    /\ (before.step = "ProcedureCodebb587f61a951" => before.turn.formalBegun)
    /\ (before.step = "ProcedureCodeb6952d25a4da" => before.phaseEndMet)
    /\ (before.step = "ProcedureCode8f113080e47f" => before.turn.formalEnded)
    /\ IF before.step = "ProcedureCode49c3ccade13b" THEN
          /\ TurnHandoff5(before.turn,after.turn,TRUE,{})
          /\ after = [before EXCEPT !.turn = OpenTurn5("SideA",before.turn.id+1,before.turn.begunCounts),
                       !.step = "ProcedureCode3557d050aec7",!.decision = "NoValue",!.phaseEndMet = FALSE]
       ELSE
          LET next == SideBNextStep5(before.step,before.decision)
          IN after = [before EXCEPT !.step = next,!.turn.phase = SideBStepInfo5(next).phase,!.decision = "NoValue"]
SideBDefaultAllotment5 == 4
SideBAllotmentAtStep5(f,before,after,effectiveAllotment) ==
    SideBProcedureValid5(f) /\ f.step = "ProcedureCode81ed7b3ac00d" /\
    GainAllottedActionPoints5(before,after,"SideB",effectiveAllotment)
SideBRefillAtStep5(f,before,after,effectiveRecurring,activeControlledBySideB) ==
    SideBProcedureValid5(f) /\ f.step = "ProcedureCoded05d55b14bf9" /\
    RecurringRefill5(before,after,effectiveRecurring,activeControlledBySideB)
SideBFormalBeginAtStep5(before,after,events) ==
    /\ SideBProcedureValid5(before) /\ before.step = "ProcedureCodebb587f61a951"
    /\ TurnFormalBegin5(before.turn,after.turn,TRUE,events)
    /\ after = [before EXCEPT !.turn = after.turn]
SideBActionPhaseEndAtStep5(before,after,events) ==
    /\ SideBProcedureValid5(before) /\ before.step = "ProcedureCodeb6952d25a4da" /\ ~before.phaseEndMet
    /\ events = {ActionPhaseEndEvent5(before.turn)}
    /\ after = [before EXCEPT !.phaseEndMet = TRUE]
SideBDiscardAtStep5(f,before,after,skip,maximum,selected,checked,winCondition,events) ==
    SideBProcedureValid5(f) /\ f.step = "ProcedureCode593c4a6fb4f5" /\
    DiscardStep5(f.turn,before,after,TRUE,skip,maximum,selected,checked,winCondition,events)
SideBLoseActionPointsAtStep5(f,before,after) ==
    SideBProcedureValid5(f) /\ f.step = "ProcedureCodede325c329e93" /\ LoseUnspentActionPoints5(before,after,"SideB")
SideBFormalEndAtStep5(before,after,events) ==
    /\ SideBProcedureValid5(before) /\ before.step = "ProcedureCode8f113080e47f"
    /\ TurnFormalEnd5(before.turn,after.turn,TRUE,events)
    /\ after = [before EXCEPT !.turn = after.turn]
=============================================================================