r1 qualified Selected asymmetric formal reference: 2,502 contracts across nine families; bounded evidence and three separate teaching models Read the evidence scope

CommitmentProbesMC¶

Complete selected asymmetric reference profile. Definitions and supplied fixtures are distinct from the three teaching specializations; review and qualification are stated in the bound evidence and release.

Package reference-profile, input revision 2. Exact prepared source; CC0 1.0.

This is a definition inventory. Start with the learning chapters for the contract and its assumptions.

This model/fact module also contains 56 local fixture helpers outside the selected contract inventory. Their complete executable text remains in the exact module download and owning definition bodies. Listed dependencies include paths through those helpers. All selected contracts and frozen nested helpers retain their own entries.

PaidProbeAdmissionT11 · operator

reference-profile · input revision 2 · CC0 1.0

PaidProbeAdmissionT11(q) == PaidProbePayT11(q,ItemInspectionPaidPaymentT11(q,PaidProbeSelectedT11(q),PaidProbeNativeAfterT11(q)),ItemInspectionPaidBeginDrainT11(q),
 ItemInspectionPaidUsesT11(q.paid),ItemInspectionPaidTurnUsesT11(q.paid),{ItemInspectionPaidUseT11(q.paid)})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidProbeNativeAfterT11, PaidProbePayT11, PaidProbeSelectedT11, ItemInspectionPaidBeginDrainT11, ItemInspectionPaidPaymentT11, ItemInspectionPaidTurnUsesT11, ItemInspectionPaidUseT11, ItemInspectionPaidUsesT11

PaidProbeBeforeT11 · operator

reference-profile · input revision 2 · CC0 1.0

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= <<ItemInspectionBeginEvent7(a)>>]
     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= <<busy>>,!.paid=p,!.paidPhases= <<"PayCosts">>],"Mid",ItemInspectionProfileAmountT11(NeutralValue00013),"PaidTargets")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionPrioritySite9, OpenPaidProcedure95, StartPriorityOptionFrame9, ItemInspectionBeginEvent7, ItemInspectionMidWindowT11, ItemInspectionPaidDefinitionT11, ItemInspectionPaidOptionT11, ItemInspectionProfileAmountT11, ItemInspectionRequestCostT11, ItemInspectionTemporalInitialT11, PriorityReadyT11, TraversalTurnT11

PaidProbeChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

PaidProbeChecksT11 == CASE guideCaseT11=1 -> PaidProbePaymentChecksT11 [] guideCaseT11=2 -> PaidProbeLifecycleChecksT11 [] guideCaseT11=3 -> PaidProbeReturnChecksT11 [] OTHER -> PaidProbeMovementChecksT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidProbeLifecycleChecksT11, PaidProbeMovementChecksT11, PaidProbePaymentChecksT11, PaidProbeReturnChecksT11, guideCaseT11

PaidProbeFinishT11 · operator

reference-profile · input revision 2 · CC0 1.0

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,<<CompletePriorityOptionFrame9(WindowTop9(q.windows))>>,p,returned,receipt,a,after)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CompletePriorityOptionFrame9, FinishPaidMidItemInspection95, WindowTop9

PaidProbeFramesT11 · operator

reference-profile · input revision 2 · CC0 1.0

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]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidProbePaidT11, ItemInspectionPaidPlanT11, ItemInspectionPaidTargetsT11

PaidProbeInitT11 · operator

reference-profile · input revision 2 · CC0 1.0

PaidProbeInitT11 == guideCaseT11 \in 1..4 /\ qT11=EmptyT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyT11, guideCaseT11, qT11

PaidProbeLifecycleChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

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))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CarryPaidInstruction95, EnterPaidInstruction95, PaidCheckpoint95, ResolvePaidWithoutInterrupt95, RuleAbilitySource9, PaidProbeFramesT11, ItemInspectionPaidCheckpointT11, ItemInspectionPaidEntryT11, ItemInspectionPaidInterruptReturnT11, ItemInspectionPaidNoModifiersT11, EmptyT11

PaidProbeMovementChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

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")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionPrioritySite9, WindowSiteAllowed9, PaidProbePaidT11, PaidProbeReturnAdmissionT11, PaidProbeReturnQ_T11, AdvanceItemInspectionStep7, CompleteNormalItemInspection7, ItemInspectionEndEvent7, ItemInspectionMovementOutcome7, ItemInspectionTargetPresent7, ReturnItemInspectionToCaller7, StillItemInspectioning7, ItemInspectionEndedT11, ItemInspectionMovedObjectsT11, ItemInspectionPaidMovementTransferT11, CardBatchTransfer8, TraversalTurnT11

PaidProbeNativeAfterT11 · operator

reference-profile · input revision 2 · CC0 1.0

PaidProbeNativeAfterT11(q) == ItemInspectionWalletSpentT11(q.wallet,PaidProbeSelectedT11(q))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidProbeSelectedT11, ItemInspectionWalletSpentT11

PaidProbeNextT11 · operator

reference-profile · input revision 2 · CC0 1.0

PaidProbeNextT11 == UNCHANGED <<guideCaseT11,qT11>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: guideCaseT11, qT11

PaidProbeOrdinaryControlsT11 · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidProbeAdmissionT11, PaidProbeBeforeT11, PaidProbePaidT11, PaidProbeReturnAdmissionT11, PaidProbeReturnQ_T11, ItemInspectionMovedObjectsT11, ItemInspectionPaidMovementTransferT11

PaidProbePaidT11 · operator

reference-profile · input revision 2 · CC0 1.0

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= <<ItemInspectionPaidUseT11(p)>>,!.paidPhases= <<"PayCosts","CostCheckpoint">>,!.stage="CostDrain"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidProbeBeforeT11, PaidProbeNativeAfterT11, PaidProbeSelectedT11, ItemInspectionPaidCommittedFrameT11, ItemInspectionPaidTurnUsesT11, ItemInspectionPaidUseT11, ItemInspectionPaidUsesT11

PaidProbePayT11 · operator

reference-profile · input revision 2 · CC0 1.0

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,{})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PayPaidMidItemInspection95, ItemInspectionPaidCommittedFrameT11, ItemInspectionTemporalMidT11, EmptyT11

PaidProbePaymentChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PayPaidTrigger95, RuleAbilitySource9, PaidProbeAdmissionT11, PaidProbeBeforeT11, PaidProbeNativeAfterT11, PaidProbePayT11, PaidProbeSelectedT11, ItemInspectionPaidBeginDrainT11, ItemInspectionPaidCommittedFrameT11, ItemInspectionPaidPaymentT11, ItemInspectionPaidTurnUsesT11, ItemInspectionPaidUseT11, ItemInspectionPaidUsesT11, EmptyT11

PaidProbeReturnAdmissionT11 · operator

reference-profile · input revision 2 · CC0 1.0

PaidProbeReturnAdmissionT11(q) == PaidProbeFinishT11(q,ItemInspectionPaidReturnT11(q))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidProbeFinishT11, ItemInspectionPaidReturnT11

PaidProbeReturnChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidProbeFinishT11, PaidProbeReturnAdmissionT11, PaidProbeReturnQ_T11, ItemInspectionPaidReturnT11

PaidProbeReturnQ_T11 · operator

reference-profile · input revision 2 · CC0 1.0

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"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidProbeFramesT11

PaidProbeSelectedT11 · operator

reference-profile · input revision 2 · CC0 1.0

PaidProbeSelectedT11(q) == IF q.cost.amount=0 THEN {} ELSE {100}

Exact module download · Source bundle and reproduction instructions

PaidProbeSpecT11 · operator

reference-profile · input revision 2 · CC0 1.0

PaidProbeSpecT11 == PaidProbeInitT11 /\ [][PaidProbeNextT11]_<<guideCaseT11,qT11>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidProbeInitT11, PaidProbeNextT11, guideCaseT11, qT11