----------------------- MODULE ActivityChecksMC -----------------------
EXTENDS RegistryChecksMC, ActivityPublication
                                                                            
                                                                   
CONSTANT ActivityProfiles
AProfiles == {"permission","conditional-entry","paid-entry","alternating","decoy-permission","overlap"}
AInitialBasis == BasisSA(0,SCatalogSA,EmptyT11,{"SharedRegistryControl","Specimen0070RegistryControl"})
ASeedLedger == NewConditionalLedger96([PInitialSnapshot EXCEPT !.definitions=ConditionalDefinitionsSA(SCatalogSA),
 !.present=ConditionalPresentSA(SCatalogSA),!.objects=EmptyT11,
 !.activationEpoch=[key \in DOMAIN ConditionalDefinitionsSA(SCatalogSA) |-> 0]])
AInitialSnapshot == ConditionalSnapshotFromRegistrySA(SCatalogSA,AInitialBasis,ASeedLedger,PInitialSnapshot)
AInitialLedger == NewConditionalLedger96(AInitialSnapshot)
AHistoricalCapture == [basis |-> MinimalCaptureSA(AInitialBasis),snapshot |-> AInitialSnapshot]
AOperation(cause,source,entry) == [cause |-> cause,target |-> KernelTargetRA(source,entry)]
APermissionOps(source) == <<AOperation("PermissionWithdraw",source,0),AOperation("PermissionRestore",source,0)>>
AEntryOps(entry) == <<AOperation("EntryWithdraw",SCatalogSA[entry].source,entry),AOperation("EntryRestore",SCatalogSA[entry].source,entry)>>
AOperations(NeutralValue00013) == CASE NeutralValue00013="permission" -> APermissionOps(SRuleSA)
 [] NeutralValue00013="conditional-entry" -> AEntryOps(2) [] NeutralValue00013="paid-entry" -> AEntryOps(3)
 [] NeutralValue00013="alternating" -> APermissionOps(SRuleSA) \o AEntryOps(2) \o AEntryOps(3)
 [] NeutralValue00013="overlap" -> <<AOperation("EntryWithdraw",SRuleSA,2),AOperation("PermissionWithdraw",SRuleSA,0),
                          AOperation("EntryRestore",SRuleSA,2),AOperation("PermissionRestore",SRuleSA,0)>>
 [] OTHER -> APermissionOps(SCatalogSA[4].source)
AInitial(NeutralValue00013) == [catalog |-> SCatalogSA,basis |-> AInitialBasis,ledger |-> AInitialLedger,
 stack |-> <<SWindowSA>>,history |-> AHistoricalCapture,current |-> AInitialSnapshot,
 snapshotIds |-> {AInitialSnapshot.id},currentBasis |-> MinimalCaptureSA(AInitialBasis),publication |-> EmptyT11,NeutralValue00013 |-> NeutralValue00013,stage |-> 0]
AInit == registryCaseSA=0 /\ guideCaseT11=0 /\ \E NeutralValue00013 \in ActivityProfiles : qT11=AInitial(NeutralValue00013)
APublish ==
 LET q==qT11 op==AOperations(q.NeutralValue00013)[q.stage+1]
     snapshotId==1001+q.stage
     basis==KernelBasisRA(q.catalog,q.basis,op.cause,op.target)
     before==ConditionalSnapshotFromRegistrySA(q.catalog,q.basis,q.ledger,q.current)
     candidateLedger==q.ledger
     candidate==ConditionalSnapshotFromRegistrySA(q.catalog,basis,candidateLedger,PublicationTemplateRA(before,snapshotId))
     observer==PublicationObserverSnapshotRA(q.ledger,candidateLedger,before,candidate)
     ledger==PublicationAfterLedgerRA(q.ledger,candidateLedger,before,candidate)
     stack==PublicationAfterStackRA(q.stack,q.ledger,ledger)
     current==ConditionalSnapshotFromRegistrySA(q.catalog,basis,ledger,observer)
     receipt==[snapshotId |-> snapshotId,cause |-> op.cause,target |-> op.target,beforeBasis |-> MinimalCaptureSA(q.basis),afterBasis |-> MinimalCaptureSA(basis),
       beforeSnapshotIds |-> q.snapshotIds,afterSnapshotIds |-> q.snapshotIds \cup {snapshotId},
       beforeLedger |-> q.ledger,candidateLedger |-> candidateLedger,afterLedger |-> ledger,beforeStack |-> q.stack,afterStack |-> stack,
       beforeSnapshot |-> before,candidateSnapshot |-> candidate,observerSnapshot |-> observer,currentSnapshot |-> current]
 IN /\ q.stage < Len(AOperations(q.NeutralValue00013))
    /\ ConditionalBindingSA(q.catalog,q.basis,q.ledger,q.current,q.current,q.currentBasis)
    /\ snapshotId \notin q.snapshotIds
    /\ AdmitKernelPublicationRA(q.catalog,q.basis,basis,op.cause,op.target,snapshotId,q.ledger,candidateLedger,ledger,q.stack,stack,before,candidate,observer,current)
    /\ qT11'=[q EXCEPT !.basis=basis,!.ledger=ledger,!.stack=stack,!.current=current,
       !.snapshotIds=@ \cup {snapshotId},!.currentBasis=MinimalCaptureSA(basis),!.publication=receipt,!.stage=@+1]
    /\ UNCHANGED <<registryCaseSA,guideCaseT11>>
ANext == IF qT11.stage < Len(AOperations(qT11.NeutralValue00013)) THEN APublish ELSE UNCHANGED <<qT11,registryCaseSA,guideCaseT11>>
ASpec == AInit /\ [][ANext]_<<qT11,registryCaseSA,guideCaseT11>> /\ WF_<<qT11,registryCaseSA,guideCaseT11>>(ANext)
AEventuallyPublished == <> (qT11.stage=Len(AOperations(qT11.NeutralValue00013)))
APublicationSafety ==
 LET q==qT11 IN
 /\ q.NeutralValue00013 \in AProfiles /\ q.catalog=SCatalogSA /\ BasisValidSA(q.catalog,q.basis)
 /\ q.basis.revision=q.stage /\ q.basis.objects=AInitialBasis.objects /\ q.ledger.instances=EmptyT11
 /\ q.snapshotIds={AInitialSnapshot.id} \cup {1000+i : i \in 1..q.stage}
 /\ ConditionalBindingSA(q.catalog,q.basis,q.ledger,q.current,q.current,q.currentBasis)
 /\ q.ledger.lastSnapshot=AInitialSnapshot
 /\ IF q.stage=0 THEN TRUE ELSE
   LET p==q.publication IN
   /\ p.snapshotId \notin p.beforeSnapshotIds /\ p.afterSnapshotIds=p.beforeSnapshotIds \cup {p.snapshotId}
   /\ p.afterSnapshotIds=q.snapshotIds
   /\ p.afterBasis=MinimalCaptureSA(q.basis) /\ p.afterLedger=q.ledger /\ p.afterStack=q.stack /\ p.currentSnapshot=q.current
   /\ AdmitKernelPublicationRA(q.catalog,p.beforeBasis,p.afterBasis,p.cause,p.target,p.snapshotId,
      p.beforeLedger,p.candidateLedger,p.afterLedger,p.beforeStack,p.afterStack,
      p.beforeSnapshot,p.candidateSnapshot,p.observerSnapshot,p.currentSnapshot)
AHistoricalSafety == qT11.history=AHistoricalCapture
AEpochSafety ==
 LET q==qT11 losses==IF q.NeutralValue00013="alternating" THEN (IF q.stage>=3 THEN 2 ELSE IF q.stage>=1 THEN 1 ELSE 0)
                    ELSE IF q.NeutralValue00013 \in {"permission","conditional-entry","overlap"} /\ q.stage>=1 THEN 1 ELSE 0
 IN q.ledger.activationEpoch[ConditionalKey96(SConditionalSA)]=losses /\ q.ledger.activationSerial=losses
ANativeActivitySafety ==
 LET q==qT11 paid==PaidContextFromRegistrySA(q.catalog,q.basis,q.ledger,EmptyT11,EmptyT11,STemplateSA,3)
     conditional==ConditionalActive96(SConditionalSA,q.current)
     paidActive==PaidEligibility95(SPaidSA,paid,SWindowSA)
     expectedConditional==IF q.NeutralValue00013="permission" THEN q.stage # 1 ELSE IF q.NeutralValue00013="conditional-entry" THEN q.stage # 1
        ELSE IF q.NeutralValue00013="alternating" THEN q.stage \notin {1,3} ELSE IF q.NeutralValue00013="overlap" THEN q.stage \notin {1,2,3} ELSE TRUE
     expectedPaid==IF q.NeutralValue00013="permission" THEN q.stage # 1 ELSE IF q.NeutralValue00013="paid-entry" THEN q.stage # 1
        ELSE IF q.NeutralValue00013="alternating" THEN q.stage \notin {1,5} ELSE IF q.NeutralValue00013="overlap" THEN q.stage \notin {2,3} ELSE TRUE
 IN /\ conditional=expectedConditional /\ paidActive=expectedPaid
    /\ 1 \in DOMAIN q.basis.registry
    /\ (2 \in DOMAIN q.basis.registry)=(IF q.NeutralValue00013="conditional-entry" THEN q.stage # 1 ELSE IF q.NeutralValue00013="alternating" THEN q.stage # 3 ELSE IF q.NeutralValue00013="overlap" THEN q.stage \notin {1,2} ELSE TRUE)
    /\ (3 \in DOMAIN q.basis.registry)=(IF q.NeutralValue00013="paid-entry" THEN q.stage # 1 ELSE IF q.NeutralValue00013="alternating" THEN q.stage # 5 ELSE TRUE)
                                                                            
                                                                            
                                                                         
ANativeCatalogSafety ==
 LET q==qT11 IN \A key \in DOMAIN q.catalog :
   LET row==q.catalog[key]
       expected==key \in DOMAIN q.basis.registry /\ row.source.rule \in q.basis.rulePermissions
       actual==IF row.kind="Conditional" THEN ConditionalActive96(row.definition,q.current)
               ELSE FlagActivity93(row.definition.syntax,PaidPresentSA(q.basis.registry),
                 AbilityActive9(row.definition.activity,q.basis.objects,PaidPresentSA(q.basis.registry),
                   SourceDefaultActivitySA(q.basis,row.source),CommonActivitySA(q.basis,q.ledger)),{},ZeroCountsT11)
   IN actual=expected
ARejectionSafety ==
 LET q==qT11 next==KernelBasisRA(q.catalog,AInitialBasis,"EntryWithdraw",KernelTargetRA(SRuleSA,2))
     replacement==[KernelBasisRA(q.catalog,next,"EntryRestore",KernelTargetRA(SRuleSA,2)) EXCEPT !.registry[2].definition.primaryCondition=2]
 IN /\ ~RegistryValidSA(q.catalog,replacement.registry)
    /\ ~KernelEffectAllowedRA(q.catalog,AInitialBasis,"PermissionRestore",KernelTargetRA(SRuleSA,0))
    /\ ~KernelEffectAllowedRA(q.catalog,AInitialBasis,"EntryRestore",KernelTargetRA(SRuleSA,2))
    /\ ~KernelEffectAllowedRA(q.catalog,AInitialBasis,"EntryWithdraw",KernelTargetRA(SCatalogSA[4].source,2))
    /\ ~KernelEffectAllowedRA(q.catalog,AInitialBasis,"EntryWithdraw",KernelTargetRA(SRuleSA,99))
    /\ ~KernelEffectAllowedRA(q.catalog,AInitialBasis,"UnknownEffect",KernelTargetRA(SRuleSA,0))
=============================================================================