-------------------------- MODULE SchedulerChecksMC -------------------------- EXTENDS AbilityContracts, SchedulerOracle EmptyT11 == [id \in {} |-> id] ZeroCountsT11 == [p \in SetupPlayers |-> 0] SideAInitialT11 == OpenSideAProcedure5(OpenTurn5("SideA",1,ZeroCountsT11)) SourcePositionT11(step) == CHOOSE i \in 1..Len(SideAOracleSteps11) : SideAOracleSteps11[i]=step 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")] 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]} DestinationT11(f) == IF f.turn.owner="SideB" THEN <<"HandoffToSideB","DeferredSideBPhase">> ELSE <> ActualSideADestinationsT11(f,workComplete) == {DestinationT11(after) : after \in {g \in SideACandidateFramesT11(f) : SideAStepAdvance5(f,g,workComplete)}} ExpectedSideADestinationsT11(step,decision) == {IF e.after="HandoffToSideB" THEN <> ELSE <> : e \in {e \in SideAOracleEdges11 : e.before=step /\ e.decision=decision}} 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== <> \o edge.via \o <> 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 <> ELSE <>) \in ActualSideADestinationsT11(PreparedSideAT11(path[i],d),TRUE) /\ \A i \in 1..Len(edge.via) : edge.via[i] \in SideAOracleHidden11 SideASiteT11(f,actionPoints) == TurnPrioritySite9(f.turn,f.step,100,actionPoints,f) 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] WindowT11(f,id) == NewPriorityWindow9(id,"Paid",SideASiteT11(f,1),EmptyT11,0,NoTimingRef9,[id |-> 0],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] PriorityReadyT11(w) == [w EXCEPT !.stage="Ready",!.checkpoint=PriorityCheckpointT11(w).id] 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]] OptionT11(kind,actor,target) == PriorityOption9(20,kind,actor,0,0,RuleAbilitySource9("AuditOption"),target,{}) LegalityT11(w,option) == [tag |-> "PriorityOptionLegality",windowId |-> w.id,reception |-> w.reception,option |-> option,legal |-> TRUE,active |-> TRUE,transactionId |-> 200,costsPayable |-> TRUE] ActualOptionT11(w,kind,actor,target) == LET option==OptionT11(kind,actor,target) IN BeginPriorityOption9(<>,<>,option,TestObjectsT11,LegalityT11(w,option),[id |-> 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(<<>>,<>,1,"Paid",w.site,EmptyT11,OpeningT11(f,1),{}) /\ CheckpointPriority9(<>,<>,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(<>,<>,[PriorityCheckpointT11(w) EXCEPT !.reactionsDrained=FALSE]) /\ ~CheckpointPriority9(<>,<>,[PriorityCheckpointT11(w) EXCEPT !.windowId=99]) /\ PassPriority9(<>,<>,"SideA",[id |-> 0]) /\ CheckpointPriority9(<>,<>,PriorityCheckpointT11(passed)) /\ PassPriority9(<>,<>,"SideB",[id |-> 0]) /\ ~WindowSiteAllowed9("Paid",[w.site EXCEPT !.timingLive=FALSE])) /\ ~WindowSiteAllowed9("NeutralValue00001",SideASiteT11(PreparedSideAT11("ProcedureCode0e20572a4bab","NoValue"),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) SideBInitialT11 == OpenSideBProcedure5(OpenTurn5("SideB",2,[SideA |-> 1,SideB |-> 0])) SideBPositionT11(step) == CHOOSE i \in 1..Len(SideBOracleSteps11) : SideBOracleSteps11[i]=step 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")] 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]} SideBDestinationT11(f) == IF f.turn.owner="SideA" THEN <<"HandoffToSideA","DeferredSideAPhase">> ELSE <> ActualSideBDestinationsT11(f,workComplete) == {SideBDestinationT11(after) : after \in {g \in SideBCandidateFramesT11(f) : SideBStepAdvance5(f,g,workComplete)}} ExpectedSideBDestinationsT11(step,decision) == {IF e.after="HandoffToSideA" THEN <> ELSE <> : e \in {e \in SideBOracleEdges11 : e.before=step /\ e.decision=decision}} 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== <> \o edge.via \o <> 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 <> ELSE <>) \in ActualSideBDestinationsT11(PreparedSideBT11(path[i],d),TRUE) /\ \A i \in 1..Len(edge.via) : edge.via[i] \in SideBOracleHidden11 SideBSiteT11(f,actionPoints) == TurnPrioritySite9(f.turn,f.step,200,actionPoints,f) 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] SideBWindowT11(f,id) == NewPriorityWindow9(id,"Paid",SideBSiteT11(f,1),EmptyT11,0,NoTimingRef9,[id |-> 0],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(<<>>,<>,1,"Paid",w.site,EmptyT11,SideBOpeningT11(f,1),{}) /\ CheckpointPriority9(<>,<>,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(<>,<>,[PriorityCheckpointT11(w) EXCEPT !.player="SideA"]) /\ ~CheckpointPriority9(<>,<>,[PriorityCheckpointT11(w) EXCEPT !.reception=99]) /\ ~CheckpointPriority9(<>,<>,[PriorityCheckpointT11(w) EXCEPT !.windowId=99]) /\ ~CheckpointPriority9(<>,<>,[PriorityCheckpointT11(w) EXCEPT !.complete=FALSE]) /\ ~CheckpointPriority9(<>,<>,[PriorityCheckpointT11(w) EXCEPT !.reactionsDrained=FALSE]) /\ PassPriority9(<>,<>,"SideB",[id |-> 0]) /\ CheckpointPriority9(<>,<>,PriorityCheckpointT11(passed)) /\ PassPriority9(<>,<>,"SideA",[id |-> 0]) /\ ~WindowSiteAllowed9("Paid",[w.site EXCEPT !.timingLive=FALSE])) /\ ~WindowSiteAllowed9("NeutralValue00001",SideBSiteT11(PreparedSideBT11("ProcedureCode989abc27e0c6","NoValue"),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))={} VARIABLES guideCaseT11, qT11 PointwiseInitT11 == guideCaseT11 \in 1..6 /\ qT11=EmptyT11 PointwiseNextT11 == UNCHANGED <> PointwiseSpecT11 == PointwiseInitT11 /\ [][PointwiseNextT11]_<> PointwiseChecksT11 == CASE guideCaseT11=1 -> SideAEntryAndGraphChecksT11 [] guideCaseT11=2 -> SideAWindowChecksT11 [] guideCaseT11=3 -> SideAEffectAndBarrierChecksT11 [] guideCaseT11=4 -> SideBEntryAndGraphChecksT11 [] guideCaseT11=5 -> SideBWindowChecksT11 [] OTHER -> SideBEffectAndBarrierChecksT11 IdleActionT11 == [NewAction5(0,"SideA",BasicActionKey5("SideA","GainResourceUnit")) EXCEPT !.status="Idle"] SideAAuditDoneT11 == qT11.flow.turn.owner="SideB" 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 |-> <<>>] 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])] 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 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(<<>>,<>,id,"Paid",site,EmptyT11,opening,qT11.usedWindows) /\ qT11'=[qT11 EXCEPT !.stack= <>,!.nextWindow=@+1,!.usedWindows=@ \cup {id}] SideAAuditWindowStepT11 == /\ ~SideAAuditDoneT11 /\ ~qT11.ready /\ Len(qT11.stack)=1 /\ LET w==WindowTop9(qT11.stack) IN \/ /\ w.stage="NeedCheckpoint" /\ CheckpointPriority9(qT11.stack,<>,PriorityCheckpointT11(w)) /\ qT11'=[qT11 EXCEPT !.stack= <>] \/ /\ w.stage="Ready" /\ PassPriority9(qT11.stack,<>,w.priority,[id |-> 0]) /\ qT11'=[qT11 EXCEPT !.stack= <>] \/ /\ w.stage="Closed" /\ PopClosedPriorityWindow9(qT11.stack,<<>>) /\ qT11'=RecordWorkT11(qT11,[qT11 EXCEPT !.stack= <<>>,!.windows=Append(@,qT11.flow.step),!.actionWindowReady=qT11.flow.step="ProcedureCoded6fbcb09dd4f"],{}) 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 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] ChildNameT11(id) == CASE id=1 -> "Child1" [] id=2 -> "Child2" [] OTHER -> "Child3" 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"],{}) 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])] SideAAuditNextT11 == /\ UNCHANGED guideCaseT11 /\ (SideAAuditWorkT11 \/ SideAAuditWindowOpenT11 \/ SideAAuditWindowStepT11 \/ SideAAuditLatchT11 \/ SideAAuditActionStartT11 \/ SideAAuditActionBodyT11 \/ SideAAuditAdvanceT11 \/ (SideAAuditDoneT11 /\ UNCHANGED qT11)) SideAAuditSpecT11 == SideAAuditInitT11 /\ [][SideAAuditNextT11]_<> /\ WF_<>(SideAAuditNextT11) 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"}} 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") SideAAuditEventuallyHandoffT11 == <>SideAAuditDoneT11 SideBIdleActionT11 == [NewAction5(0,"SideB",BasicActionKey5("SideB","GainResourceUnit")) EXCEPT !.status="Idle"] SideBAuditDoneT11 == qT11.flow.turn.owner="SideA" 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 |-> <<>>] 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])] 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 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(<<>>,<>,id,"Paid",site,EmptyT11,opening,qT11.usedWindows) /\ qT11'=[qT11 EXCEPT !.stack= <>,!.nextWindow=@+1,!.usedWindows=@ \cup {id}] SideBAuditWindowStepT11 == /\ ~SideBAuditDoneT11 /\ ~qT11.ready /\ Len(qT11.stack)=1 /\ LET w==WindowTop9(qT11.stack) IN \/ /\ w.stage="NeedCheckpoint" /\ CheckpointPriority9(qT11.stack,<>,PriorityCheckpointT11(w)) /\ qT11'=[qT11 EXCEPT !.stack= <>] \/ /\ w.stage="Ready" /\ PassPriority9(qT11.stack,<>,w.priority,[id |-> 0]) /\ qT11'=[qT11 EXCEPT !.stack= <>] \/ /\ w.stage="Closed" /\ PopClosedPriorityWindow9(qT11.stack,<<>>) /\ qT11'=SideBRecordWorkT11(qT11,[qT11 EXCEPT !.stack= <<>>,!.windows=Append(@,qT11.flow.step),!.actionWindowReady=qT11.flow.step="ProcedureCode484be3e50aa9"],{}) 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 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] SideBChildNameT11(id) == CASE id=1 -> "Child1" [] id=2 -> "Child2" [] id=3 -> "Child3" [] OTHER -> "Child4" 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"],{}) 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])] SideBAuditNextT11 == /\ UNCHANGED guideCaseT11 /\ (SideBAuditWorkT11 \/ SideBAuditWindowOpenT11 \/ SideBAuditWindowStepT11 \/ SideBAuditLatchT11 \/ SideBAuditActionStartT11 \/ SideBAuditActionBodyT11 \/ SideBAuditAdvanceT11 \/ (SideBAuditDoneT11 /\ UNCHANGED qT11)) SideBAuditSpecT11 == SideBAuditInitT11 /\ [][SideBAuditNextT11]_<> /\ WF_<>(SideBAuditNextT11) 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"}} 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") SideBAuditEventuallyHandoffT11 == <>SideBAuditDoneT11 =============================================================================