----------------------------- MODULE InspectionContracts ----------------------------- EXTENDS TraversalContracts OpenItemInspection7(id,object,card,traversalId,siteInspectionId,caller,encounterAncestors) == [id |-> id,object |-> object,originLoc |-> card.loc,sourceZone |-> card.zone, traversalId |-> traversalId,siteInspectionId |-> siteInspectionId,caller |-> caller,encounterAncestors |-> encounterAncestors, step |-> "ProcedureCodefd91bef8bbd3",active |-> FALSE,beginMet |-> FALSE,complete |-> FALSE,returned |-> FALSE, midUsed |-> FALSE,midDone |-> FALSE,midResolving |-> FALSE, claimObjectiveDone |-> FALSE,claimObjectiveResolving |-> FALSE,completionReason |-> "NoValue"] ItemInspectionTargetPresent7(a,objects) == IF a.object \notin DOMAIN objects THEN FALSE ELSE objects[a.object].form = "Card" /\ objects[a.object].side = "SideA" /\ objects[a.object].loc = a.originLoc StillItemInspectioning7(a,objects) == a.active /\ ~a.complete /\ ItemInspectionTargetPresent7(a,objects) ItemInspectionFrameValid7(a) == /\ a.id \in Nat \ {0} /\ a.encounterAncestors \subseteq Nat \ {0} /\ a.active \in BOOLEAN /\ a.complete \in BOOLEAN /\ a.beginMet \in BOOLEAN /\ a.active => a.beginMet /\ ~a.complete /\ a.complete => ~a.active /\ a.midResolving => a.midUsed /\ ~a.midDone /\ a.claimObjectiveResolving => ~a.claimObjectiveDone ItemInspectionLookGrant7(a,objects,player) == StillItemInspectioning7(a,objects) /\ (player = "SideB" \/ (player = "SideA" /\ a.sourceZone # "SideADeck")) ItemInspectionViewers7(a,objects,otherLawfulViewers,actualRevealToBoth) == otherLawfulViewers \cup {p \in SetupPlayers : ItemInspectionLookGrant7(a,objects,p)} \cup (IF StillItemInspectioning7(a,objects) /\ actualRevealToBoth THEN SetupPlayers ELSE {}) ItemInspectionAbilityActive7(normallyActive,ability) == normallyActive \/ (ability.kind = "Conditional" /\ ability.trigger = "SourceItemInspectioned") ItemInspectionAbilityMatches7(ability,event) == ability.kind = "Conditional" /\ ability.trigger = "SourceItemInspectioned" /\ event.tag = "ItemInspectionCard" /\ ability.source = event.object ExampleFamily034Trigger7(actualAbilityActive,hasRetireCost,earlierCostItemInspectionesThisTurn) == actualAbilityActive /\ hasRetireCost /\ earlierCostItemInspectionesThisTurn = 0 ExampleFamily034Reveal7(beforeReveals,afterReveals,a,objects,abilityId,actualTriggeredInstanceResolving,events) == /\ StillItemInspectioning7(a,objects) /\ actualTriggeredInstanceResolving /\ abilityId \in Nat \ {0} /\ afterReveals = beforeReveals \cup {[object |-> a.object,loc |-> a.originLoc,viewers |-> SetupPlayers,ability |-> abilityId]} /\ events = {[tag |-> "Reveal",object |-> a.object,ability |-> abilityId]} MidOption7(id,trashesItemInspectioned,canPay,legal) == [id |-> id,timing |-> "MidItemInspection",trashesItemInspectioned |-> trashesItemInspectioned,canPay |-> canPay,legal |-> legal] BasicRetireOption7(card,effectiveRetirePart,actualAllCostsPayable,actualBasicRetireAllowed) == MidOption7("BasicRetire",TRUE,actualAllCostsPayable, ItemInspectionRetireCostOpportunity("SideB",card,TRUE,effectiveRetirePart) /\ actualBasicRetireAllowed) MidOptionsValid7(cardOptions) == /\ \A o \in cardOptions : o.id \notin {"BasicRetire","Decline"} /\ Cardinality({o.id : o \in cardOptions}) = Cardinality(cardOptions) ItemInspectionMidOptions7(card,cardOptions,trashPart,basicPayable,basicAllowed) == {o \in cardOptions \cup {BasicRetireOption7(card,trashPart,basicPayable,basicAllowed)} : o.timing = "MidItemInspection" /\ (card.zone # "SideADiscard" \/ ~o.trashesItemInspectioned)} PayableMidOptions7(options) == {o \in options : o.legal /\ o.canPay} MidItemInspectionChoiceAllowed7(choice,options,mustRetireIfAble,exampleFamily034Applies) == LET payable == PayableMidOptions7(options) basicPayable == \E o \in payable : o.id = "BasicRetire" trashPayable == \E o \in payable : o.trashesItemInspectioned IN /\ choice = "Decline" \/ \E o \in payable : o.id = choice /\ (exampleFamily034Applies /\ basicPayable) => choice = "BasicRetire" /\ (mustRetireIfAble /\ trashPayable) => choice # "Decline" /\ \E o \in payable : o.id = choice /\ o.trashesItemInspectioned UseMidItemInspection7(before,after,objects,option,options,mustRetireIfAble,exampleFamily034Applies, actualAllCostsPaid,beginReactionsAndCheckpointDrained) == /\ StillItemInspectioning7(before,objects) /\ before.step = "ProcedureCode1dd0e8f05be2" /\ ~before.midUsed /\ ~before.midDone /\ ~before.midResolving /\ beginReactionsAndCheckpointDrained /\ actualAllCostsPaid /\ option \in PayableMidOptions7(options) /\ option.timing = "MidItemInspection" /\ objects[before.object].zone # "SideADiscard" \/ ~option.trashesItemInspectioned /\ MidItemInspectionChoiceAllowed7(option.id,options,mustRetireIfAble,exampleFamily034Applies) /\ after = [before EXCEPT !.midUsed = TRUE,!.midResolving = TRUE] DeclineMidItemInspection7(before,after,objects,options,mustRetireIfAble,exampleFamily034Applies,beginReactionsAndCheckpointDrained) == /\ StillItemInspectioning7(before,objects) /\ before.step = "ProcedureCode1dd0e8f05be2" /\ ~before.midUsed /\ ~before.midDone /\ ~before.midResolving /\ beginReactionsAndCheckpointDrained /\ MidItemInspectionChoiceAllowed7("Decline",options,mustRetireIfAble,exampleFamily034Applies) /\ after = [before EXCEPT !.midDone = TRUE] FinishMidItemInspection7(before,after,actualAbilityAndReactionsComplete) == /\ before.midResolving /\ actualAbilityAndReactionsComplete /\ after = [before EXCEPT !.midResolving = FALSE,!.midDone = TRUE] ItemInspectionClaimObjectiveDisposition7(card,hasAdditionalCost,acceptsAdditionalCost,allAdditionalCostsPayable,actualClaimObjectiveAllowed) == IF card.kind # "Objective" THEN "NotObjective" ELSE IF hasAdditionalCost /\ ~acceptsAdditionalCost THEN "DeclineAdditional" ELSE IF (hasAdditionalCost /\ ~allAdditionalCostsPayable) \/ ~actualClaimObjectiveAllowed THEN "Unable" ELSE "ClaimObjective" ResolveItemInspectionClaimObjective7(before,after,objects,hasAdditionalCost,acceptsAdditionalCost, allAdditionalCostsPayable,actualClaimObjectiveAllowed,allClaimObjectiveCostsPaid,actualCostCheckpointDrained) == /\ StillItemInspectioning7(before,objects) /\ before.step = "ProcedureCode546db7cc4546" /\ before.midDone /\ ~before.midResolving /\ ~before.claimObjectiveResolving /\ ~before.claimObjectiveDone /\ LET result == ItemInspectionClaimObjectiveDisposition7(objects[before.object],hasAdditionalCost,acceptsAdditionalCost, allAdditionalCostsPayable,actualClaimObjectiveAllowed) IN IF result = "ClaimObjective" THEN /\ allClaimObjectiveCostsPaid /\ (hasAdditionalCost => actualCostCheckpointDrained) /\ after = [before EXCEPT !.claimObjectiveResolving = TRUE] ELSE after = [before EXCEPT !.claimObjectiveDone = TRUE] FinishItemInspectionClaimObjective7(before,after,actualClaimObjectiveProcedureAndReactionsComplete) == /\ before.claimObjectiveResolving /\ actualClaimObjectiveProcedureAndReactionsComplete /\ after = [before EXCEPT !.claimObjectiveResolving = FALSE,!.claimObjectiveDone = TRUE] ItemInspectionEndEvent7(a) == [tag |-> "ItemInspectionEnds",itemInspectionId |-> a.id,object |-> a.object] EndItemInspection7(before,after,reason,actualEndAuthorized,events) == /\ before.active /\ ~before.complete /\ actualEndAuthorized /\ reason \in {"Moved","EndTraversal","Normal"} /\ after = [before EXCEPT !.active = FALSE,!.complete = TRUE,!.step = "Complete",!.completionReason = reason] /\ events = {ItemInspectionEndEvent7(before)} ItemInspectionMovementOutcome7(before,after,objectsAfter,actualMovementResolved,events) == /\ actualMovementResolved /\ IF before.active /\ ~ItemInspectionTargetPresent7(before,objectsAfter) THEN EndItemInspection7(before,after,"Moved",TRUE,events) ELSE after = before /\ events = {} ApplyItemInspectionAborts7(before,after,actualAbortedItemInspectionIds,events) == IF before.active /\ before.id \in actualAbortedItemInspectionIds THEN EndItemInspection7(before,after,"EndTraversal",TRUE,events) ELSE after = before /\ events = {} InformationSiftingOrder7(targets,order) == SubIds6(order) = targets /\ Cardinality(targets) = Len(order) InformationSiftingPlan7(targets,order,instructions,usedInstructionIds) == /\ InformationSiftingOrder7(targets,order) /\ Len(instructions) = Len(order) /\ Cardinality({instructions[i].id : i \in 1..Len(instructions)}) = Len(instructions) /\ \A i \in 1..Len(instructions) : instructions[i].id \in Nat \ {0} /\ instructions[i].id \notin usedInstructionIds /\ instructions[i].kind = "ItemInspection" /\ instructions[i].target = order[i] InformationSiftingNext7(beforeIndex,afterIndex,instructions,actualPreviousInstructionAndChildItemInspectionComplete, normalInstructionCheckpointAndReactionsDrained) == /\ beforeIndex \in 1..Len(instructions) /\ actualPreviousInstructionAndChildItemInspectionComplete /\ normalInstructionCheckpointAndReactionsDrained /\ afterIndex = beforeIndex+1 InspectionPolicy7(mode,targetCount) == [randomLimitEnabled |-> mode # "CounterExampleFamily064",chosenCapEnabled |-> mode = "CounterExampleFamily064",chosenCap |-> targetCount] SelectionWithinPolicy7(policy,chosenCount) == chosenCount \in Nat /\ (~policy.chosenCapEnabled \/ chosenCount < policy.chosenCap) InspectionPolicyComplete7(policy,chosenCount,candidatesEmpty) == candidatesEmpty \/ (policy.chosenCapEnabled /\ chosenCount >= policy.chosenCap) ItemInspectionSteps7 == {"ProcedureCodefd91bef8bbd3","ProcedureCode1dd0e8f05be2","ProcedureCode546db7cc4546","ProcedureCode662478499367"} ItemInspectionStepInfo7(step) == [kind |-> CASE step = "ProcedureCodefd91bef8bbd3" -> "ItemInspectionCard" [] step = "ProcedureCode1dd0e8f05be2" -> "MidItemInspection" [] step = "ProcedureCode546db7cc4546" -> "ClaimObjective" [] step = "ProcedureCode662478499367" -> "CompleteItemInspection" [] OTHER -> "Invalid", paidWindow |-> FALSE,objectivePlacementWindow |-> FALSE] NextItemInspectionStep7(step) == CASE step = "ProcedureCodefd91bef8bbd3" -> "ProcedureCode1dd0e8f05be2" [] step = "ProcedureCode1dd0e8f05be2" -> "ProcedureCode546db7cc4546" [] step = "ProcedureCode546db7cc4546" -> "ProcedureCode662478499367" [] step = "ProcedureCode662478499367" -> "Complete" [] OTHER -> "NoValue" ItemInspectionBeginEvent7(a) == [tag |-> "ItemInspectionCard",itemInspectionId |-> a.id,object |-> a.object,traversalId |-> a.traversalId,siteInspectionId |-> a.siteInspectionId] BeginItemInspection7(before,after,objects,actualItemInspectionAndNewTimingAllowed,allItemInspectionCostsPaid, actualCostCheckpointAndReactionsDrained,events) == /\ before.step = "ProcedureCodefd91bef8bbd3" /\ ~before.active /\ ~before.beginMet /\ ~before.complete /\ before.id \in Nat \ {0} /\ ItemInspectionTargetPresent7(before,objects) /\ actualItemInspectionAndNewTimingAllowed /\ allItemInspectionCostsPaid /\ actualCostCheckpointAndReactionsDrained /\ after = [before EXCEPT !.active = TRUE,!.beginMet = TRUE] /\ events = {ItemInspectionBeginEvent7(before)} CancelUnstartedItemInspection7(before,after,reason,actualInstructionWithoutItemInspectionCompleted,events) == /\ before.step = "ProcedureCodefd91bef8bbd3" /\ ~before.active /\ ~before.beginMet /\ ~before.complete /\ actualInstructionWithoutItemInspectionCompleted /\ reason \in {"Replaced","ItemInspectionCostDeclined","Prohibited","MissingTarget","Cancelled"} /\ after = [before EXCEPT !.complete = TRUE,!.step = "Complete",!.completionReason = reason] /\ events = {} AdvanceItemInspectionStep7(before,after,objects,actualStepAndChildProceduresComplete,normalCheckpointAndReactionsDrained) == /\ StillItemInspectioning7(before,objects) /\ before.step \in {"ProcedureCodefd91bef8bbd3","ProcedureCode1dd0e8f05be2","ProcedureCode546db7cc4546"} /\ actualStepAndChildProceduresComplete /\ normalCheckpointAndReactionsDrained /\ CASE before.step = "ProcedureCodefd91bef8bbd3" -> before.beginMet [] before.step = "ProcedureCode1dd0e8f05be2" -> before.midDone /\ ~before.midResolving [] OTHER -> before.claimObjectiveDone /\ ~before.claimObjectiveResolving /\ after = [before EXCEPT !.step = NextItemInspectionStep7(before.step)] CompleteNormalItemInspection7(before,after,objects,allStepThreeReactionsAndCheckpointComplete,events) == /\ StillItemInspectioning7(before,objects) /\ before.step = "ProcedureCode662478499367" /\ before.beginMet /\ before.midDone /\ before.claimObjectiveDone /\ ~before.midResolving /\ ~before.claimObjectiveResolving /\ allStepThreeReactionsAndCheckpointComplete /\ EndItemInspection7(before,after,"Normal",TRUE,events) CloseEndedItemInspectionBeginReaction7(before,after,a) == /\ a.complete /\ a.beginMet /\ before.open /\ before.kind = "Reaction" /\ before.beginItemInspectionId = a.id /\ after = [before EXCEPT !.open = FALSE,!.pending = {},!.priority = "NoValue", !.lostPending = @ \cup before.pending] ReturnItemInspectionToCaller7(before,after,actualItemInspectionEndWindowsAndCheckpointComplete,caller) == /\ before.complete /\ ~before.returned /\ ~before.midResolving /\ ~before.claimObjectiveResolving /\ actualItemInspectionEndWindowsAndCheckpointComplete /\ caller = before.caller /\ after = [before EXCEPT !.returned = TRUE] ItemInspectionProcedureValid7(a,objects) == /\ ItemInspectionFrameValid7(a) /\ IF a.complete THEN a.step = "Complete" ELSE IF a.active THEN a.step \in ItemInspectionSteps7 /\ ItemInspectionTargetPresent7(a,objects) ELSE a.step = "ProcedureCodefd91bef8bbd3" /\ ~a.beginMet InspectionTargetSiteCategory7(targetSite) == IF targetSite \in CentralTargetSites4 THEN targetSite ELSE "SchemaAtom132" OpenInspection7(id,targetSite,kind,traversalId,origin,caller,encounterAncestors,policy) == [id |-> id,targetSite |-> targetSite,kind |-> kind,traversalId |-> traversalId,origin |-> origin,caller |-> caller, encounterAncestors |-> encounterAncestors,policy |-> policy,step |-> "ProcedureCode839b301bad95", active |-> FALSE,beginMet |-> FALSE,complete |-> FALSE,returned |-> FALSE, archivesPrepared |-> FALSE,randomLimit |-> 1,limitSet |-> FALSE, choices |-> <<>>,selectionPending |-> FALSE,selectedObject |-> 0,selectedSource |-> "NoValue", currentItemInspectionId |-> 0,usedItemInspectionIds |-> {},completionReason |-> "NoValue"] InspectionChoiceObjects7(b) == {b.choices[i].object : i \in 1..Len(b.choices)} InspectionCentralChoices7(b) == Cardinality({i \in 1..Len(b.choices) : b.choices[i].source = "SchemaAtom033"}) RandomLimitApplies7(b) == b.kind \in {"SchemaAtom082","SchemaAtom129"} /\ b.policy.randomLimitEnabled AddAdditionalItemInspectiones7(before,after,amount,actualBeginningAbilityApplies) == /\ before.active /\ ~before.complete /\ ~before.limitSet /\ RandomLimitApplies7(before) /\ before.step \in {"ProcedureCode839b301bad95","ProcedureCodeb6067693902e","ProcedureCode91f3ee0da236"} /\ amount \in Nat /\ actualBeginningAbilityApplies /\ after = [before EXCEPT !.randomLimit = @+amount] FreezeInspectionLimit7(before,after,allBeginningModifiersAndReactionsComplete) == /\ before.active /\ ~before.complete /\ before.step = "ProcedureCode91f3ee0da236" /\ ~before.limitSet /\ RandomLimitApplies7(before) /\ before.randomLimit \in Nat /\ allBeginningModifiersAndReactionsComplete /\ after = [before EXCEPT !.limitSet = TRUE] PrepareDiscardSite7(before,after,objects,afterObjects) == /\ before.active /\ ~before.complete /\ before.kind = "SchemaAtom018" /\ before.step = "ProcedureCodeb6067693902e" /\ ~before.archivesPrepared /\ after = [before EXCEPT !.archivesPrepared = TRUE] /\ afterObjects = [id \in DOMAIN objects |-> IF objects[id].form = "Card" /\ objects[id].side = "SideA" /\ objects[id].zone = "SideADiscard" THEN [objects[id] EXCEPT !.face = "Up"] ELSE objects[id]] InspectionSelectionReady7(b) == b.active /\ ~b.complete /\ b.step = "ProcedureCode1404a82ab3ee" /\ ~b.selectionPending /\ b.currentItemInspectionId = 0 /\ (RandomLimitApplies7(b) => b.limitSet) /\ (b.kind = "SchemaAtom018" => b.archivesPrepared) /\ SelectionWithinPolicy7(b.policy,Len(b.choices)) CandidateViewValid7(view) == view.roots \cap view.central = {} InspectionPresentation7(b,view) == [specific |-> view.roots \cup (IF b.kind = "SchemaAtom082" THEN {} ELSE view.central), randomCentralAOffered |-> b.kind = "SchemaAtom082" /\ view.central # {}] RecordInspectionChoice7(before,after,object,source,view,method,actualSelectionAuthority) == /\ InspectionSelectionReady7(before) /\ CandidateViewValid7(view) /\ actualSelectionAuthority /\ object # 0 /\ object \notin InspectionChoiceObjects7(before) /\ source \in {"Root","SchemaAtom033"} /\ object \in (IF source = "Root" THEN view.roots ELSE view.central) /\ (source = "SchemaAtom033" /\ RandomLimitApplies7(before)) => InspectionCentralChoices7(before) < before.randomLimit /\ IF source = "SchemaAtom033" /\ before.kind = "SchemaAtom082" THEN method \in {"RandomCentralA","SideADirectedCentralA"} ELSE method = "Specific" /\ after = [before EXCEPT !.choices = Append(@,[object |-> object,source |-> source,chooser |-> "SideB"]), !.selectionPending = TRUE,!.selectedObject = object,!.selectedSource = source] ChooseSpecificInspectionCard7(before,after,object,view) == /\ object \in InspectionPresentation7(before,view).specific /\ RecordInspectionChoice7(before,after,object,IF object \in view.roots THEN "Root" ELSE "SchemaAtom033",view,"Specific",TRUE) ChooseCentralAInspectionCard7(before,after,view,randomResult,sideAChoice,dedicatedNeuralNetApplies,actualRandomDrawValid) == /\ before.kind = "SchemaAtom082" /\ LET object == IF dedicatedNeuralNetApplies THEN sideAChoice ELSE randomResult IN RecordInspectionChoice7(before,after,object,"SchemaAtom033",view, IF dedicatedNeuralNetApplies THEN "SideADirectedCentralA" ELSE "RandomCentralA", dedicatedNeuralNetApplies \/ actualRandomDrawValid) InspectionItemInspectionCaller7(b) == <<"InspectionItemInspection",b.id>> AttachChosenItemInspection7(before,after,a,actualItemInspectionBeginEvent) == /\ before.active /\ ~before.complete /\ before.step = "ProcedureCodee35e7c8fc57b" /\ before.selectionPending /\ before.currentItemInspectionId = 0 /\ a.beginMet /\ a.id \in Nat \ {0} /\ a.id \notin before.usedItemInspectionIds /\ a.object = before.selectedObject /\ a.siteInspectionId = before.id /\ a.caller = InspectionItemInspectionCaller7(before) /\ actualItemInspectionBeginEvent = ItemInspectionBeginEvent7(a) /\ after = [before EXCEPT !.currentItemInspectionId = a.id,!.usedItemInspectionIds = @ \cup {a.id}] FinishInspectionItemInspectionInstruction7(before,after,actualChosenInstructionAndItemInspectionReturnComplete) == /\ before.active /\ ~before.complete /\ before.step = "ProcedureCodee35e7c8fc57b" /\ before.selectionPending /\ actualChosenInstructionAndItemInspectionReturnComplete /\ after = [before EXCEPT !.selectionPending = FALSE,!.selectedObject = 0, !.selectedSource = "NoValue",!.currentItemInspectionId = 0] RecordActualItemInspection7(beforeHistory,afterHistory,a,turnId,hadRetireCostAtStart,actualItemInspectionBeginEvent) == /\ a.beginMet /\ a.id \in Nat \ {0} /\ a.id \notin DOMAIN beforeHistory /\ turnId \in Nat /\ actualItemInspectionBeginEvent = ItemInspectionBeginEvent7(a) /\ afterHistory = [id \in DOMAIN beforeHistory \cup {a.id} |-> IF id = a.id THEN [object |-> a.object,traversalId |-> a.traversalId,siteInspectionId |-> a.siteInspectionId, turnId |-> turnId,hadRetireCost |-> hadRetireCostAtStart] ELSE beforeHistory[id]] ActualItemInspectionesInTraversal7(history,traversalId) == IF traversalId = 0 THEN {} ELSE {id \in DOMAIN history : history[id].traversalId = traversalId} ActualItemInspectionesInInspection7(history,siteInspectionId) == IF siteInspectionId = 0 THEN {} ELSE {id \in DOMAIN history : history[id].siteInspectionId = siteInspectionId} InspectionSeenObjects7(b,history) == {history[id].object : id \in ActualItemInspectionesInInspection7(history,b.id)} InspectionObjectVisible7(b,history,objects,object) == b.active /\ ~b.complete /\ object \in DOMAIN objects /\ object \in InspectionSeenObjects7(b,history) ItemInspectionHistoryCostCount7(history,turnId) == Cardinality({id \in DOMAIN history : history[id].turnId = turnId /\ history[id].hadRetireCost}) InspectionEndEvent7(b) == [tag |-> "InspectionEnds",siteInspectionId |-> b.id,targetSite |-> b.targetSite] EndInspection7(before,after,reason,actualEndAuthorized,events) == /\ before.active /\ ~before.complete /\ actualEndAuthorized /\ reason \in {"Normal","EndTraversal"} /\ after = [before EXCEPT !.active = FALSE,!.complete = TRUE,!.step = "Complete",!.completionReason = reason] /\ events = {InspectionEndEvent7(before)} ApplyInspectionAborts7(before,after,actualAbortedInspectionIds,events) == IF before.active /\ before.id \in actualAbortedInspectionIds THEN EndInspection7(before,after,"EndTraversal",TRUE,events) ELSE after = before /\ events = {} DelayInspection7(before,after,conditionId,usedConditionIds,currentInspectionId,request,actualInspectionWouldBegin) == /\ currentInspectionId \in Nat \ {0} /\ actualInspectionWouldBegin /\ conditionId \in Nat \ {0} /\ conditionId \notin usedConditionIds /\ conditionId \notin DOMAIN before /\ after = [id \in DOMAIN before \cup {conditionId} |-> IF id = conditionId THEN [controller |-> "SideB",triggerInspectionId |-> currentInspectionId,request |-> request,pending |-> FALSE] ELSE before[id]] MarkDelayedInspectiones7(before,after,actualInspectionEndEvent) == /\ actualInspectionEndEvent.tag = "InspectionEnds" /\ after = [id \in DOMAIN before |-> IF before[id].triggerInspectionId = actualInspectionEndEvent.siteInspectionId THEN [before[id] EXCEPT !.pending = TRUE] ELSE before[id]] TakeDelayedInspection7(before,after,conditionId,currentInspectionId,actualSideBMayResolve,actualNewTimingAllowed,outcome) == /\ conditionId \in DOMAIN before /\ before[conditionId].pending /\ before[conditionId].controller = "SideB" /\ currentInspectionId = 0 /\ actualSideBMayResolve /\ after = [id \in DOMAIN before \ {conditionId} |-> before[id]] /\ outcome = [perform |-> actualNewTimingAllowed, request |-> [before[conditionId].request EXCEPT !.caller = <<"DelayedInspection",conditionId>>]] SideAZoneCards7(objects,zone) == {id \in DOMAIN objects : objects[id].form = "Card" /\ objects[id].side = "SideA" /\ objects[id].zone = zone} InspectionRootCards7(b,objects) == {id \in SideAZoneCards7(objects,"Play") : objects[id].area = "Root" /\ objects[id].targetSite = b.targetSite /\ objects[id].host = 0} OpenCandidateCapacity7(b,objects) == [siteInspectionId |-> b.id,admittedRoots |-> InspectionRootCards7(b,objects),pendingRoots |-> {},deniedRoots |-> {}] ObserveRootEntries7(before,after,b,objectsAfter,actualRootEntriesDuringInspection) == /\ b.active /\ ~b.complete /\ before.siteInspectionId = b.id /\ LET roots == InspectionRootCards7(b,objectsAfter) arrivals == actualRootEntriesDuringInspection \cap roots IN after = [before EXCEPT !.admittedRoots = (@ \cap roots) \ arrivals, !.pendingRoots = (@ \cup arrivals) \cap roots] DecideRootAdmissions7(before,after,b,objects,accepted,actualCheckpointStep,normalEarlierStepsComplete) == /\ b.active /\ ~b.complete /\ before.siteInspectionId = b.id /\ actualCheckpointStep = "ProcedureCode7f181ce21011" /\ normalEarlierStepsComplete /\ accepted \subseteq before.pendingRoots \cap InspectionRootCards7(b,objects) /\ after = [before EXCEPT !.admittedRoots = (@ \cup (accepted \ before.deniedRoots)) \cap InspectionRootCards7(b,objects), !.deniedRoots = @ \cup (before.pendingRoots \ accepted), !.pendingRoots = {}] CandidateCapacityValid7(m,b,objects) == /\ m.siteInspectionId = b.id /\ m.admittedRoots \subseteq InspectionRootCards7(b,objects) /\ m.pendingRoots \subseteq InspectionRootCards7(b,objects) /\ m.admittedRoots \cap (m.pendingRoots \cup m.deniedRoots) = {} DeckOrderValid7(objects,deck) == SubIds6(deck) = SideAZoneCards7(objects,"SideADeck") /\ Len(deck) = Cardinality(SubIds6(deck)) CandidateInputsValid7(b,m,objects,deck) == CandidateCapacityValid7(m,b,objects) /\ (b.kind = "SchemaAtom129" => DeckOrderValid7(objects,deck)) OneCardTraversalProhibition7(b,history,liveObjects,actualRestrictionApplies,exceptions) == IF actualRestrictionApplies /\ ActualItemInspectionesInTraversal7(history,b.traversalId) # {} THEN liveObjects \ exceptions ELSE {} CentralQuotaAvailable7(b) == ~RandomLimitApplies7(b) \/ InspectionCentralChoices7(b) < b.randomLimit DeckCandidate7(deck,excluded,exampleFamily058Off) == LET eligible == {i \in 1..Len(deck) : deck[i] \notin excluded} IN IF eligible = {} THEN {} ELSE {deck[CHOOSE i \in eligible : \A j \in eligible : IF exampleFamily058Off THEN i >= j ELSE i <= j]} InspectionCandidatesDirection7(b,m,objects,deck,prohibited,exampleFamily058Off) == LET excluded == prohibited \cup InspectionChoiceObjects7(b) \cup m.deniedRoots roots == (InspectionRootCards7(b,objects) \cap m.admittedRoots) \ (excluded \cup m.deniedRoots \cup m.pendingRoots) central == IF ~CentralQuotaAvailable7(b) THEN {} ELSE CASE b.kind = "SchemaAtom082" -> SideAZoneCards7(objects,"SideAHand") \ excluded [] b.kind = "SchemaAtom018" -> SideAZoneCards7(objects,"SideADiscard") \ excluded [] b.kind = "SchemaAtom129" -> DeckCandidate7(deck,excluded,exampleFamily058Off) [] OTHER -> {} IN IF b.active /\ ~b.complete THEN [roots |-> roots,central |-> central] ELSE [roots |-> {},central |-> {}] InspectionCandidates7(b,m,objects,deck,prohibited) == InspectionCandidatesDirection7(b,m,objects,deck,prohibited,FALSE) DeriveCandidateView7(b,m,objects,deck,prohibited,exampleFamily058Off,view) == CandidateInputsValid7(b,m,objects,deck) /\ view = InspectionCandidatesDirection7(b,m,objects,deck,prohibited,exampleFamily058Off) InspectionSteps7 == {"ProcedureCode839b301bad95","ProcedureCodeb6067693902e","ProcedureCode91f3ee0da236","ProcedureCode1404a82ab3ee","ProcedureCodee35e7c8fc57b","ProcedureCodeb1fbc90c4ab0","ProcedureCode8c612115d469"} InspectionStepInfo7(step) == [kind |-> CASE step = "ProcedureCode839b301bad95" -> "BeginInspection" [] step = "ProcedureCodeb6067693902e" -> "PrepareDiscardSite" [] step = "ProcedureCode91f3ee0da236" -> "SetLimit" [] step = "ProcedureCode1404a82ab3ee" -> "Choose" [] step = "ProcedureCodee35e7c8fc57b" -> "ItemInspection" [] step = "ProcedureCodeb1fbc90c4ab0" -> "Repeat" [] step = "ProcedureCode8c612115d469" -> "CompleteInspection" [] OTHER -> "Invalid", paidWindow |-> FALSE,objectivePlacementWindow |-> FALSE] NextInspectionStep7(step) == CASE step = "ProcedureCode839b301bad95" -> "ProcedureCodeb6067693902e" [] step = "ProcedureCodeb6067693902e" -> "ProcedureCode91f3ee0da236" [] step = "ProcedureCode91f3ee0da236" -> "ProcedureCode1404a82ab3ee" [] step = "ProcedureCode1404a82ab3ee" -> "ProcedureCodee35e7c8fc57b" [] step = "ProcedureCodee35e7c8fc57b" -> "ProcedureCodeb1fbc90c4ab0" [] step = "ProcedureCodeb1fbc90c4ab0" -> "ProcedureCode1404a82ab3ee" [] step = "ProcedureCode8c612115d469" -> "Complete" [] OTHER -> "NoValue" InspectionBeginEvent7(b) == [tag |-> "InspectionTargetSite",siteInspectionId |-> b.id,targetSite |-> b.targetSite,traversalId |-> b.traversalId] BeginInspection7(before,after,currentInspectionId,actualLiveTargetSites,actualNewTimingAllowed,actualAllInspectionPrerequisitesComplete,events) == /\ before.step = "ProcedureCode839b301bad95" /\ ~before.active /\ ~before.beginMet /\ ~before.complete /\ before.id \in Nat \ {0} /\ currentInspectionId = 0 /\ before.targetSite \in actualLiveTargetSites /\ before.kind = InspectionTargetSiteCategory7(before.targetSite) /\ actualNewTimingAllowed /\ actualAllInspectionPrerequisitesComplete /\ after = [before EXCEPT !.active = TRUE,!.beginMet = TRUE] /\ events = {InspectionBeginEvent7(before)} BeginInspectionWithCandidates7(before,after,afterCapacity,objects,currentInspectionId,actualLiveTargetSites, actualNewTimingAllowed,actualAllInspectionPrerequisitesComplete,events) == BeginInspection7(before,after,currentInspectionId,actualLiveTargetSites,actualNewTimingAllowed,actualAllInspectionPrerequisitesComplete,events) /\ afterCapacity = OpenCandidateCapacity7(after,objects) AdvanceInspectionStep7(before,after,actualStepAndChildProceduresComplete,normalCheckpointAndReactionsDrained) == /\ before.active /\ ~before.complete /\ before.beginMet /\ before.step \in {"ProcedureCode839b301bad95","ProcedureCodeb6067693902e","ProcedureCode91f3ee0da236","ProcedureCodee35e7c8fc57b","ProcedureCodeb1fbc90c4ab0"} /\ actualStepAndChildProceduresComplete /\ normalCheckpointAndReactionsDrained /\ CASE before.step = "ProcedureCodeb6067693902e" -> before.kind # "SchemaAtom018" \/ before.archivesPrepared [] before.step = "ProcedureCode91f3ee0da236" -> ~RandomLimitApplies7(before) \/ before.limitSet [] before.step \in {"ProcedureCodee35e7c8fc57b","ProcedureCodeb1fbc90c4ab0"} -> ~before.selectionPending /\ before.currentItemInspectionId = 0 [] OTHER -> TRUE /\ after = [before EXCEPT !.step = NextInspectionStep7(before.step)] AdvanceInspectionSelection7(before,after,actualChoiceInstructionAndNormalCheckpointDrained) == /\ before.active /\ ~before.complete /\ before.step = "ProcedureCode1404a82ab3ee" /\ before.selectionPending /\ before.selectedObject \in InspectionChoiceObjects7(before) /\ actualChoiceInstructionAndNormalCheckpointDrained /\ after = [before EXCEPT !.step = "ProcedureCodee35e7c8fc57b"] SkipInspectionSelection7(before,after,m,objects,deck,prohibited,exampleFamily058Off,actualReevaluationAndCheckpointComplete) == /\ before.active /\ ~before.complete /\ before.step = "ProcedureCode1404a82ab3ee" /\ ~before.selectionPending /\ before.currentItemInspectionId = 0 /\ (RandomLimitApplies7(before) => before.limitSet) /\ (before.kind = "SchemaAtom018" => before.archivesPrepared) /\ CandidateInputsValid7(before,m,objects,deck) /\ actualReevaluationAndCheckpointComplete /\ LET view == InspectionCandidatesDirection7(before,m,objects,deck,prohibited,exampleFamily058Off) IN InspectionPolicyComplete7(before.policy,Len(before.choices),view.roots \cup view.central = {}) /\ after = [before EXCEPT !.step = "ProcedureCode8c612115d469"] CompleteNormalInspection7(before,after,actualPriorStepsAndNormalReactionsComplete,events) == /\ before.active /\ ~before.complete /\ before.step = "ProcedureCode8c612115d469" /\ before.beginMet /\ ~before.selectionPending /\ before.currentItemInspectionId = 0 /\ actualPriorStepsAndNormalReactionsComplete /\ EndInspection7(before,after,"Normal",TRUE,events) CloseEndedInspectionBeginReaction7(before,after,b) == /\ b.complete /\ b.beginMet /\ before.open /\ before.kind = "Reaction" /\ before.beginInspectionId = b.id /\ after = [before EXCEPT !.open = FALSE,!.pending = {},!.priority = "NoValue", !.lostPending = @ \cup before.pending] DrainEndedInspectionInstruction7(before,after,actualSelectedInstructionAndAllChildrenComplete) == /\ before.complete /\ ~before.returned /\ (before.selectionPending \/ before.currentItemInspectionId # 0) /\ actualSelectedInstructionAndAllChildrenComplete /\ after = [before EXCEPT !.selectionPending = FALSE,!.selectedObject = 0, !.selectedSource = "NoValue",!.currentItemInspectionId = 0] ReturnInspectionToCaller7(before,after,actualInspectionEndWindowsAndCheckpointComplete,caller) == /\ before.complete /\ ~before.returned /\ ~before.selectionPending /\ before.currentItemInspectionId = 0 /\ actualInspectionEndWindowsAndCheckpointComplete /\ caller = before.caller /\ after = [before EXCEPT !.returned = TRUE] InspectionProcedureValid7(b) == /\ b.id \in Nat \ {0} /\ b.kind = InspectionTargetSiteCategory7(b.targetSite) /\ b.active => b.beginMet /\ ~b.complete /\ b.step \in InspectionSteps7 /\ b.complete => ~b.active /\ b.step = "Complete" /\ (~b.active /\ ~b.complete) => ~b.beginMet /\ b.step = "ProcedureCode839b301bad95" /\ b.returned => b.complete /\ ~b.selectionPending /\ b.currentItemInspectionId = 0 /\ b.randomLimit \in Nat /\ b.usedItemInspectionIds \subseteq Nat \ {0} /\ Cardinality(InspectionChoiceObjects7(b)) = Len(b.choices) /\ IF b.selectionPending THEN b.selectedObject \in InspectionChoiceObjects7(b) /\ b.selectedObject # 0 ELSE b.selectedObject = 0 /\ b.selectedSource = "NoValue" /\ b.currentItemInspectionId = 0 =============================================================================