---------------------------- MODULE InspectionChecksMC ---------------------------- EXTENDS InspectionContracts VARIABLE block7 Init7 == block7 \in 1..5 Next7 == UNCHANGED block7 Spec7 == Init7 /\ [][Next7]_block7 ItemInspectionCardFixture7(zone,kind) == [form |-> "Card",side |-> "SideA",zone |-> zone,loc |-> zone,kind |-> kind,deployed |-> zone = "Play"] ActiveItemInspectionFixture7(card) == [OpenItemInspection7(77,1,card,1,2,"siteInspection2",{}) EXCEPT !.active = TRUE,!.beginMet = TRUE,!.step = "ProcedureCode1dd0e8f05be2"] ItemInspectionConceptChecks7 == LET card == ItemInspectionCardFixture7("SideAHand","Facility") objects == [i \in {1} |-> card] a == ActiveItemInspectionFixture7(card) up == [a EXCEPT !.midUsed = TRUE,!.midResolving = TRUE] finish == [up EXCEPT !.midResolving = FALSE,!.midDone = TRUE] trashPart == [exists |-> TRUE,amount |-> 3] basic == BasicRetireOption7(card,trashPart,TRUE,TRUE) Specimen0115 == MidOption7("Imp",TRUE,TRUE,TRUE) other == MidOption7("Other",FALSE,TRUE,TRUE) options == ItemInspectionMidOptions7(card,{Specimen0115,other},trashPart,TRUE,TRUE) noBasic == ItemInspectionMidOptions7(card,{Specimen0115,other},[exists |-> FALSE,amount |-> 0],FALSE,TRUE) noneAffordable == {MidOption7("BasicRetire",TRUE,FALSE,TRUE),MidOption7("Imp",TRUE,FALSE,TRUE),other} archiveCard == ItemInspectionCardFixture7("SideADiscard","Facility") archiveOptions == ItemInspectionMidOptions7(archiveCard,{Specimen0115,other},trashPart,TRUE,TRUE) aDrawPileCard == ItemInspectionCardFixture7("SideADeck","Plan") aDrawPileObjects == [i \in {1} |-> aDrawPileCard] aDrawPileItemInspection == ActiveItemInspectionFixture7(aDrawPileCard) objective == ItemInspectionCardFixture7("SideAHand","Objective") objectiveObjects == [i \in {1} |-> objective] claimObjective == [ActiveItemInspectionFixture7(objective) EXCEPT !.step = "ProcedureCode546db7cc4546",!.midDone = TRUE] claimingObjective == [claimObjective EXCEPT !.claimObjectiveResolving = TRUE] moved == [a EXCEPT !.active = FALSE,!.complete = TRUE,!.step = "Complete",!.completionReason = "Moved"] endedMid == [up EXCEPT !.active = FALSE,!.complete = TRUE,!.step = "Complete",!.completionReason = "Moved"] ability == [kind |-> "Conditional",trigger |-> "SourceItemInspectioned",source |-> 1] plan == <<[id |-> 10,kind |-> "ItemInspection",target |-> 2],[id |-> 11,kind |-> "ItemInspection",target |-> 1]>> policy == InspectionPolicy7("CounterExampleFamily064",2) zeroBasic == BasicRetireOption7(card,[exists |-> TRUE,amount |-> 0],TRUE,TRUE) outerItemInspection == [a EXCEPT !.traversalId = 0,!.siteInspectionId = 4,!.caller = "siteInspection4",!.encounterAncestors = {}] innerItemInspection == [a EXCEPT !.id = 78,!.traversalId = 0,!.siteInspectionId = 3,!.caller = "siteInspection3",!.encounterAncestors = {50}] noTraversalControl == [traversal |-> NoTraversal6,encounter |-> 50, siteInspections |-> [id \in {3,4} |-> [encounterAncestors |-> IF id = 3 THEN {50} ELSE {}]], itemInspections |-> [id \in {77,78} |-> IF id = 77 THEN outerItemInspection ELSE innerItemInspection], abortedEncounters |-> {},abortedInspectiones |-> {},abortedItemInspectiones |-> {}, paidOpen |-> FALSE,windows |-> {"outerItemInspectionReaction"},windowCleanupDue |-> FALSE, onlyWindowCleanup |-> FALSE,phaseEndedIds |-> {},phaseStepsSkipped |-> FALSE, redirect |-> NoTraversalRedirect6,redirectStage |-> "NoValue",redirectCheckpointDue |-> FALSE] scopedEnd == EndTraversalOutcome6(noTraversalControl,0) IN /\ ItemInspectionFrameValid7(a) /\ ItemInspectionFrameValid7(moved) /\ ItemInspectionLookGrant7(a,objects,"SideB") /\ ItemInspectionLookGrant7(a,objects,"SideA") /\ ItemInspectionLookGrant7(aDrawPileItemInspection,aDrawPileObjects,"SideB") /\ ~ItemInspectionLookGrant7(aDrawPileItemInspection,aDrawPileObjects,"SideA") /\ ItemInspectionViewers7(aDrawPileItemInspection,aDrawPileObjects,{},FALSE) = {"SideB"} /\ ItemInspectionViewers7(aDrawPileItemInspection,aDrawPileObjects,{},TRUE) = SetupPlayers /\ ~ItemInspectionLookGrant7(moved,objects,"SideB") /\ ItemInspectionAbilityActive7(FALSE,ability) /\ ~ItemInspectionAbilityActive7(FALSE,[ability EXCEPT !.kind = "Paid"]) /\ ~ItemInspectionAbilityActive7(FALSE,[ability EXCEPT !.trigger = "OtherItemInspectioned"]) /\ ItemInspectionAbilityMatches7(ability,[tag |-> "ItemInspectionCard",object |-> 1]) /\ ~ItemInspectionAbilityMatches7(ability,[tag |-> "ItemInspectionCard",object |-> 2]) /\ ExampleFamily034Trigger7(TRUE,TRUE,0) /\ ~ExampleFamily034Trigger7(TRUE,TRUE,1) /\ ~ExampleFamily034Trigger7(TRUE,FALSE,0) /\ ExampleFamily034Reveal7({},{[object |-> 1,loc |-> "SideADeck",viewers |-> SetupPlayers,ability |-> 5]}, aDrawPileItemInspection,aDrawPileObjects,5,TRUE,{[tag |-> "Reveal",object |-> 1,ability |-> 5]}) /\ ~ExampleFamily034Reveal7({},{[object |-> 1,loc |-> "SideADeck",viewers |-> SetupPlayers,ability |-> 5]}, aDrawPileItemInspection,aDrawPileObjects,5,FALSE,{[tag |-> "Reveal",object |-> 1,ability |-> 5]}) /\ MidOptionsValid7({Specimen0115,other}) /\ ~MidOptionsValid7({basic}) /\ zeroBasic.legal /\ zeroBasic.canPay /\ UseMidItemInspection7(a,up,objects,zeroBasic,{zeroBasic},FALSE,FALSE,TRUE,TRUE) /\ MidItemInspectionChoiceAllowed7("Imp",options,TRUE,FALSE) /\ ~MidItemInspectionChoiceAllowed7("Other",options,TRUE,FALSE) /\ ~MidItemInspectionChoiceAllowed7("Decline",options,TRUE,FALSE) /\ MidItemInspectionChoiceAllowed7("BasicRetire",options,TRUE,TRUE) /\ ~MidItemInspectionChoiceAllowed7("Imp",options,FALSE,TRUE) /\ MidItemInspectionChoiceAllowed7("Other",noneAffordable,TRUE,TRUE) /\ MidItemInspectionChoiceAllowed7("Decline",noneAffordable,TRUE,TRUE) /\ MidItemInspectionChoiceAllowed7("Imp",noBasic,TRUE,TRUE) /\ ~MidItemInspectionChoiceAllowed7("Decline",noBasic,TRUE,TRUE) /\ ~MidItemInspectionChoiceAllowed7("BasicRetire",noBasic,FALSE,FALSE) /\ ~MidItemInspectionChoiceAllowed7("Imp",archiveOptions,FALSE,FALSE) /\ ~MidItemInspectionChoiceAllowed7("BasicRetire",archiveOptions,FALSE,FALSE) /\ MidItemInspectionChoiceAllowed7("Other",archiveOptions,FALSE,FALSE) /\ UseMidItemInspection7(a,up,objects,basic,options,FALSE,FALSE,TRUE,TRUE) /\ ~UseMidItemInspection7(a,up,objects,basic,options,FALSE,FALSE,FALSE,TRUE) /\ ~UseMidItemInspection7(a,up,objects,basic,options,FALSE,FALSE,TRUE,FALSE) /\ ~UseMidItemInspection7([a EXCEPT !.midUsed = TRUE],[up EXCEPT !.midUsed = TRUE],objects,basic,options,FALSE,FALSE,TRUE,TRUE) /\ DeclineMidItemInspection7(a,[a EXCEPT !.midDone = TRUE],objects,options,FALSE,FALSE,TRUE) /\ ~DeclineMidItemInspection7(a,[a EXCEPT !.midDone = TRUE],objects,options,TRUE,FALSE,TRUE) /\ FinishMidItemInspection7(up,finish,TRUE) /\ ~FinishMidItemInspection7(up,finish,FALSE) /\ FinishMidItemInspection7(endedMid,[endedMid EXCEPT !.midResolving = FALSE,!.midDone = TRUE],TRUE) /\ ~UseMidItemInspection7(ActiveItemInspectionFixture7(archiveCard), [ActiveItemInspectionFixture7(archiveCard) EXCEPT !.midUsed = TRUE,!.midResolving = TRUE], [i \in {1} |-> archiveCard],Specimen0115,{Specimen0115},FALSE,FALSE,TRUE,TRUE) /\ ItemInspectionClaimObjectiveDisposition7(objective,FALSE,FALSE,FALSE,TRUE) = "ClaimObjective" /\ ItemInspectionClaimObjectiveDisposition7(objective,TRUE,FALSE,TRUE,TRUE) = "DeclineAdditional" /\ ItemInspectionClaimObjectiveDisposition7(objective,TRUE,TRUE,FALSE,TRUE) = "Unable" /\ ResolveItemInspectionClaimObjective7(claimObjective,claimingObjective,objectiveObjects,FALSE,FALSE,FALSE,TRUE,TRUE,FALSE) /\ ResolveItemInspectionClaimObjective7(claimObjective,[claimObjective EXCEPT !.claimObjectiveDone = TRUE],objectiveObjects,TRUE,FALSE,TRUE,TRUE,FALSE,FALSE) /\ ~ResolveItemInspectionClaimObjective7(claimObjective,claimingObjective,objectiveObjects,TRUE,TRUE,TRUE,TRUE,FALSE,TRUE) /\ ~ResolveItemInspectionClaimObjective7(claimObjective,claimingObjective,objectiveObjects,TRUE,TRUE,TRUE,TRUE,TRUE,FALSE) /\ ~ResolveItemInspectionClaimObjective7([claimObjective EXCEPT !.midDone = FALSE],[claimingObjective EXCEPT !.midDone = FALSE],objectiveObjects,FALSE,TRUE,TRUE,TRUE,TRUE,TRUE) /\ FinishItemInspectionClaimObjective7(claimingObjective,[claimingObjective EXCEPT !.claimObjectiveResolving = FALSE,!.claimObjectiveDone = TRUE],TRUE) /\ ~FinishItemInspectionClaimObjective7(claimingObjective,[claimingObjective EXCEPT !.claimObjectiveResolving = FALSE,!.claimObjectiveDone = TRUE],FALSE) /\ FinishItemInspectionClaimObjective7([claimingObjective EXCEPT !.active = FALSE,!.complete = TRUE,!.step = "Complete",!.completionReason = "Moved"], [claimingObjective EXCEPT !.active = FALSE,!.complete = TRUE,!.step = "Complete",!.completionReason = "Moved",!.claimObjectiveResolving = FALSE,!.claimObjectiveDone = TRUE],TRUE) /\ ItemInspectionMovementOutcome7(a,a,objects,TRUE,{}) /\ ItemInspectionMovementOutcome7(a,moved,[i \in {1} |-> [card EXCEPT !.loc = "other"]],TRUE,{ItemInspectionEndEvent7(a)}) /\ ItemInspectionMovementOutcome7(a,moved,[i \in {2} |-> card],TRUE,{ItemInspectionEndEvent7(a)}) /\ ItemInspectionMovementOutcome7(moved,moved,objects,TRUE,{}) /\ ApplyItemInspectionAborts7(a,[moved EXCEPT !.completionReason = "EndTraversal"],{77},{ItemInspectionEndEvent7(a)}) /\ ApplyItemInspectionAborts7(a,a,{78},{}) /\ EndTheTraversal6(noTraversalControl,scopedEnd,0,TRUE,EndTraversalEffectEvents6(noTraversalControl)) /\ scopedEnd.abortedItemInspectiones = {78} /\ scopedEnd.abortedInspectiones = {3} /\ DOMAIN scopedEnd.itemInspections = {77} /\ DOMAIN scopedEnd.siteInspections = {4} /\ scopedEnd.traversal = NoTraversal6 /\ scopedEnd.onlyWindowCleanup /\ ApplyItemInspectionAborts7(outerItemInspection,outerItemInspection,scopedEnd.abortedItemInspectiones,{}) /\ ApplyItemInspectionAborts7(innerItemInspection, [innerItemInspection EXCEPT !.active = FALSE,!.complete = TRUE,!.step = "Complete",!.completionReason = "EndTraversal"], scopedEnd.abortedItemInspectiones,{ItemInspectionEndEvent7(innerItemInspection)}) /\ InformationSiftingPlan7({1,2},<<2,1>>,plan,{}) /\ ~InformationSiftingPlan7({1,2},<<2,1>>,[plan EXCEPT ![2].id = 10],{}) /\ ~InformationSiftingPlan7({1,2},<<2,1>>,plan,{10}) /\ InformationSiftingNext7(1,2,plan,TRUE,TRUE) /\ ~InformationSiftingNext7(1,2,plan,FALSE,TRUE) /\ ~InformationSiftingNext7(1,2,plan,TRUE,FALSE) /\ ~policy.randomLimitEnabled /\ SelectionWithinPolicy7(policy,1) /\ ~SelectionWithinPolicy7(policy,2) /\ InspectionPolicyComplete7(policy,2,FALSE) /\ InspectionPolicyComplete7(policy,1,TRUE) /\ ~SelectionWithinPolicy7(InspectionPolicy7("CounterExampleFamily064",0),0) ItemInspectionProcedureChecks7 == LET card == ItemInspectionCardFixture7("SideAHand","Facility") objects == [i \in {1} |-> card] initial == OpenItemInspection7(77,1,card,1,2,"siteInspection2",{}) begun == [initial EXCEPT !.active = TRUE,!.beginMet = TRUE] mid == [begun EXCEPT !.step = "ProcedureCode1dd0e8f05be2"] decided == [mid EXCEPT !.midDone = TRUE] claimingObjectiveStep == [decided EXCEPT !.step = "ProcedureCode546db7cc4546"] claimObjectiveDone == [claimingObjectiveStep EXCEPT !.claimObjectiveDone = TRUE] last == [claimObjectiveDone EXCEPT !.step = "ProcedureCode662478499367"] complete == [last EXCEPT !.complete = TRUE,!.active = FALSE,!.step = "Complete",!.completionReason = "Normal"] cancelled == [initial EXCEPT !.complete = TRUE,!.step = "Complete",!.completionReason = "ItemInspectionCostDeclined"] movedMid == [mid EXCEPT !.midUsed = TRUE,!.midResolving = TRUE,!.active = FALSE,!.complete = TRUE,!.step = "Complete",!.completionReason = "Moved"] movedClaimObjective == [complete EXCEPT !.claimObjectiveDone = FALSE,!.claimObjectiveResolving = TRUE,!.completionReason = "Moved"] reaction == [kind |-> "Reaction",open |-> TRUE,beginItemInspectionId |-> 77,pending |-> {"mandatory","optional"},lostPending |-> {},priority |-> "SideA"] closed == [reaction EXCEPT !.open = FALSE,!.pending = {},!.lostPending = {"mandatory","optional"},!.priority = "NoValue"] IN /\ Cardinality(ItemInspectionSteps7) = 4 /\ \A s \in ItemInspectionSteps7 : ItemInspectionStepInfo7(s).kind # "Invalid" /\ ~ItemInspectionStepInfo7(s).paidWindow /\ ~ItemInspectionStepInfo7(s).objectivePlacementWindow /\ ~ItemInspectionLookGrant7(initial,objects,"SideB") /\ BeginItemInspection7(initial,begun,objects,TRUE,TRUE,TRUE,{ItemInspectionBeginEvent7(initial)}) /\ ~BeginItemInspection7(initial,begun,objects,FALSE,TRUE,TRUE,{ItemInspectionBeginEvent7(initial)}) /\ ~BeginItemInspection7(initial,begun,objects,TRUE,FALSE,TRUE,{ItemInspectionBeginEvent7(initial)}) /\ ~BeginItemInspection7(initial,begun,objects,TRUE,TRUE,FALSE,{ItemInspectionBeginEvent7(initial)}) /\ ~BeginItemInspection7(initial,begun,[i \in {} |-> card],TRUE,TRUE,TRUE,{ItemInspectionBeginEvent7(initial)}) /\ ~BeginItemInspection7(initial,begun,[i \in {1} |-> [card EXCEPT !.loc = "other"]],TRUE,TRUE,TRUE,{ItemInspectionBeginEvent7(initial)}) /\ ~BeginItemInspection7(begun,begun,objects,TRUE,TRUE,TRUE,{ItemInspectionBeginEvent7(initial)}) /\ AdvanceItemInspectionStep7(begun,mid,objects,TRUE,TRUE) /\ ~AdvanceItemInspectionStep7(begun,mid,objects,TRUE,FALSE) /\ ~AdvanceItemInspectionStep7(begun,mid,objects,FALSE,TRUE) /\ ~AdvanceItemInspectionStep7(mid,[mid EXCEPT !.step = "ProcedureCode546db7cc4546"],objects,TRUE,TRUE) /\ AdvanceItemInspectionStep7(decided,claimingObjectiveStep,objects,TRUE,TRUE) /\ ~AdvanceItemInspectionStep7(claimingObjectiveStep,[claimingObjectiveStep EXCEPT !.step = "ProcedureCode662478499367"],objects,TRUE,TRUE) /\ ResolveItemInspectionClaimObjective7(claimingObjectiveStep,claimObjectiveDone,objects,FALSE,FALSE,FALSE,TRUE,TRUE,TRUE) /\ AdvanceItemInspectionStep7(claimObjectiveDone,last,objects,TRUE,TRUE) /\ CompleteNormalItemInspection7(last,complete,objects,TRUE,{ItemInspectionEndEvent7(last)}) /\ ~CompleteNormalItemInspection7(last,complete,objects,FALSE,{ItemInspectionEndEvent7(last)}) /\ ~CompleteNormalItemInspection7([last EXCEPT !.claimObjectiveDone = FALSE],[complete EXCEPT !.claimObjectiveDone = FALSE],objects,TRUE,{ItemInspectionEndEvent7(last)}) /\ ~CompleteNormalItemInspection7(complete,complete,objects,TRUE,{ItemInspectionEndEvent7(last)}) /\ CancelUnstartedItemInspection7(initial,cancelled,"ItemInspectionCostDeclined",TRUE,{}) /\ ~CancelUnstartedItemInspection7(begun,[cancelled EXCEPT !.active = TRUE,!.beginMet = TRUE],"ItemInspectionCostDeclined",TRUE,{}) /\ ~cancelled.beginMet /\ CloseEndedItemInspectionBeginReaction7(reaction,closed,complete) /\ ~CloseEndedItemInspectionBeginReaction7(reaction,closed,begun) /\ ~CloseEndedItemInspectionBeginReaction7([reaction EXCEPT !.beginItemInspectionId = 78],[closed EXCEPT !.beginItemInspectionId = 78],complete) /\ ~CloseEndedItemInspectionBeginReaction7(reaction,closed,cancelled) /\ ReturnItemInspectionToCaller7(complete,[complete EXCEPT !.returned = TRUE],TRUE,"siteInspection2") /\ ReturnItemInspectionToCaller7(cancelled,[cancelled EXCEPT !.returned = TRUE],TRUE,"siteInspection2") /\ ~ReturnItemInspectionToCaller7(complete,[complete EXCEPT !.returned = TRUE],FALSE,"siteInspection2") /\ ~ReturnItemInspectionToCaller7(complete,[complete EXCEPT !.returned = TRUE],TRUE,"other") /\ ~ReturnItemInspectionToCaller7(movedMid,[movedMid EXCEPT !.returned = TRUE],TRUE,"siteInspection2") /\ ~ReturnItemInspectionToCaller7(movedClaimObjective,[movedClaimObjective EXCEPT !.returned = TRUE],TRUE,"siteInspection2") /\ FinishItemInspectionClaimObjective7(movedClaimObjective,[movedClaimObjective EXCEPT !.claimObjectiveResolving = FALSE,!.claimObjectiveDone = TRUE],TRUE) /\ ReturnItemInspectionToCaller7([movedClaimObjective EXCEPT !.claimObjectiveResolving = FALSE,!.claimObjectiveDone = TRUE], [movedClaimObjective EXCEPT !.claimObjectiveResolving = FALSE,!.claimObjectiveDone = TRUE,!.returned = TRUE],TRUE,"siteInspection2") /\ ~ReturnItemInspectionToCaller7([complete EXCEPT !.returned = TRUE],[complete EXCEPT !.returned = TRUE],TRUE,"siteInspection2") /\ ReturnItemInspectionToCaller7([movedMid EXCEPT !.midResolving = FALSE,!.midDone = TRUE], [movedMid EXCEPT !.midResolving = FALSE,!.midDone = TRUE,!.returned = TRUE],TRUE,"siteInspection2") /\ ItemInspectionProcedureValid7(initial,objects) /\ ItemInspectionProcedureValid7(begun,objects) /\ ItemInspectionProcedureValid7(complete,objects) ArchiveCardFixture7(zone) == [form |-> "Card",side |-> "SideA",zone |-> zone,loc |-> zone,kind |-> "Facility",deployed |-> FALSE,face |-> "Down"] InspectionConceptChecks7 == LET empty == [id \in {} |-> id] b == [OpenInspection7(2,"SchemaAtom082","SchemaAtom082",1,"RulesTraversalInspection","traversal1",{},InspectionPolicy7("Normal",0)) EXCEPT !.active = TRUE,!.beginMet = TRUE,!.step = "ProcedureCode91f3ee0da236"] added == [b EXCEPT !.randomLimit = 2] fixed == [added EXCEPT !.limitSet = TRUE] choose == [fixed EXCEPT !.step = "ProcedureCode1404a82ab3ee"] view == [roots |-> {3},central |-> {1,2}] chosen == [choose EXCEPT !.choices = <<[object |-> 1,source |-> "SchemaAtom033",chooser |-> "SideB"]>>, !.selectionPending = TRUE,!.selectedObject = 1,!.selectedSource = "SchemaAtom033"] itemInspectionStep == [chosen EXCEPT !.step = "ProcedureCodee35e7c8fc57b"] card == ItemInspectionCardFixture7("SideAHand","Facility") a == [OpenItemInspection7(77,1,card,1,2,InspectionItemInspectionCaller7(b),{}) EXCEPT !.beginMet = TRUE,!.active = TRUE] attached == [itemInspectionStep EXCEPT !.currentItemInspectionId = 77,!.usedItemInspectionIds = {77}] history == [id \in {77} |-> [object |-> 1,traversalId |-> 1,siteInspectionId |-> 2,turnId |-> 1,hadRetireCost |-> TRUE]] objects == [id \in {1,2,3} |-> ArchiveCardFixture7(IF id=3 THEN "SideAHand" ELSE "SideADiscard")] archive == [b EXCEPT !.targetSite = "SchemaAtom018",!.kind = "SchemaAtom018",!.step = "ProcedureCodeb6067693902e"] archiveReady == [archive EXCEPT !.archivesPrepared = TRUE] flipped == [id \in DOMAIN objects |-> IF id \in {1,2} THEN [objects[id] EXCEPT !.face = "Up"] ELSE objects[id]] request == [targetSite |-> "SchemaAtom018",kind |-> "SchemaAtom018",traversalId |-> 1,origin |-> "CardEffectInspection",caller |-> "oldAbility"] delayed == [id \in {9} |-> [controller |-> "SideB",triggerInspectionId |-> 2,request |-> request,pending |-> FALSE]] pending == [delayed EXCEPT ![9].pending = TRUE] take == [perform |-> TRUE,request |-> [request EXCEPT !.caller = <<"DelayedInspection",9>>]] rootChosen == [choose EXCEPT !.choices = <<[object |-> 3,source |-> "Root",chooser |-> "SideB"]>>, !.selectionPending = TRUE,!.selectedObject = 3,!.selectedSource = "Root"] limitReached == [choose EXCEPT !.randomLimit = 1,!.choices = <<[object |-> 1,source |-> "SchemaAtom033",chooser |-> "SideB"]>>] capBefore == [choose EXCEPT !.limitSet = FALSE,!.policy = InspectionPolicy7("CounterExampleFamily064",2), !.choices = <<[object |-> 3,source |-> "Root",chooser |-> "SideB"]>>] capAfter == [capBefore EXCEPT !.selectionPending = TRUE,!.selectedObject = 1,!.selectedSource = "SchemaAtom033", !.choices = Append(@,[object |-> 1,source |-> "SchemaAtom033",chooser |-> "SideB"])] twoPending == [id \in {9,10} |-> [controller |-> "SideB",triggerInspectionId |-> 2,request |-> request,pending |-> TRUE]] mixedDelayed == [id \in {9,10} |-> [controller |-> "SideB",triggerInspectionId |-> IF id=9 THEN 2 ELSE 4,request |-> request,pending |-> FALSE]] lateObjects == [id \in {1,2,3,4} |-> IF id=4 THEN ArchiveCardFixture7("SideADiscard") ELSE flipped[id]] successorObjects == [id \in {2,3,4} |-> IF id=4 THEN objects[1] ELSE objects[id]] lateItemInspection == [OpenItemInspection7(78,4,lateObjects[4],1,2,InspectionItemInspectionCaller7(archive),{}) EXCEPT !.active = TRUE,!.beginMet = TRUE] IN /\ b.randomLimit = 1 /\ AddAdditionalItemInspectiones7(b,added,1,TRUE) /\ ~AddAdditionalItemInspectiones7(b,added,1,FALSE) /\ FreezeInspectionLimit7(added,fixed,TRUE) /\ ~FreezeInspectionLimit7(added,fixed,FALSE) /\ ~AddAdditionalItemInspectiones7(fixed,[fixed EXCEPT !.randomLimit = 3],1,TRUE) /\ PrepareDiscardSite7(archive,archiveReady,objects,flipped) /\ ~PrepareDiscardSite7(archiveReady,archiveReady,flipped,flipped) /\ flipped[3].face = "Down" /\ lateObjects[4].face = "Down" /\ ItemInspectionLookGrant7(lateItemInspection,lateObjects,"SideB") /\ ~PrepareDiscardSite7(archiveReady,archiveReady,lateObjects, [id \in DOMAIN lateObjects |-> IF id=4 THEN [lateObjects[id] EXCEPT !.face = "Up"] ELSE lateObjects[id]]) /\ InspectionPresentation7(choose,view).specific = {3} /\ InspectionPresentation7(choose,view).randomCentralAOffered /\ ChooseCentralAInspectionCard7(choose,chosen,view,1,0,FALSE,TRUE) /\ ChooseCentralAInspectionCard7(choose,chosen,view,0,1,TRUE,FALSE) /\ ChooseSpecificInspectionCard7(choose,rootChosen,3,view) /\ ChooseSpecificInspectionCard7(limitReached,[rootChosen EXCEPT !.randomLimit = 1, !.choices = <<[object |-> 1,source |-> "SchemaAtom033",chooser |-> "SideB"],[object |-> 3,source |-> "Root",chooser |-> "SideB"]>>],3,view) /\ ChooseCentralAInspectionCard7(capBefore,capAfter,view,1,0,FALSE,TRUE) /\ ~InspectionSelectionReady7([capAfter EXCEPT !.selectionPending = FALSE]) /\ ~ChooseCentralAInspectionCard7(choose,chosen,view,1,0,FALSE,FALSE) /\ ~ChooseSpecificInspectionCard7(choose,chosen,1,view) /\ ~ChooseCentralAInspectionCard7(choose,[chosen EXCEPT !.selectedObject = 4, !.choices = <<[object |-> 4,source |-> "SchemaAtom033",chooser |-> "SideB"]>>],view,4,0,FALSE,TRUE) /\ ~RecordInspectionChoice7([choose EXCEPT !.choices = <<[object |-> 2,source |-> "SchemaAtom033",chooser |-> "SideB"]>>,!.randomLimit = 1], [chosen EXCEPT !.randomLimit = 1,!.choices = <<[object |-> 2,source |-> "SchemaAtom033",chooser |-> "SideB"],[object |-> 1,source |-> "SchemaAtom033",chooser |-> "SideB"]>>], 1,"SchemaAtom033",view,"RandomCentralA",TRUE) /\ AttachChosenItemInspection7(itemInspectionStep,attached,a,ItemInspectionBeginEvent7(a)) /\ ~AttachChosenItemInspection7(itemInspectionStep,attached,[a EXCEPT !.object = 2],ItemInspectionBeginEvent7([a EXCEPT !.object = 2])) /\ FinishInspectionItemInspectionInstruction7(attached,[attached EXCEPT !.selectionPending = FALSE,!.selectedObject = 0,!.selectedSource = "NoValue",!.currentItemInspectionId = 0],TRUE) /\ ~FinishInspectionItemInspectionInstruction7(attached,[attached EXCEPT !.selectionPending = FALSE,!.selectedObject = 0,!.selectedSource = "NoValue",!.currentItemInspectionId = 0],FALSE) /\ RecordActualItemInspection7(empty,history,a,1,TRUE,ItemInspectionBeginEvent7(a)) /\ RecordActualItemInspection7(empty,[history EXCEPT ![77].turnId = 0],a,0,TRUE,ItemInspectionBeginEvent7(a)) /\ ~RecordActualItemInspection7(empty,history,[a EXCEPT !.beginMet = FALSE],1,TRUE,ItemInspectionBeginEvent7(a)) /\ ~RecordActualItemInspection7(history,history,a,1,TRUE,ItemInspectionBeginEvent7(a)) /\ ActualItemInspectionesInTraversal7(history,1) = {77} /\ ActualItemInspectionesInTraversal7(history,0) = {} /\ ActualItemInspectionesInInspection7(history,2) = {77} /\ ItemInspectionHistoryCostCount7(history,1) = 1 /\ InspectionObjectVisible7(choose,history,objects,1) /\ ~InspectionObjectVisible7(choose,history,objects,2) /\ ~InspectionObjectVisible7(choose,history,successorObjects,4) /\ ~InspectionObjectVisible7(choose,history,successorObjects,1) /\ ~InspectionObjectVisible7(choose,[history EXCEPT ![77].siteInspectionId = 4],objects,1) /\ ~InspectionObjectVisible7(choose,history,[id \in {2,3} |-> objects[id]],1) /\ ~InspectionObjectVisible7([choose EXCEPT !.active = FALSE,!.complete = TRUE],history,objects,1) /\ Len(chosen.choices) = 1 /\ InspectionCentralChoices7(chosen) = 1 /\ ActualItemInspectionesInInspection7(empty,2) = {} /\ DelayInspection7(empty,delayed,9,{},2,request,TRUE) /\ ~DelayInspection7(empty,delayed,9,{9},2,request,TRUE) /\ ~DelayInspection7(empty,[delayed EXCEPT ![9].triggerInspectionId = 0],9,{},0,request,TRUE) /\ MarkDelayedInspectiones7(delayed,pending,InspectionEndEvent7(b)) /\ MarkDelayedInspectiones7(mixedDelayed,[mixedDelayed EXCEPT ![9].pending = TRUE],InspectionEndEvent7(b)) /\ MarkDelayedInspectiones7(mixedDelayed,mixedDelayed,[InspectionEndEvent7(b) EXCEPT !.siteInspectionId = 5]) /\ TakeDelayedInspection7(pending,empty,9,0,TRUE,TRUE,take) /\ ~TakeDelayedInspection7(delayed,empty,9,0,TRUE,TRUE,take) /\ ~TakeDelayedInspection7(pending,empty,9,3,TRUE,TRUE,take) /\ TakeDelayedInspection7(pending,empty,9,0,TRUE,FALSE,[take EXCEPT !.perform = FALSE]) /\ TakeDelayedInspection7(twoPending,[id \in {9} |-> twoPending[id]],10,0,TRUE,TRUE, [perform |-> TRUE,request |-> [request EXCEPT !.caller = <<"DelayedInspection",10>>]]) /\ ApplyInspectionAborts7(choose,[choose EXCEPT !.active = FALSE,!.complete = TRUE,!.step = "Complete",!.completionReason = "EndTraversal"],{2},{InspectionEndEvent7(choose)}) /\ ApplyInspectionAborts7(choose,choose,{3},{}) CandidateCardFixture7(zone,targetSite,area,host) == [form |-> "Card",side |-> "SideA",zone |-> zone,loc |-> <>, kind |-> "Attachment",deployed |-> zone = "Play",face |-> "Down",targetSite |-> targetSite,area |-> area,host |-> host] CandidateChecks7 == LET b == [OpenInspection7(2,"SchemaAtom082","SchemaAtom082",1,"RulesTraversalInspection","traversal1",{},InspectionPolicy7("Normal",0)) EXCEPT !.active = TRUE,!.beginMet = TRUE,!.step = "ProcedureCode1404a82ab3ee",!.limitSet = TRUE,!.randomLimit = 2] hand == CandidateCardFixture7("SideAHand","NoValue","NoValue",0) deckCard == CandidateCardFixture7("SideADeck","NoValue","NoValue",0) discard == CandidateCardFixture7("SideADiscard","NoValue","NoValue",0) root == CandidateCardFixture7("Play","SchemaAtom082","Root",0) objects == [id \in 1..7 |-> CASE id \in {1,2} -> hand [] id = 3 -> root [] id = 4 -> [root EXCEPT !.targetSite = "SchemaAtom018"] [] id = 5 -> discard [] id = 6 -> [root EXCEPT !.area = "Hosted",!.host = 3] [] OTHER -> [root EXCEPT !.area = "Protecting"]] m == OpenCandidateCapacity7(b,objects) chosen == [b EXCEPT !.choices = <<[object |-> 1,source |-> "SchemaAtom033",chooser |-> "SideB"]>>] capped == [chosen EXCEPT !.choices = Append(@,[object |-> 2,source |-> "SchemaAtom033",chooser |-> "SideB"])] history == [id \in {77} |-> [object |-> 1,traversalId |-> 1,siteInspectionId |-> 10,turnId |-> 1,hadRetireCost |-> FALSE]] emptyHistory == [id \in {} |-> id] arrived == [id \in 1..8 |-> IF id=8 THEN [root EXCEPT !.deployed = FALSE] ELSE objects[id]] waiting == [m EXCEPT !.pendingRoots = {8}] admitted == [waiting EXCEPT !.admittedRoots = {3,8},!.pendingRoots = {}] denied == [waiting EXCEPT !.deniedRoots = {8},!.pendingRoots = {}] reentry == [admitted EXCEPT !.admittedRoots = {3},!.pendingRoots = {8}] archives == [b EXCEPT !.targetSite = "SchemaAtom018",!.kind = "SchemaAtom018",!.archivesPrepared = TRUE] am == OpenCandidateCapacity7(archives,objects) movedUpgrade == [id \in {1,2,3,5,6,7,8} |-> IF id=8 THEN discard ELSE objects[id]] archiveChosen == [archives EXCEPT !.choices = <<[object |-> 4,source |-> "Root",chooser |-> "SideB"]>>] aDrawPile == [b EXCEPT !.targetSite = "SchemaAtom129",!.kind = "SchemaAtom129",!.randomLimit = 4] aDrawPileObjects == [id \in {1,2,3} |-> deckCard] rm == OpenCandidateCapacity7(aDrawPile,aDrawPileObjects) aDrawPileChosen == [aDrawPile EXCEPT !.choices = <<[object |-> 1,source |-> "SchemaAtom033",chooser |-> "SideB"]>>] addedTop == [id \in {1,2,3,4} |-> deckCard] renewed == [id \in {2,3,4} |-> deckCard] deniedReentry == [denied EXCEPT !.pendingRoots = {8}] IN /\ InspectionRootCards7(b,objects) = {3} /\ CandidateInputsValid7(b,m,objects,<<>>) /\ InspectionCandidates7(b,m,objects,<<>>,{} ) = [roots |-> {3},central |-> {1,2}] /\ InspectionCandidates7(b,m,objects,<<>>,{1,3}) = [roots |-> {},central |-> {2}] /\ InspectionCandidates7(chosen,m,objects,<<>>,{}).central = {2} /\ InspectionCandidates7(chosen,m,objects,<<>>,{2}).central = {} /\ InspectionCandidates7(chosen,m,objects,<<>>,{}).central = {2} /\ InspectionCandidates7(capped,m,objects,<<>>,{}).central = {} /\ InspectionCandidates7(capped,m,objects,<<>>,{}).roots = {3} /\ InspectionCandidates7(capped,m,[id \in 1..8 |-> IF id=8 THEN hand ELSE objects[id]],<<>>,{}).central = {} /\ InspectionCandidates7([capped EXCEPT !.policy = InspectionPolicy7("CounterExampleFamily064",3)],m, [id \in 1..8 |-> IF id=8 THEN hand ELSE objects[id]],<<>>,{}).central = {8} /\ InspectionCandidates7([capped EXCEPT !.policy = InspectionPolicy7("CounterExampleFamily064",3)],m,arrived,<<>>,{}).central = {} /\ OneCardTraversalProhibition7(b,emptyHistory,DOMAIN objects,TRUE,{3}) = {} /\ OneCardTraversalProhibition7(b,history,DOMAIN objects,TRUE,{3}) = DOMAIN objects \ {3} /\ OneCardTraversalProhibition7(b,history,DOMAIN objects,FALSE,{3}) = {} /\ OneCardTraversalProhibition7([b EXCEPT !.traversalId = 2],history,DOMAIN objects,TRUE,{3}) = {} /\ b.randomLimit = 2 /\ InspectionCandidates7(b,m,objects,<<>>,OneCardTraversalProhibition7(b,history,DOMAIN objects,TRUE,{3})) = [roots |-> {3},central |-> {}] /\ InspectionCandidates7(b,m,objects,<<>>,OneCardTraversalProhibition7(b,history,DOMAIN objects,FALSE,{3})).central = {1,2} /\ ObserveRootEntries7(m,waiting,b,arrived,{8}) /\ InspectionCandidates7(b,waiting,arrived,<<>>,{}).roots = {3} /\ DecideRootAdmissions7(waiting,admitted,b,arrived,{8},"ProcedureCode7f181ce21011",TRUE) /\ ~DecideRootAdmissions7(waiting,admitted,b,arrived,{8},"ProcedureCode2d6279f9d639",TRUE) /\ ~DecideRootAdmissions7(waiting,admitted,b,arrived,{8},"ProcedureCode7f181ce21011",FALSE) /\ ~DecideRootAdmissions7(waiting,admitted,b,arrived,{1},"ProcedureCode7f181ce21011",TRUE) /\ InspectionCandidates7(b,admitted,arrived,<<>>,{}).roots = {3,8} /\ DecideRootAdmissions7(waiting,denied,b,arrived,{},"ProcedureCode7f181ce21011",TRUE) /\ InspectionCandidates7(b,denied,arrived,<<>>,{}).roots = {3} /\ InspectionCandidates7(b,denied,[id \in 1..8 |-> IF id=8 THEN hand ELSE objects[id]],<<>>,{}).central = {1,2} /\ InspectionCandidates7(b,admitted,arrived,<<>>,{8}).roots = {3} /\ InspectionCandidates7(b,admitted,arrived,<<>>,{}).roots = {3,8} /\ ObserveRootEntries7(admitted,reentry,b,arrived,{8}) /\ InspectionCandidates7(b,reentry,arrived,<<>>,{}).roots = {3} /\ ObserveRootEntries7(denied,deniedReentry,b,arrived,{8}) /\ DecideRootAdmissions7(deniedReentry,denied,b,arrived,{8},"ProcedureCode7f181ce21011",TRUE) /\ ObserveRootEntries7(admitted,[admitted EXCEPT !.admittedRoots = {3}],b,objects,{}) /\ InspectionCandidates7(archives,am,objects,<<>>,{} ) = [roots |-> {4},central |-> {5}] /\ InspectionCandidates7(archiveChosen,[am EXCEPT !.admittedRoots = {}],movedUpgrade,<<>>,{}).central = {5,8} /\ InspectionCandidates7(b,m,[id \in {2,3,4,5,6,7,8} |-> IF id=8 THEN hand ELSE objects[id]],<<>>,{}).central = {2,8} /\ DeckOrderValid7(aDrawPileObjects,<<1,2,3>>) /\ ~DeckOrderValid7(aDrawPileObjects,<<1,1,2,3>>) /\ ~DeckOrderValid7(aDrawPileObjects,<<1,2>>) /\ ~DeckOrderValid7(aDrawPileObjects,<<4,1,2,3>>) /\ ~DeckOrderValid7([id \in 1..4 |-> IF id=4 THEN hand ELSE deckCard],<<4,1,2,3>>) /\ InspectionCandidates7(aDrawPile,rm,aDrawPileObjects,<<1,2,3>>,{}).central = {1} /\ InspectionCandidates7(aDrawPileChosen,rm,aDrawPileObjects,<<1,2,3>>,{}).central = {2} /\ InspectionCandidates7(aDrawPileChosen,rm,aDrawPileObjects,<<1,2,3>>,{2}).central = {3} /\ InspectionCandidates7(aDrawPileChosen,rm,addedTop,<<4,1,2,3>>,{}).central = {4} /\ InspectionCandidates7(aDrawPileChosen,rm,addedTop,<<1,4,2,3>>,{}).central = {4} /\ InspectionCandidates7(aDrawPileChosen,rm,renewed,<<4,2,3>>,{}).central = {4} /\ InspectionCandidatesDirection7(aDrawPileChosen,rm,aDrawPileObjects,<<1,2,3>> ,{},TRUE).central = {3} /\ InspectionCandidates7([aDrawPileChosen EXCEPT !.randomLimit = 1],rm,addedTop,<<4,1,2,3>>,{}).central = {} /\ \A prohibited \in SUBSET {1,2,3} : Cardinality(InspectionCandidates7(aDrawPileChosen,rm,aDrawPileObjects,<<3,2,1>>,prohibited).central) <= 1 /\ DeriveCandidateView7(aDrawPile,rm,aDrawPileObjects,<<1,2,3>>,{},FALSE,[roots |-> {},central |-> {1}]) /\ ~DeriveCandidateView7(aDrawPile,[rm EXCEPT !.siteInspectionId = 4],aDrawPileObjects,<<1,2,3>>,{},FALSE,[roots |-> {},central |-> {1}]) /\ ~DeriveCandidateView7(aDrawPile,rm,aDrawPileObjects,<<4,1,2,3>>,{},FALSE,[roots |-> {},central |-> {4}]) /\ ~DeriveCandidateView7(aDrawPile,rm,[id \in 1..4 |-> IF id=4 THEN hand ELSE deckCard],<<4,1,2,3>>,{},FALSE,[roots |-> {},central |-> {4}]) /\ ~DeriveCandidateView7(aDrawPile,rm,aDrawPileObjects,<<1,2,3>>,{},FALSE,[roots |-> {},central |-> {2}]) /\ ~DeriveCandidateView7(aDrawPile,rm,aDrawPileObjects,<<1,1,2,3>>,{},FALSE,[roots |-> {},central |-> {1}]) /\ InspectionCandidates7([b EXCEPT !.active = FALSE,!.complete = TRUE],m,objects,<<>>,{} ) = [roots |-> {},central |-> {}] InspectionProcedureChecks7 == LET objects == [id \in {1} |-> CandidateCardFixture7("SideAHand","NoValue","NoValue",0)] initial == OpenInspection7(2,"SchemaAtom082","SchemaAtom082",1,"RulesTraversalInspection","traversal1",{},InspectionPolicy7("Normal",0)) begun == [initial EXCEPT !.active = TRUE,!.beginMet = TRUE] m == OpenCandidateCapacity7(begun,objects) prepare == [begun EXCEPT !.step = "ProcedureCodeb6067693902e"] limits == [prepare EXCEPT !.step = "ProcedureCode91f3ee0da236"] fixed == [limits EXCEPT !.limitSet = TRUE] select == [fixed EXCEPT !.step = "ProcedureCode1404a82ab3ee"] chosen == [select EXCEPT !.choices = <<[object |-> 1,source |-> "SchemaAtom033",chooser |-> "SideB"]>>, !.selectionPending = TRUE,!.selectedObject = 1,!.selectedSource = "SchemaAtom033"] itemInspection == [chosen EXCEPT !.step = "ProcedureCodee35e7c8fc57b"] finished == [itemInspection EXCEPT !.selectionPending = FALSE,!.selectedObject = 0,!.selectedSource = "NoValue"] repeat == [finished EXCEPT !.step = "ProcedureCodeb1fbc90c4ab0"] again == [repeat EXCEPT !.step = "ProcedureCode1404a82ab3ee"] last == [again EXCEPT !.step = "ProcedureCode8c612115d469"] complete == [last EXCEPT !.step = "Complete",!.active = FALSE,!.complete = TRUE,!.completionReason = "Normal"] aborted == [itemInspection EXCEPT !.currentItemInspectionId = 77,!.usedItemInspectionIds = {77},!.active = FALSE, !.complete = TRUE,!.step = "Complete",!.completionReason = "EndTraversal"] drained == [aborted EXCEPT !.selectionPending = FALSE,!.selectedObject = 0,!.selectedSource = "NoValue",!.currentItemInspectionId = 0] reaction == [kind |-> "Reaction",open |-> TRUE,beginInspectionId |-> 2,pending |-> {"mandatory","optional"}, lostPending |-> {},priority |-> "SideB"] closed == [reaction EXCEPT !.open = FALSE,!.pending = {},!.lostPending = {"mandatory","optional"},!.priority = "NoValue"] emptyObjects == [id \in {} |-> id] IN /\ Cardinality(InspectionSteps7) = 7 /\ \A step \in InspectionSteps7 : InspectionStepInfo7(step).kind # "Invalid" /\ ~InspectionStepInfo7(step).paidWindow /\ ~InspectionStepInfo7(step).objectivePlacementWindow /\ BeginInspectionWithCandidates7(initial,begun,m,objects,0,{"SchemaAtom082"},TRUE,TRUE,{InspectionBeginEvent7(initial)}) /\ ~BeginInspection7(initial,begun,3,{"SchemaAtom082"},TRUE,TRUE,{InspectionBeginEvent7(initial)}) /\ ~BeginInspection7(initial,begun,0,{"SchemaAtom018"},TRUE,TRUE,{InspectionBeginEvent7(initial)}) /\ ~BeginInspection7(initial,begun,0,{"SchemaAtom082"},FALSE,TRUE,{InspectionBeginEvent7(initial)}) /\ ~BeginInspection7(initial,begun,0,{"SchemaAtom082"},TRUE,FALSE,{InspectionBeginEvent7(initial)}) /\ ~BeginInspection7([initial EXCEPT !.kind = "SchemaAtom132"],[begun EXCEPT !.kind = "SchemaAtom132"],0,{"SchemaAtom082"},TRUE,TRUE,{InspectionBeginEvent7(initial)}) /\ ~BeginInspection7(begun,begun,0,{"SchemaAtom082"},TRUE,TRUE,{InspectionBeginEvent7(initial)}) /\ AdvanceInspectionStep7(begun,prepare,TRUE,TRUE) /\ ~AdvanceInspectionStep7(begun,prepare,TRUE,FALSE) /\ ~AdvanceInspectionStep7(begun,prepare,FALSE,TRUE) /\ AdvanceInspectionStep7(prepare,limits,TRUE,TRUE) /\ ~AdvanceInspectionStep7([prepare EXCEPT !.kind = "SchemaAtom018",!.targetSite = "SchemaAtom018"], [limits EXCEPT !.kind = "SchemaAtom018",!.targetSite = "SchemaAtom018"],TRUE,TRUE) /\ ~AdvanceInspectionStep7(limits,[limits EXCEPT !.step = "ProcedureCode1404a82ab3ee"],TRUE,TRUE) /\ FreezeInspectionLimit7(limits,fixed,TRUE) /\ AdvanceInspectionStep7(fixed,select,TRUE,TRUE) /\ ~SkipInspectionSelection7(select,[select EXCEPT !.step = "ProcedureCode8c612115d469"],m,objects,<<>>,{},FALSE,TRUE) /\ SkipInspectionSelection7(select,[select EXCEPT !.step = "ProcedureCode8c612115d469"],m,objects,<<>>,{1},FALSE,TRUE) /\ SkipInspectionSelection7(select,[select EXCEPT !.step = "ProcedureCode8c612115d469"],m,emptyObjects,<<>>,{},FALSE,TRUE) /\ ~SkipInspectionSelection7(select,[select EXCEPT !.step = "ProcedureCode8c612115d469"],m,emptyObjects,<<>>,{},FALSE,FALSE) /\ SkipInspectionSelection7([select EXCEPT !.policy = InspectionPolicy7("CounterExampleFamily064",0)], [select EXCEPT !.policy = InspectionPolicy7("CounterExampleFamily064",0),!.step = "ProcedureCode8c612115d469"],m,objects,<<>>,{},FALSE,TRUE) /\ ~SkipInspectionSelection7(chosen,[chosen EXCEPT !.step = "ProcedureCode8c612115d469"],m,objects,<<>>,{},FALSE,TRUE) /\ AdvanceInspectionSelection7(chosen,itemInspection,TRUE) /\ ~AdvanceInspectionSelection7(chosen,itemInspection,FALSE) /\ ~AdvanceInspectionSelection7(select,[select EXCEPT !.step = "ProcedureCodee35e7c8fc57b"],TRUE) /\ ~AdvanceInspectionStep7(itemInspection,[itemInspection EXCEPT !.step = "ProcedureCodeb1fbc90c4ab0"],TRUE,TRUE) /\ ~AdvanceInspectionStep7([finished EXCEPT !.currentItemInspectionId = 77],[repeat EXCEPT !.currentItemInspectionId = 77],TRUE,TRUE) /\ AdvanceInspectionStep7(finished,repeat,TRUE,TRUE) /\ AdvanceInspectionStep7(repeat,again,TRUE,TRUE) /\ SkipInspectionSelection7(again,last,m,objects,<<>>,{},FALSE,TRUE) /\ CompleteNormalInspection7(last,complete,TRUE,{InspectionEndEvent7(last)}) /\ ~CompleteNormalInspection7(select,[select EXCEPT !.step = "Complete",!.active = FALSE, !.complete = TRUE,!.completionReason = "Normal"],TRUE,{InspectionEndEvent7(select)}) /\ ~CompleteNormalInspection7(last,complete,FALSE,{InspectionEndEvent7(last)}) /\ ~CompleteNormalInspection7([last EXCEPT !.selectionPending = TRUE], [complete EXCEPT !.selectionPending = TRUE],TRUE,{InspectionEndEvent7(last)}) /\ ~CompleteNormalInspection7(complete,complete,TRUE,{InspectionEndEvent7(last)}) /\ CloseEndedInspectionBeginReaction7(reaction,closed,complete) /\ ~CloseEndedInspectionBeginReaction7(reaction,closed,begun) /\ ~CloseEndedInspectionBeginReaction7([reaction EXCEPT !.beginInspectionId = 3],[closed EXCEPT !.beginInspectionId = 3],complete) /\ ~ReturnInspectionToCaller7(aborted,[aborted EXCEPT !.returned = TRUE],TRUE,"traversal1") /\ ~ReturnInspectionToCaller7([aborted EXCEPT !.currentItemInspectionId = 0], [aborted EXCEPT !.currentItemInspectionId = 0,!.returned = TRUE],TRUE,"traversal1") /\ DrainEndedInspectionInstruction7(aborted,drained,TRUE) /\ ~DrainEndedInspectionInstruction7(aborted,drained,FALSE) /\ ReturnInspectionToCaller7(drained,[drained EXCEPT !.returned = TRUE],TRUE,"traversal1") /\ ReturnInspectionToCaller7(complete,[complete EXCEPT !.returned = TRUE],TRUE,"traversal1") /\ ~ReturnInspectionToCaller7(complete,[complete EXCEPT !.returned = TRUE],FALSE,"traversal1") /\ ~ReturnInspectionToCaller7(complete,[complete EXCEPT !.returned = TRUE],TRUE,"another") /\ ~ReturnInspectionToCaller7([complete EXCEPT !.returned = TRUE],[complete EXCEPT !.returned = TRUE],TRUE,"traversal1") /\ InspectionProcedureValid7(initial) /\ InspectionProcedureValid7(begun) /\ InspectionProcedureValid7(complete) /\ InspectionProcedureValid7(aborted) Block7Assertions == CASE block7 = 0 -> TRUE [] block7 = 1 -> ItemInspectionConceptChecks7 [] block7 = 2 -> ItemInspectionProcedureChecks7 [] block7 = 3 -> InspectionConceptChecks7 [] block7 = 4 -> CandidateChecks7 [] block7 = 5 -> InspectionProcedureChecks7 =============================================================================