InspectionChecksMC¶
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 122 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.
ActiveItemInspectionFixture7 · operator
reference-profile · input revision 2 · CC0 1.0
ActiveItemInspectionFixture7(card) ==
[OpenItemInspection7(77,1,card,1,2,"siteInspection2",{}) EXCEPT !.active = TRUE,!.beginMet = TRUE,!.step = "ProcedureCode1dd0e8f05be2"]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: OpenItemInspection7
ArchiveCardFixture7 · operator
reference-profile · input revision 2 · CC0 1.0
ArchiveCardFixture7(zone) ==
[form |-> "Card",side |-> "SideA",zone |-> zone,loc |-> zone,kind |-> "Facility",deployed |-> FALSE,face |-> "Down"]Exact module download · Source bundle and reproduction instructions
Block7Assertions · operator
reference-profile · input revision 2 · CC0 1.0
Block7Assertions ==
CASE block7 = 0 -> TRUE
[] block7 = 1 -> ItemInspectionConceptChecks7
[] block7 = 2 -> ItemInspectionProcedureChecks7
[] block7 = 3 -> InspectionConceptChecks7
[] block7 = 4 -> CandidateChecks7
[] block7 = 5 -> InspectionProcedureChecks7Exact module download · Source bundle and reproduction instructions
Resolved project definitions: CandidateChecks7, InspectionConceptChecks7, InspectionProcedureChecks7, ItemInspectionConceptChecks7, ItemInspectionProcedureChecks7, block7
CandidateCardFixture7 · operator
reference-profile · input revision 2 · CC0 1.0
CandidateCardFixture7(zone,targetSite,area,host) ==
[form |-> "Card",side |-> "SideA",zone |-> zone,loc |-> <<zone,targetSite,area,host>>,
kind |-> "Attachment",deployed |-> zone = "Play",face |-> "Down",targetSite |-> targetSite,area |-> area,host |-> host]Exact module download · Source bundle and reproduction instructions
CandidateChecks7 · operator
reference-profile · input revision 2 · CC0 1.0
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 |-> {}]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: CandidateCardFixture7, CandidateInputsValid7, DecideRootAdmissions7, DeckOrderValid7, DeriveCandidateView7, InspectionCandidates7, InspectionCandidatesDirection7, InspectionPolicy7, InspectionRootCards7, ObserveRootEntries7, OneCardTraversalProhibition7, OpenCandidateCapacity7, OpenInspection7
Init7 · operator
reference-profile · input revision 2 · CC0 1.0
Init7 == block7 \in 1..5Exact module download · Source bundle and reproduction instructions
Resolved project definitions: block7
InspectionConceptChecks7 · operator
reference-profile · input revision 2 · CC0 1.0
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},{})Exact module download · Source bundle and reproduction instructions
Resolved project definitions: ArchiveCardFixture7, ItemInspectionCardFixture7, ActualItemInspectionesInInspection7, ActualItemInspectionesInTraversal7, AddAdditionalItemInspectiones7, ApplyInspectionAborts7, AttachChosenItemInspection7, ChooseCentralAInspectionCard7, ChooseSpecificInspectionCard7, DelayInspection7, FinishInspectionItemInspectionInstruction7, FreezeInspectionLimit7, InspectionCentralChoices7, InspectionEndEvent7, InspectionItemInspectionCaller7, InspectionObjectVisible7, InspectionPolicy7, InspectionPresentation7, InspectionSelectionReady7, ItemInspectionBeginEvent7, ItemInspectionHistoryCostCount7, ItemInspectionLookGrant7, MarkDelayedInspectiones7, OpenInspection7, OpenItemInspection7, PrepareDiscardSite7, RecordActualItemInspection7, RecordInspectionChoice7, TakeDelayedInspection7
InspectionProcedureChecks7 · operator
reference-profile · input revision 2 · CC0 1.0
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)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: CandidateCardFixture7, AdvanceInspectionSelection7, AdvanceInspectionStep7, BeginInspection7, BeginInspectionWithCandidates7, CloseEndedInspectionBeginReaction7, CompleteNormalInspection7, DrainEndedInspectionInstruction7, FreezeInspectionLimit7, InspectionBeginEvent7, InspectionEndEvent7, InspectionPolicy7, InspectionProcedureValid7, InspectionStepInfo7, InspectionSteps7, OpenCandidateCapacity7, OpenInspection7, ReturnInspectionToCaller7, SkipInspectionSelection7
ItemInspectionCardFixture7 · operator
reference-profile · input revision 2 · CC0 1.0
ItemInspectionCardFixture7(zone,kind) ==
[form |-> "Card",side |-> "SideA",zone |-> zone,loc |-> zone,kind |-> kind,deployed |-> zone = "Play"]Exact module download · Source bundle and reproduction instructions
ItemInspectionConceptChecks7 · operator
reference-profile · input revision 2 · CC0 1.0
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)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: ActiveItemInspectionFixture7, ItemInspectionCardFixture7, ApplyItemInspectionAborts7, BasicRetireOption7, DeclineMidItemInspection7, ExampleFamily034Reveal7, ExampleFamily034Trigger7, FinishItemInspectionClaimObjective7, FinishMidItemInspection7, InformationSiftingNext7, InformationSiftingPlan7, InspectionPolicy7, InspectionPolicyComplete7, ItemInspectionAbilityActive7, ItemInspectionAbilityMatches7, ItemInspectionClaimObjectiveDisposition7, ItemInspectionEndEvent7, ItemInspectionFrameValid7, ItemInspectionLookGrant7, ItemInspectionMidOptions7, ItemInspectionMovementOutcome7, ItemInspectionViewers7, MidItemInspectionChoiceAllowed7, MidOption7, MidOptionsValid7, ResolveItemInspectionClaimObjective7, SelectionWithinPolicy7, UseMidItemInspection7, SetupPlayers, EndTheTraversal6, EndTraversalEffectEvents6, EndTraversalOutcome6, NoTraversal6, NoTraversalRedirect6
ItemInspectionProcedureChecks7 · operator
reference-profile · input revision 2 · CC0 1.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)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: ItemInspectionCardFixture7, AdvanceItemInspectionStep7, BeginItemInspection7, CancelUnstartedItemInspection7, CloseEndedItemInspectionBeginReaction7, CompleteNormalItemInspection7, FinishItemInspectionClaimObjective7, ItemInspectionBeginEvent7, ItemInspectionEndEvent7, ItemInspectionLookGrant7, ItemInspectionProcedureValid7, ItemInspectionStepInfo7, ItemInspectionSteps7, OpenItemInspection7, ResolveItemInspectionClaimObjective7, ReturnItemInspectionToCaller7
Next7 · operator
reference-profile · input revision 2 · CC0 1.0
Next7 == UNCHANGED block7Exact module download · Source bundle and reproduction instructions
Resolved project definitions: block7
Spec7 · operator
reference-profile · input revision 2 · CC0 1.0
Spec7 == Init7 /\ [][Next7]_block7Exact module download · Source bundle and reproduction instructions
block7 · variable
reference-profile · input revision 2 · CC0 1.0
block7Exact module download · Source bundle and reproduction instructions