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

InspectionTimingMC¶

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 86 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.

ActualInspectionDestinationsT11 · operator

reference-profile · input revision 2 · CC0 1.0

ActualInspectionDestinationsT11(b,completed,drained) ==
 LET objects==InspectionObjectsT11("SchemaAtom082",1,0) m==OpenCandidateCapacity7(b,objects)
     done==[b EXCEPT !.active=FALSE,!.complete=TRUE,!.step="Complete",!.completionReason="Normal"] returned==[done EXCEPT !.returned=TRUE]
 IN {InspectionDestinationT11(g) : g \in {a \in InspectionCandidateFramesT11(b) : AdvanceInspectionStep7(b,a,completed,drained) \/ AdvanceInspectionSelection7(b,a,completed /\ drained) \/ SkipInspectionSelection7(b,a,m,objects,<<>> ,{},FALSE,completed /\ drained)}} \cup
    (IF CompleteNormalInspection7(b,done,completed,{InspectionEndEvent7(b)}) /\ ReturnInspectionToCaller7(done,returned,drained,"InspectionAuditCaller") THEN {InspectionDestinationT11(returned)} ELSE {})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AdvanceInspectionSelection7, AdvanceInspectionStep7, CompleteNormalInspection7, InspectionEndEvent7, OpenCandidateCapacity7, ReturnInspectionToCaller7, SkipInspectionSelection7, InspectionCandidateFramesT11, InspectionDestinationT11, InspectionObjectsT11

InspectionAuditAdvanceT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionAuditAdvanceT11 ==
 /\ qT11.ready /\ qT11.drained /\ ~qT11.siteInspection.complete /\ ~qT11.skipPending
 /\ \E after \in InspectionCandidateFramesT11(qT11.siteInspection) :
      /\ AdvanceInspectionStep7(qT11.siteInspection,after,qT11.ready,qT11.drained) \/ AdvanceInspectionSelection7(qT11.siteInspection,after,qT11.ready /\ qT11.drained)
      /\ qT11'=InspectionRecordEdgeT11(qT11,[qT11 EXCEPT !.siteInspection=after,!.ready=FALSE,!.drained=FALSE,!.pendingEvents={}],qT11.siteInspection.step,after.step,IF qT11.siteInspection.step="ProcedureCode1404a82ab3ee" THEN qT11.decision ELSE "Next")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AdvanceInspectionSelection7, AdvanceInspectionStep7, InspectionCandidateFramesT11, InspectionRecordEdgeT11, qT11

InspectionAuditAfterSkipT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionAuditAfterSkipT11 ==
 /\ qT11.ready /\ qT11.drained /\ qT11.skipPending
 /\ qT11'=[qT11 EXCEPT !.ready=FALSE,!.drained=FALSE,!.skipPending=FALSE,!.pendingEvents={}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

InspectionAuditDoneT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionAuditDoneT11 == qT11.siteInspection.returned

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

InspectionAuditDrainT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionAuditDrainT11 ==
 /\ qT11.ready /\ ~qT11.drained
 /\ qT11'=[qT11 EXCEPT !.drained=TRUE,!.checkpoints=Append(@,[step |-> qT11.pendingStep,ongoingInspection |-> qT11.siteInspection.active /\ ~qT11.siteInspection.complete])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: qT11

InspectionAuditEventuallyReturnsT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionAuditEventuallyReturnsT11 == <>InspectionAuditDoneT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InspectionAuditDoneT11

InspectionAuditInitT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionAuditInitT11 ==
 /\ guideCaseT11=9
 /\ \E kind \in {"SchemaAtom082","SchemaAtom129","SchemaAtom018","SchemaAtom132"} :
      \E n \in 0..2,roots \in 0..1,extra \in 0..1,perform \in BOOLEAN,late \in IF kind="SchemaAtom018" THEN BOOLEAN ELSE {FALSE} :
       LET b==InspectionInitialT11(kind,7) objects==InspectionObjectsT11(kind,n,roots) IN
       qT11=[siteInspection |-> b,objects |-> objects,deck |-> InspectionDeckT11(kind,n),capacity |-> OpenCandidateCapacity7(b,objects),
        n |-> n,roots |-> roots,extra |-> extra,perform |-> perform,latePlan |-> late,lateInjected |-> FALSE,modifierDone |-> FALSE,
        pendingEvents |-> {},eventOccurrences |-> <<>>,ready |-> FALSE,drained |-> FALSE,skipPending |-> FALSE,pendingStep |-> "NoValue",decision |-> "Next",
        child |-> EmptyT11,childState |-> "NoValue",itemInspectionHistory |-> EmptyT11,limitSnapshot |-> 0,history |-> <<>>,edges |-> <<>>,checkpoints |-> <<>>]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenCandidateCapacity7, InspectionDeckT11, InspectionInitialT11, InspectionObjectsT11, EmptyT11, guideCaseT11, qT11

InspectionAuditInvariantT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionAuditInvariantT11 ==
 /\ guideCaseT11=9 /\ InspectionProcedureValid7(qT11.siteInspection) /\ CandidateCapacityValid7(qT11.capacity,qT11.siteInspection,qT11.objects)
 /\ (qT11.siteInspection.limitSet => qT11.siteInspection.randomLimit=qT11.limitSnapshot)
 /\ (RandomLimitApplies7(qT11.siteInspection) => InspectionCentralChoices7(qT11.siteInspection)<=qT11.siteInspection.randomLimit)
 /\ Cardinality(ActualItemInspectionesInInspection7(qT11.itemInspectionHistory,20))<=Len(qT11.siteInspection.choices)
 /\ (~qT11.perform => qT11.itemInspectionHistory=EmptyT11 /\ qT11.siteInspection.usedItemInspectionIds={})
 /\ \A i \in 1..Len(qT11.edges) : qT11.edges[i] \in InspectionOracleEdges11 /\ qT11.edges[i].before=qT11.history[i].step
 /\ \A i \in 1..Len(qT11.history) :
      LET row==qT11.history[i] IN
      /\ row.kind=InspectionOracleKinds11[row.step]
      /\ InspectionFormalConditionsT11(row.events)=IF row.step \in DOMAIN InspectionOracleFormalConditions11 THEN InspectionOracleFormalConditions11[row.step] ELSE {}
      /\ row.performed<=row.chosen /\ row.central<=row.chosen
 /\ \A i \in 1..Len(qT11.checkpoints) : qT11.checkpoints[i].step="ProcedureCode8c612115d469" => ~qT11.checkpoints[i].ongoingInspection
 /\ (qT11.siteInspection.archivesPrepared => \A id \in 1..qT11.n : qT11.objects[id].face="Up")
 /\ (qT11.lateInjected => qT11.objects[90].face="Down")
 /\ (qT11.lateInjected /\ qT11.siteInspection.active /\ 90 \in InspectionSeenObjects7(qT11.siteInspection,qT11.itemInspectionHistory) => InspectionObjectVisible7(qT11.siteInspection,qT11.itemInspectionHistory,qT11.objects,90))
 /\ (InspectionAuditDoneT11 =>
       LET expectedCentral==IF qT11.siteInspection.kind \in {"SchemaAtom082","SchemaAtom129"} THEN MinOf(qT11.n,1+qT11.extra) ELSE IF qT11.siteInspection.kind="SchemaAtom018" THEN qT11.n+(IF qT11.latePlan THEN 1 ELSE 0) ELSE 0 IN
       /\ qT11.siteInspection.complete /\ ~qT11.siteInspection.active /\ qT11.drained /\ Len(qT11.edges)=Len(qT11.history)
       /\ InspectionCentralChoices7(qT11.siteInspection)=expectedCentral /\ Len(qT11.siteInspection.choices)=expectedCentral+qT11.roots
       /\ Cardinality(ActualItemInspectionesInInspection7(qT11.itemInspectionHistory,20))=IF qT11.perform THEN Len(qT11.siteInspection.choices) ELSE 0)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinOf, ActualItemInspectionesInInspection7, CandidateCapacityValid7, InspectionCentralChoices7, InspectionObjectVisible7, InspectionProcedureValid7, InspectionSeenObjects7, RandomLimitApplies7, InspectionAuditDoneT11, InspectionFormalConditionsT11, EmptyT11, guideCaseT11, qT11, InspectionOracleEdges11, InspectionOracleFormalConditions11, InspectionOracleKinds11

InspectionAuditLateArrivalT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionAuditLateArrivalT11 ==
 /\ ~qT11.ready /\ qT11.siteInspection.step="ProcedureCode91f3ee0da236" /\ qT11.siteInspection.kind="SchemaAtom018" /\ qT11.latePlan /\ ~qT11.lateInjected
 /\ qT11'=[qT11 EXCEPT !.objects=[id \in DOMAIN @ \cup {90} |-> IF id=90 THEN InspectionCardT11(90,"SideADiscard","SchemaAtom018") ELSE @[id]],!.lateInjected=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InspectionCardT11, qT11

InspectionAuditNextT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionAuditNextT11 == /\ UNCHANGED guideCaseT11
 /\ (InspectionAuditWorkT11 \/ InspectionAuditLateArrivalT11 \/ InspectionAuditDrainT11 \/ InspectionAuditAdvanceT11 \/ InspectionAuditAfterSkipT11 \/ InspectionAuditReturnT11 \/ (InspectionAuditDoneT11 /\ UNCHANGED qT11))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InspectionAuditAdvanceT11, InspectionAuditAfterSkipT11, InspectionAuditDoneT11, InspectionAuditDrainT11, InspectionAuditLateArrivalT11, InspectionAuditReturnT11, InspectionAuditWorkT11, guideCaseT11, qT11

InspectionAuditReturnT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionAuditReturnT11 ==
 /\ qT11.ready /\ qT11.drained /\ qT11.siteInspection.complete /\ ~InspectionAuditDoneT11
 /\ LET after==[qT11.siteInspection EXCEPT !.returned=TRUE] IN
      /\ ReturnInspectionToCaller7(qT11.siteInspection,after,qT11.drained,"InspectionAuditCaller")
      /\ qT11'=InspectionRecordEdgeT11(qT11,[qT11 EXCEPT !.siteInspection=after],"ProcedureCode8c612115d469","ReturnToCaller","Next")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReturnInspectionToCaller7, InspectionAuditDoneT11, InspectionRecordEdgeT11, qT11

InspectionAuditSpecT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionAuditSpecT11 == InspectionAuditInitT11 /\ [][InspectionAuditNextT11]_<<guideCaseT11,qT11>> /\ WF_<<guideCaseT11,qT11>>(InspectionAuditNextT11)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InspectionAuditInitT11, InspectionAuditNextT11, guideCaseT11, qT11

InspectionAuditWorkT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionAuditWorkT11 ==
 /\ ~InspectionAuditDoneT11 /\ ~qT11.ready
 /\ LET b==qT11.siteInspection kind==InspectionStepInfo7(b.step).kind IN
    CASE kind="BeginInspection" ->
      IF ~b.beginMet THEN
        LET after==[b EXCEPT !.active=TRUE,!.beginMet=TRUE] capacity==OpenCandidateCapacity7(after,qT11.objects) ev=={InspectionBeginEvent7(b)} IN
        /\ BeginInspectionWithCandidates7(b,after,capacity,qT11.objects,0,{b.targetSite},TRUE,TRUE,ev)
        /\ qT11'=[qT11 EXCEPT !.siteInspection=after,!.capacity=capacity,!.pendingEvents=ev,!.eventOccurrences=Append(@,ev)]
      ELSE IF ~qT11.modifierDone THEN
        /\ (qT11.extra=0 \/ ~RandomLimitApplies7(b) \/ AddAdditionalItemInspectiones7(b,[b EXCEPT !.randomLimit=@+qT11.extra],qT11.extra,TRUE))
        /\ qT11'=[qT11 EXCEPT !.modifierDone=TRUE,!.siteInspection.randomLimit=IF RandomLimitApplies7(b) THEN @+qT11.extra ELSE @]
      ELSE qT11'=InspectionRecordWorkT11(qT11,qT11,qT11.pendingEvents)
    [] kind="PrepareDiscardSite" ->
      IF b.kind="SchemaAtom018" THEN
        LET after==[b EXCEPT !.archivesPrepared=TRUE] objects==[id \in DOMAIN qT11.objects |-> IF qT11.objects[id].zone="SideADiscard" THEN [qT11.objects[id] EXCEPT !.face="Up"] ELSE qT11.objects[id]] IN
        /\ PrepareDiscardSite7(b,after,qT11.objects,objects)
        /\ qT11'=InspectionRecordWorkT11(qT11,[qT11 EXCEPT !.siteInspection=after,!.objects=objects],{})
      ELSE qT11'=InspectionRecordWorkT11(qT11,qT11,{})
    [] kind="SetLimit" ->
      /\ (~qT11.latePlan \/ qT11.lateInjected)
      /\ IF RandomLimitApplies7(b) THEN
            LET after==[b EXCEPT !.limitSet=TRUE] IN
            /\ FreezeInspectionLimit7(b,after,qT11.modifierDone)
            /\ qT11'=InspectionRecordWorkT11(qT11,[qT11 EXCEPT !.siteInspection=after,!.limitSnapshot=b.randomLimit],{})
         ELSE qT11'=InspectionRecordWorkT11(qT11,qT11,{})
    [] kind="Choose" ->
      LET view==InspectionViewT11(qT11) IN
      /\ DeriveCandidateView7(b,qT11.capacity,qT11.objects,qT11.deck,{},FALSE,view)
      /\ IF view.roots \cup view.central={} THEN
            LET after==[b EXCEPT !.step="ProcedureCode8c612115d469"] next==InspectionRecordWorkT11(qT11,[qT11 EXCEPT !.siteInspection=after,!.decision="Done",!.skipPending=TRUE],{}) IN
            /\ SkipInspectionSelection7(b,after,qT11.capacity,qT11.objects,qT11.deck,{},FALSE,TRUE)
            /\ qT11'=InspectionRecordEdgeT11(qT11,next,"ProcedureCode1404a82ab3ee","ProcedureCode8c612115d469","Done")
         ELSE \E id \in view.roots \cup view.central :
            LET source==IF id \in view.roots THEN "Root" ELSE "SchemaAtom033" after==InspectionSelectT11(b,id,source) IN
            /\ IF b.kind="SchemaAtom082" /\ source="SchemaAtom033" THEN ChooseCentralAInspectionCard7(b,after,view,id,0,FALSE,TRUE) ELSE ChooseSpecificInspectionCard7(b,after,id,view)
            /\ qT11'=InspectionRecordWorkT11(qT11,[qT11 EXCEPT !.siteInspection=after,!.decision="Choose",!.childState="NoValue"],{})
    [] kind="ItemInspection" ->
      IF qT11.perform THEN
        IF qT11.childState="NoValue" THEN
          LET a==InspectionChildProjectionT11(b,100+Len(b.choices),b.selectedObject,qT11.objects[b.selectedObject])
              after==[b EXCEPT !.currentItemInspectionId=a.id,!.usedItemInspectionIds=@ \cup {a.id}] ev==ItemInspectionBeginEvent7(a)
              history==[id \in DOMAIN qT11.itemInspectionHistory \cup {a.id} |-> IF id=a.id THEN [object |-> a.object,traversalId |-> a.traversalId,siteInspectionId |-> a.siteInspectionId,turnId |-> 2,hadRetireCost |-> FALSE] ELSE qT11.itemInspectionHistory[id]] IN
          /\ AttachChosenItemInspection7(b,after,a,ev) /\ RecordActualItemInspection7(qT11.itemInspectionHistory,history,a,2,FALSE,ev)
          /\ qT11'=[qT11 EXCEPT !.siteInspection=after,!.child=a,!.childState="Begun",!.itemInspectionHistory=history,!.eventOccurrences=Append(@,{ev})]
        ELSE IF qT11.childState="Begun" THEN
          qT11'=[qT11 EXCEPT !.child.active=FALSE,!.child.complete=TRUE,!.child.returned=TRUE,!.child.step="Complete",!.childState="Returned"]
        ELSE
          LET after==[b EXCEPT !.selectionPending=FALSE,!.selectedObject=0,!.selectedSource="NoValue",!.currentItemInspectionId=0] IN
          /\ qT11.childState="Returned" /\ FinishInspectionItemInspectionInstruction7(b,after,InspectionChildReturnedT11(b,qT11.child))
          /\ qT11'=InspectionRecordWorkT11(qT11,[qT11 EXCEPT !.siteInspection=after],{})
      ELSE IF qT11.childState="NoValue" THEN qT11'=[qT11 EXCEPT !.childState="AlternativeDone"]
      ELSE LET after==[b EXCEPT !.selectionPending=FALSE,!.selectedObject=0,!.selectedSource="NoValue",!.currentItemInspectionId=0] IN
        /\ qT11.childState="AlternativeDone" /\ FinishInspectionItemInspectionInstruction7(b,after,TRUE)
        /\ qT11'=InspectionRecordWorkT11(qT11,[qT11 EXCEPT !.siteInspection=after],{})
    [] kind="Repeat" -> qT11'=InspectionRecordWorkT11(qT11,qT11,{})
    [] kind="CompleteInspection" ->
      LET after==[b EXCEPT !.active=FALSE,!.complete=TRUE,!.step="Complete",!.completionReason="Normal"] ev=={InspectionEndEvent7(b)} IN
      /\ CompleteNormalInspection7(b,after,TRUE,ev)
      /\ qT11'=InspectionRecordWorkT11(qT11,[qT11 EXCEPT !.siteInspection=after,!.eventOccurrences=Append(@,ev)],ev)
    [] OTHER -> FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AddAdditionalItemInspectiones7, AttachChosenItemInspection7, BeginInspectionWithCandidates7, ChooseCentralAInspectionCard7, ChooseSpecificInspectionCard7, CompleteNormalInspection7, DeriveCandidateView7, FinishInspectionItemInspectionInstruction7, FreezeInspectionLimit7, InspectionBeginEvent7, InspectionEndEvent7, InspectionStepInfo7, ItemInspectionBeginEvent7, OpenCandidateCapacity7, PrepareDiscardSite7, RandomLimitApplies7, RecordActualItemInspection7, SkipInspectionSelection7, InspectionAuditDoneT11, InspectionChildProjectionT11, InspectionChildReturnedT11, InspectionRecordEdgeT11, InspectionRecordWorkT11, InspectionSelectT11, InspectionViewT11, qT11

InspectionBeginningChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionBeginningChecksT11 ==
 LET b==InspectionInitialT11("SchemaAtom082",0) begun==[b EXCEPT !.active=TRUE,!.beginMet=TRUE] ev=={InspectionBeginEvent7(b)}
     set==[InspectionWorkedT11("SchemaAtom082","ProcedureCode91f3ee0da236","Next") EXCEPT !.limitSet=FALSE] fixed==[set EXCEPT !.limitSet=TRUE]
     ar==[InspectionWorkedT11("SchemaAtom018","ProcedureCodeb6067693902e","Next") EXCEPT !.archivesPrepared=FALSE] arp==[ar EXCEPT !.archivesPrepared=TRUE]
     objects==InspectionObjectsT11("SchemaAtom018",2,1) up==[id \in DOMAIN objects |-> IF objects[id].zone="SideADiscard" THEN [objects[id] EXCEPT !.face="Up"] ELSE objects[id]]
 IN /\ BeginInspection7(b,begun,0,{"SchemaAtom082"},TRUE,TRUE,ev) /\ ~BeginInspection7(b,begun,99,{"SchemaAtom082"},TRUE,TRUE,ev)
    /\ ~BeginInspection7(b,begun,0,{},TRUE,TRUE,ev) /\ ~BeginInspection7(b,begun,0,{"SchemaAtom082"},FALSE,TRUE,ev)
    /\ ~BeginInspection7(b,begun,0,{"SchemaAtom082"},TRUE,FALSE,ev) /\ ~BeginInspection7(b,begun,0,{"SchemaAtom082"},TRUE,TRUE,{})
    /\ InspectionBeginEvent7(b)=[tag |-> "InspectionTargetSite",siteInspectionId |-> 20,targetSite |-> "SchemaAtom082",traversalId |-> 0]
    /\ FreezeInspectionLimit7(set,fixed,TRUE) /\ ~FreezeInspectionLimit7(set,fixed,FALSE)
    /\ ~AddAdditionalItemInspectiones7(fixed,[fixed EXCEPT !.randomLimit=@+1],1,TRUE)
    /\ AddAdditionalItemInspectiones7(set,[set EXCEPT !.randomLimit=@+1],1,TRUE)
    /\ PrepareDiscardSite7(ar,arp,objects,up) /\ up[1].face="Up" /\ up[10].face="Down" /\ up[1].loc=objects[1].loc /\ up[1].marks=objects[1].marks
    /\ ~PrepareDiscardSite7(arp,arp,objects,up)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AddAdditionalItemInspectiones7, BeginInspection7, FreezeInspectionLimit7, InspectionBeginEvent7, PrepareDiscardSite7, InspectionInitialT11, InspectionObjectsT11, InspectionWorkedT11

InspectionCandidateChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionCandidateChecksT11 ==
 LET b==[InspectionWorkedT11("SchemaAtom129","ProcedureCode1404a82ab3ee","Next") EXCEPT !.choices= <<>>,!.randomLimit=3] objects==InspectionObjectsT11("SchemaAtom129",3,0) m==OpenCandidateCapacity7(b,objects)
     first==InspectionSelectT11(b,1,"SchemaAtom033") after==InspectionRoundAfterT11(first)
     h==[b EXCEPT !.targetSite="SchemaAtom082",!.kind="SchemaAtom082"] ho==InspectionObjectsT11("SchemaAtom082",2,0) hm==OpenCandidateCapacity7(h,ho)
     newer==[id \in {2,3,4} |-> IF id=4 THEN [InspectionCardT11(4,"SideADeck","SchemaAtom129") EXCEPT !.physical=1] ELSE objects[id]]
     base==InspectionObjectsT11("SchemaAtom082",1,1) rb==[h EXCEPT !.randomLimit=3] rm==OpenCandidateCapacity7(rb,base)
     arrived==[id \in DOMAIN base \cup {90} |-> IF id=90 THEN InspectionCardT11(90,"Play","SchemaAtom082") ELSE base[id]]
     pending==[rm EXCEPT !.pendingRoots={90}] admitted==[pending EXCEPT !.pendingRoots={},!.admittedRoots=@ \cup {90}] denied==[pending EXCEPT !.pendingRoots={},!.deniedRoots={90}]
 IN /\ InspectionCandidates7(b,m,objects,<<1,2,3>>,{}).central={1}
    /\ InspectionCandidates7(b,m,objects,<<1,2,3>>,{1,2,3}).central={}
                                                                            
    /\ ChooseSpecificInspectionCard7(b,first,1,[roots |-> {},central |-> {1}]) /\ InspectionNonItemInspectionRoundT11(first,after)
    /\ InspectionCandidates7(after,m,objects,<<1,2,3>>,{2}).central={3}
    /\ InspectionCandidates7(after,m,objects,<<3,2,1>>,{}).central={3}
    /\ InspectionCandidates7(after,OpenCandidateCapacity7(after,newer),newer,<<4,2,3>>,{}).central={4}
    /\ InspectionCandidates7(h,hm,ho,<<>>,{1}).central={2} /\ InspectionCandidates7(h,hm,ho,<<>>,{}).central={1,2}
    /\ ObserveRootEntries7(rm,pending,rb,arrived,{90})
    /\ InspectionCandidates7(rb,pending,arrived,<<>>,{}).roots={10}
    /\ DecideRootAdmissions7(pending,admitted,rb,arrived,{90},"ProcedureCode7f181ce21011",TRUE)
    /\ ~DecideRootAdmissions7(pending,admitted,rb,arrived,{90},"ProcedureCode2d6279f9d639",TRUE)
    /\ ~DecideRootAdmissions7(pending,admitted,rb,arrived,{90},"ProcedureCode7f181ce21011",FALSE)
    /\ DecideRootAdmissions7(pending,denied,rb,arrived,{},"ProcedureCode7f181ce21011",TRUE)
    /\ InspectionCandidates7(rb,admitted,arrived,<<>>,{}).roots={10,90} /\ InspectionCandidates7(rb,denied,arrived,<<>>,{}).roots={10}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ChooseSpecificInspectionCard7, DecideRootAdmissions7, InspectionCandidates7, ObserveRootEntries7, OpenCandidateCapacity7, InspectionCardT11, InspectionNonItemInspectionRoundT11, InspectionObjectsT11, InspectionRoundAfterT11, InspectionSelectT11, InspectionWorkedT11

InspectionCandidateFramesT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionCandidateFramesT11(b) == {[b EXCEPT !.step=step] : step \in InspectionOracleStepSet11 \cup {"UnauthorizedStep"}}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InspectionOracleStepSet11

InspectionCardT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionCardT11(id,zone,targetSite) == [form |-> "Card",side |-> "SideA",kind |-> "Attachment",zone |-> zone,targetSite |-> IF zone="Play" THEN targetSite ELSE "NoValue",area |-> IF zone="Play" THEN "Root" ELSE "NoValue",host |-> 0,deployed |-> zone="Play",face |-> "Down",loc |-> <<zone,id>>,physical |-> id,marks |-> {}]

Exact module download · Source bundle and reproduction instructions

InspectionChildAndEndChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionChildAndEndChecksT11 ==
 LET b==InspectionWorkedT11("SchemaAtom082","ProcedureCodee35e7c8fc57b","Next") chosen==[b EXCEPT !.selectionPending=TRUE,!.selectedObject=1,!.selectedSource="SchemaAtom033"]
     card==InspectionCardT11(1,"SideAHand","SchemaAtom082") a==InspectionChildProjectionT11(chosen,101,1,card) attached==[chosen EXCEPT !.currentItemInspectionId=101,!.usedItemInspectionIds={101}]
     doneChild==[a EXCEPT !.active=FALSE,!.complete=TRUE,!.returned=TRUE,!.step="Complete"] finished==[attached EXCEPT !.selectionPending=FALSE,!.selectedObject=0,!.selectedSource="NoValue",!.currentItemInspectionId=0]
     itemInspectionHistory==[id \in {101} |-> [object |-> 1,traversalId |-> 7,siteInspectionId |-> 20,turnId |-> 2,hadRetireCost |-> FALSE]]
     visibleObjects==[id \in {1,2} |-> InspectionCardT11(id,"SideAHand","SchemaAtom082")]
     last==[finished EXCEPT !.step="ProcedureCode8c612115d469"] complete==[last EXCEPT !.active=FALSE,!.complete=TRUE,!.step="Complete",!.completionReason="Normal"]
     interrupted==[attached EXCEPT !.active=FALSE,!.complete=TRUE,!.step="Complete",!.completionReason="EndTraversal"] drained==[interrupted EXCEPT !.selectionPending=FALSE,!.selectedObject=0,!.selectedSource="NoValue",!.currentItemInspectionId=0]
 IN /\ AttachChosenItemInspection7(chosen,attached,a,ItemInspectionBeginEvent7(a))
    /\ RecordActualItemInspection7(EmptyT11,itemInspectionHistory,a,2,FALSE,ItemInspectionBeginEvent7(a))
    /\ InspectionObjectVisible7(attached,itemInspectionHistory,visibleObjects,1) /\ ~InspectionObjectVisible7(attached,itemInspectionHistory,visibleObjects,2)
    /\ ~InspectionObjectVisible7(attached,itemInspectionHistory,[id \in {3} |-> [InspectionCardT11(3,"SideAHand","SchemaAtom082") EXCEPT !.physical=1]],3)
    /\ ~InspectionObjectVisible7(complete,itemInspectionHistory,visibleObjects,1)
    /\ ~AttachChosenItemInspection7(chosen,attached,[a EXCEPT !.object=2],ItemInspectionBeginEvent7([a EXCEPT !.object=2]))
    /\ ~AttachChosenItemInspection7(chosen,attached,[a EXCEPT !.caller= <<"InspectionItemInspection",99>>],ItemInspectionBeginEvent7(a))
    /\ InspectionChildReturnedT11(attached,doneChild) /\ ~InspectionChildReturnedT11(attached,a)
    /\ ~InspectionChildReturnedT11(attached,[doneChild EXCEPT !.id=102]) /\ ~InspectionChildReturnedT11(attached,[doneChild EXCEPT !.returned=FALSE])
    /\ FinishInspectionItemInspectionInstruction7(attached,finished,InspectionChildReturnedT11(attached,doneChild))
    /\ ~FinishInspectionItemInspectionInstruction7(attached,finished,InspectionChildReturnedT11(attached,a))
    /\ CompleteNormalInspection7(last,complete,TRUE,{InspectionEndEvent7(last)}) /\ ~CompleteNormalInspection7(last,complete,FALSE,{InspectionEndEvent7(last)})
    /\ ReturnInspectionToCaller7(complete,[complete EXCEPT !.returned=TRUE],TRUE,"InspectionAuditCaller")
    /\ ~ReturnInspectionToCaller7(complete,[complete EXCEPT !.returned=TRUE],FALSE,"InspectionAuditCaller")
    /\ ~ReturnInspectionToCaller7(complete,[complete EXCEPT !.returned=TRUE],TRUE,"WrongInspectionCaller")
    /\ ApplyInspectionAborts7(attached,interrupted,{20},{InspectionEndEvent7(attached)})
    /\ ~ReturnInspectionToCaller7(interrupted,[interrupted EXCEPT !.returned=TRUE],TRUE,"InspectionAuditCaller")
    /\ DrainEndedInspectionInstruction7(interrupted,drained,TRUE) /\ ~DrainEndedInspectionInstruction7(interrupted,drained,FALSE)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ApplyInspectionAborts7, AttachChosenItemInspection7, CompleteNormalInspection7, DrainEndedInspectionInstruction7, FinishInspectionItemInspectionInstruction7, InspectionEndEvent7, InspectionObjectVisible7, ItemInspectionBeginEvent7, RecordActualItemInspection7, ReturnInspectionToCaller7, InspectionCardT11, InspectionChildProjectionT11, InspectionChildReturnedT11, InspectionWorkedT11, EmptyT11

InspectionChildProjectionT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionChildProjectionT11(b,id,object,card) == [OpenItemInspection7(id,object,card,b.traversalId,b.id,InspectionItemInspectionCaller7(b),b.encounterAncestors) EXCEPT !.active=TRUE,!.beginMet=TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InspectionItemInspectionCaller7, OpenItemInspection7

InspectionChildReturnedT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionChildReturnedT11(b,a) == a.id=b.currentItemInspectionId /\ a.object=b.selectedObject /\ a.siteInspectionId=b.id /\ a.traversalId=b.traversalId /\ a.caller=InspectionItemInspectionCaller7(b) /\ a.beginMet /\ a.complete /\ a.returned /\ ~a.active

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InspectionItemInspectionCaller7

InspectionDeckT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionDeckT11(kind,n) == IF kind="SchemaAtom129" THEN IF n=0 THEN <<>> ELSE IF n=1 THEN <<1>> ELSE IF n=2 THEN <<1,2>> ELSE <<1,2,3>> ELSE <<>>

Exact module download · Source bundle and reproduction instructions

InspectionDestinationT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionDestinationT11(b) == IF b.returned THEN "ReturnToCaller" ELSE b.step

Exact module download · Source bundle and reproduction instructions

InspectionFormalConditionsT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionFormalConditionsT11(events) == {IF event.tag="InspectionTargetSite" THEN "InspectionBegins" ELSE "InspectionEnds" : event \in {e \in events : e.tag \in {"InspectionTargetSite","InspectionEnds"}}}

Exact module download · Source bundle and reproduction instructions

InspectionGraphChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionGraphChecksT11 ==
 /\ InspectionInitialT11("SchemaAtom082",7).step=InspectionOracleEntry11 /\ ~InspectionInitialT11("SchemaAtom082",7).active /\ ~InspectionInitialT11("SchemaAtom082",7).beginMet
 /\ InspectionInitialT11("SchemaAtom082",7).randomLimit=InspectionOracleDefaultLimit11 /\ InspectionSteps7=InspectionOracleStepSet11 /\ InspectionOracleHidden11={}
 /\ \A step \in InspectionOracleStepSet11 : InspectionStepInfo7(step).kind=InspectionOracleKinds11[step]
 /\ \A edge \in InspectionOracleEdges11 : LET b==InspectionWorkedT11("SchemaAtom082",edge.before,edge.decision) IN
      /\ ActualInspectionDestinationsT11(b,TRUE,TRUE)={edge.after}
      /\ ActualInspectionDestinationsT11(b,FALSE,TRUE)={} /\ ActualInspectionDestinationsT11(b,TRUE,FALSE)={}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InspectionStepInfo7, InspectionSteps7, ActualInspectionDestinationsT11, InspectionInitialT11, InspectionWorkedT11, InspectionOracleDefaultLimit11, InspectionOracleEdges11, InspectionOracleEntry11, InspectionOracleHidden11, InspectionOracleKinds11, InspectionOracleStepSet11

InspectionInitialT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionInitialT11(kind,traversal) == OpenInspection7(20,InspectionTargetSiteT11(kind),kind,traversal,"AuditInspection","InspectionAuditCaller",{},InspectionPolicy7("Normal",0))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InspectionPolicy7, OpenInspection7, InspectionTargetSiteT11

InspectionNonItemInspectionRoundT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionNonItemInspectionRoundT11(b,after) ==
 LET entry==[b EXCEPT !.step="ProcedureCodee35e7c8fc57b"] finished==[entry EXCEPT !.selectionPending=FALSE,!.selectedObject=0,!.selectedSource="NoValue",!.currentItemInspectionId=0] loop==[finished EXCEPT !.step="ProcedureCodeb1fbc90c4ab0"] IN
 /\ AdvanceInspectionSelection7(b,entry,TRUE) /\ FinishInspectionItemInspectionInstruction7(entry,finished,TRUE)
 /\ AdvanceInspectionStep7(finished,loop,TRUE,TRUE) /\ AdvanceInspectionStep7(loop,after,TRUE,TRUE)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AdvanceInspectionSelection7, AdvanceInspectionStep7, FinishInspectionItemInspectionInstruction7

InspectionObjectsT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionObjectsT11(kind,n,roots) ==
 [id \in (1..n) \cup (IF roots=1 THEN {10} ELSE {}) |->
   InspectionCardT11(id,IF id=10 THEN "Play" ELSE CASE kind="SchemaAtom082" -> "SideAHand" [] kind="SchemaAtom129" -> "SideADeck" [] kind="SchemaAtom018" -> "SideADiscard" [] OTHER -> "SideAHand",InspectionTargetSiteT11(kind))]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InspectionCardT11, InspectionTargetSiteT11

InspectionPermissionsChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionPermissionsChecksT11 ==
 /\ InspectionOraclePaidSteps11={}
 /\ \A step \in InspectionOracleStepSet11 :
      /\ ~InspectionStepInfo7(step).paidWindow /\ ~InspectionStepInfo7(step).objectivePlacementWindow
      /\ \A player \in SetupPlayers :
           LET b==InspectionWorkedT11("SchemaAtom082",step,"Next") site==InspectionPrioritySite9(TraversalTurnT11(player),b) IN
           /\ ~WindowSiteAllowed9("Paid",site) /\ ~WindowSiteAllowed9("NeutralValue00001",site)
           /\ WindowSiteAllowed9("Reaction",site) /\ WindowSiteAllowed9("Interrupt",site)
 /\ LET b==[InspectionWorkedT11("SchemaAtom082","ProcedureCode8c612115d469","Next") EXCEPT !.complete=TRUE,!.active=FALSE,!.step="Complete"]
        site==InspectionPrioritySite9(TraversalTurnT11("SideB"),b) IN
      /\ site.live /\ ~site.timingLive /\ WindowSiteAllowed9("Reaction",site)
      /\ ~WindowSiteAllowed9("Paid",site) /\ ~WindowSiteAllowed9("Reaction",InspectionPrioritySite9(TraversalTurnT11("SideB"),[b EXCEPT !.returned=TRUE]))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InspectionPrioritySite9, WindowSiteAllowed9, InspectionStepInfo7, InspectionWorkedT11, InspectionOraclePaidSteps11, InspectionOracleStepSet11, SetupPlayers, TraversalTurnT11

InspectionPointwiseChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionPointwiseChecksT11 == CASE guideCaseT11=1 -> InspectionGraphChecksT11 [] guideCaseT11=2 -> InspectionPermissionsChecksT11
 [] guideCaseT11=3 -> InspectionBeginningChecksT11 [] guideCaseT11=4 -> InspectionQuotaAndGroupsChecksT11
 [] guideCaseT11=5 -> InspectionCandidateChecksT11 [] OTHER -> InspectionChildAndEndChecksT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InspectionBeginningChecksT11, InspectionCandidateChecksT11, InspectionChildAndEndChecksT11, InspectionGraphChecksT11, InspectionPermissionsChecksT11, InspectionQuotaAndGroupsChecksT11, guideCaseT11

InspectionPointwiseInitT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionPointwiseInitT11 == guideCaseT11 \in 1..6 /\ qT11=EmptyT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: EmptyT11, guideCaseT11, qT11

InspectionPointwiseSpecT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionPointwiseSpecT11 == InspectionPointwiseInitT11 /\ [][PointwiseNextT11]_<<guideCaseT11,qT11>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InspectionPointwiseInitT11, PointwiseNextT11, guideCaseT11, qT11

InspectionQuotaAndGroupsChecksT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionQuotaAndGroupsChecksT11 ==
 LET b==[InspectionWorkedT11("SchemaAtom082","ProcedureCode1404a82ab3ee","Next") EXCEPT !.choices= <<>>] objects==InspectionObjectsT11("SchemaAtom082",2,1) m==OpenCandidateCapacity7(b,objects)
     view==[roots |-> {10},central |-> {1,2}] hand==InspectionSelectT11(b,1,"SchemaAtom033") root==InspectionSelectT11(b,10,"Root") after==InspectionRoundAfterT11(hand)
     exhausted==InspectionCandidates7(after,m,objects,<<>>,{} ) emptyObjects==InspectionObjectsT11("SchemaAtom082",0,0)
 IN /\ DeriveCandidateView7(b,m,objects,<<>>,{},FALSE,view)
    /\ InspectionPresentation7(b,view)=[specific |-> {10},randomCentralAOffered |-> TRUE]
    /\ ChooseSpecificInspectionCard7(b,root,10,view) /\ ~ChooseSpecificInspectionCard7(b,hand,1,view)
    /\ ChooseCentralAInspectionCard7(b,hand,view,1,0,FALSE,TRUE) /\ ~ChooseCentralAInspectionCard7(b,hand,view,1,0,FALSE,FALSE)
    /\ ChooseCentralAInspectionCard7(b,hand,view,0,1,TRUE,FALSE) /\ hand.choices[1].chooser="SideB"
    /\ ~ChooseCentralAInspectionCard7(b,[hand EXCEPT !.selectedObject=99],view,99,0,FALSE,TRUE)
    /\ InspectionNonItemInspectionRoundT11(hand,after) /\ InspectionCentralChoices7(after)=1 /\ ActualItemInspectionesInInspection7(EmptyT11,20)={}
    /\ exhausted=[roots |-> {10},central |-> {}]
    /\ ChooseSpecificInspectionCard7(after,InspectionSelectT11(after,10,"Root"),10,exhausted)
    /\ InspectionCentralChoices7(root)=0 /\ InspectionCandidates7(InspectionRoundAfterT11(root),m,objects,<<>>,{}).central={1,2}
    /\ ~SkipInspectionSelection7(b,[b EXCEPT !.step="ProcedureCode8c612115d469"],m,objects,<<>>,{},FALSE,TRUE)
    /\ SkipInspectionSelection7(b,[b EXCEPT !.step="ProcedureCode8c612115d469"],OpenCandidateCapacity7(b,emptyObjects),emptyObjects,<<>>,{},FALSE,TRUE)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualItemInspectionesInInspection7, ChooseCentralAInspectionCard7, ChooseSpecificInspectionCard7, DeriveCandidateView7, InspectionCandidates7, InspectionCentralChoices7, InspectionPresentation7, OpenCandidateCapacity7, SkipInspectionSelection7, InspectionNonItemInspectionRoundT11, InspectionObjectsT11, InspectionRoundAfterT11, InspectionSelectT11, InspectionWorkedT11, EmptyT11

InspectionRecordEdgeT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionRecordEdgeT11(before,after,source,target,decision) ==
 [after EXCEPT !.edges=Append(@,[before |-> source,after |-> target,decision |-> decision])]

Exact module download · Source bundle and reproduction instructions

InspectionRecordWorkT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionRecordWorkT11(before,after,events) ==
 [after EXCEPT !.ready=TRUE,!.drained=FALSE,!.pendingStep=before.siteInspection.step,
    !.history=Append(@,[step |-> before.siteInspection.step,kind |-> InspectionStepInfo7(before.siteInspection.step).kind,events |-> events,
      chosen |-> Len(after.siteInspection.choices),central |-> InspectionCentralChoices7(after.siteInspection),performed |-> Cardinality(ActualItemInspectionesInInspection7(after.itemInspectionHistory,after.siteInspection.id))])]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActualItemInspectionesInInspection7, InspectionCentralChoices7, InspectionStepInfo7

InspectionRoundAfterT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionRoundAfterT11(b) == [b EXCEPT !.step="ProcedureCode1404a82ab3ee",!.selectionPending=FALSE,!.selectedObject=0,!.selectedSource="NoValue",!.currentItemInspectionId=0]

Exact module download · Source bundle and reproduction instructions

InspectionSelectT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionSelectT11(b,id,source) == [b EXCEPT !.choices=Append(@,[object |-> id,source |-> source,chooser |-> "SideB"]),!.selectionPending=TRUE,!.selectedObject=id,!.selectedSource=source]

Exact module download · Source bundle and reproduction instructions

InspectionTargetSiteT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionTargetSiteT11(kind) == IF kind="SchemaAtom132" THEN "AuxiliarySite1" ELSE kind

Exact module download · Source bundle and reproduction instructions

InspectionViewT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionViewT11(s) == InspectionCandidates7(s.siteInspection,s.capacity,s.objects,s.deck,{})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InspectionCandidates7

InspectionWorkedT11 · operator

reference-profile · input revision 2 · CC0 1.0

InspectionWorkedT11(kind,step,decision) ==
 LET b==[InspectionInitialT11(kind,7) EXCEPT !.active=TRUE,!.beginMet=TRUE,!.step=step,
          !.archivesPrepared=kind="SchemaAtom018" /\ step \notin {"ProcedureCode839b301bad95"},!.limitSet=kind \in {"SchemaAtom082","SchemaAtom129"} /\ step \notin {"ProcedureCode839b301bad95","ProcedureCodeb6067693902e"}]
 IN IF step \in {"ProcedureCode1404a82ab3ee","ProcedureCodee35e7c8fc57b","ProcedureCodeb1fbc90c4ab0","ProcedureCode8c612115d469"} THEN
      [b EXCEPT !.choices= <<[object |-> 1,source |-> "SchemaAtom033",chooser |-> "SideB"]>>,
       !.selectionPending=step="ProcedureCode1404a82ab3ee" /\ decision="Choose",!.selectedObject=IF step="ProcedureCode1404a82ab3ee" /\ decision="Choose" THEN 1 ELSE 0,
       !.selectedSource=IF step="ProcedureCode1404a82ab3ee" /\ decision="Choose" THEN "SchemaAtom033" ELSE "NoValue"] ELSE b

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InspectionInitialT11