--------------------- MODULE CommitmentProbesMC --------------------- EXTENDS ItemTimingMC PaidProbeBeforeT11(NeutralValue00013) == LET base==ItemInspectionTemporalInitialT11("SideAHand","NoValue",NeutralValue00013) a==[base.itemInspection EXCEPT !.active=TRUE,!.beginMet=TRUE,!.step="ProcedureCode1dd0e8f05be2"] q==[base EXCEPT !.itemInspection=a,!.history= <<"ProcedureCodefd91bef8bbd3">>,!.normalDrains= <<[step |-> "ProcedureCodefd91bef8bbd3",ongoingItemInspection |-> TRUE]>>,!.events= <>] d==ItemInspectionPaidDefinitionT11(q) w==PriorityReadyT11(ItemInspectionMidWindowT11(1,ItemInspectionPrioritySite9(TraversalTurnT11("SideA"),a,q.objects))) option==ItemInspectionPaidOptionT11(q,w,d) busy==StartPriorityOptionFrame9(w,option,200) p==OpenPaidProcedure95(250,d,option,w,200,"Rule") IN ItemInspectionRequestCostT11([q EXCEPT !.windows= <>,!.paid=p,!.paidPhases= <<"PayCosts">>],"Mid",ItemInspectionProfileAmountT11(NeutralValue00013),"PaidTargets") PaidProbeSelectedT11(q) == IF q.cost.amount=0 THEN {} ELSE {100} PaidProbeNativeAfterT11(q) == ItemInspectionWalletSpentT11(q.wallet,PaidProbeSelectedT11(q)) PaidProbePayT11(q,payment,begin,afterUses,afterTurnUses,events) == LET p==q.paid mid==ItemInspectionTemporalMidT11(q) used==[q.itemInspection EXCEPT !.midUsed=TRUE,!.midResolving=TRUE] IN PayPaidMidItemInspection95(q.windows,p,ItemInspectionPaidCommittedFrameT11(p),q.objects,q.objects,EmptyT11,EmptyT11,EmptyT11,DOMAIN q.objects, payment,q.uses,afterUses,q.turnUses,afterTurnUses,1,events,q.itemInspection,used,mid,{mid},FALSE,FALSE,begin,{}) PaidProbeAdmissionT11(q) == PaidProbePayT11(q,ItemInspectionPaidPaymentT11(q,PaidProbeSelectedT11(q),PaidProbeNativeAfterT11(q)),ItemInspectionPaidBeginDrainT11(q), ItemInspectionPaidUsesT11(q.paid),ItemInspectionPaidTurnUsesT11(q.paid),{ItemInspectionPaidUseT11(q.paid)}) PaidProbePaidT11(NeutralValue00013) == LET q==PaidProbeBeforeT11(NeutralValue00013) after==PaidProbeNativeAfterT11(q) p==q.paid IN [q EXCEPT !.wallet=after,!.cost.before=q.wallet,!.cost.after=after,!.cost.selected=PaidProbeSelectedT11(q),!.cost.paid=TRUE, !.paid=ItemInspectionPaidCommittedFrameT11(p),!.itemInspection.midUsed=TRUE,!.itemInspection.midResolving=TRUE,!.midUses=1, !.uses=ItemInspectionPaidUsesT11(p),!.turnUses=ItemInspectionPaidTurnUsesT11(p),!.useEvents= <>,!.paidPhases= <<"PayCosts","CostCheckpoint">>,!.stage="CostDrain"] PaidProbePaymentChecksT11 == \A NeutralValue00013 \in {"FacilityObserve0","FacilityObserve1","FacilityRetire0","FacilityRetire1"} : LET q==PaidProbeBeforeT11(NeutralValue00013) p==q.paid payment==ItemInspectionPaidPaymentT11(q,PaidProbeSelectedT11(q),PaidProbeNativeAfterT11(q)) begin==ItemInspectionPaidBeginDrainT11(q) uses==ItemInspectionPaidUsesT11(p) turnUses==ItemInspectionPaidTurnUsesT11(p) events=={ItemInspectionPaidUseT11(p)} wrongs=={[payment EXCEPT !.abilityInstance=251],[payment EXCEPT !.transactionId=201], [payment EXCEPT !.ability="WrongAbility"],[payment EXCEPT !.source=RuleAbilitySource9("WrongSource")], [payment EXCEPT !.triggerCost= <<[kind |-> "ResourceUnits",amount |-> 2]>>],[payment EXCEPT !.beforeObjects=EmptyT11], [payment EXCEPT !.afterObjects=EmptyT11],[payment EXCEPT !.allPaid=FALSE],[payment EXCEPT !.additionalCostsPaid=FALSE], [payment EXCEPT !.announced=FALSE],[payment EXCEPT !.simultaneousProcedureComplete=FALSE]} IN /\ PaidProbeAdmissionT11(q) /\ \A bad \in wrongs : ~PaidProbePayT11(q,bad,begin,uses,turnUses,events) /\ ~PaidProbePayT11(q,payment,begin,EmptyT11,turnUses,events) /\ ~PaidProbePayT11(q,payment,begin,uses,EmptyT11,events) /\ ~PaidProbePayT11(q,payment,begin,uses,turnUses,{}) /\ ~PaidProbePayT11(q,payment,begin,[uses EXCEPT ![1].source=RuleAbilitySource9("WrongSource")],turnUses,events) /\ ~PaidProbePayT11(q,payment,begin,uses,[turnUses EXCEPT ![1].turnId=3],events) /\ \A bad \in {[begin EXCEPT !.itemInspectionId=78],[begin EXCEPT !.windowId=2],[begin EXCEPT !.checkpointId=0], [begin EXCEPT !.checkpointId=999],[begin EXCEPT !.complete=FALSE]} : ~PaidProbePayT11(q,payment,bad,uses,turnUses,events) /\ ~PaidProbeAdmissionT11([q EXCEPT !.uses=uses,!.turnUses=turnUses]) /\ ~PaidProbeAdmissionT11([q EXCEPT !.itemInspection.midUsed=TRUE,!.itemInspection.midResolving=TRUE]) /\ ~PayPaidTrigger95(q.windows,p,ItemInspectionPaidCommittedFrameT11(p),q.objects,q.objects,EmptyT11,EmptyT11,EmptyT11,DOMAIN q.objects, payment,q.uses,uses,q.turnUses,turnUses,1,events) /\ \A bad \in { [q EXCEPT !.cost.binding.itemInspection=78],[q EXCEPT !.cost.binding.object=2],[q EXCEPT !.cost.binding.caller="WrongCaller"], [q EXCEPT !.cost.binding.window=2],[q EXCEPT !.cost.binding.reception=99],[q EXCEPT !.cost.binding.transaction=201], [q EXCEPT !.cost.binding.option.target=2],[q EXCEPT !.cost.purpose="Entry"],[q EXCEPT !.cost.amount=2], [q EXCEPT !.itemInspection.id=78],[q EXCEPT !.itemInspection.object=2],[q EXCEPT !.itemInspection.caller="WrongCaller"], [q EXCEPT !.windows[1].id=2],[q EXCEPT !.windows[1].reception=99],[q EXCEPT !.windows[1].site.structure.id=78], [q EXCEPT !.paid.transaction=201],[q EXCEPT !.paid.initialCheckpoint=999],[q EXCEPT !.paid.ability.caller=2], [q EXCEPT !.paid.ability.source=RuleAbilitySource9("WrongSource")], [q EXCEPT !.wallet.obj[100].virtual=TRUE,!.cost.before.obj[100].virtual=TRUE]} : IF bad.wallet.obj[100].virtual /\ q.cost.amount=0 THEN PaidProbeAdmissionT11(bad) ELSE ~PaidProbeAdmissionT11(bad) PaidProbeFramesT11(NeutralValue00013) == LET q==PaidProbePaidT11(NeutralValue00013) p==q.paid planning==[p EXCEPT !.phase="Targets",!.checkpoint=300] plan==ItemInspectionPaidPlanT11(p) targets==ItemInspectionPaidTargetsT11(plan,q.objects) imminentPlan==[plan EXCEPT !.targets=targets.targets,!.announced=TRUE,!.phase="Imminent"] imminent==[planning EXCEPT !.phase="Imminent",!.checkpoint=0,!.ability.phase="Imminent",!.ability.firstImminent=TRUE] resolving==[imminent EXCEPT !.phase="Resolve",!.ability.phase="Resolving"] resolvingPlan==[imminentPlan EXCEPT !.phase="Resolving"] tailPlan==[resolvingPlan EXCEPT !.completedSteps= <<"MidEffect">>,!.cursor=2] finishedPlan==[tailPlan EXCEPT !.completedSteps= <<"MidEffect","MidTail">>,!.cursor=3,!.phase="Complete"] finished==[resolving EXCEPT !.phase="InstructionCheckpoint",!.ability.phase="Complete",!.ability.complete=TRUE,!.ability.lastFinished=TRUE] final==[finished EXCEPT !.phase="Complete",!.checkpoint=301] IN [q |-> q,planning |-> planning,plan |-> plan,targets |-> targets,imminent |-> imminent,imminentPlan |-> imminentPlan, resolving |-> resolving,resolvingPlan |-> resolvingPlan,tailPlan |-> tailPlan,finished |-> finished,finishedPlan |-> finishedPlan,final |-> final] PaidProbeLifecycleChecksT11 == LET f==PaidProbeFramesT11("FacilityObserve1") q==f.q stack==q.windows p==q.paid IN /\ PaidCheckpoint95(stack,p,f.planning,q.objects,EmptyT11,ItemInspectionPaidCheckpointT11(p,300,TRUE)) /\ \A bad \in {[ItemInspectionPaidCheckpointT11(p,300,TRUE) EXCEPT !.complete=FALSE], [ItemInspectionPaidCheckpointT11(p,300,TRUE) EXCEPT !.allNewerChainsComplete=FALSE], [ItemInspectionPaidCheckpointT11(p,300,TRUE) EXCEPT !.transactionId=201], [ItemInspectionPaidCheckpointT11(p,300,TRUE) EXCEPT !.abilityInstance=251], [ItemInspectionPaidCheckpointT11(p,300,TRUE) EXCEPT !.source=RuleAbilitySource9("WrongSource")], [ItemInspectionPaidCheckpointT11(p,300,TRUE) EXCEPT !.phase="InstructionCheckpoint"], [ItemInspectionPaidCheckpointT11(p,300,TRUE) EXCEPT !.id=0]} : ~PaidCheckpoint95(stack,p,f.planning,q.objects,EmptyT11,bad) /\ ~EnterPaidInstruction95(stack,p,f.imminent,f.plan,f.imminentPlan,f.targets,ItemInspectionPaidEntryT11(f.plan,0)) /\ EnterPaidInstruction95(stack,f.planning,f.imminent,f.plan,f.imminentPlan,f.targets,ItemInspectionPaidEntryT11(f.plan,300)) /\ \A bad \in {[ItemInspectionPaidEntryT11(f.plan,300) EXCEPT !.checkpointId=299], [ItemInspectionPaidEntryT11(f.plan,300) EXCEPT !.instruction=701],[ItemInspectionPaidEntryT11(f.plan,300) EXCEPT !.source=RuleAbilitySource9("WrongSource")]} : ~EnterPaidInstruction95(stack,f.planning,f.imminent,f.plan,f.imminentPlan,f.targets,bad) /\ ~EnterPaidInstruction95(stack,f.planning,f.imminent,f.plan,f.imminentPlan,[f.targets EXCEPT !.valid=FALSE],ItemInspectionPaidEntryT11(f.plan,300)) /\ ResolvePaidWithoutInterrupt95(stack,f.imminent,f.resolving,f.imminentPlan,f.resolvingPlan,ItemInspectionPaidNoModifiersT11(f.imminentPlan),ItemInspectionPaidInterruptReturnT11(f.imminentPlan)) /\ ~ResolvePaidWithoutInterrupt95(stack,f.imminent,f.resolving,f.imminentPlan,f.resolvingPlan, [ItemInspectionPaidNoModifiersT11(f.imminentPlan) EXCEPT !.paidInterruptAbilities={55}],ItemInspectionPaidInterruptReturnT11(f.imminentPlan)) /\ ~ResolvePaidWithoutInterrupt95(stack,f.imminent,f.resolving,f.imminentPlan,f.resolvingPlan, ItemInspectionPaidNoModifiersT11(f.imminentPlan),[ItemInspectionPaidInterruptReturnT11(f.imminentPlan) EXCEPT !.complete=FALSE]) /\ CarryPaidInstruction95(stack,f.resolving,f.resolving,f.resolvingPlan,f.tailPlan, [tag |-> "InstructionStepReturn",instruction |-> 700,index |-> 1,step |-> "MidEffect",complete |-> TRUE]) /\ CarryPaidInstruction95(stack,f.resolving,f.finished,f.tailPlan,f.finishedPlan, [tag |-> "InstructionStepReturn",instruction |-> 700,index |-> 2,step |-> "MidTail",complete |-> TRUE]) /\ ~CarryPaidInstruction95(stack,f.resolving,f.finished,f.tailPlan,f.finishedPlan, [tag |-> "InstructionStepReturn",instruction |-> 700,index |-> 2,step |-> "MidTail",complete |-> FALSE]) /\ ~CarryPaidInstruction95(stack,f.resolving,f.finished,f.tailPlan,f.finishedPlan, [tag |-> "InstructionStepReturn",instruction |-> 700,index |-> 1,step |-> "MidEffect",complete |-> TRUE]) /\ PaidCheckpoint95(stack,f.finished,f.final,q.objects,EmptyT11,ItemInspectionPaidCheckpointT11(f.finished,301,TRUE)) /\ ~PaidCheckpoint95(stack,f.resolving,f.final,q.objects,EmptyT11,ItemInspectionPaidCheckpointT11(f.resolving,301,TRUE)) PaidProbeReturnQ_T11(NeutralValue00013) == LET f==PaidProbeFramesT11(NeutralValue00013) q==f.q after==[q.cost.after EXCEPT !.checkpointDue=FALSE] IN [q EXCEPT !.paid=f.final,!.plan=f.finishedPlan,!.wallet=after,!.cost.drained=TRUE, !.paidPhases= <<"PayCosts","CostCheckpoint","Targets","Imminent","Resolve","InstructionCheckpoint","Complete">>,!.stage="FinishMid"] PaidProbeFinishT11(q,receipt) == LET p==q.paid returned==[p EXCEPT !.ability.returned=TRUE,!.phase="Returned"] a==q.itemInspection after==[a EXCEPT !.midResolving=FALSE,!.midDone=TRUE] IN FinishPaidMidItemInspection95(q.windows,<>,p,returned,receipt,a,after) PaidProbeReturnAdmissionT11(q) == PaidProbeFinishT11(q,ItemInspectionPaidReturnT11(q)) PaidProbeReturnChecksT11 == LET q==PaidProbeReturnQ_T11("FacilityObserve1") receipt==ItemInspectionPaidReturnT11(q) IN /\ PaidProbeReturnAdmissionT11(q) /\ \A bad \in {[receipt EXCEPT !.windowId=2],[receipt EXCEPT !.transactionId=201],[receipt EXCEPT !.option.target=2], [receipt EXCEPT !.finalCheckpointId=300],[receipt EXCEPT !.childrenReturned=FALSE], [receipt EXCEPT !.reactionsDrained=FALSE],[receipt EXCEPT !.optionComplete=FALSE], [receipt EXCEPT !.triggerPayment.costCheckpointAndReactionsDrained=FALSE]} : ~PaidProbeFinishT11(q,bad) /\ \A bad \in {[q EXCEPT !.itemInspection.id=78],[q EXCEPT !.itemInspection.object=2],[q EXCEPT !.itemInspection.caller="WrongCaller"], [q EXCEPT !.windows[1].site.structure.id=78],[q EXCEPT !.windows[1].id=2], [q EXCEPT !.paid.ability.caller=2],[q EXCEPT !.paid.transaction=201], [q EXCEPT !.paid.phase="InstructionCheckpoint"],[q EXCEPT !.paid.phase="Resolve"], [q EXCEPT !.paid.phase="Imminent"],[q EXCEPT !.paid.ability.returned=TRUE], [q EXCEPT !.plan.phase="Resolving"],[q EXCEPT !.cost.drained=FALSE]} : ~PaidProbeReturnAdmissionT11(bad) PaidProbeMovementChecksT11 == LET q==PaidProbePaidT11("FacilityCostMove1") a==q.itemInspection moved==ItemInspectionMovedObjectsT11(q.objects,"SideADiscard") ended==ItemInspectionEndedT11(a,"Moved") after==[ended EXCEPT !.midResolving=FALSE,!.midDone=TRUE] finalQ==[PaidProbeReturnQ_T11("FacilityCostMove1") EXCEPT !.objects=moved,!.itemInspection=ended] IN /\ ItemInspectionPaidMovementTransferT11(q,moved) /\ ItemInspectionMovementOutcome7(a,ended,moved,TRUE,{ItemInspectionEndEvent7(a)}) /\ ~StillItemInspectioning7(ended,moved) /\ ended.midResolving /\ ended.object=1 /\ DOMAIN moved={2} /\ ~ReturnItemInspectionToCaller7(ended,[ended EXCEPT !.returned=TRUE],TRUE,"ItemInspectionAuditCaller") /\ ~AdvanceItemInspectionStep7(ended,[ended EXCEPT !.step="ProcedureCode546db7cc4546"],moved,TRUE,TRUE) /\ ~CompleteNormalItemInspection7(ended,ended,moved,TRUE,{ItemInspectionEndEvent7(ended)}) /\ ~ItemInspectionTargetPresent7(ended,moved) /\ ~WindowSiteAllowed9("MidItemInspection",ItemInspectionPrioritySite9(TraversalTurnT11("SideA"),ended,moved)) /\ ~CardBatchTransfer8(q.objects,[id \in {1} |-> moved[2]],{1},[id \in {1} |-> 1],{1},"SideADiscard","Up",[id \in {1} |-> <<"SideADiscard",2>>]) /\ PaidProbeReturnAdmissionT11(finalQ) /\ ~PaidProbeReturnAdmissionT11([finalQ EXCEPT !.itemInspection.object=2]) /\ ReturnItemInspectionToCaller7(after,[after EXCEPT !.returned=TRUE],TRUE,"ItemInspectionAuditCaller") /\ ~ReturnItemInspectionToCaller7(after,[after EXCEPT !.returned=TRUE],TRUE,"WrongCaller") /\ ~ReturnItemInspectionToCaller7([after EXCEPT !.returned=TRUE],[after EXCEPT !.returned=TRUE],TRUE,"ItemInspectionAuditCaller") PaidProbeOrdinaryControlsT11 == /\ \A NeutralValue00013 \in {"FacilityObserve0","FacilityObserve1","FacilityRetire0","FacilityRetire1"} : /\ PaidProbeAdmissionT11(PaidProbeBeforeT11(NeutralValue00013)) /\ PaidProbeReturnAdmissionT11(PaidProbeReturnQ_T11(NeutralValue00013)) /\ LET q==PaidProbePaidT11("FacilityCostMove1") moved==ItemInspectionMovedObjectsT11(q.objects,"SideADiscard") IN ItemInspectionPaidMovementTransferT11(q,moved) PaidProbeInitT11 == guideCaseT11 \in 1..4 /\ qT11=EmptyT11 PaidProbeNextT11 == UNCHANGED <> PaidProbeSpecT11 == PaidProbeInitT11 /\ [][PaidProbeNextT11]_<> PaidProbeChecksT11 == CASE guideCaseT11=1 -> PaidProbePaymentChecksT11 [] guideCaseT11=2 -> PaidProbeLifecycleChecksT11 [] guideCaseT11=3 -> PaidProbeReturnChecksT11 [] OTHER -> PaidProbeMovementChecksT11 =============================================================================