------------------------- MODULE RegistryChecksMC -------------------------
EXTENDS AbilityRegistry, CommittedCompositionMC
                                                                               
                                                                                      
VARIABLE registryCaseSA
SCasesSA == 1..11
SRuleSA == RuleAbilitySource9("SharedRegistryControl")
SPaidSA == [ProtocolP!RootDefinition9p EXCEPT !.syntax.id="RepeatableControl",!.syntax.source=SRuleSA,
 !.activity.id="RepeatableControl",!.activity.source=SRuleSA,!.activity.provider="Rule"]
SMidSA == [ItemInspectionPaidDefinitionT11([NeutralValue00013 |-> "FacilityObserve0"]) EXCEPT !.syntax.source=SRuleSA,!.activity.source=SRuleSA]
SConditionalSA == [PChildDefinition EXCEPT !.syntax.source=SRuleSA,!.activity.source=SRuleSA]
SSpecimen0070SA == [SPaidSA EXCEPT !.syntax.id="Specimen0070Control",!.activity.id="Specimen0070Control",
 !.syntax.source=RuleAbilitySource9("Specimen0070RegistryControl"),!.activity.source=RuleAbilitySource9("Specimen0070RegistryControl")]
SRowSA(kind,d) == [kind |-> kind,nativeId |-> d.syntax.id,source |-> d.syntax.source,definition |-> d]
SCatalogSA == [key \in 1..4 |-> CASE key=1 -> SRowSA("Paid",SMidSA) [] key=2 -> SRowSA("Conditional",SConditionalSA)
 [] key=3 -> SRowSA("Paid",SPaidSA) [] OTHER -> SRowSA("Paid",SSpecimen0070SA)]
SWithoutSA(registry,key) == [id \in DOMAIN registry \ {key} |-> registry[id]]
SBasisSA == BasisSA(4,SCatalogSA,EmptyT11,{"SharedRegistryControl","Specimen0070RegistryControl"})
SLedgerSA == NewConditionalLedger96([PInitialSnapshot EXCEPT !.definitions=ConditionalDefinitionsSA(SCatalogSA),
 !.present=ConditionalPresentSA(SCatalogSA),!.objects=EmptyT11,
 !.activationEpoch=[key \in DOMAIN ConditionalDefinitionsSA(SCatalogSA) |-> 0]])
STemplateSA == [ProtocolP!RootContext9p EXCEPT !.ownRestrictions.ability=SPaidSA.syntax.id,!.ownRestrictions.source=SRuleSA,
 !.otherRestrictions.ability=SPaidSA.syntax.id,!.otherRestrictions.source=SRuleSA]
SContextSA(basis) == PaidContextFromRegistrySA(SCatalogSA,basis,SLedgerSA,EmptyT11,EmptyT11,STemplateSA,3)
SSnapshotSA(basis) == ConditionalSnapshotFromRegistrySA(SCatalogSA,basis,SLedgerSA,SLedgerSA.lastSnapshot)
SWindowSA == [ProtocolP!Window9p(30,"Paid",EmptyT11,0) EXCEPT !.stage="Ready",!.checkpoint=1]
SProcedureSA(key,id) == [id |-> id,definition |-> SCatalogSA[key].definition,
 ability |-> [source |-> SCatalogSA[key].source],turnId |-> 1]
SProceduresSA == [id \in 11..14 |-> SProcedureSA(CASE id=11 -> 1 [] id=12 -> 2 [] id=13 -> 4 [] OTHER -> 3,id)]
SIndexSA == [id \in 1..4 |-> CASE id=1 -> 1 [] id=2 -> 2 [] id=3 -> 4 [] OTHER -> 3]
SUsesSA == [id \in 1..4 |-> [tag |-> "AbilityUsed",useId |-> id,abilityInstance |-> 10+id,
 source |-> SCatalogSA[SIndexSA[id]].source,player |-> "SideB"]]
STurnUsesSA == [id \in 1..4 |-> [turnId |-> 1,ability |-> SCatalogSA[SIndexSA[id]].nativeId,
 source |-> SCatalogSA[SIndexSA[id]].source,useId |-> id]]
SFlaggedConditionalSA == [SConditionalSA.syntax EXCEPT !.units= <<TextUnit93(99,"AbilityFlag","OncePerTurn",FALSE,0)>> \o @]
SProjectionChecksSA ==
 /\ RegistryValidSA(SCatalogSA,SCatalogSA)
 /\ DOMAIN ConditionalDefinitionsSA(SCatalogSA)={ConditionalKey96(SConditionalSA)}
 /\ ConditionalPresentSA(SCatalogSA)={200}
 /\ PaidPresentSA(SCatalogSA)={"SyntheticObserve","RepeatableControl","Specimen0070Control"}
 /\ MidOptionsValid7({MidOption7(SMidSA.syntax.id,FALSE,TRUE,TRUE)})
 /\ ConditionalDefinitionValid96(SConditionalSA)
 /\ PaidEligibility95(SPaidSA,SContextSA(SBasisSA),SWindowSA)
 /\ ConditionalActive96(SConditionalSA,SSnapshotSA(SBasisSA))
SAvailabilityChecksSA ==
 LET inactive==[SBasisSA EXCEPT !.rulePermissions={"Specimen0070RegistryControl"}]
     absentPaid==[SBasisSA EXCEPT !.registry=SWithoutSA(@,3)]
     absentConditional==[SBasisSA EXCEPT !.registry=SWithoutSA(@,2)]
 IN /\ BasisValidSA(SCatalogSA,inactive) /\ BasisValidSA(SCatalogSA,absentPaid) /\ BasisValidSA(SCatalogSA,absentConditional)
    /\ 3 \in DOMAIN inactive.registry /\ 2 \in DOMAIN inactive.registry
    /\ ~PaidEligibility95(SPaidSA,SContextSA(inactive),SWindowSA)
    /\ ~ConditionalActive96(SConditionalSA,SSnapshotSA(inactive))
    /\ ~PaidEligibility95(SPaidSA,SContextSA(absentPaid),SWindowSA)
    /\ ~ConditionalActive96(SConditionalSA,SSnapshotSA(absentConditional))
    /\ RegistryValidSA(SCatalogSA,SWithoutSA(SCatalogSA,2))
    /\ RegistryValidSA(SCatalogSA,PJoin(SWithoutSA(SCatalogSA,2),[key \in {2} |-> SCatalogSA[2]]))
SInvalidCatalogChecksSA ==
 LET duplicate==PJoin(SCatalogSA,[key \in {5} |-> SCatalogSA[2]])
     wrongSource==[SCatalogSA EXCEPT ![2].source=RuleAbilitySource9("Other")]
     wrongKind==[SCatalogSA EXCEPT ![2].kind="Paid"]
     wrongNative==[SCatalogSA EXCEPT ![1].nativeId="ForeignPaid"]
     replacement==[SCatalogSA EXCEPT ![2].definition.primaryCondition=2]
 IN /\ ~CatalogValidSA(duplicate) /\ ~RegistryValidSA(duplicate,SWithoutSA(duplicate,5))
    /\ ~CatalogValidSA([key \in {"1"} |-> SCatalogSA[1]])
    /\ ~RegistryValidSA(SCatalogSA,[key \in {"1"} |-> SCatalogSA[1]])
    /\ ~CatalogValidSA(wrongSource) /\ ~CatalogValidSA(wrongKind) /\ ~CatalogValidSA(wrongNative)
    /\ ~RegistryValidSA(SCatalogSA,replacement)
    /\ ~RegistryValidSA(SCatalogSA,PJoin(SCatalogSA,[key \in {5} |-> SCatalogSA[2]]))
SMalformedChecksSA ==
 LET missingRow==[k \in RowHeaderSA \ {"source"} |-> SCatalogSA[2][k]]
     missingDefinition==[k \in ConditionalHeaderSA \ {"trigger"} |-> SConditionalSA[k]]
     badSyntax==[SConditionalSA EXCEPT !.syntax=[id |-> 200]]
     badUnits==[SConditionalSA EXCEPT !.syntax.units= <<[id |-> 1]>>]
     badConditionalId==[SCatalogSA[2] EXCEPT !.nativeId="NotConditionalNat"]
     badPaidId==[SCatalogSA[1] EXCEPT !.nativeId=9]
 IN /\ ~RowValidSA(missingRow)
    /\ ~RowValidSA(9)
    /\ ~RowValidSA(<<1,2,3,4>>)
    /\ ~RuleSourceValidSA(<<"Rule",0,"SharedRegistryControl">>)
    /\ ~RowValidSA([SCatalogSA[2] EXCEPT !.definition.syntax= <<1,2,3,4,5,6,7,8,9,10>>])
    /\ ~RowValidSA([SCatalogSA[2] EXCEPT !.definition=FALSE])
    /\ ~RowValidSA([SCatalogSA[2] EXCEPT !.definition.syntax.id="200"])
    /\ ~RowValidSA([SCatalogSA[2] EXCEPT !.definition.activity.id="200"])
    /\ ~RowValidSA([SCatalogSA[2] EXCEPT !.definition.syntax.source.object="0"])
    /\ ~RowValidSA([SCatalogSA[2] EXCEPT !.definition.activity.source.object="0"])
    /\ ~RowValidSA([SCatalogSA[1] EXCEPT !.definition.syntax.id=200])
    /\ ~RowValidSA([SCatalogSA[1] EXCEPT !.definition.activity.id=200])
    /\ ~RowValidSA([SCatalogSA[2] EXCEPT !.definition=missingDefinition])
    /\ ~RowValidSA([SCatalogSA[2] EXCEPT !.definition=badSyntax])
    /\ ~RowValidSA([SCatalogSA[2] EXCEPT !.definition=badUnits])
    /\ ~RowValidSA(badConditionalId) /\ ~RowValidSA(badPaidId)
    /\ ~RowValidSA([SCatalogSA[2] EXCEPT !.source=[kind |-> "Rule"]])
SPaidBindingChecksSA ==
 LET context==SContextSA(SBasisSA) capture==MinimalCaptureSA(SBasisSA) IN
 /\ PaidBindingSA(SCatalogSA,SBasisSA,SLedgerSA,EmptyT11,EmptyT11,STemplateSA,3,context,capture)
 /\ ~PaidBindingSA(SCatalogSA,SBasisSA,SLedgerSA,EmptyT11,EmptyT11,STemplateSA,3,[context EXCEPT !.present={}],capture)
 /\ ~PaidBindingSA(SCatalogSA,SBasisSA,SLedgerSA,EmptyT11,EmptyT11,STemplateSA,3,[context EXCEPT !.present=@ \cup {"Forged"}],capture)
 /\ ~PaidBindingSA(SCatalogSA,SBasisSA,SLedgerSA,EmptyT11,EmptyT11,STemplateSA,3,[context EXCEPT !.defaultActive=TRUE],capture)
 /\ ~PaidBindingSA(SCatalogSA,SBasisSA,SLedgerSA,EmptyT11,EmptyT11,STemplateSA,3,[context EXCEPT !.activity.activeRules={}],capture)
 /\ ~PaidBindingSA(SCatalogSA,SBasisSA,SLedgerSA,EmptyT11,EmptyT11,STemplateSA,3,[context EXCEPT !.objects=PObjects],capture)
 /\ ~PaidBindingSA(SCatalogSA,SBasisSA,SLedgerSA,EmptyT11,EmptyT11,STemplateSA,3,context,[capture EXCEPT !.revision=3])
SConditionalBindingChecksSA ==
 LET snapshot==SSnapshotSA(SBasisSA) capture==MinimalCaptureSA(SBasisSA) IN
 /\ ConditionalBindingSA(SCatalogSA,SBasisSA,SLedgerSA,SLedgerSA.lastSnapshot,snapshot,capture)
 /\ ~ConditionalBindingSA(SCatalogSA,SBasisSA,SLedgerSA,SLedgerSA.lastSnapshot,[snapshot EXCEPT !.present={}],capture)
 /\ ~ConditionalBindingSA(SCatalogSA,SBasisSA,SLedgerSA,SLedgerSA.lastSnapshot,[snapshot EXCEPT !.present=@ \cup {201}],capture)
 /\ ~ConditionalBindingSA(SCatalogSA,SBasisSA,SLedgerSA,SLedgerSA.lastSnapshot,[snapshot EXCEPT !.definitions=EmptyT11],capture)
 /\ ~ConditionalBindingSA(SCatalogSA,SBasisSA,SLedgerSA,SLedgerSA.lastSnapshot,[snapshot EXCEPT !.ordinaryActivity[ConditionalKey96(SConditionalSA)]=TRUE],capture)
 /\ ~ConditionalBindingSA(SCatalogSA,SBasisSA,SLedgerSA,SLedgerSA.lastSnapshot,[snapshot EXCEPT !.activity.activeRules={}],capture)
 /\ ~ConditionalBindingSA(SCatalogSA,SBasisSA,SLedgerSA,SLedgerSA.lastSnapshot,[snapshot EXCEPT !.activationSerial=1],capture)
 /\ ~ConditionalBindingSA(SCatalogSA,SBasisSA,SLedgerSA,SLedgerSA.lastSnapshot,snapshot,[capture EXCEPT !.revision=3])
SProvenanceChecksSA ==
 /\ UseProvenanceValidSA(SCatalogSA,SUsesSA,STurnUsesSA,SIndexSA,SProceduresSA)
 /\ ~UseProvenanceValidSA(SCatalogSA,SUsesSA,STurnUsesSA,SWithoutSA(SIndexSA,2),SProceduresSA)
 /\ ~UseProvenanceValidSA(SCatalogSA,SUsesSA,STurnUsesSA,[SIndexSA EXCEPT ![1]="1"],SProceduresSA)
 /\ ~UseProvenanceValidSA(SCatalogSA,SUsesSA,STurnUsesSA,[SIndexSA EXCEPT ![1]=4],SProceduresSA)
 /\ ~UseProvenanceValidSA(SCatalogSA,SUsesSA,STurnUsesSA,[SIndexSA EXCEPT ![1]=2],SProceduresSA)
 /\ ~UseProvenanceValidSA(SCatalogSA,SUsesSA,STurnUsesSA,[SIndexSA EXCEPT ![1]=3],SProceduresSA)
 /\ ~UseProvenanceValidSA(SCatalogSA,SUsesSA,[STurnUsesSA EXCEPT ![1].ability="RepeatableControl"],SIndexSA,SProceduresSA)
 /\ ~UseProvenanceValidSA(SCatalogSA,SUsesSA,[STurnUsesSA EXCEPT ![1].ability=200],SIndexSA,SProceduresSA)
 /\ ~UseProvenanceValidSA(SCatalogSA,SUsesSA,[STurnUsesSA EXCEPT ![2].turnId=2],SIndexSA,SProceduresSA)
 /\ ~UseProvenanceValidSA(SCatalogSA,[SUsesSA EXCEPT ![2].source=RuleAbilitySource9("Foreign")],STurnUsesSA,SIndexSA,SProceduresSA)
 /\ ~UseProvenanceValidSA(SCatalogSA,SUsesSA,STurnUsesSA,SIndexSA,[SProceduresSA EXCEPT ![12].definition.primaryCondition=7])
SQueryChecksSA ==
 LET paid==FamilyTurnUsesSA(SCatalogSA,SIndexSA,STurnUsesSA,"Paid",SRuleSA)
     conditional==FamilyTurnUsesSA(SCatalogSA,SIndexSA,STurnUsesSA,"Conditional",SRuleSA)
     noConditional==SWithoutSA(conditional,2)
     withdrawn==SWithoutSA(SCatalogSA,2)
 IN /\ DOMAIN paid={1,4} /\ DOMAIN conditional={2}
    /\ paid[1]=STurnUsesSA[1] /\ paid[4]=STurnUsesSA[4] /\ conditional[2]=STurnUsesSA[2]
    /\ ~OncePerTurnAllowed93(SMidSA.syntax,1,paid)
    /\ ~OncePerTurnAllowed93(SFlaggedConditionalSA,1,conditional)
    /\ OncePerTurnAllowed93(SFlaggedConditionalSA,1,noConditional)
    /\ OncePerTurnAllowed93(SFlaggedConditionalSA,2,conditional)
    /\ RegistryValidSA(SCatalogSA,withdrawn)
    /\ UseProvenanceValidSA(SCatalogSA,SUsesSA,STurnUsesSA,SIndexSA,SProceduresSA)
    /\ ~OncePerTurnAllowed93(SFlaggedConditionalSA,1,FamilyTurnUsesSA(SCatalogSA,SIndexSA,STurnUsesSA,"Conditional",SRuleSA))
SHistoryChecksSA ==
 LET captured==MinimalCaptureSA(SBasisSA)
     inactive==[SBasisSA EXCEPT !.revision=5,!.rulePermissions={}]
     historical==SSnapshotSA(SBasisSA)
 IN /\ captured.revision=4 /\ captured.registry=SCatalogSA
    /\ historical.activity.activeRules=SBasisSA.rulePermissions
    /\ ~ConditionalBindingSA(SCatalogSA,inactive,SLedgerSA,SLedgerSA.lastSnapshot,historical,captured)
    /\ ConditionalActive96(SConditionalSA,historical)
    /\ ~ConditionalActive96(SConditionalSA,SSnapshotSA(inactive))
SLedgerBindingChecksSA ==
 LET snapshot==SSnapshotSA(SBasisSA) capture==MinimalCaptureSA(SBasisSA)
     holds==[snapshot EXCEPT !.holds=[key \in {ConditionalKey96(SConditionalSA)} |-> [ability |-> 200,object |-> 1,instances |-> {}]]]
     instances==[snapshot EXCEPT !.activity.instances=[id \in {99} |-> [ability |-> 200,sourceObject |-> 0,status |-> "Pending"]]]
 IN /\ ~ConditionalBindingSA(SCatalogSA,SBasisSA,SLedgerSA,SLedgerSA.lastSnapshot,holds,capture)
    /\ ~ConditionalBindingSA(SCatalogSA,SBasisSA,SLedgerSA,SLedgerSA.lastSnapshot,instances,capture)
SAdmissionChecksSA ==
 LET view==PaidContextFromRegistrySA(SCatalogSA,SBasisSA,SLedgerSA,SIndexSA,STurnUsesSA,STemplateSA,3)
     capture==MinimalCaptureSA(SBasisSA)
 IN /\ AdmitPaidContextSA(SCatalogSA,SBasisSA,SLedgerSA,SUsesSA,STurnUsesSA,SIndexSA,SProceduresSA,STemplateSA,3,view,capture)
    /\ ~AdmitPaidContextSA(SCatalogSA,SBasisSA,SLedgerSA,SUsesSA,STurnUsesSA,SWithoutSA(SIndexSA,2),SProceduresSA,STemplateSA,3,view,capture)
    /\ ~AdmitConditionalSnapshotSA(SCatalogSA,SBasisSA,SLedgerSA,SUsesSA,STurnUsesSA,SWithoutSA(SIndexSA,2),SProceduresSA,SLedgerSA.lastSnapshot,SSnapshotSA(SBasisSA),capture)
    /\ ~ConditionalBindingSA(SCatalogSA,SBasisSA,[SLedgerSA EXCEPT !.effects=[id \in {1} |-> TRUE]],SLedgerSA.lastSnapshot,SSnapshotSA(SBasisSA),capture)
SAssertionsSA == CASE registryCaseSA=1 -> SProjectionChecksSA [] registryCaseSA=2 -> SAvailabilityChecksSA
 [] registryCaseSA=3 -> SInvalidCatalogChecksSA [] registryCaseSA=4 -> SMalformedChecksSA
 [] registryCaseSA=5 -> SPaidBindingChecksSA [] registryCaseSA=6 -> SConditionalBindingChecksSA
 [] registryCaseSA=7 -> SProvenanceChecksSA [] registryCaseSA=8 -> SQueryChecksSA
 [] registryCaseSA=9 -> SHistoryChecksSA [] registryCaseSA=10 -> SLedgerBindingChecksSA [] OTHER -> SAdmissionChecksSA
SInitSA == registryCaseSA \in SCasesSA /\ guideCaseT11=0 /\ qT11=EmptyT11
SNextSA == UNCHANGED <<registryCaseSA,guideCaseT11,qT11>>
SSpecSA == SInitSA /\ [][SNextSA]_<<registryCaseSA,guideCaseT11,qT11>>
=============================================================================