----------------------- MODULE ActivityPublication -----------------------
EXTENDS AbilityRegistry
                                                                             
                                                                        
KernelTargetRA(source,entry) == [source |-> source,entry |-> entry]
KernelEffectAllowedRA(catalog,basis,cause,target) ==
 IF ~BasisValidSA(catalog,basis) THEN FALSE
 ELSE IF ~RecordFieldsSA(target,{"source","entry"}) THEN FALSE
 ELSE IF ~RuleSourceValidSA(target.source) THEN FALSE
 ELSE IF ~IsNaturalValueSA(target.entry) THEN FALSE
 ELSE IF cause \in {"PermissionWithdraw","PermissionRestore"} THEN
   /\ target.entry=0 /\ target.source \in {catalog[key].source : key \in DOMAIN catalog}
   /\ IF cause="PermissionWithdraw" THEN target.source.rule \in basis.rulePermissions
      ELSE target.source.rule \notin basis.rulePermissions
 ELSE IF cause \in {"EntryWithdraw","EntryRestore"} THEN
   IF target.entry \notin DOMAIN catalog THEN FALSE
   ELSE /\ target.source=catalog[target.entry].source
        /\ IF cause="EntryWithdraw" THEN target.entry \in DOMAIN basis.registry
           ELSE target.entry \notin DOMAIN basis.registry
 ELSE FALSE
KernelBasisRA(catalog,basis,cause,target) ==
 [basis EXCEPT !.revision=@+1,
  !.rulePermissions=CASE cause="PermissionWithdraw" -> @ \ {target.source.rule}
                    [] cause="PermissionRestore" -> @ \cup {target.source.rule} [] OTHER -> @,
  !.registry=CASE cause="EntryWithdraw" -> [key \in DOMAIN @ \ {target.entry} |-> @[key]]
              [] cause="EntryRestore" -> [key \in DOMAIN @ \cup {target.entry} |->
                   IF key=target.entry THEN catalog[key] ELSE @[key]] [] OTHER -> @]
PublicationTemplateRA(snapshot,snapshotId) ==
 [snapshot EXCEPT !.id=snapshotId,!.point="NormalizedKernelPublication"]
PublicationEpochLedgerRA(before,candidate,beforeSnapshot,candidateSnapshot) ==
 LET lost==ConditionalActivityLosses96(beforeSnapshot,candidateSnapshot)
     keys==DOMAIN before.activationEpoch \cup DOMAIN beforeSnapshot.definitions \cup DOMAIN candidateSnapshot.definitions
 IN [candidate EXCEPT
   !.activationEpoch=[key \in keys |-> (IF key \in DOMAIN before.activationEpoch THEN before.activationEpoch[key] ELSE 0)+(IF key \in lost THEN 1 ELSE 0)],
   !.activationSerial=before.activationSerial+(IF lost={} THEN 0 ELSE 1)]
PublicationObserverSnapshotRA(before,candidate,beforeSnapshot,candidateSnapshot) ==
 LET observed==PublicationEpochLedgerRA(before,candidate,beforeSnapshot,candidateSnapshot)
 IN [candidateSnapshot EXCEPT !.activationEpoch=observed.activationEpoch,!.activationSerial=observed.activationSerial]
PublicationAfterLedgerRA(before,candidate,beforeSnapshot,candidateSnapshot) ==
 LET snapshot==PublicationObserverSnapshotRA(before,candidate,beforeSnapshot,candidateSnapshot)
     observed==PublicationEpochLedgerRA(before,candidate,beforeSnapshot,candidateSnapshot)
 IN ConditionalActivityLedger96(observed,snapshot.definitions,snapshot)
PublicationAfterStackRA(beforeStack,beforeLedger,afterLedger) ==
 [i \in 1..Len(beforeStack) |->
   LET lost=={id \in beforeStack[i].pending \cap DOMAIN beforeLedger.instances : afterLedger.instances[id].status # "Pending"}
   IN [beforeStack[i] EXCEPT !.pending=@ \ lost,!.lostPending=@ \cup lost]]
                                                                                
                                                                              
                                                                               
                                                                               
                                                                              
                                                                               
                                                                               
AdmitKernelPublicationRA(catalog,beforeBasis,afterBasis,cause,target,snapshotId,
 beforeLedger,candidateLedger,afterLedger,beforeStack,afterStack,
 beforeSnapshot,candidateSnapshot,observerSnapshot,currentSnapshot) ==
 /\ snapshotId \in Nat \ {0} /\ snapshotId # beforeSnapshot.id
 /\ KernelEffectAllowedRA(catalog,beforeBasis,cause,target)
 /\ afterBasis=KernelBasisRA(catalog,beforeBasis,cause,target) /\ BasisValidSA(catalog,afterBasis)
 /\ LedgerDomainSA(beforeLedger) /\ candidateLedger=beforeLedger
 /\ beforeSnapshot=ConditionalSnapshotFromRegistrySA(catalog,beforeBasis,beforeLedger,beforeSnapshot)
 /\ candidateSnapshot=ConditionalSnapshotFromRegistrySA(catalog,afterBasis,candidateLedger,
       PublicationTemplateRA(beforeSnapshot,snapshotId))
 /\ observerSnapshot=PublicationObserverSnapshotRA(beforeLedger,candidateLedger,beforeSnapshot,candidateSnapshot)
 /\ ObserveConditionalActivity96(beforeLedger,candidateLedger,afterLedger,beforeStack,afterStack,beforeSnapshot,observerSnapshot)
 /\ currentSnapshot=ConditionalSnapshotFromRegistrySA(catalog,afterBasis,afterLedger,observerSnapshot)
=============================================================================