------------------------- MODULE InspectionTimingMC ------------------------- EXTENDS TraversalTimingMC InspectionTargetSiteT11(kind) == IF kind="SchemaAtom132" THEN "AuxiliarySite1" ELSE kind InspectionInitialT11(kind,traversal) == OpenInspection7(20,InspectionTargetSiteT11(kind),kind,traversal,"AuditInspection","InspectionAuditCaller",{},InspectionPolicy7("Normal",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 |-> <>,physical |-> id,marks |-> {}] 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))] 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 <<>> 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 InspectionCandidateFramesT11(b) == {[b EXCEPT !.step=step] : step \in InspectionOracleStepSet11 \cup {"UnauthorizedStep"}} InspectionDestinationT11(b) == IF b.returned THEN "ReturnToCaller" ELSE b.step 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 {}) 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)={} 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])) 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) InspectionSelectT11(b,id,source) == [b EXCEPT !.choices=Append(@,[object |-> id,source |-> source,chooser |-> "SideB"]),!.selectionPending=TRUE,!.selectedObject=id,!.selectedSource=source] InspectionRoundAfterT11(b) == [b EXCEPT !.step="ProcedureCode1404a82ab3ee",!.selectionPending=FALSE,!.selectedObject=0,!.selectedSource="NoValue",!.currentItemInspectionId=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) 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) 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} InspectionChildProjectionT11(b,id,object,card) == [OpenItemInspection7(id,object,card,b.traversalId,b.id,InspectionItemInspectionCaller7(b),b.encounterAncestors) EXCEPT !.active=TRUE,!.beginMet=TRUE] 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 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) InspectionPointwiseInitT11 == guideCaseT11 \in 1..6 /\ qT11=EmptyT11 InspectionPointwiseSpecT11 == InspectionPointwiseInitT11 /\ [][PointwiseNextT11]_<> InspectionPointwiseChecksT11 == CASE guideCaseT11=1 -> InspectionGraphChecksT11 [] guideCaseT11=2 -> InspectionPermissionsChecksT11 [] guideCaseT11=3 -> InspectionBeginningChecksT11 [] guideCaseT11=4 -> InspectionQuotaAndGroupsChecksT11 [] guideCaseT11=5 -> InspectionCandidateChecksT11 [] OTHER -> InspectionChildAndEndChecksT11 InspectionViewT11(s) == InspectionCandidates7(s.siteInspection,s.capacity,s.objects,s.deck,{}) InspectionAuditDoneT11 == qT11.siteInspection.returned 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 |-> <<>>] 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))])] InspectionRecordEdgeT11(before,after,source,target,decision) == [after EXCEPT !.edges=Append(@,[before |-> source,after |-> target,decision |-> decision])] 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 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] InspectionAuditDrainT11 == /\ qT11.ready /\ ~qT11.drained /\ qT11'=[qT11 EXCEPT !.drained=TRUE,!.checkpoints=Append(@,[step |-> qT11.pendingStep,ongoingInspection |-> qT11.siteInspection.active /\ ~qT11.siteInspection.complete])] 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") InspectionAuditAfterSkipT11 == /\ qT11.ready /\ qT11.drained /\ qT11.skipPending /\ qT11'=[qT11 EXCEPT !.ready=FALSE,!.drained=FALSE,!.skipPending=FALSE,!.pendingEvents={}] 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") InspectionAuditNextT11 == /\ UNCHANGED guideCaseT11 /\ (InspectionAuditWorkT11 \/ InspectionAuditLateArrivalT11 \/ InspectionAuditDrainT11 \/ InspectionAuditAdvanceT11 \/ InspectionAuditAfterSkipT11 \/ InspectionAuditReturnT11 \/ (InspectionAuditDoneT11 /\ UNCHANGED qT11)) InspectionAuditSpecT11 == InspectionAuditInitT11 /\ [][InspectionAuditNextT11]_<> /\ WF_<>(InspectionAuditNextT11) InspectionFormalConditionsT11(events) == {IF event.tag="InspectionTargetSite" THEN "InspectionBegins" ELSE "InspectionEnds" : event \in {e \in events : e.tag \in {"InspectionTargetSite","InspectionEnds"}}} 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) InspectionAuditEventuallyReturnsT11 == <>InspectionAuditDoneT11 =============================================================================