TurnChecksMC¶
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 55 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.
ActionChecks5 · operator
reference-profile · input revision 2 · CC0 1.0
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(<<BasicActionKey5("SideA","Play"),BasicActionKey5("SideA","Play")>>)
/\ ~AllDifferentActions5(<<BasicActionKey5("SideA","Play"),BasicActionKey5("SideA","Play")>>)
/\ AllDifferentActions5(<<CardActionKey5("copy1","abilityA"),CardActionKey5("copy2","abilityA")>>)
/\ AllDifferentActions5(<<CardActionKey5("copy1","abilityA"),CardActionKey5("copy1","abilityB")>>)
/\ 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)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: SetupPlayers, ZeroBegunCounts5, ActionComplete5, ActionCompletionReactionStep5, ActionEffectsBegin5, ActionNestedBegin5, ActionNestedReturn5, ActionReadyToContinue5, ActionStart5, ActionVoluntaryOption5, AllDifferentActions5, AllSameActions5, BasicAction5, BasicActionIds5, BasicActionKey5, BasicActionLocalGate5, BasicCardTarget5, CardActionKey5, DirectedActionOutsidePhase5, IsAction5, NewAction5, OpenTurn5, WithBasicEffect5
ActionPhaseChecks5 · operator
reference-profile · input revision 2 · CC0 1.0
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,{})Exact module download · Source bundle and reproduction instructions
Resolved project definitions: SetupPlayers, SetupRange, ActionPhaseFixture5, ActionPhaseDecision5, ActionPhaseEndCheckpoint5, ActionPhaseEndDrain5, ActionPhaseEndEvent5, ActionPhaseEndOutsidePhase5, ActionPhaseMayTakeAction5, ForceActionPhaseEnd5, OwnActionPhase5, TurnPhases5
ActionPhaseFixture5 · operator
reference-profile · input revision 2 · CC0 1.0
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]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: ZeroBegunCounts5, OpenTurn5
Block5Assertions · operator
reference-profile · input revision 2 · CC0 1.0
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 -> SideBProcedureChecks5Exact module download · Source bundle and reproduction instructions
Resolved project definitions: ActionChecks5, ActionPhaseChecks5, DiscardPhaseChecks5, DrawPhaseChecks5, GeneralTurnChecks5, SideAProcedureChecks5, SideBProcedureChecks5, block5
DiscardPhaseChecks5 · operator
reference-profile · input revision 2 · CC0 1.0
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"})})Exact module download · Source bundle and reproduction instructions
Resolved project definitions: ZeroBegunCounts5, DiscardBatchEvent5, DiscardStep5, DiscardStepId5, MaximumHandSize5, OpenTurn5, PersistentCapacityLossAccrual5
DrawPhaseChecks5 · operator
reference-profile · input revision 2 · CC0 1.0
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.actionExact module download · Source bundle and reproduction instructions
Resolved project definitions: ZeroBegunCounts5, HasDrawPhase5, MandatoryDrawEvent5, OpenTurn5, TurnPhases5, UnmodifiedMandatoryDraw5
GeneralTurnChecks5 · operator
reference-profile · input revision 2 · CC0 1.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"])Exact module download · Source bundle and reproduction instructions
Resolved project definitions: ZeroBegunCounts5, DuringPlayersTurn5, NoBetweenTurns5, OpenTurn5, TurnActivePlayer5, TurnBeginEvent5, TurnEndEvents5, TurnFirstPriority5, TurnFormalBegin5, TurnFormalEnd5, TurnFrameValid5, TurnHandoff5, TurnPhaseAdvance5, TurnPhases5
Init5 · operator
reference-profile · input revision 2 · CC0 1.0
Init5 == block5 \in 1..7Exact module download · Source bundle and reproduction instructions
Resolved project definitions: block5
Next5 · operator
reference-profile · input revision 2 · CC0 1.0
Next5 == UNCHANGED block5Exact module download · Source bundle and reproduction instructions
Resolved project definitions: block5
SideAProcedureChecks5 · operator
reference-profile · input revision 2 · CC0 1.0
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.formalBegunExact module download · Source bundle and reproduction instructions
Resolved project definitions: ZeroBegunCounts5, ActionPhaseEndEvent5, LoseUnspentActionPoints5, OpenSideAProcedure5, OpenTurn5, RecurringRefill5, SideAActionPhaseEndAtStep5, SideAAllotmentAtStep5, SideADefaultAllotment5, SideAFormalBeginAtStep5, SideAFormalEndAtStep5, SideALatchDecision5, SideALoseActionPointsAtStep5, SideANextStep5, SideAProcedureValid5, SideARefillAtStep5, SideAStepAdvance5, SideAStepInfo5, SideASteps5, TurnBeginEvent5, TurnEndEvents5
SideBProcedureChecks5 · operator
reference-profile · input revision 2 · CC0 1.0
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.formalBegunExact module download · Source bundle and reproduction instructions
Resolved project definitions: SetupRange, ZeroBegunCounts5, ActionPhaseEndEvent5, OpenSideBProcedure5, OpenTurn5, SideBActionPhaseEndAtStep5, SideBAllotmentAtStep5, SideBDefaultAllotment5, SideBFormalBeginAtStep5, SideBFormalEndAtStep5, SideBLatchDecision5, SideBLoseActionPointsAtStep5, SideBNextStep5, SideBProcedureValid5, SideBRefillAtStep5, SideBStepAdvance5, SideBStepInfo5, SideBSteps5, TurnBeginEvent5, TurnEndEvents5
Spec5 · operator
reference-profile · input revision 2 · CC0 1.0
Spec5 == Init5 /\ [][Next5]_block5Exact module download · Source bundle and reproduction instructions
ZeroBegunCounts5 · operator
reference-profile · input revision 2 · CC0 1.0
ZeroBegunCounts5 == [p \in SetupPlayers |-> 0]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: SetupPlayers
block5 · variable
reference-profile · input revision 2 · CC0 1.0
block5Exact module download · Source bundle and reproduction instructions