---------------------------- MODULE TurnChecksMC ---------------------------- EXTENDS TurnContracts VARIABLE block5 Init5 == block5 \in 1..7 Next5 == UNCHANGED block5 Spec5 == Init5 /\ [][Next5]_block5 ZeroBegunCounts5 == [p \in SetupPlayers |-> 0] GeneralTurnChecks5 == LET opening == OpenTurn5("SideA",1,ZeroBegunCounts5) begun == [opening EXCEPT !.formalBegun = TRUE,!.begunCounts["SideA"] = 1] action == [begun EXCEPT !.phase = "NeutralValue00001"] discard == [begun EXCEPT !.phase = "Discard"] ended == [discard EXCEPT !.formalEnded = TRUE] next == OpenTurn5("SideB",2,begun.begunCounts) IN /\ TurnPhases5("SideA") = <<"Draw","NeutralValue00001","Discard">> /\ TurnPhases5("SideB") = <<"NeutralValue00001","Discard">> /\ TurnFrameValid5(opening) /\ NoBetweenTurns5(TRUE,opening) /\ TurnActivePlayer5(opening) = "SideA" /\ TurnFirstPriority5(opening) = "SideA" /\ DuringPlayersTurn5(opening,"SideA") /\ DuringPlayersTurn5(ended,"SideA") /\ ~DuringPlayersTurn5(ended,"SideB") /\ TurnFormalBegin5(opening,begun,TRUE,{TurnBeginEvent5(opening)}) /\ ~TurnFormalBegin5(opening,begun,FALSE,{TurnBeginEvent5(opening)}) /\ ~TurnFormalBegin5(opening,begun,TRUE,{}) /\ ~TurnFormalBegin5(begun,begun,TRUE,{TurnBeginEvent5(begun)}) /\ TurnBeginEvent5(opening).sideATurn = 1 /\ TurnPhaseAdvance5(begun,action,TRUE) /\ ~TurnPhaseAdvance5(begun,action,FALSE) /\ ~TurnPhaseAdvance5(begun,discard,TRUE) /\ TurnFormalEnd5(discard,ended,TRUE,TurnEndEvents5(discard)) /\ ~TurnFormalEnd5(discard,ended,FALSE,TurnEndEvents5(discard)) /\ ~TurnFormalEnd5(discard,ended,TRUE,{}) /\ TurnHandoff5(ended,next,TRUE,{}) /\ ~TurnHandoff5(ended,next,FALSE,{}) /\ ~TurnHandoff5(discard,next,TRUE,{}) /\ ~TurnHandoff5(ended,next,TRUE,{TurnBeginEvent5(next)}) /\ ~next.formalBegun /\ next.begunCounts = begun.begunCounts /\ TurnActivePlayer5(next) = "SideB" /\ TurnFirstPriority5(next) = "SideB" /\ ~NoBetweenTurns5(TRUE,[opening EXCEPT !.owner = "none"]) /\ ~TurnFrameValid5([next EXCEPT !.phase = "Draw"]) ActionChecks5 == LET cost == <<[kind |-> "SpendActionPoints",amount |-> 1]>> lose == <<[kind |-> "LoseActionPoints",amount |-> 1]>> t == [OpenTurn5("SideB",1,ZeroBegunCounts5) EXCEPT !.formalBegun = TRUE] key == BasicActionKey5("SideB","Play") a == NewAction5(1,"SideB",key) e == [a EXCEPT !.status = "Effects"] n == [e EXCEPT !.status = "Nested",!.nested = "traversal1"] c == [e EXCEPT !.status = "Complete"] IN /\ IsAction5(TRUE,cost) /\ ~IsAction5(TRUE,lose) /\ ~IsAction5(FALSE,cost) /\ ~IsAction5(TRUE,<<>>) /\ ~IsAction5(TRUE,<<[kind |-> "ResourceUnit",amount |-> 1],cost[1]>>) /\ ActionStart5(t,"SideB",TRUE,cost,TRUE,TRUE,TRUE,1,key,a) /\ ~ActionStart5(t,"SideB",TRUE,cost,FALSE,TRUE,TRUE,1,key,a) /\ ~ActionStart5(t,"SideB",TRUE,cost,TRUE,FALSE,TRUE,1,key,a) /\ ~ActionStart5(t,"SideB",TRUE,cost,TRUE,TRUE,FALSE,1,key,a) /\ ~ActionStart5(t,"SideA",TRUE,cost,TRUE,TRUE,TRUE,1,key,a) /\ ActionEffectsBegin5(a,e,TRUE) /\ ~ActionEffectsBegin5(a,e,FALSE) /\ ActionNestedBegin5(e,n,"traversal1") /\ ~ActionComplete5(n,c,TRUE) /\ ~ActionReadyToContinue5(n) /\ ~ActionNestedReturn5(n,e,"traversal2",TRUE) /\ ~ActionNestedReturn5(n,e,"traversal1",FALSE) /\ ActionNestedReturn5(n,e,"traversal1",TRUE) /\ ~ActionComplete5(e,c,FALSE) /\ ActionComplete5(e,c,TRUE) /\ ActionReadyToContinue5(c) /\ ~ActionVoluntaryOption5(e,"Activation",{"Activation"}) /\ ActionVoluntaryOption5(n,"Activation",{"PaidAbility","Activation"}) /\ ~ActionVoluntaryOption5(n,"ObjectiveCompletion",{"PaidAbility","Activation"}) /\ DirectedActionOutsidePhase5([t EXCEPT !.phase = "Discard"],"SideB",a,a) /\ ~DirectedActionOutsidePhase5(t,"SideB",a,a) /\ ActionCompletionReactionStep5("SideA") = "After5.6.2b" /\ ActionCompletionReactionStep5("SideB") = "After5.7.1f" /\ AllSameActions5(<>) /\ ~AllDifferentActions5(<>) /\ AllDifferentActions5(<>) /\ AllDifferentActions5(<>) /\ WithBasicEffect5("Basic",1,1,"Draw","Draw") /\ ~WithBasicEffect5("Card",1,1,"Draw","Draw") /\ ~WithBasicEffect5("Basic",1,2,"Draw","Draw") /\ Cardinality(BasicActionIds5("SideA")) = 7 /\ Cardinality(BasicActionIds5("SideB")) = 6 /\ BasicAction5("SideA","Purge").actionPoints = 3 /\ BasicAction5("SideA","Purge").quantity = "AllClusterCounters" /\ BasicAction5("SideA","AddProgress").resourceUnits = 1 /\ BasicAction5("SideA","RetireResource").resourceUnits = 2 /\ BasicAction5("SideB","RemoveExposureMarker").resourceUnits = 2 /\ \A p \in SetupPlayers: \A id \in BasicActionIds5(p): /\ BasicActionLocalGate5(p,id,TRUE) /\ BasicAction5(p,id).actionPoints = IF id = "Purge" THEN 3 ELSE 1 /\ BasicAction5(p,id).quantity = IF id = "Purge" THEN "AllClusterCounters" ELSE 1 /\ ~BasicActionLocalGate5("SideA","RetireResource",FALSE) /\ ~BasicActionLocalGate5("SideB","RemoveExposureMarker",FALSE) /\ ~BasicActionLocalGate5("SideB","Purge",TRUE) /\ BasicCardTarget5("SideA","Deploy","Barrier","SchemaAtom082",FALSE) /\ ~BasicCardTarget5("SideA","Deploy","Technique","SchemaAtom082",FALSE) /\ ~BasicCardTarget5("SideA","Play","Plan","SchemaAtom018",FALSE) /\ BasicCardTarget5("SideB","Deploy","Equipment","BHand",FALSE) /\ ~BasicCardTarget5("SideB","Play","Plan","BHand",FALSE) /\ ~BasicCardTarget5("SideA","AddProgress","Facility","TargetSite",FALSE) DrawPhaseChecks5 == LET t == OpenTurn5("SideA",1,ZeroBegunCounts5) before == [deck |-> <<"top","SchemaAtom187">>,hand |-> {"old"},actionPoints |-> 3] after == [before EXCEPT !.deck = <<"SchemaAtom187">>,!.hand = {"old","top"}] empty == [before EXCEPT !.deck = <<>>] IN /\ HasDrawPhase5("SideA") /\ ~HasDrawPhase5("SideB") /\ TurnPhases5("SideA")[1] = "Draw" /\ UnmodifiedMandatoryDraw5(t,before,after,TRUE,TRUE,"NoValue",{MandatoryDrawEvent5}) /\ ~UnmodifiedMandatoryDraw5(t,before,[after EXCEPT !.actionPoints = 2],TRUE,TRUE,"NoValue",{MandatoryDrawEvent5}) /\ ~UnmodifiedMandatoryDraw5(t,before,[after EXCEPT !.hand = {"old","SchemaAtom187"}],TRUE,TRUE,"NoValue",{MandatoryDrawEvent5}) /\ ~UnmodifiedMandatoryDraw5(t,before,after,FALSE,TRUE,"NoValue",{MandatoryDrawEvent5}) /\ ~UnmodifiedMandatoryDraw5(t,before,after,TRUE,FALSE,"NoValue",{MandatoryDrawEvent5}) /\ ~UnmodifiedMandatoryDraw5(OpenTurn5("SideB",2,ZeroBegunCounts5),before,after,TRUE,TRUE,"NoValue",{MandatoryDrawEvent5}) /\ ~UnmodifiedMandatoryDraw5([t EXCEPT !.phase = "NeutralValue00001"],before,after,TRUE,TRUE,"NoValue",{MandatoryDrawEvent5}) /\ UnmodifiedMandatoryDraw5(t,empty,empty,TRUE,TRUE,"SideB",{}) /\ ~UnmodifiedMandatoryDraw5(t,empty,empty,TRUE,TRUE,"NoValue",{}) /\ MandatoryDrawEvent5.amount = 1 /\ ~MandatoryDrawEvent5.action ActionPhaseFixture5(owner,phase) == [turn |-> [OpenTurn5(owner,1,ZeroBegunCounts5) EXCEPT !.phase = phase], ending |-> FALSE,step |-> "AnActionStep",remainingSteps |-> <<"loop","end","complete">>, openWindows |-> {"paid","nested"},priority |-> "SideB", pending |-> {"a","b","outside"}, pendingWindow |-> [a |-> "paid",b |-> "nested",outside |-> "old"], resolvingActions |-> {"action1"},resolvingAbilities |-> {"ability1"}, completedActions |-> {"oldAction"},completedAbilities |-> {"oldAbility"}, checkpointDue |-> FALSE] ActionPhaseChecks5 == LET b == ActionPhaseFixture5("SideB","NeutralValue00001") f == [b EXCEPT !.ending = TRUE,!.step = "EndingCheckpoint",!.remainingSteps = <<>>, !.openWindows = {},!.priority = "none",!.pending = {"outside"}, !.resolvingActions = {},!.resolvingAbilities = {}, !.completedActions = {"oldAction","action1"}, !.completedAbilities = {"oldAbility","ability1"},!.checkpointDue = TRUE] r == [f EXCEPT !.step = "EndingReactions",!.checkpointDue = FALSE] d == [r EXCEPT !.turn.phase = "Discard",!.ending = FALSE,!.step = "DiscardStep"] IN /\ ActionPhaseDecision5(b.turn,FALSE,1,TRUE,TRUE) = "MustTakeAction" /\ ActionPhaseDecision5(b.turn,FALSE,0,TRUE,TRUE) = "ProceedToFormalEnd" /\ ActionPhaseDecision5(b.turn,FALSE,-1,TRUE,TRUE) = "ProceedToFormalEnd" /\ ActionPhaseDecision5(b.turn,FALSE,0,FALSE,TRUE) = "Unavailable" /\ ActionPhaseDecision5(b.turn,FALSE,0,TRUE,FALSE) = "Unavailable" /\ ForceActionPhaseEnd5(b,f,"SideB",TRUE,{ActionPhaseEndEvent5(b.turn)}) /\ ~ForceActionPhaseEnd5(b,f,"SideB",FALSE,{ActionPhaseEndEvent5(b.turn)}) /\ ~ForceActionPhaseEnd5(b,f,"SideA",TRUE,{ActionPhaseEndEvent5(b.turn)}) /\ ~ForceActionPhaseEnd5(b,[f EXCEPT !.pending = {}],"SideB",TRUE,{ActionPhaseEndEvent5(b.turn)}) /\ ~ForceActionPhaseEnd5(b,[f EXCEPT !.openWindows = {"nested"}],"SideB",TRUE,{ActionPhaseEndEvent5(b.turn)}) /\ ~ForceActionPhaseEnd5(b,[f EXCEPT !.resolvingAbilities = {"ability1"}],"SideB",TRUE,{ActionPhaseEndEvent5(b.turn)}) /\ ~ForceActionPhaseEnd5(b,[f EXCEPT !.turn.phase = "Discard"],"SideB",TRUE,{ActionPhaseEndEvent5(b.turn)}) /\ ~ActionPhaseMayTakeAction5(r.turn,r.ending,"SideB") /\ ~ActionPhaseEndDrain5(f,d,TRUE) /\ ActionPhaseEndCheckpoint5(f,r,TRUE) /\ ~ActionPhaseEndCheckpoint5(f,r,FALSE) /\ ActionPhaseEndDrain5(r,d,TRUE) /\ ~ActionPhaseEndDrain5(r,d,FALSE) /\ ~d.turn.formalBegun /\ \A owner \in SetupPlayers: \A player \in SetupPlayers: \A phase \in SetupRange(TurnPhases5(owner)): LET x == ActionPhaseFixture5(owner,phase) IN (~OwnActionPhase5(x.turn,player)) => ActionPhaseEndOutsidePhase5(x,x,player,{}) DiscardPhaseChecks5 == LET t == [OpenTurn5("SideA",1,ZeroBegunCounts5) EXCEPT !.phase = "Discard"] sideB == [t EXCEPT !.owner = "SideB"] b == [hand |-> {"a","b","c"},discard |-> {"old"}, faces |-> [a |-> "Up",b |-> "Up",c |-> "Down",old |-> "Up",other |-> "Down"]] a == [b EXCEPT !.hand = {"c"},!.discard = {"a","b","old"}, !.faces["a"] = "Down",!.faces["b"] = "Down"] ra == [b EXCEPT !.hand = {"c"},!.discard = {"a","b","old"}] all == [b EXCEPT !.hand = {},!.discard = {"a","b","c","old"}, !.faces["a"] = "Down",!.faces["b"] = "Down"] IN /\ MaximumHandSize5("SideA",9,0) = 5 /\ MaximumHandSize5("SideB",0,0) = 5 /\ MaximumHandSize5("SideB",6,0) = -1 /\ MaximumHandSize5("SideB",2,3) = 6 /\ PersistentCapacityLossAccrual5(2,4,2) /\ ~PersistentCapacityLossAccrual5(2,1,0) /\ DiscardStepId5("SideA") = "ProcedureCode93af477f9d95" /\ DiscardStepId5("SideB") = "ProcedureCode593c4a6fb4f5" /\ DiscardStep5(t,b,a,TRUE,FALSE,1,{"a","b"},TRUE,"NoValue",{DiscardBatchEvent5("SideA",{"a","b"})}) /\ ~DiscardStep5(t,b,ra,TRUE,FALSE,1,{"a","b"},TRUE,"NoValue",{DiscardBatchEvent5("SideA",{"a","b"})}) /\ DiscardStep5(sideB,b,ra,TRUE,FALSE,1,{"a","b"},TRUE,"NoValue",{DiscardBatchEvent5("SideB",{"a","b"})}) /\ ~DiscardStep5(t,b,a,FALSE,FALSE,1,{"a","b"},TRUE,"NoValue",{DiscardBatchEvent5("SideA",{"a","b"})}) /\ ~DiscardStep5(t,b,a,TRUE,FALSE,2,{"a","b"},TRUE,"NoValue",{DiscardBatchEvent5("SideA",{"a","b"})}) /\ DiscardStep5(t,b,b,TRUE,FALSE,3,{},TRUE,"NoValue",{}) /\ DiscardStep5(t,b,b,TRUE,FALSE,5,{},TRUE,"NoValue",{}) /\ DiscardStep5(sideB,b,b,TRUE,FALSE,-1,{},TRUE,"SideA",{}) /\ ~DiscardStep5(sideB,b,all,TRUE,FALSE,-1,{"a","b","c"},TRUE,"NoValue",{DiscardBatchEvent5("SideB",{"a","b","c"})}) /\ DiscardStep5(sideB,b,b,TRUE,TRUE,-1,{},FALSE,"NoValue",{}) /\ ~DiscardStep5(sideB,b,b,TRUE,TRUE,-1,{},TRUE,"SideA",{}) /\ DiscardStep5(t,b,all,TRUE,FALSE,-2,{"a","b","c"},TRUE,"NoValue",{DiscardBatchEvent5("SideA",{"a","b","c"})}) /\ ~DiscardStep5(t,b,a,TRUE,FALSE,1,{"a","b"},TRUE,"NoValue",{[tag |-> "Retire"]}) /\ ~DiscardStep5(t,b,[a EXCEPT !.faces["other"] = "Up"],TRUE,FALSE,1,{"a","b"},TRUE,"NoValue",{DiscardBatchEvent5("SideA",{"a","b"})}) SideAProcedureChecks5 == LET f == OpenSideAProcedure5(OpenTurn5("SideA",1,ZeroBegunCounts5)) d == [f EXCEPT !.step = "ProcedureCode824821d07be7"] begun == [d EXCEPT !.turn.formalBegun = TRUE,!.turn.begunCounts["SideA"] = 1] b == [begun EXCEPT !.step = "ProcedureCode0e20572a4bab",!.turn.phase = "NeutralValue00001"] action == [b EXCEPT !.decision = "NeutralValue00001"] end == [b EXCEPT !.decision = "End"] formalEnd == [b EXCEPT !.step = "ProcedureCode042aa78ff256"] phaseEnded == [formalEnd EXCEPT !.phaseEndMet = TRUE] te == [phaseEnded EXCEPT !.step = "ProcedureCodea107cee5c079",!.turn.phase = "Discard"] ended == [te EXCEPT !.turn.formalEnded = TRUE] handoff == [ended EXCEPT !.step = "ProcedureCode72a65676fb11"] next == [handoff EXCEPT !.turn = OpenTurn5("SideB",2,begun.turn.begunCounts), !.step = "ProcedureCode81ed7b3ac00d",!.phaseEndMet = FALSE] actionPoints == [SideA |-> 1,SideB |-> -1] IN /\ Len(SideASteps5) = 16 /\ SideAProcedureValid5(f) /\ SideAStepInfo5("ProcedureCode36065334a34a").options = {"PaidAbility","Activation","ObjectiveCompletion"} /\ SideAStepInfo5("ProcedureCoded6fbcb09dd4f").options = {"PaidAbility","Activation","ObjectiveCompletion"} /\ SideAStepInfo5("ProcedureCode438597bede05").options = {"PaidAbility","Activation"} /\ \A s \in {"ProcedureCode36065334a34a","ProcedureCoded6fbcb09dd4f","ProcedureCode438597bede05"}: SideAStepInfo5(s).activationNonBarrierOnly /\ SideAAllotmentAtStep5(f,actionPoints,[actionPoints EXCEPT !["SideA"] = 4],SideADefaultAllotment5) /\ ~SideAAllotmentAtStep5(d,actionPoints,[actionPoints EXCEPT !["SideA"] = 4],3) /\ SideARefillAtStep5([f EXCEPT !.step = "ProcedureCode599a3c2d7264"],0,2,2,TRUE) /\ ~SideARefillAtStep5(f,0,2,2,TRUE) /\ RecurringRefill5(3,3,2,TRUE) /\ ~RecurringRefill5(0,2,2,FALSE) /\ SideAFormalBeginAtStep5(d,begun,{TurnBeginEvent5(d.turn)}) /\ ~SideAStepAdvance5(d,[d EXCEPT !.step = "ProcedureCode59141ee1a13b"],TRUE) /\ SideAStepAdvance5(begun,[begun EXCEPT !.step = "ProcedureCode59141ee1a13b"],TRUE) /\ SideALatchDecision5(b,action,1,TRUE) /\ SideALatchDecision5(b,end,0,TRUE) /\ SideALatchDecision5(b,end,-1,TRUE) /\ ~SideALatchDecision5(b,action,1,FALSE) /\ SideAStepAdvance5(action,[action EXCEPT !.step = "ProcedureCodeb6035cb98279",!.decision = "NoValue"],TRUE) /\ ~SideAStepAdvance5(action,[action EXCEPT !.step = "ProcedureCode042aa78ff256",!.decision = "NoValue"],TRUE) /\ SideAStepAdvance5(end,formalEnd,TRUE) /\ ~SideAStepAdvance5(b,formalEnd,TRUE) /\ ~SideAStepAdvance5(action,[action EXCEPT !.step = "ProcedureCodeb6035cb98279",!.decision = "NoValue"],FALSE) /\ SideANextStep5("ProcedureCodeb6035cb98279","NoValue") = "ProcedureCoded6fbcb09dd4f" /\ SideAActionPhaseEndAtStep5(formalEnd,phaseEnded,{ActionPhaseEndEvent5(formalEnd.turn)}) /\ ~SideAStepAdvance5(formalEnd,[formalEnd EXCEPT !.step = "ProcedureCode79efdf0ee977"],TRUE) /\ SideAStepAdvance5(phaseEnded,[phaseEnded EXCEPT !.step = "ProcedureCode79efdf0ee977"],TRUE) /\ SideALoseActionPointsAtStep5([te EXCEPT !.step = "ProcedureCode4e363e6bb7cf"],actionPoints,[actionPoints EXCEPT !["SideA"] = 0]) /\ LoseUnspentActionPoints5(actionPoints,actionPoints,"SideB") /\ SideAFormalEndAtStep5(te,ended,TurnEndEvents5(te.turn)) /\ ~SideAStepAdvance5(te,[te EXCEPT !.step = "ProcedureCode72a65676fb11"],TRUE) /\ SideAStepAdvance5(handoff,next,TRUE) /\ ~next.turn.formalBegun SideBProcedureChecks5 == LET f == OpenSideBProcedure5(OpenTurn5("SideB",2,ZeroBegunCounts5)) d == [f EXCEPT !.step = "ProcedureCodebb587f61a951"] begun == [d EXCEPT !.turn.formalBegun = TRUE,!.turn.begunCounts["SideB"] = 1] b == [begun EXCEPT !.step = "ProcedureCode989abc27e0c6"] action == [b EXCEPT !.decision = "NeutralValue00001"] end == [b EXCEPT !.decision = "End"] formalEnd == [b EXCEPT !.step = "ProcedureCodeb6952d25a4da"] phaseEnded == [formalEnd EXCEPT !.phaseEndMet = TRUE] te == [phaseEnded EXCEPT !.step = "ProcedureCode8f113080e47f",!.turn.phase = "Discard"] ended == [te EXCEPT !.turn.formalEnded = TRUE] handoff == [ended EXCEPT !.step = "ProcedureCode49c3ccade13b"] next == [handoff EXCEPT !.turn = OpenTurn5("SideA",3,begun.turn.begunCounts), !.step = "ProcedureCode3557d050aec7",!.phaseEndMet = FALSE] actionPoints == [SideA |-> -1,SideB |-> 1] IN /\ Len(SideBSteps5) = 14 /\ SideBProcedureValid5(f) /\ \A s \in SetupRange(SideBSteps5): /\ SideBStepInfo5(s).phase # "Draw" /\ SideBStepInfo5(s).kind # "MandatoryDraw" /\ "ObjectiveCompletion" \notin SideBStepInfo5(s).options /\ \A s \in {"ProcedureCodef53fc09e15ad","ProcedureCode484be3e50aa9","ProcedureCode13c5f7239eb2"}: /\ SideBStepInfo5(s).options = {"PaidAbility","Activation"} /\ SideBStepInfo5(s).activationNonBarrierOnly /\ SideBAllotmentAtStep5(f,actionPoints,[actionPoints EXCEPT !["SideB"] = 5],SideBDefaultAllotment5) /\ ~SideBAllotmentAtStep5(d,actionPoints,[actionPoints EXCEPT !["SideB"] = 5],4) /\ SideBRefillAtStep5([f EXCEPT !.step = "ProcedureCoded05d55b14bf9"],0,2,2,TRUE) /\ ~SideBRefillAtStep5([f EXCEPT !.step = "ProcedureCodef53fc09e15ad"],0,2,2,TRUE) /\ SideBFormalBeginAtStep5(d,begun,{TurnBeginEvent5(d.turn)}) /\ ~SideBStepAdvance5(d,[d EXCEPT !.step = "ProcedureCode484be3e50aa9"],TRUE) /\ SideBStepAdvance5(begun,[begun EXCEPT !.step = "ProcedureCode484be3e50aa9"],TRUE) /\ SideBLatchDecision5(b,action,1,TRUE) /\ SideBLatchDecision5(b,end,0,TRUE) /\ SideBLatchDecision5(b,end,-1,TRUE) /\ ~SideBLatchDecision5(b,action,1,FALSE) /\ SideBStepAdvance5(action,[action EXCEPT !.step = "ProcedureCodea439ce381bba",!.decision = "NoValue"],TRUE) /\ ~SideBStepAdvance5(action,[action EXCEPT !.step = "ProcedureCodeb6952d25a4da",!.decision = "NoValue"],TRUE) /\ SideBStepAdvance5(end,formalEnd,TRUE) /\ ~SideBStepAdvance5(b,formalEnd,TRUE) /\ SideBNextStep5("ProcedureCodea439ce381bba","NoValue") = "ProcedureCode484be3e50aa9" /\ SideBActionPhaseEndAtStep5(formalEnd,phaseEnded,{ActionPhaseEndEvent5(formalEnd.turn)}) /\ ~SideBStepAdvance5(formalEnd,[formalEnd EXCEPT !.step = "ProcedureCoded3bf6d016bb1"],TRUE) /\ SideBStepAdvance5(phaseEnded,[phaseEnded EXCEPT !.step = "ProcedureCoded3bf6d016bb1"],TRUE) /\ SideBLoseActionPointsAtStep5([te EXCEPT !.step = "ProcedureCodede325c329e93"],actionPoints,[actionPoints EXCEPT !["SideB"] = 0]) /\ SideBFormalEndAtStep5(te,ended,TurnEndEvents5(te.turn)) /\ ~SideBStepAdvance5(te,[te EXCEPT !.step = "ProcedureCode49c3ccade13b"],TRUE) /\ SideBStepAdvance5(handoff,next,TRUE) /\ ~next.turn.formalBegun Block5Assertions == CASE block5 = 0 -> TRUE [] block5 = 1 -> GeneralTurnChecks5 [] block5 = 2 -> ActionChecks5 [] block5 = 3 -> DrawPhaseChecks5 [] block5 = 4 -> ActionPhaseChecks5 [] block5 = 5 -> DiscardPhaseChecks5 [] block5 = 6 -> SideAProcedureChecks5 [] block5 = 7 -> SideBProcedureChecks5 =============================================================================