------------------------- MODULE ItemTimingMC ------------------------- EXTENDS InspectionTimingMC NoItemInspectionCostCommandsT11(t) == {} NoItemInspectionCostOverrideT11(t,c,r) == FALSE NoItemInspectionCheckpointOverrideT11(t,c) == FALSE ItemInspectionCostOwnerT11 == INSTANCE ObjectRuntime WITH s <- qT11.wallet,CardData <- EmptyT11,InitialState <- EmptyT11, Commands <- NoItemInspectionCostCommandsT11,CardOverride <- NoItemInspectionCostOverrideT11,CheckpointOverrideAllowed <- NoItemInspectionCheckpointOverrideT11 ItemInspectionCardT11(zone,kind) == [form |-> "Card",side |-> "SideA",kind |-> kind,zone |-> zone,loc |-> <>,card |-> "SyntheticItemInspectionPhysical1", host |-> 0,deployed |-> zone="Play",face |-> IF zone \in {"SideAHand","SideADeck"} THEN "NA" ELSE "Down",activated |-> FALSE, marks |-> {"ObjectLocalProbe"},physical |-> 1] ItemInspectionObjectsT11(zone,kind) == [id \in {1} |-> ItemInspectionCardT11(zone,kind)] ItemInspectionInitialT11(zone,kind,traversal,siteInspection) == OpenItemInspection7(77,1,ItemInspectionCardT11(zone,kind),traversal,siteInspection,"ItemInspectionAuditCaller",{}) ItemInspectionWorkedT11(step) == [ItemInspectionInitialT11("SideAHand","Facility",0,0) EXCEPT !.active=TRUE,!.beginMet=TRUE,!.step=step, !.midDone=step#"ProcedureCodefd91bef8bbd3",!.claimObjectiveDone=step \in {"ProcedureCode546db7cc4546","ProcedureCode662478499367"}] ItemInspectionEndedT11(a,reason) == [a EXCEPT !.active=FALSE,!.complete=TRUE,!.step="Complete",!.completionReason=reason] ItemInspectionCandidateFramesT11(a) == {[a EXCEPT !.step=step] : step \in ItemInspectionOracleStepSet11 \cup {"UnauthorizedStep"}} ItemInspectionDestinationT11(a) == IF a.returned THEN "ReturnToCaller" ELSE a.step ActualItemInspectionDestinationsT11(a,completed,drained) == LET objects==ItemInspectionObjectsT11("SideAHand","Facility") done==ItemInspectionEndedT11(a,"Normal") returned==[done EXCEPT !.returned=TRUE] IN {ItemInspectionDestinationT11(g) : g \in {f \in ItemInspectionCandidateFramesT11(a) : AdvanceItemInspectionStep7(a,f,objects,completed,drained)}} \cup (IF CompleteNormalItemInspection7(a,done,objects,completed,{ItemInspectionEndEvent7(a)}) /\ ReturnItemInspectionToCaller7(done,returned,drained,"ItemInspectionAuditCaller") THEN {ItemInspectionDestinationT11(returned)} ELSE {}) ItemInspectionFormalLabelT11(e) == IF e.tag="ItemInspectionCard" THEN "CardItemInspectioned" ELSE e.tag ItemInspectionGraphChecksT11 == /\ ItemInspectionInitialT11("SideAHand","Facility",0,0).step=ItemInspectionOracleEntry11 /\ ~ItemInspectionInitialT11("SideAHand","Facility",0,0).beginMet /\ ItemInspectionSteps7=ItemInspectionOracleStepSet11 /\ ItemInspectionOracleHidden11={} /\ ItemInspectionOracleFormalConditions11["ProcedureCodefd91bef8bbd3"]={ItemInspectionFormalLabelT11(ItemInspectionBeginEvent7(ItemInspectionWorkedT11("ProcedureCodefd91bef8bbd3")))} /\ ItemInspectionOracleFormalConditions11["ProcedureCode662478499367"]={ItemInspectionFormalLabelT11(ItemInspectionEndEvent7(ItemInspectionWorkedT11("ProcedureCode662478499367")))} /\ \A step \in ItemInspectionOracleStepSet11 : ItemInspectionStepInfo7(step).kind=ItemInspectionOracleKinds11[step] /\ \A edge \in ItemInspectionOracleEdges11 : LET a==ItemInspectionWorkedT11(edge.before) IN /\ ActualItemInspectionDestinationsT11(a,TRUE,TRUE)={edge.after} /\ ActualItemInspectionDestinationsT11(a,FALSE,TRUE)={} /\ ActualItemInspectionDestinationsT11(a,TRUE,FALSE)={} ItemInspectionMidOpeningT11(id,site) == [tag |-> "PriorityWindowOpening",windowId |-> id,kind |-> "MidItemInspection",site |-> site, members |-> {},instances |-> EmptyT11,group |-> 0,beginning |-> NoTimingRef9,instruction |-> [id |-> 0],effectRevision |-> 0] ItemInspectionMidWindowT11(id,site) == NewPriorityWindow9(id,"MidItemInspection",site,EmptyT11,0,NoTimingRef9,[id |-> 0],0) ItemInspectionPriorityOptionT11(a,mid,actor,kind) == PriorityOption9(20,kind,actor,mid.id,0,RuleAbilitySource9("AuditMidItemInspection"),a.object,{}) ItemInspectionPaymentT11(w,paid,drained) == [tag |-> "PriorityOptionPayment",windowId |-> w.id,option |-> w.busy, transactionId |-> w.busyTransaction,allTriggerCostsPaid |-> paid,costCheckpointAndReactionsDrained |-> drained] ItemInspectionOptionReturnT11(w,payment) == [tag |-> "PriorityOptionReturn",windowId |-> w.id,option |-> w.busy, transactionId |-> w.busyTransaction,triggerPayment |-> payment,allCostsPaid |-> payment.allTriggerCostsPaid, optionComplete |-> TRUE,childrenReturned |-> TRUE,reactionsDrained |-> TRUE] ActualItemInspectionOptionT11(w,a,objects,mid,actor,kind) == LET option==ItemInspectionPriorityOptionT11(a,mid,actor,kind) IN BeginMidItemInspectionOption9(<>,<>,option,objects,LegalityT11(w,option),a,a,mid,{mid},FALSE,FALSE) ItemInspectionWindowChecksT11 == /\ ItemInspectionOraclePaidSteps11={} /\ ItemInspectionOracleMidPlayers11={"SideB"} /\ ItemInspectionOracleMaxMidUses11=1 /\ \A step \in ItemInspectionOracleStepSet11,player \in SetupPlayers : LET a==ItemInspectionWorkedT11(step) objects==ItemInspectionObjectsT11("SideAHand","Facility") site==ItemInspectionPrioritySite9(TraversalTurnT11(player),a,objects) IN /\ ~WindowSiteAllowed9("Paid",site) /\ ~WindowSiteAllowed9("NeutralValue00001",site) /\ WindowSiteAllowed9("MidItemInspection",site)=(step \in ItemInspectionOracleMidSteps11) /\ ~ItemInspectionStepInfo7(step).paidWindow /\ ~ItemInspectionStepInfo7(step).objectivePlacementWindow /\ \A player \in SetupPlayers : LET a==[ItemInspectionWorkedT11("ProcedureCode1dd0e8f05be2") EXCEPT !.midDone=FALSE] objects==ItemInspectionObjectsT11("SideAHand","Facility") site==ItemInspectionPrioritySite9(TraversalTurnT11(player),a,objects) w==ItemInspectionMidWindowT11(1,site) ready==PriorityReadyT11(w) mid==MidOption7("SyntheticObserve",FALSE,TRUE,TRUE) passed==[a EXCEPT !.midDone=TRUE] IN /\ w.priority="SideB" /\ OpenPriorityWindow9(<<>>,<>,1,"MidItemInspection",site,EmptyT11,ItemInspectionMidOpeningT11(1,site),{}) /\ CheckpointPriority9(<>,<>,PriorityCheckpointT11(w)) /\ ~CheckpointPriority9(<>,<>,[PriorityCheckpointT11(w) EXCEPT !.reactionsDrained=FALSE]) /\ ActualItemInspectionOptionT11(ready,a,objects,mid,"SideB","MidItemInspection") /\ ~ActualItemInspectionOptionT11(ready,a,objects,mid,"SideA","MidItemInspection") /\ \A kind \in {"RegularPaid","Activation","ObjectiveCompletion","NeutralValue00001"} : ~ActualItemInspectionOptionT11(ready,a,objects,mid,"SideB",kind) /\ PassMidItemInspection9(<>,<>,a,passed,objects,{mid},FALSE,FALSE) /\ ~PassMidItemInspection9(<>,<>,passed,passed,objects,{mid},FALSE,FALSE) ItemInspectionBeginVisibilityChecksT11 == /\ \A zone \in {"SideAHand","SideADeck","SideADiscard","Play"} : LET objects==ItemInspectionObjectsT11(zone,"Facility") a==ItemInspectionInitialT11(zone,"Facility",0,0) begun==[a EXCEPT !.active=TRUE,!.beginMet=TRUE] ended==ItemInspectionEndedT11(begun,"Normal") cancelled==[a EXCEPT !.complete=TRUE,!.step="Complete",!.completionReason="ItemInspectionCostDeclined"] IN /\ BeginItemInspection7(a,begun,objects,TRUE,TRUE,TRUE,{ItemInspectionBeginEvent7(a)}) /\ ~BeginItemInspection7(a,begun,objects,FALSE,TRUE,TRUE,{ItemInspectionBeginEvent7(a)}) /\ ~BeginItemInspection7(a,begun,objects,TRUE,FALSE,TRUE,{ItemInspectionBeginEvent7(a)}) /\ ~BeginItemInspection7(a,begun,objects,TRUE,TRUE,FALSE,{ItemInspectionBeginEvent7(a)}) /\ ~BeginItemInspection7(a,begun,EmptyT11,TRUE,TRUE,TRUE,{ItemInspectionBeginEvent7(a)}) /\ ~BeginItemInspection7(a,begun,objects,TRUE,TRUE,TRUE,{}) /\ ItemInspectionBeginEvent7(a)=[tag |-> "ItemInspectionCard",itemInspectionId |-> 77,object |-> 1,traversalId |-> 0,siteInspectionId |-> 0] /\ ~ItemInspectionLookGrant7(a,objects,"SideB") /\ ItemInspectionLookGrant7(begun,objects,"SideB") /\ ItemInspectionLookGrant7(begun,objects,"SideA")=(zone#"SideADeck") /\ ItemInspectionViewers7(begun,objects,{},FALSE)=(IF zone="SideADeck" THEN {"SideB"} ELSE SetupPlayers) /\ ItemInspectionViewers7(begun,objects,{"SideA"},FALSE)=SetupPlayers /\ ~ItemInspectionLookGrant7(ended,objects,"SideB") /\ CancelUnstartedItemInspection7(a,cancelled,"ItemInspectionCostDeclined",TRUE,{}) /\ ~cancelled.beginMet /\ ~CancelUnstartedItemInspection7(begun,ItemInspectionEndedT11(begun,"ItemInspectionCostDeclined"),"ItemInspectionCostDeclined",TRUE,{}) /\ LET objects==ItemInspectionObjectsT11("SideAHand","Objective") ability==AbilityDefinition9(5,"Conditional",ObjectAbilitySource9(1),"Card") trigger==[ability EXCEPT !.sourceItemInspection=TRUE] cost==[ability EXCEPT !.kind="Static",!.ownClaimObjectiveAdditionalCost=TRUE] IN /\ AbilityActive9(trigger,objects,{5},FALSE,ActivityContext9) /\ AbilityActive9(cost,objects,{5},FALSE,ActivityContext9) /\ ~AbilityActive9(ability,objects,{5},FALSE,ActivityContext9) /\ AbilitySourceItemInspectionMatches9(trigger,[tag |-> "ItemInspectionCard",object |-> 1]) /\ ~AbilitySourceItemInspectionMatches9(trigger,[tag |-> "ItemInspectionCard",object |-> 2]) ItemInspectionMidObligationChecksT11 == LET objects==ItemInspectionObjectsT11("SideAHand","Facility") a==[ItemInspectionWorkedT11("ProcedureCode1dd0e8f05be2") EXCEPT !.midDone=FALSE] used==[a EXCEPT !.midUsed=TRUE,!.midResolving=TRUE] finished==[used EXCEPT !.midResolving=FALSE,!.midDone=TRUE] zero==BasicRetireOption7(objects[1],[exists |-> TRUE,amount |-> 0],TRUE,TRUE) absent==BasicRetireOption7(objects[1],[exists |-> FALSE,amount |-> 0],TRUE,TRUE) trash==MidOption7("SyntheticRetire",TRUE,TRUE,TRUE) other==MidOption7("SyntheticObserve",FALSE,TRUE,TRUE) options=={zero,trash,other} unavailable=={[zero EXCEPT !.canPay=FALSE],[trash EXCEPT !.canPay=FALSE],other} ar==ItemInspectionObjectsT11("SideADiscard","Facility") arOptions==ItemInspectionMidOptions7(ar[1],{trash,other},[exists |-> TRUE,amount |-> 0],TRUE,TRUE) IN /\ zero.legal /\ ~absent.legal /\ PayableMidOptions7({absent})={} /\ MidItemInspectionChoiceAllowed7("Decline",options,FALSE,FALSE) /\ ~MidItemInspectionChoiceAllowed7("Decline",options,TRUE,FALSE) /\ ~MidItemInspectionChoiceAllowed7("SyntheticObserve",options,TRUE,FALSE) /\ MidItemInspectionChoiceAllowed7("SyntheticRetire",options,TRUE,FALSE) /\ MidItemInspectionChoiceAllowed7("BasicRetire",options,TRUE,TRUE) /\ ~MidItemInspectionChoiceAllowed7("SyntheticRetire",options,FALSE,TRUE) /\ MidItemInspectionChoiceAllowed7("Decline",unavailable,TRUE,TRUE) /\ ~MidItemInspectionChoiceAllowed7("BasicRetire",arOptions,FALSE,FALSE) /\ ~MidItemInspectionChoiceAllowed7("SyntheticRetire",arOptions,FALSE,FALSE) /\ MidItemInspectionChoiceAllowed7("SyntheticObserve",arOptions,FALSE,FALSE) /\ UseMidItemInspection7(a,used,objects,zero,options,FALSE,FALSE,TRUE,TRUE) /\ ~UseMidItemInspection7(a,used,objects,zero,options,FALSE,FALSE,FALSE,TRUE) /\ ~UseMidItemInspection7(a,used,objects,zero,options,FALSE,FALSE,TRUE,FALSE) /\ ~UseMidItemInspection7([a EXCEPT !.midUsed=TRUE],used,objects,zero,options,FALSE,FALSE,TRUE,TRUE) /\ FinishMidItemInspection7(used,finished,TRUE) /\ ~FinishMidItemInspection7(used,finished,FALSE) ItemInspectionMovedObjectsT11(objects,zone) == [id \in {2} |-> [objects[1] EXCEPT !.zone=zone,!.loc= <>,!.face="Up",!.deployed=FALSE,!.activated=FALSE,!.host=0,!.marks={}]] ItemInspectionMovementChecksT11 == LET objects==ItemInspectionObjectsT11("SideAHand","Facility") a==[ItemInspectionWorkedT11("ProcedureCode1dd0e8f05be2") EXCEPT !.midDone=FALSE,!.midUsed=TRUE,!.midResolving=TRUE] moved==ItemInspectionMovedObjectsT11(objects,"SideADiscard") ended==ItemInspectionEndedT11(a,"Moved") finished==[ended EXCEPT !.midResolving=FALSE,!.midDone=TRUE] changed==[objects EXCEPT ![1].face="Up",![1].marks={}] begunWindow==[kind |-> "Reaction",open |-> TRUE,beginItemInspectionId |-> a.id,pending |-> {5},lostPending |-> {},priority |-> "SideA"] closedWindow==[begunWindow EXCEPT !.open=FALSE,!.pending={},!.lostPending={5},!.priority="NoValue"] IN /\ CardBatchTransfer8(objects,moved,{1},[id \in {1} |-> 2],{1},"SideADiscard","Up",[id \in {1} |-> <<"SideADiscard",2>>]) /\ ItemInspectionMovementOutcome7(a,ended,moved,TRUE,{ItemInspectionEndEvent7(a)}) /\ ~StillItemInspectioning7(ended,moved) /\ ItemInspectionMovementOutcome7(a,a,changed,TRUE,{}) /\ ItemInspectionMovementOutcome7(a,ended,[objects EXCEPT ![1].loc= <<"OtherPosition",1>>],TRUE,{ItemInspectionEndEvent7(a)}) /\ ~AdvanceItemInspectionStep7(ended,[ended EXCEPT !.step="ProcedureCode546db7cc4546"],moved,TRUE,TRUE) /\ ~CompleteNormalItemInspection7(ended,ended,moved,TRUE,{ItemInspectionEndEvent7(a)}) /\ ~ReturnItemInspectionToCaller7(ended,[ended EXCEPT !.returned=TRUE],TRUE,"ItemInspectionAuditCaller") /\ FinishMidItemInspection7(ended,finished,TRUE) /\ ReturnItemInspectionToCaller7(finished,[finished EXCEPT !.returned=TRUE],TRUE,"ItemInspectionAuditCaller") /\ ~ReturnItemInspectionToCaller7(finished,[finished EXCEPT !.returned=TRUE],FALSE,"ItemInspectionAuditCaller") /\ ~ReturnItemInspectionToCaller7(finished,[finished EXCEPT !.returned=TRUE],TRUE,"WrongItemInspectionCaller") /\ CloseEndedItemInspectionBeginReaction7(begunWindow,closedWindow,ended) /\ ~CloseEndedItemInspectionBeginReaction7([begunWindow EXCEPT !.beginItemInspectionId=78],[closedWindow EXCEPT !.beginItemInspectionId=78],ended) ItemInspectionEndScopeChecksT11 == LET a==ItemInspectionWorkedT11("ProcedureCodefd91bef8bbd3") outer==[a EXCEPT !.id=77,!.encounterAncestors={}] inner==[a EXCEPT !.id=78,!.encounterAncestors={50}] frames==[id \in {77,78} |-> IF id=77 THEN outer ELSE inner] base==[TraversalControlT11(NoTraversal6) EXCEPT !.encounter=50,!.itemInspections=frames] scoped==EndTraversalOutcome6(base,0) none==[base EXCEPT !.encounter=0] running==[base EXCEPT !.traversal=TraversalGraphFixtureT11("ProcedureCodebbb14496b09b","Next").control.traversal] endedTraversal==EndTraversalOutcome6(running,1001) objects==ItemInspectionObjectsT11("SideAHand","Facility") site==ItemInspectionPrioritySite9(TraversalTurnT11("SideA"),a,objects) instances==[id \in {5} |-> ConditionalInstance9(5,50,RuleAbilitySource9("SyntheticReaction"),"SideA",TRUE,1,10,FALSE)] w==NewPriorityWindow9(10,"Reaction",site,instances,1,TimingRef9("ItemInspection",77),[id |-> 0],0) receipt==[tag |-> "TimingStructureEnded",structure |-> TimingRef9("ItemInspection",77)] IN /\ EndTheTraversal6(base,scoped,0,TRUE,EndTraversalEffectEvents6(base)) /\ scoped.abortedItemInspectiones={78} /\ DOMAIN scoped.itemInspections={77} /\ ApplyItemInspectionAborts7(outer,outer,scoped.abortedItemInspectiones,{}) /\ ApplyItemInspectionAborts7(inner,ItemInspectionEndedT11(inner,"EndTraversal"),scoped.abortedItemInspectiones,{ItemInspectionEndEvent7(inner)}) /\ EndTheTraversal6(none,none,0,TRUE,{}) /\ EndTheTraversal6(running,endedTraversal,1001,TRUE,EndTraversalEffectEvents6(running)) /\ endedTraversal.abortedItemInspectiones={77,78} /\ CancelBeginningReactions9(<>,<>,receipt) /\ CancelBeginningReactions9(<<[w EXCEPT !.beginning=TimingRef9("ItemInspection",78)]>>,<<[w EXCEPT !.beginning=TimingRef9("ItemInspection",78)]>>,receipt) ItemInspectionClaimObjectiveChecksT11 == LET objects==ItemInspectionObjectsT11("SideAHand","Objective") a==[ItemInspectionWorkedT11("ProcedureCode546db7cc4546") EXCEPT !.claimObjectiveDone=FALSE] claimingObjective==[a EXCEPT !.claimObjectiveResolving=TRUE] done==[a EXCEPT !.claimObjectiveDone=TRUE] moved==ItemInspectionMovedObjectsT11(objects,"SideBObjectiveCompletion") ended==ItemInspectionEndedT11(claimingObjective,"Moved") finished==[ended EXCEPT !.claimObjectiveResolving=FALSE,!.claimObjectiveDone=TRUE] IN /\ ItemInspectionClaimObjectiveDisposition7(objects[1],FALSE,FALSE,FALSE,TRUE)="ClaimObjective" /\ ResolveItemInspectionClaimObjective7(a,claimingObjective,objects,FALSE,FALSE,FALSE,TRUE,TRUE,FALSE) /\ ResolveItemInspectionClaimObjective7(a,done,objects,TRUE,FALSE,TRUE,TRUE,FALSE,FALSE) /\ ResolveItemInspectionClaimObjective7(a,done,objects,TRUE,TRUE,FALSE,TRUE,FALSE,FALSE) /\ ResolveItemInspectionClaimObjective7(a,done,objects,FALSE,TRUE,TRUE,FALSE,FALSE,FALSE) /\ ~ResolveItemInspectionClaimObjective7(a,claimingObjective,objects,TRUE,TRUE,TRUE,TRUE,FALSE,TRUE) /\ ~ResolveItemInspectionClaimObjective7(a,claimingObjective,objects,TRUE,TRUE,TRUE,TRUE,TRUE,FALSE) /\ ~ResolveItemInspectionClaimObjective7([a EXCEPT !.midDone=FALSE],[claimingObjective EXCEPT !.midDone=FALSE],objects,FALSE,FALSE,FALSE,TRUE,TRUE,TRUE) /\ CardBatchTransfer8(objects,moved,{1},[id \in {1} |-> 2],{1},"SideBObjectiveCompletion","Up",[id \in {1} |-> <<"SideBObjectiveCompletion",2>>]) /\ ItemInspectionMovementOutcome7(claimingObjective,ended,moved,TRUE,{ItemInspectionEndEvent7(claimingObjective)}) /\ FinishItemInspectionClaimObjective7(ended,finished,TRUE) /\ ~FinishItemInspectionClaimObjective7(ended,finished,FALSE) /\ ~ReturnItemInspectionToCaller7(ended,[ended EXCEPT !.returned=TRUE],TRUE,"ItemInspectionAuditCaller") ItemInspectionWalletInitialT11 == [obj |-> [i \in {100,101,102} |-> ItemInspectionCostOwnerT11!Token("ResourceUnit","SideBResourceUnits",0,"SideB",FALSE)],past |-> EmptyT11,pendingRetire |-> {},checkpointDue |-> FALSE,used |-> {},event |-> "NoValue"] ItemInspectionPaymentChecksT11 == LET wallet==ItemInspectionWalletInitialT11 virtual==[wallet EXCEPT !.obj[100].virtual=TRUE] a==[ItemInspectionWorkedT11("ProcedureCode1dd0e8f05be2") EXCEPT !.midDone=FALSE] used==[a EXCEPT !.midUsed=TRUE,!.midResolving=TRUE] objects==ItemInspectionObjectsT11("SideAHand","Facility") mid==MidOption7("SyntheticObserve",FALSE,TRUE,TRUE) site==ItemInspectionPrioritySite9(TraversalTurnT11("SideA"),a,objects) ready==PriorityReadyT11(ItemInspectionMidWindowT11(1,site)) option==ItemInspectionPriorityOptionT11(a,mid,"SideB","MidItemInspection") busy==StartPriorityOptionFrame9(ready,option,200) paid==ItemInspectionPaymentT11(busy,TRUE,TRUE) IN /\ ItemInspectionCostOwnerT11!SpendResourceUnitsOK(wallet,"SideB",{},0,{}) /\ ItemInspectionCostOwnerT11!SpendResourceUnitsOK(wallet,"SideB",{100,101},2,{}) /\ ~ItemInspectionCostOwnerT11!SpendResourceUnitsOK(wallet,"SideB",{100},2,{}) /\ ~ItemInspectionCostOwnerT11!SpendResourceUnitsOK(virtual,"SideB",{100},1,{}) /\ BeginMidItemInspectionOption9(<>,<>,option,objects,LegalityT11(ready,option),a,a,mid,{mid},FALSE,FALSE) /\ PayMidItemInspectionOption9(<>,a,used,objects,mid,{mid},FALSE,FALSE,paid) /\ ~PayMidItemInspectionOption9(<>,a,used,objects,mid,{mid},FALSE,FALSE,[paid EXCEPT !.transactionId=201]) /\ ~PayMidItemInspectionOption9(<>,a,used,objects,mid,{mid},FALSE,FALSE,[paid EXCEPT !.allTriggerCostsPaid=FALSE]) /\ ~PayMidItemInspectionOption9(<>,a,used,objects,mid,{mid},FALSE,FALSE,[paid EXCEPT !.costCheckpointAndReactionsDrained=FALSE]) /\ ~CompleteMidItemInspectionOption9(<>,<>,[ItemInspectionOptionReturnT11(busy,paid) EXCEPT !.childrenReturned=FALSE],used,[used EXCEPT !.midResolving=FALSE,!.midDone=TRUE]) ItemInspectionPointwiseInitT11 == guideCaseT11 \in 1..7 /\ qT11=EmptyT11 ItemInspectionPointwiseNextT11 == UNCHANGED <> ItemInspectionPointwiseSpecT11 == ItemInspectionPointwiseInitT11 /\ [][ItemInspectionPointwiseNextT11]_<> ItemInspectionPointwiseBaseChecksT11 == CASE guideCaseT11=1 -> ItemInspectionGraphChecksT11 [] guideCaseT11=2 -> ItemInspectionWindowChecksT11 [] guideCaseT11=3 -> ItemInspectionBeginVisibilityChecksT11 [] guideCaseT11=4 -> ItemInspectionMidObligationChecksT11 [] guideCaseT11=5 -> ItemInspectionMovementChecksT11 /\ ItemInspectionEndScopeChecksT11 [] guideCaseT11=6 -> ItemInspectionClaimObjectiveChecksT11 [] OTHER -> ItemInspectionPaymentChecksT11 ItemInspectionProfilesT11 == {"FacilityPass","FacilityObserve0","FacilityObserve1","FacilityRetire0","FacilityRetire1","ObjectiveFree","ObjectiveCost0","ObjectiveCost1","ObjectiveDecline","ObjectiveUnable"} ItemInspectionProfileObjectiveT11(NeutralValue00013) == NeutralValue00013 \in {"ObjectiveFree","ObjectiveCost0","ObjectiveCost1","ObjectiveDecline","ObjectiveUnable"} ItemInspectionProfileMidT11(NeutralValue00013) == NeutralValue00013 \in {"FacilityObserve0","FacilityObserve1","FacilityRetire0","FacilityRetire1","FacilityCostMove0","FacilityCostMove1"} ItemInspectionProfileRetireT11(NeutralValue00013) == NeutralValue00013 \in {"FacilityRetire0","FacilityRetire1"} ItemInspectionProfileAmountT11(NeutralValue00013) == IF NeutralValue00013 \in {"FacilityObserve1","FacilityRetire1","ObjectiveCost1","FacilityCostMove1"} THEN 1 ELSE 0 ItemInspectionTemporalMidT11(q) == IF ItemInspectionProfileRetireT11(q.NeutralValue00013) THEN BasicRetireOption7(q.objects[1],[exists |-> TRUE,amount |-> ItemInspectionProfileAmountT11(q.NeutralValue00013)],TRUE,TRUE) ELSE MidOption7("SyntheticObserve",FALSE,TRUE,TRUE) ItemInspectionCostCommandT11(selected,amount) == [player |-> "SideB",selected |-> selected,amount |-> amount,permittedHosted |-> {},announced |-> TRUE,restrictionsHold |-> TRUE,mandatoryPrevents |-> FALSE,permissionSources |-> EmptyT11] ItemInspectionWalletSpentT11(wallet,selected) == [ItemInspectionCostOwnerT11!Remove(wallet,selected) EXCEPT !.checkpointDue=TRUE,!.used={},!.event="PayResourceUnits"] ItemInspectionCostBindingT11(q,purpose) == IF purpose="Mid" THEN LET w==WindowTop9(q.windows) IN [purpose |-> purpose,itemInspection |-> q.itemInspection.id,object |-> q.itemInspection.object,caller |-> q.itemInspection.caller,window |-> w.id,reception |-> w.reception,option |-> w.busy,transaction |-> w.busyTransaction] ELSE [purpose |-> purpose,itemInspection |-> q.itemInspection.id,object |-> q.itemInspection.object,caller |-> q.itemInspection.caller,step |-> q.itemInspection.step] ItemInspectionRequestCostT11(q,purpose,amount,resume) == [q EXCEPT !.stage="PayCost",!.costResume=resume,!.cost=[id |-> q.nextCost,purpose |-> purpose,amount |-> amount, binding |-> ItemInspectionCostBindingT11(q,purpose),paid |-> FALSE,drained |-> FALSE,selected |-> {},before |-> q.wallet,after |-> q.wallet],!.nextCost=@+1] ItemInspectionCommittedCostT11(q,purpose,amount) == /\ q.cost.purpose=purpose /\ q.cost.amount=amount /\ q.cost.binding=ItemInspectionCostBindingT11(q,purpose) /\ q.cost.paid /\ q.cost.drained /\ q.cost.after=ItemInspectionWalletSpentT11(q.cost.before,q.cost.selected) /\ ItemInspectionCostOwnerT11!SpendResourceUnitsOK(q.cost.before,"SideB",q.cost.selected,amount,{}) /\ q.wallet=[q.cost.after EXCEPT !.checkpointDue=FALSE] ItemInspectionMidPaymentFromStateT11(q) == ItemInspectionPaymentT11(WindowTop9(q.windows),ItemInspectionCommittedCostT11(q,"Mid",ItemInspectionProfileAmountT11(q.NeutralValue00013)),q.cost.drained) ItemInspectionRecordWorkT11(q,step,resume) == [q EXCEPT !.history=Append(@,step),!.stage="NormalDrain",!.resume=resume] ItemInspectionPaidDefinitionT11(q) == LET mid==ItemInspectionTemporalMidT11(q) source==RuleAbilitySource9(IF ItemInspectionProfileRetireT11(q.NeutralValue00013) THEN "BasicRetire" ELSE "AuditPaidObserve") flags==IF ItemInspectionProfileRetireT11(q.NeutralValue00013) THEN <<>> ELSE <> syntax==[id |-> mid.id,kind |-> "Paid",side |-> "SideB",controller |-> "SideB",cardKind |-> "Rule",source |-> source, units |-> flags \o <>, arrowAfterFlags |-> TRUE,barrierInstructionPrefix |-> FALSE,paidPrefix |-> [present |-> TRUE,bold |-> TRUE,colon |-> TRUE]] IN [syntax |-> syntax,activity |-> AbilityDefinition9(mid.id,"Paid",source,"Rule"), triggerCost |-> <<[kind |-> "ResourceUnits",amount |-> ItemInspectionProfileAmountT11(q.NeutralValue00013)]>>,instructions |-> <<700>>, instructionHasWould |-> FALSE,ruleTiming |-> IF ItemInspectionProfileRetireT11(q.NeutralValue00013) THEN "BasicRetire" ELSE "NoValue", canSuppressBarrierInstructions |-> FALSE,refersApproachedBarrier |-> FALSE,refersEncounteredBarrier |-> FALSE, approachRequirements |-> [subtypes |-> {},activated |-> FALSE,otherIds |-> {}],encounterRequirements |-> [subtypes |-> {},activated |-> FALSE,otherIds |-> {}], interfaceSubtype |-> [present |-> FALSE,name |-> "NoValue"],otherRestrictionIds |-> {},refersHosted |-> FALSE] ItemInspectionPaidContextT11(q,d) == [objects |-> q.objects,turn |-> TraversalTurnT11("SideA"),traversal |-> NoTraversal6, traversalControl |-> TraversalControlT11(NoTraversal6),encounter |-> OpenEncounter6(20,2,0,TRUE,"SyntheticUnused",<<>>), approach |-> [id |-> 0,traversalId |-> 0,begun |-> FALSE],layout |-> TraversalLayoutT11(0), subtypes |-> [id \in DOMAIN q.objects |-> {}],strengths |-> [id \in DOMAIN q.objects |-> [exists |-> TRUE,amount |-> 1]], references |-> EmptyT11,currentEffect |-> EmptyT11,paidRelevance |-> EmptyT11,present |-> {d.syntax.id},defaultActive |-> TRUE, activity |-> [ActivityContext9 EXCEPT !.activeRules={d.syntax.source.rule}],points |-> [p \in SetupPlayers |-> 0],uses |-> q.turnUses,useProhibitions |-> {}, ownRestrictions |-> [tag |-> "AbilityRestrictions",ability |-> d.syntax.id,source |-> d.syntax.source,results |-> EmptyT11], otherRestrictions |-> [tag |-> "OtherPaidRestrictions",ability |-> d.syntax.id,source |-> d.syntax.source,results |-> EmptyT11]] ItemInspectionPaidOptionT11(q,w,d) == PriorityOption9(20,"MidItemInspection","SideB",d.syntax.id,0,d.syntax.source,q.itemInspection.object,{}) ItemInspectionPaidUseT11(p) == [tag |-> "AbilityUsed",useId |-> 1,abilityInstance |-> p.id,source |-> p.ability.source,player |-> "SideB"] ItemInspectionPaidUsesT11(p) == [id \in {1} |-> ItemInspectionPaidUseT11(p)] ItemInspectionPaidTurnUsesT11(p) == [id \in {1} |-> [turnId |-> p.turnId,ability |-> p.definition.syntax.id,source |-> p.ability.source,useId |-> 1]] ItemInspectionPaidCommittedFrameT11(p) == [p EXCEPT !.ability.detached=TRUE,!.phase="CostCheckpoint",!.costPaid=TRUE] ItemInspectionNativePaidT11(q,selected,after) == /\ q.cost.purpose="Mid" /\ ~q.cost.paid /\ ~q.cost.drained /\ q.cost.binding=ItemInspectionCostBindingT11(q,"Mid") /\ q.cost.amount=ItemInspectionProfileAmountT11(q.NeutralValue00013) /\ q.paid.transaction=q.cost.binding.transaction /\ q.paid.windowId=q.cost.binding.window /\ q.paid.option=q.cost.binding.option /\ q.paid.option.target=q.cost.binding.object /\ q.paid.ability.caller=q.cost.binding.window /\ q.paid.initialCheckpoint=WindowTop9(q.windows).checkpoint /\ after=ItemInspectionWalletSpentT11(q.wallet,selected) /\ ItemInspectionCostOwnerT11!SpendResourceUnitsOK(q.wallet,"SideB",selected,q.cost.amount,{}) ItemInspectionPaidPaymentT11(q,selected,after) == [tag |-> "PaidTriggerPayment",abilityInstance |-> q.paid.id,transactionId |-> q.cost.binding.transaction, ability |-> q.paid.definition.syntax.id,source |-> q.paid.ability.source,triggerCost |-> q.paid.definition.triggerCost, beforeObjects |-> q.objects,afterObjects |-> q.objects,announced |-> TRUE,allPaid |-> ItemInspectionNativePaidT11(q,selected,after), additionalCostsPaid |-> TRUE,restrictionsBefore |-> TRUE,restrictionsAfter |-> TRUE,simultaneousProcedureComplete |-> TRUE, sourceAfter |-> 0,sourceUninstalled |-> FALSE,sourceForfeited |-> FALSE,paidOperations |-> {},publicEvents |-> {}] ItemInspectionPaidBeginDrainT11(q) == [tag |-> "MidItemInspectionBeginDrained",itemInspectionId |-> q.itemInspection.id,windowId |-> q.paid.windowId,checkpointId |-> q.paid.initialCheckpoint,complete |-> TRUE] ItemInspectionPaidCheckpointT11(p,id,complete) == [tag |-> "PaidCheckpoint",id |-> id,abilityInstance |-> p.id,transactionId |-> p.transaction, source |-> p.ability.source,phase |-> p.phase,complete |-> complete,allNewerChainsComplete |-> complete] ItemInspectionPaidPlanT11(p) == OpenInstruction93(700,"Ability",p.id,p.ability.source,p.ability.sourceZone,1,"NoValue",<<"MidEffect","MidTail">>,TRUE) ItemInspectionPaidTargetsT11(plan,objects) == [tag |-> "InstructionTargets",instruction |-> plan.id,abilityInstance |-> plan.abilityInstance, source |-> plan.source,sourceZone |-> plan.sourceZone,index |-> plan.index,valid |-> TRUE,targets |-> IF 1 \in DOMAIN objects THEN {1} ELSE {}] ItemInspectionPaidEntryT11(plan,checkpoint) == [tag |-> "AbilityInstructionEntry",abilityInstance |-> plan.abilityInstance,instruction |-> plan.id, source |-> plan.source,sourceZone |-> plan.sourceZone,index |-> plan.index,schedulerAllows |-> TRUE,sourceEligible |-> FALSE, checkpointAndAllNewerChainsComplete |-> TRUE,checkpointId |-> checkpoint] ItemInspectionPaidNoModifiersT11(plan) == [tag |-> "NoInstructionInterruptModifiers",instruction |-> InstructionWindowRef93(plan),conditionalInstances |-> {},paidInterruptAbilities |-> {}] ItemInspectionPaidInterruptReturnT11(plan) == [tag |-> "InstructionInterruptReturn",instruction |-> plan.id,revision |-> plan.revision,origin |-> plan.origin, abilityInstance |-> plan.abilityInstance,index |-> plan.index,source |-> plan.source,sourceZone |-> plan.sourceZone,windowId |-> 0,openingRevision |-> plan.revision,complete |-> TRUE] ItemInspectionPaidReturnT11(q) == [tag |-> "PriorityOptionReturn",windowId |-> q.paid.windowId,option |-> q.paid.option,transactionId |-> q.paid.transaction, triggerPayment |-> ItemInspectionMidPaymentFromStateT11(q),allCostsPaid |-> ItemInspectionCommittedCostT11(q,"Mid",q.cost.amount), optionComplete |-> q.paid.ability.complete,childrenReturned |-> q.plan.phase="Complete",reactionsDrained |-> q.paid.phase="Complete",finalCheckpointId |-> q.paid.checkpoint] ItemInspectionCostMovementProfileT11(NeutralValue00013) == NeutralValue00013 \in {"FacilityCostMove0","FacilityCostMove1"} ItemInspectionPaidMovementTransferT11(q,moved) == /\ q.cost.paid /\ ~q.cost.drained /\ q.paid.phase="CostCheckpoint" /\ q.itemInspection.midUsed /\ q.itemInspection.midResolving /\ CardBatchTransfer8(q.objects,moved,{1},[id \in {1} |-> 2],{1},"SideADiscard","Up",[id \in {1} |-> <<"SideADiscard",2>>]) ItemInspectionTemporalInitialT11(zone,entry,NeutralValue00013) == [itemInspection |-> ItemInspectionInitialT11(zone,IF ItemInspectionProfileObjectiveT11(NeutralValue00013) THEN "Objective" ELSE "Facility",0,0),objects |-> ItemInspectionObjectsT11(zone,IF ItemInspectionProfileObjectiveT11(NeutralValue00013) THEN "Objective" ELSE "Facility"), NeutralValue00013 |-> NeutralValue00013,entry |-> entry,stage |-> "Entry",resume |-> "NoValue",costResume |-> "NoValue",wallet |-> ItemInspectionWalletInitialT11,cost |-> [purpose |-> "NoValue"],nextCost |-> 1, paid |-> EmptyT11,plan |-> EmptyT11,uses |-> EmptyT11,turnUses |-> EmptyT11,useEvents |-> <<>>,paidPhases |-> <<>>,costReactionDone |-> FALSE, costHistory |-> <<>>,history |-> <<>>,events |-> <<>>,normalDrains |-> <<>>,windows |-> <<>>,midUses |-> 0,done |-> FALSE] ItemInspectionTemporalInitT11 == (guideCaseT11=0 /\ \E zone \in {"SideAHand","SideADeck"},entry \in {"NoValue","Zero","One"},NeutralValue00013 \in ItemInspectionProfilesT11 : qT11=ItemInspectionTemporalInitialT11(zone,entry,NeutralValue00013)) \/ (guideCaseT11=0 /\ \E NeutralValue00013 \in {"FacilityCostMove0","FacilityCostMove1"} : qT11=ItemInspectionTemporalInitialT11("SideAHand","NoValue",NeutralValue00013)) ItemInspectionTemporalWorkT11 == LET q==qT11 a==q.itemInspection objects==q.objects IN /\ ~qT11.done /\ UNCHANGED guideCaseT11 /\ CASE q.stage="Entry" -> qT11'=IF q.entry="NoValue" THEN [q EXCEPT !.stage="Begin"] ELSE ItemInspectionRequestCostT11(q,"Entry",IF q.entry="One" THEN 1 ELSE 0,"Begin") [] q.stage="PayCost" -> LET selected==IF q.cost.amount=0 THEN {} ELSE {ItemInspectionCostOwnerT11!Least(DOMAIN q.wallet.obj)} after==ItemInspectionWalletSpentT11(q.wallet,selected) IN /\ IF q.cost.purpose="Mid" THEN LET p==q.paid paid==ItemInspectionPaidCommittedFrameT11(p) used==[a EXCEPT !.midUsed=TRUE,!.midResolving=TRUE] mid==ItemInspectionTemporalMidT11(q) use==ItemInspectionPaidUseT11(p) IN /\ PayPaidMidItemInspection95(q.windows,p,paid,objects,objects,EmptyT11,EmptyT11,EmptyT11,DOMAIN objects, ItemInspectionPaidPaymentT11(q,selected,after),q.uses,ItemInspectionPaidUsesT11(p),q.turnUses,ItemInspectionPaidTurnUsesT11(p),1,{use}, a,used,mid,{mid},FALSE,FALSE,ItemInspectionPaidBeginDrainT11(q),{}) /\ qT11'=[q EXCEPT !.wallet=after,!.cost.before=q.wallet,!.cost.after=after,!.cost.selected=selected,!.cost.paid=TRUE, !.itemInspection=used,!.midUses=@+1,!.paid=paid,!.uses=ItemInspectionPaidUsesT11(p),!.turnUses=ItemInspectionPaidTurnUsesT11(p), !.useEvents=Append(@,use),!.paidPhases=Append(@,"CostCheckpoint"),!.stage=IF ItemInspectionCostMovementProfileT11(q.NeutralValue00013) THEN "CostReactionMove" ELSE "CostDrain"] ELSE qT11'=[q EXCEPT !.wallet=after,!.cost.before=q.wallet,!.cost.after=after,!.cost.selected=selected,!.cost.paid=TRUE,!.stage="CostDrain"] /\ ItemInspectionCostOwnerT11!DoSpendResourceUnits(ItemInspectionCostCommandT11(selected,q.cost.amount)) [] q.stage="CostDrain" -> /\ q.cost.paid /\ q.wallet=q.cost.after /\ q.wallet.checkpointDue /\ LET drained==[q EXCEPT !.wallet.checkpointDue=FALSE,!.cost.drained=TRUE, !.costHistory=Append(@,[id |-> q.cost.id,purpose |-> q.cost.purpose,amount |-> q.cost.amount,binding |-> q.cost.binding,selected |-> q.cost.selected]),!.stage=q.costResume] IN IF q.cost.purpose="Mid" THEN LET planning==[q.paid EXCEPT !.phase="Targets",!.checkpoint=300] IN /\ PaidCheckpoint95(q.windows,q.paid,planning,objects,EmptyT11, ItemInspectionPaidCheckpointT11(q.paid,300,~ItemInspectionCostMovementProfileT11(q.NeutralValue00013) \/ q.costReactionDone)) /\ qT11'=[drained EXCEPT !.paid=planning,!.paidPhases=Append(@,"Targets")] ELSE qT11'=drained [] q.stage="CostReactionMove" -> LET moved==ItemInspectionMovedObjectsT11(objects,"SideADiscard") ended==ItemInspectionEndedT11(a,"Moved") IN /\ ItemInspectionPaidMovementTransferT11(q,moved) /\ ItemInspectionMovementOutcome7(a,ended,moved,TRUE,{ItemInspectionEndEvent7(a)}) /\ qT11'=[q EXCEPT !.objects=moved,!.itemInspection=ended,!.events=Append(@,ItemInspectionEndEvent7(a)),!.costReactionDone=TRUE,!.stage="CostDrain"] [] q.stage="Begin" -> LET after==[a EXCEPT !.active=TRUE,!.beginMet=TRUE] paid==q.entry="NoValue" \/ ItemInspectionCommittedCostT11(q,"Entry",IF q.entry="One" THEN 1 ELSE 0) IN /\ BeginItemInspection7(a,after,objects,TRUE,paid,paid,{ItemInspectionBeginEvent7(a)}) /\ qT11'=ItemInspectionRecordWorkT11([q EXCEPT !.itemInspection=after,!.events=Append(@,ItemInspectionBeginEvent7(a))],"ProcedureCodefd91bef8bbd3","AddProgress") [] q.stage="NormalDrain" -> qT11'=[q EXCEPT !.normalDrains=Append(@,[step |-> q.history[Len(q.history)],ongoingItemInspection |-> StillItemInspectioning7(a,objects)]),!.stage=q.resume] [] q.stage="AddProgress" -> LET after==[a EXCEPT !.step=NextItemInspectionStep7(a.step)] next==CASE a.step="ProcedureCodefd91bef8bbd3" -> "OpenMid" [] a.step="ProcedureCode1dd0e8f05be2" -> "ClaimObjective" [] OTHER -> "Complete" IN /\ AdvanceItemInspectionStep7(a,after,objects,TRUE,TRUE) /\ qT11'=[q EXCEPT !.itemInspection=after,!.stage=next] [] q.stage="OpenMid" -> LET site==ItemInspectionPrioritySite9(TraversalTurnT11("SideA"),a,objects) w==ItemInspectionMidWindowT11(1,site) IN /\ OpenPriorityWindow9(q.windows,<>,1,"MidItemInspection",site,EmptyT11,ItemInspectionMidOpeningT11(1,site),{}) /\ qT11'=[q EXCEPT !.windows= <>,!.stage="MidCheckpoint"] [] q.stage="MidCheckpoint" -> LET w==WindowTop9(q.windows) ready==PriorityReadyT11(w) IN /\ CheckpointPriority9(q.windows,<>,PriorityCheckpointT11(w)) /\ qT11'=[q EXCEPT !.windows= <>,!.stage="MidChoose"] [] q.stage="MidChoose" -> LET w==WindowTop9(q.windows) mid==ItemInspectionTemporalMidT11(q) IN IF ~ItemInspectionProfileMidT11(q.NeutralValue00013) THEN LET after==[a EXCEPT !.midDone=TRUE] closed==ClosePriorityWindow9(w) IN /\ PassMidItemInspection9(q.windows,<>,a,after,objects,{mid},FALSE,FALSE) /\ qT11'=[q EXCEPT !.itemInspection=after,!.windows= <>,!.stage="PopMid"] ELSE LET d==ItemInspectionPaidDefinitionT11(q) option==ItemInspectionPaidOptionT11(q,w,d) busy==StartPriorityOptionFrame9(w,option,200) p==OpenPaidProcedure95(250,d,option,w,200,"Rule") reserved==[q EXCEPT !.windows= <>,!.paid=p,!.paidPhases= <<"PayCosts">>] IN /\ ReservePaidMidItemInspection95(q.windows,<>,p,250,d,ItemInspectionPaidContextT11(q,d),option,LegalityT11(w,option),{},a,a,mid,{mid},FALSE,FALSE) /\ qT11'=ItemInspectionRequestCostT11(reserved,"Mid",ItemInspectionProfileAmountT11(q.NeutralValue00013),"PaidTargets") [] q.stage="PaidTargets" -> LET p==q.paid plan==ItemInspectionPaidPlanT11(p) targets==ItemInspectionPaidTargetsT11(plan,objects) imminentPlan==[plan EXCEPT !.targets=targets.targets,!.announced=TRUE,!.phase="Imminent"] imminent==[p EXCEPT !.ability.phase="Imminent",!.ability.firstImminent=TRUE,!.phase="Imminent",!.checkpoint=0] IN /\ EnterPaidInstruction95(q.windows,p,imminent,plan,imminentPlan,targets,ItemInspectionPaidEntryT11(plan,p.checkpoint)) /\ qT11'=[q EXCEPT !.paid=imminent,!.plan=imminentPlan,!.paidPhases=Append(@,"Imminent"),!.stage="PaidInterrupt"] [] q.stage="PaidInterrupt" -> LET p==q.paid resolving==[p EXCEPT !.ability.phase="Resolving",!.phase="Resolve"] plan==[q.plan EXCEPT !.phase="Resolving"] IN /\ ResolvePaidWithoutInterrupt95(q.windows,p,resolving,q.plan,plan,ItemInspectionPaidNoModifiersT11(q.plan),ItemInspectionPaidInterruptReturnT11(q.plan)) /\ qT11'=[q EXCEPT !.paid=resolving,!.plan=plan,!.paidPhases=Append(@,"Resolve"),!.stage="MidBody"] [] q.stage="MidBody" -> LET p==q.paid plan==q.plan afterPlan==[plan EXCEPT !.completedSteps=Append(@,"MidEffect"),!.cursor=2] IN /\ CarryPaidInstruction95(q.windows,p,p,plan,afterPlan,[tag |-> "InstructionStepReturn",instruction |-> plan.id,index |-> 1,step |-> "MidEffect",complete |-> TRUE]) /\ IF ItemInspectionProfileRetireT11(q.NeutralValue00013) THEN LET moved==ItemInspectionMovedObjectsT11(objects,"SideADiscard") ended==ItemInspectionEndedT11(a,"Moved") IN /\ CardBatchTransfer8(objects,moved,{1},[id \in {1} |-> 2],{1},"SideADiscard","Up",[id \in {1} |-> <<"SideADiscard",2>>]) /\ ItemInspectionMovementOutcome7(a,ended,moved,TRUE,{ItemInspectionEndEvent7(a)}) /\ qT11'=[q EXCEPT !.plan=afterPlan,!.itemInspection=ended,!.objects=moved,!.events=Append(@,ItemInspectionEndEvent7(a)),!.stage="MidBodyTail"] ELSE qT11'=[q EXCEPT !.plan=afterPlan,!.stage="MidBodyTail"] [] q.stage="MidBodyTail" -> LET p==q.paid plan==q.plan afterPlan==[plan EXCEPT !.completedSteps=Append(@,"MidTail"),!.cursor=3,!.phase="Complete"] finished==[p EXCEPT !.ability.phase="Complete",!.ability.lastFinished=TRUE,!.ability.complete=TRUE,!.phase="InstructionCheckpoint",!.checkpoint=0] IN /\ CarryPaidInstruction95(q.windows,p,finished,plan,afterPlan,[tag |-> "InstructionStepReturn",instruction |-> plan.id,index |-> 2,step |-> "MidTail",complete |-> TRUE]) /\ qT11'=[q EXCEPT !.paid=finished,!.plan=afterPlan,!.paidPhases=Append(@,"InstructionCheckpoint"),!.stage="PaidFinalDrain"] [] q.stage="PaidFinalDrain" -> LET final==[q.paid EXCEPT !.phase="Complete",!.checkpoint=301] IN /\ PaidCheckpoint95(q.windows,q.paid,final,objects,EmptyT11,ItemInspectionPaidCheckpointT11(q.paid,301,TRUE)) /\ qT11'=[q EXCEPT !.paid=final,!.paidPhases=Append(@,"Complete"),!.stage="FinishMid"] [] q.stage="FinishMid" -> LET w==WindowTop9(q.windows) after==[a EXCEPT !.midResolving=FALSE,!.midDone=TRUE] returned==[q.paid EXCEPT !.ability.returned=TRUE,!.phase="Returned"] closed==CompletePriorityOptionFrame9(w) IN /\ FinishPaidMidItemInspection95(q.windows,<>,q.paid,returned,ItemInspectionPaidReturnT11(q),a,after) /\ qT11'=[q EXCEPT !.itemInspection=after,!.paid=returned,!.windows= <>,!.paidPhases=Append(@,"Returned"),!.stage="PopMid"] [] q.stage="PopMid" -> /\ PopClosedPriorityWindow9(q.windows,<<>>) /\ qT11'=ItemInspectionRecordWorkT11([q EXCEPT !.windows= <<>>],"ProcedureCode1dd0e8f05be2",IF a.complete THEN "Return" ELSE "AddProgress") [] q.stage="ClaimObjective" -> IF q.NeutralValue00013 \in {"ObjectiveCost0","ObjectiveCost1"} THEN qT11'=ItemInspectionRequestCostT11(q,"ClaimObjective",ItemInspectionProfileAmountT11(q.NeutralValue00013),"ClaimObjectiveBegin") ELSE IF q.NeutralValue00013="ObjectiveFree" THEN LET after==[a EXCEPT !.claimObjectiveResolving=TRUE] IN /\ ResolveItemInspectionClaimObjective7(a,after,objects,FALSE,FALSE,FALSE,TRUE,TRUE,FALSE) /\ qT11'=[q EXCEPT !.itemInspection=after,!.stage="ClaimObjectiveMove"] ELSE LET after==[a EXCEPT !.claimObjectiveDone=TRUE] IN /\ ResolveItemInspectionClaimObjective7(a,after,objects,q.NeutralValue00013="ObjectiveDecline",FALSE,TRUE,q.NeutralValue00013#"ObjectiveUnable",FALSE,FALSE) /\ qT11'=ItemInspectionRecordWorkT11([q EXCEPT !.itemInspection=after],"ProcedureCode546db7cc4546","AddProgress") [] q.stage="ClaimObjectiveBegin" -> LET after==[a EXCEPT !.claimObjectiveResolving=TRUE] paid==ItemInspectionCommittedCostT11(q,"ClaimObjective",ItemInspectionProfileAmountT11(q.NeutralValue00013)) IN /\ ResolveItemInspectionClaimObjective7(a,after,objects,TRUE,TRUE,TRUE,TRUE,paid,paid) /\ qT11'=[q EXCEPT !.itemInspection=after,!.stage="ClaimObjectiveMove"] [] q.stage="ClaimObjectiveMove" -> LET moved==ItemInspectionMovedObjectsT11(objects,"SideBObjectiveCompletion") ended==ItemInspectionEndedT11(a,"Moved") IN /\ CardBatchTransfer8(objects,moved,{1},[id \in {1} |-> 2],{1},"SideBObjectiveCompletion","Up",[id \in {1} |-> <<"SideBObjectiveCompletion",2>>]) /\ ItemInspectionMovementOutcome7(a,ended,moved,TRUE,{ItemInspectionEndEvent7(a)}) /\ qT11'=[q EXCEPT !.itemInspection=ended,!.objects=moved,!.events=Append(@,ItemInspectionEndEvent7(a)),!.stage="FinishClaimObjective"] [] q.stage="FinishClaimObjective" -> LET after==[a EXCEPT !.claimObjectiveResolving=FALSE,!.claimObjectiveDone=TRUE] IN /\ FinishItemInspectionClaimObjective7(a,after,TRUE) /\ qT11'=ItemInspectionRecordWorkT11([q EXCEPT !.itemInspection=after],"ProcedureCode546db7cc4546","Return") [] q.stage="Complete" -> LET after==ItemInspectionEndedT11(a,"Normal") IN /\ CompleteNormalItemInspection7(a,after,objects,TRUE,{ItemInspectionEndEvent7(a)}) /\ qT11'=ItemInspectionRecordWorkT11([q EXCEPT !.itemInspection=after,!.events=Append(@,ItemInspectionEndEvent7(a))],"ProcedureCode662478499367","Return") [] q.stage="Return" -> LET after==[a EXCEPT !.returned=TRUE] IN /\ ReturnItemInspectionToCaller7(a,after,TRUE,"ItemInspectionAuditCaller") /\ qT11'=[q EXCEPT !.itemInspection=after,!.done=TRUE,!.stage="Done"] ItemInspectionTemporalNextT11 == ItemInspectionTemporalWorkT11 \/ (qT11.done /\ UNCHANGED <>) ItemInspectionTemporalSpecT11 == ItemInspectionTemporalInitT11 /\ [][ItemInspectionTemporalNextT11]_<> /\ WF_<>(ItemInspectionTemporalNextT11) ItemInspectionTemporalSafetyT11 == /\ ItemInspectionProcedureValid7(qT11.itemInspection,qT11.objects) /\ qT11.itemInspection.object=1 /\ qT11.midUses \in 0..1 /\ \A i \in 1..Len(qT11.windows) : PriorityWindowValid9(qT11.windows[i]) /\ \A i \in 1..Len(qT11.normalDrains) : qT11.normalDrains[i].step=qT11.history[i] /\ Len(qT11.normalDrains) <= Len(qT11.history) /\ Len(qT11.history)-Len(qT11.normalDrains) \in 0..1 /\ (qT11.itemInspection.complete => ~StillItemInspectioning7(qT11.itemInspection,qT11.objects)) /\ (qT11.itemInspection.complete /\ qT11.itemInspection.midResolving => ~qT11.itemInspection.returned /\ qT11.stage \in {"CostDrain","PaidTargets","PaidInterrupt","MidBody","MidBodyTail","PaidFinalDrain","FinishMid"}) /\ (qT11.itemInspection.complete /\ qT11.itemInspection.claimObjectiveResolving => ~qT11.itemInspection.returned /\ qT11.stage="FinishClaimObjective") /\ qT11.itemInspection.beginMet=(Cardinality({i \in 1..Len(qT11.events) : qT11.events[i].tag="ItemInspectionCard"})=1) /\ qT11.itemInspection.complete=(Cardinality({i \in 1..Len(qT11.events) : qT11.events[i].tag="ItemInspectionEnds"})=1) /\ (qT11.done => /\ qT11.itemInspection.returned /\ qT11.itemInspection.complete /\ qT11.windows= <<>> /\ qT11.normalDrains[Len(qT11.normalDrains)].ongoingItemInspection=FALSE /\ Len(qT11.costHistory)=(IF qT11.entry="NoValue" THEN 0 ELSE 1)+(IF ItemInspectionProfileMidT11(qT11.NeutralValue00013) \/ qT11.NeutralValue00013 \in {"ObjectiveCost0","ObjectiveCost1"} THEN 1 ELSE 0) /\ Cardinality(DOMAIN qT11.wallet.obj)=3-(IF qT11.entry="One" THEN 1 ELSE 0)-ItemInspectionProfileAmountT11(qT11.NeutralValue00013) /\ IF ItemInspectionProfileRetireT11(qT11.NeutralValue00013) \/ ItemInspectionCostMovementProfileT11(qT11.NeutralValue00013) THEN qT11.history= <<"ProcedureCodefd91bef8bbd3","ProcedureCode1dd0e8f05be2">> /\ qT11.objects[2].zone="SideADiscard" ELSE IF qT11.NeutralValue00013 \in {"ObjectiveFree","ObjectiveCost0","ObjectiveCost1"} THEN qT11.history= <<"ProcedureCodefd91bef8bbd3","ProcedureCode1dd0e8f05be2","ProcedureCode546db7cc4546">> /\ qT11.objects[2].zone="SideBObjectiveCompletion" ELSE qT11.history=ItemInspectionOracleSteps11 /\ DOMAIN qT11.objects={1}) ItemInspectionPaidAtPaymentT11 == IF qT11.cost.purpose="Mid" THEN qT11.cost.paid => qT11.itemInspection.midUsed /\ qT11.midUses=1 ELSE TRUE ItemInspectionPaidLifecycleSafetyT11 == /\ ItemInspectionPaidAtPaymentT11 /\ qT11.midUses=Len(qT11.useEvents) /\ DOMAIN qT11.uses=(IF qT11.midUses=0 THEN {} ELSE {1}) /\ DOMAIN qT11.turnUses=DOMAIN qT11.uses /\ (qT11.midUses=1 => /\ qT11.uses=ItemInspectionPaidUsesT11(qT11.paid) /\ qT11.turnUses=ItemInspectionPaidTurnUsesT11(qT11.paid) /\ qT11.useEvents= <> /\ qT11.paid.costPaid /\ qT11.paid.ability.detached /\ qT11.cost.binding.itemInspection=qT11.itemInspection.id /\ qT11.cost.binding.object=qT11.itemInspection.object /\ qT11.cost.binding.caller=qT11.itemInspection.caller /\ qT11.cost.binding.transaction=qT11.paid.transaction /\ qT11.cost.binding.option=qT11.paid.option /\ qT11.cost.binding.window=qT11.paid.windowId /\ qT11.paid.ability.caller=qT11.paid.windowId /\ (ItemInspectionCostMovementProfileT11(qT11.NeutralValue00013) /\ qT11.paid.phase#"CostCheckpoint" => qT11.costReactionDone) /\ qT11.cost.after=ItemInspectionWalletSpentT11(qT11.cost.before,qT11.cost.selected) /\ ItemInspectionCostOwnerT11!SpendResourceUnitsOK(qT11.cost.before,"SideB",qT11.cost.selected,qT11.cost.amount,{}) /\ qT11.wallet=(IF qT11.cost.drained THEN [qT11.cost.after EXCEPT !.checkpointDue=FALSE] ELSE qT11.cost.after)) /\ (qT11.midUses=1 /\ ~qT11.cost.drained => /\ qT11.paid.phase="CostCheckpoint" /\ qT11.itemInspection.midResolving /\ ~qT11.paid.ability.firstImminent /\ ~AbilityIsResolving9(qT11.paid.ability)) /\ (qT11.midUses=1 /\ qT11.paid.ability.firstImminent => qT11.cost.drained) /\ (ItemInspectionCostMovementProfileT11(qT11.NeutralValue00013) /\ qT11.costReactionDone => /\ qT11.itemInspection.complete /\ qT11.itemInspection.completionReason="Moved" /\ ~StillItemInspectioning7(qT11.itemInspection,qT11.objects) /\ qT11.itemInspection.object=1 /\ DOMAIN qT11.objects={2} /\ ~ItemInspectionTargetPresent7(qT11.itemInspection,qT11.objects) /\ (qT11.paid.ability.firstImminent => qT11.plan.targets={}) /\ qT11.history=IF qT11.stage \in {"Return","Done","NormalDrain"} THEN <<"ProcedureCodefd91bef8bbd3","ProcedureCode1dd0e8f05be2">> ELSE <<"ProcedureCodefd91bef8bbd3">>) /\ (qT11.midUses=1 /\ qT11.itemInspection.midDone => /\ qT11.paid.phase="Returned" /\ qT11.paid.ability.returned /\ qT11.paid.ability.lastFinished /\ qT11.paid.checkpoint=301 /\ qT11.plan.completedSteps= <<"MidEffect","MidTail">> /\ qT11.paidPhases= <<"PayCosts","CostCheckpoint","Targets","Imminent","Resolve","InstructionCheckpoint","Complete","Returned">>) ItemInspectionNativeLedgerSafetyT11 == LET history==qT11.costHistory committed==UNION {history[i].selected : i \in 1..Len(history)} pending==IF qT11.cost.purpose="NoValue" THEN {} ELSE IF qT11.cost.paid /\ ~qT11.cost.drained THEN qT11.cost.selected ELSE {} IN /\ DOMAIN qT11.wallet.past=committed \cup pending /\ DOMAIN qT11.wallet.obj \cap DOMAIN qT11.wallet.past={} /\ DOMAIN qT11.wallet.obj \cup DOMAIN qT11.wallet.past={100,101,102} /\ \A i \in 1..Len(history) : history[i].id=i /\ Cardinality(history[i].selected)=history[i].amount /\ \A i,j \in 1..Len(history) : i#j => history[i].selected \cap history[j].selected={} /\ pending \cap committed={} ItemInspectionTemporalTerminatesT11 == <>qT11.done ItemInspectionPreparedCostT11 == LET a==[ItemInspectionWorkedT11("ProcedureCode1dd0e8f05be2") EXCEPT !.midDone=FALSE] objects==ItemInspectionObjectsT11("SideAHand","Facility") mid==MidOption7("SyntheticObserve",FALSE,TRUE,TRUE) w==PriorityReadyT11(ItemInspectionMidWindowT11(1,ItemInspectionPrioritySite9(TraversalTurnT11("SideA"),a,objects))) option==ItemInspectionPriorityOptionT11(a,mid,"SideB","MidItemInspection") busy==StartPriorityOptionFrame9(w,option,200) q==[ItemInspectionTemporalInitialT11("SideAHand","NoValue","FacilityObserve1") EXCEPT !.itemInspection=a,!.windows= <>,!.history= <<"ProcedureCodefd91bef8bbd3">>,!.normalDrains= <<[step |-> "ProcedureCodefd91bef8bbd3",ongoingItemInspection |-> TRUE]>>,!.events= <>,!.resume="AddProgress"] requested==ItemInspectionRequestCostT11(q,"Mid",1,"UseMid") after==ItemInspectionWalletSpentT11(q.wallet,{100}) IN [requested EXCEPT !.wallet=[after EXCEPT !.checkpointDue=FALSE],!.cost.before=q.wallet,!.cost.after=after,!.cost.selected={100},!.cost.paid=TRUE,!.cost.drained=TRUE,!.costHistory= <<[id |-> 1,purpose |-> "Mid",amount |-> 1,binding |-> requested.cost.binding,selected |-> {100}]>>,!.stage="UseMid"] ItemInspectionStoredPaymentChecksT11 == LET q==ItemInspectionPreparedCostT11 a==q.itemInspection used==[a EXCEPT !.midUsed=TRUE,!.midResolving=TRUE] mid==ItemInspectionTemporalMidT11(q) wrong==[q EXCEPT !.cost.binding.transaction=201] IN /\ ItemInspectionCommittedCostT11(q,"Mid",1) /\ PayMidItemInspectionOption9(q.windows,a,used,q.objects,mid,{mid},FALSE,FALSE,ItemInspectionMidPaymentFromStateT11(q)) /\ ~ItemInspectionCommittedCostT11(wrong,"Mid",1) /\ ~PayMidItemInspectionOption9(q.windows,a,used,q.objects,mid,{mid},FALSE,FALSE,ItemInspectionMidPaymentFromStateT11(wrong)) /\ ~ItemInspectionCommittedCostT11([q EXCEPT !.cost.paid=FALSE],"Mid",1) /\ ~ItemInspectionCommittedCostT11([q EXCEPT !.cost.drained=FALSE],"Mid",1) ItemInspectionPointwiseChecksT11 == ItemInspectionPointwiseBaseChecksT11 /\ (guideCaseT11=7 => ItemInspectionStoredPaymentChecksT11) =============================================================================