-------------------------- MODULE AbilityRegistry --------------------------
EXTENDS AdditionalContracts, TLC
                                                                         
                                                                               
                                                                                
                                                                                 
EmptySA == [id \in {} |-> id]
                                                                          
                                                                             
                                                                                  
IsFunctionValueSA(value) == SubSeq(ToString(value),1,1) \in {"[","(","<"}
IsStringValueSA(value) == SubSeq(ToString(value),1,1)="\""
IsNaturalValueSA(value) ==
 \A i \in 1..Len(ToString(value)) : SubSeq(ToString(value),i,i) \in {"0","1","2","3","4","5","6","7","8","9"}
RecordFieldsSA(value,fields) ==
 IF ~IsFunctionValueSA(value) THEN FALSE
 ELSE IF ~(\A key \in DOMAIN value : IsStringValueSA(key)) THEN FALSE
 ELSE DOMAIN value=fields
SyntaxHeaderSA == {"id","kind","side","controller","cardKind","source","units","arrowAfterFlags","barrierInstructionPrefix","paidPrefix"}
ActivityHeaderSA == {"id","kind","source","provider","sourceItemInspection","statedZones","rulesOnlyZones","ownPermissionModifier", "ownCostModifier","ownProgressRequirement","ownClaimObjectiveAdditionalCost","allowsProgress"}
SourceShapeSA == [kind : {"Rule","Object"},object : Nat,rule : STRING]
UnitShapeSA == [id : Nat,category : STRING,subtype : STRING,primary : BOOLEAN,value : Int]
SyntaxShapeSA(ids) == [id : ids,kind : STRING,side : SetupPlayers,controller : SetupPlayers,cardKind : STRING,
 source : SourceShapeSA,units : Seq(UnitShapeSA),arrowAfterFlags : BOOLEAN,barrierInstructionPrefix : BOOLEAN,
 paidPrefix : [present : BOOLEAN,bold : BOOLEAN,colon : BOOLEAN]]
ActivityShapeSA(ids) == [id : ids,kind : STRING,source : SourceShapeSA,provider : STRING,sourceItemInspection : BOOLEAN,
 statedZones : SUBSET STRING,rulesOnlyZones : SUBSET STRING,ownPermissionModifier : BOOLEAN,ownCostModifier : BOOLEAN,
 ownProgressRequirement : BOOLEAN,ownClaimObjectiveAdditionalCost : BOOLEAN,allowsProgress : BOOLEAN]
ReferenceShapeSA == [subtypes : SUBSET STRING,activated : BOOLEAN,otherIds : SUBSET Nat]
PaidShapeSA == [syntax : SyntaxShapeSA(STRING),activity : ActivityShapeSA(STRING),
 triggerCost : Seq([kind : STRING,amount : Nat]),instructions : Seq(Nat),instructionHasWould : BOOLEAN,ruleTiming : STRING,
 canSuppressBarrierInstructions : BOOLEAN,refersApproachedBarrier : BOOLEAN,refersEncounteredBarrier : BOOLEAN,
 approachRequirements : ReferenceShapeSA,encounterRequirements : ReferenceShapeSA,
 interfaceSubtype : [present : BOOLEAN,name : STRING],otherRestrictionIds : SUBSET Nat,refersHosted : BOOLEAN]
                                                                             
                                                                                
                                                                             
                                     
ConditionalHeaderSA == {"syntax","activity","primaryKind","primaryCondition","instructions","instructionHasWould",
 "trigger","triggerRequirements","effectChoices","optionalParts","partsByInstruction","delayedEffect","thisTraversal"}
RowHeaderSA == {"kind","nativeId","source","definition"}
RuleSourceValidSA(source) ==
 IF ~IsFunctionValueSA(source) THEN FALSE
 ELSE IF ~RecordFieldsSA(source,{"kind","object","rule"}) THEN FALSE
 ELSE IF ~IsNaturalValueSA(source.object) THEN FALSE
 ELSE IF ~IsStringValueSA(source.kind) \/ ~IsStringValueSA(source.rule) THEN FALSE
 ELSE IF source \notin SourceShapeSA THEN FALSE
 ELSE IF source.kind # "Rule" THEN FALSE ELSE source.object=0 /\ source.rule # "NoValue"
PaidHeaderSA == {"syntax","activity","triggerCost","instructions","instructionHasWould","ruleTiming","canSuppressBarrierInstructions",
 "refersApproachedBarrier","refersEncounteredBarrier","approachRequirements","encounterRequirements","interfaceSubtype","otherRestrictionIds","refersHosted"}
PaidDefinitionValidSA(d) ==
 IF ~IsFunctionValueSA(d) THEN FALSE
 ELSE IF ~RecordFieldsSA(d,PaidHeaderSA) THEN FALSE
 ELSE IF ~IsFunctionValueSA(d.syntax) \/ ~IsFunctionValueSA(d.activity) THEN FALSE
 ELSE IF ~RecordFieldsSA(d.syntax,SyntaxHeaderSA) \/ ~RecordFieldsSA(d.activity,ActivityHeaderSA) THEN FALSE
 ELSE IF ~IsStringValueSA(d.syntax.id) \/ ~IsStringValueSA(d.activity.id) THEN FALSE
 ELSE IF ~RuleSourceValidSA(d.syntax.source) \/ ~RuleSourceValidSA(d.activity.source) THEN FALSE
 ELSE IF d \notin PaidShapeSA THEN FALSE
 ELSE /\ d.syntax.kind="Paid" /\ d.activity.kind="Paid"
      /\ d.syntax.id \notin {"BasicRetire","Decline"}
      /\ d.activity.id=d.syntax.id /\ d.activity.source=d.syntax.source
      /\ RuleSourceValidSA(d.syntax.source) /\ d.activity.provider \in {"Printed","Rule"}
      /\ AbilityTextValid93(d.syntax) /\ Len(d.triggerCost)>0 /\ Len(d.instructions)>0
ConditionalDefinitionValidSA(d) ==
 IF ~IsFunctionValueSA(d) THEN FALSE
 ELSE IF ~RecordFieldsSA(d,ConditionalHeaderSA) THEN FALSE
 ELSE IF ~IsFunctionValueSA(d.syntax) \/ ~IsFunctionValueSA(d.activity) THEN FALSE
 ELSE IF ~RecordFieldsSA(d.syntax,SyntaxHeaderSA) \/ ~RecordFieldsSA(d.activity,ActivityHeaderSA) THEN FALSE
 ELSE IF ~IsNaturalValueSA(d.syntax.id) \/ ~IsNaturalValueSA(d.activity.id) THEN FALSE
 ELSE IF ~RuleSourceValidSA(d.syntax.source) \/ ~RuleSourceValidSA(d.activity.source) THEN FALSE
 ELSE IF d.syntax \notin SyntaxShapeSA(Nat) THEN FALSE
 ELSE IF d.activity \notin ActivityShapeSA(Nat) THEN FALSE
 ELSE IF d.instructions \notin Seq(Nat) THEN FALSE
 ELSE IF d.trigger \notin [kinds : SUBSET STRING,subject : STRING,actor : STRING,side : STRING] THEN FALSE
 ELSE IF d.partsByInstruction \notin [SubIds6(d.instructions) -> SUBSET Nat] THEN FALSE
 ELSE IF d.primaryKind \notin STRING \/ d.primaryCondition \notin Nat \/ d.instructionHasWould \notin BOOLEAN \/
         d.triggerRequirements \notin SUBSET Nat \/ d.effectChoices \notin SUBSET (SUBSET Nat) \/
         d.optionalParts \notin SUBSET Nat \/ d.delayedEffect \notin Nat \/ d.thisTraversal \notin BOOLEAN THEN FALSE
 ELSE /\ RuleSourceValidSA(d.syntax.source) /\ d.activity.provider \in {"Printed","Rule"}
      /\ ConditionalDefinitionValid96(d)
RowValidSA(row) ==
 IF ~IsFunctionValueSA(row) THEN FALSE
 ELSE IF ~RecordFieldsSA(row,RowHeaderSA) THEN FALSE
 ELSE IF ~IsStringValueSA(row.kind) THEN FALSE
 ELSE IF row.kind \notin {"Paid","Conditional"} THEN FALSE
 ELSE IF ~RuleSourceValidSA(row.source) THEN FALSE
 ELSE IF row.kind="Paid" THEN
   IF ~PaidDefinitionValidSA(row.definition) THEN FALSE
   ELSE ToString(row.nativeId)=ToString(row.definition.syntax.id) /\ row.source=row.definition.syntax.source
 ELSE IF ~ConditionalDefinitionValidSA(row.definition) THEN FALSE
 ELSE ToString(row.nativeId)=ToString(row.definition.syntax.id) /\ row.source=row.definition.syntax.source
CatalogValidSA(catalog) ==
 IF ~IsFunctionValueSA(catalog) THEN FALSE
 ELSE IF ~IsFiniteSet(DOMAIN catalog) THEN FALSE
 ELSE IF ~(\A key \in DOMAIN catalog : IsNaturalValueSA(key)) THEN FALSE
 ELSE IF ~(DOMAIN catalog \subseteq Nat \ {0}) THEN FALSE
 ELSE IF ~(\A key \in DOMAIN catalog : RowValidSA(catalog[key])) THEN FALSE
 ELSE \A a,b \in DOMAIN catalog :
   IF catalog[a].kind=catalog[b].kind THEN (catalog[a].nativeId=catalog[b].nativeId => a=b) ELSE TRUE
RegistryValidSA(catalog,currentRegistry) ==
 IF ~CatalogValidSA(catalog) THEN FALSE
 ELSE IF ~IsFunctionValueSA(currentRegistry) THEN FALSE
 ELSE IF ~(\A key \in DOMAIN currentRegistry : IsNaturalValueSA(key)) THEN FALSE
 ELSE IF ~(DOMAIN currentRegistry \subseteq DOMAIN catalog) THEN FALSE
 ELSE \A key \in DOMAIN currentRegistry :
   IF ~RowValidSA(currentRegistry[key]) THEN FALSE
   ELSE IF currentRegistry[key].kind # catalog[key].kind THEN FALSE
   ELSE currentRegistry[key]=catalog[key]
KeysOfKindSA(registry,kind) == {key \in DOMAIN registry : registry[key].kind=kind}
PaidPresentSA(registry) == {registry[key].nativeId : key \in KeysOfKindSA(registry,"Paid")}
ConditionalPresentSA(registry) == {registry[key].nativeId : key \in KeysOfKindSA(registry,"Conditional")}
ConditionalDefinitionsSA(registry) ==
 LET keys==KeysOfKindSA(registry,"Conditional")
     nativeKeys=={ConditionalKey96(registry[key].definition) : key \in keys}
 IN [native \in nativeKeys |-> registry[CHOOSE key \in keys : ConditionalKey96(registry[key].definition)=native].definition]
SourceDefaultActivitySA(basis,source) == FALSE
CommonActivitySA(basis,ledger) ==
 [ActivityContext9 EXCEPT !.activeRules=basis.rulePermissions,!.instances=ConditionalActivityRows96(ledger.instances),
  !.departureHolds=EmptySA,!.persistentAbilities={},!.lingeringAbilities={}]
BasisSA(revision,registry,objects,permissions) ==
 [revision |-> revision,registry |-> registry,objects |-> objects,rulePermissions |-> permissions]
LedgerDomainSA(ledger) == ledger.holds=EmptySA /\ ledger.effects=EmptySA
BasisValidSA(catalog,basis) ==
 /\ basis.revision \in Nat /\ RegistryValidSA(catalog,basis.registry)
 /\ basis.rulePermissions \subseteq {catalog[key].source.rule : key \in DOMAIN catalog}
MinimalCaptureSA(basis) == [revision |-> basis.revision,registry |-> basis.registry,objects |-> basis.objects,rulePermissions |-> basis.rulePermissions]
FamilyTurnUsesSA(catalog,index,turnUses,kind,source) ==
 [id \in {use \in DOMAIN turnUses :
    IF catalog[index[use]].kind=kind THEN catalog[index[use]].source=source ELSE FALSE} |-> turnUses[id]]
                                                                       
                                                                                               
UseProvenanceValidSA(catalog,uses,turnUses,index,procedures) ==
 IF ~CatalogValidSA(catalog) THEN FALSE
 ELSE IF DOMAIN uses # DOMAIN turnUses \/ DOMAIN index # DOMAIN uses THEN FALSE
 ELSE IF ~(\A id \in DOMAIN index : IsNaturalValueSA(index[id])) THEN FALSE
 ELSE IF ~(\A id \in DOMAIN index : index[id] \in DOMAIN catalog) THEN FALSE
 ELSE \A id \in DOMAIN uses :
   LET row==catalog[index[id]] event==uses[id] turn==turnUses[id] IN
   IF event.abilityInstance \notin DOMAIN procedures THEN FALSE
   ELSE LET p==procedures[event.abilityInstance] IN
   IF p.definition.syntax.kind # row.kind THEN FALSE
   ELSE /\ event.tag="AbilityUsed" /\ event.useId=id /\ event.abilityInstance=p.id
     /\ p.definition=row.definition /\ p.ability.source=row.source /\ event.source=row.source
     /\ event.player=row.definition.syntax.controller
     /\ turn.useId=id /\ turn.turnId=p.turnId /\ turn.source=row.source
     /\ IF row.kind="Paid" THEN
          ToString(turn.ability)=ToString(row.nativeId)
        ELSE ToString(turn.ability)=ToString(row.nativeId)
PaidContextFromRegistrySA(catalog,basis,ledger,index,turnUses,template,key) ==
 [template EXCEPT !.objects=basis.objects,!.present=PaidPresentSA(basis.registry),
  !.defaultActive=SourceDefaultActivitySA(basis,catalog[key].source),!.activity=CommonActivitySA(basis,ledger),
  !.uses=FamilyTurnUsesSA(catalog,index,turnUses,"Paid",catalog[key].source)]
ConditionalSnapshotFromRegistrySA(catalog,basis,ledger,template) ==
 [SnapshotWithConditionalRegistry96(template,ledger) EXCEPT
  !.definitions=ConditionalDefinitionsSA(basis.registry),!.present=ConditionalPresentSA(basis.registry),!.objects=basis.objects,
  !.ordinaryActivity=[native \in DOMAIN ConditionalDefinitionsSA(catalog) |-> SourceDefaultActivitySA(basis,native.source)],
  !.activity=CommonActivitySA(basis,ledger),!.activationEpoch=ConditionalEpochMap96(ledger,ConditionalDefinitionsSA(basis.registry)),
  !.activationSerial=ledger.activationSerial]
PaidBindingSA(catalog,basis,ledger,index,turnUses,template,key,view,capture) ==
 IF ~BasisValidSA(catalog,basis) THEN FALSE
 ELSE IF ~LedgerDomainSA(ledger) THEN FALSE
 ELSE IF key \notin DOMAIN basis.registry THEN FALSE
 ELSE IF catalog[key].kind # "Paid" THEN FALSE
 ELSE capture=MinimalCaptureSA(basis) /\ view=PaidContextFromRegistrySA(catalog,basis,ledger,index,turnUses,template,key)
ConditionalBindingSA(catalog,basis,ledger,template,view,capture) ==
 IF ~BasisValidSA(catalog,basis) THEN FALSE
 ELSE IF ~LedgerDomainSA(ledger) THEN FALSE
 ELSE capture=MinimalCaptureSA(basis) /\ view=ConditionalSnapshotFromRegistrySA(catalog,basis,ledger,template)
                                                                             
                                                                                   
AdmitPaidContextSA(catalog,basis,ledger,uses,turnUses,index,procedures,template,key,view,capture) ==
 IF ~BasisValidSA(catalog,basis) THEN FALSE
 ELSE IF ~UseProvenanceValidSA(catalog,uses,turnUses,index,procedures) THEN FALSE
 ELSE PaidBindingSA(catalog,basis,ledger,index,turnUses,template,key,view,capture)
AdmitConditionalSnapshotSA(catalog,basis,ledger,uses,turnUses,index,procedures,template,view,capture) ==
 IF ~BasisValidSA(catalog,basis) THEN FALSE
 ELSE IF ~UseProvenanceValidSA(catalog,uses,turnUses,index,procedures) THEN FALSE
 ELSE ConditionalBindingSA(catalog,basis,ledger,template,view,capture)
=============================================================================