r1 qualified Selected asymmetric formal reference: 2,502 contracts across nine families; bounded evidence and three separate teaching models Read the evidence scope

RegistryChecksMC¶

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 31 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.

SAdmissionChecksSA · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: AdmitConditionalSnapshotSA, AdmitPaidContextSA, ConditionalBindingSA, MinimalCaptureSA, PaidContextFromRegistrySA, SBasisSA, SCatalogSA, SIndexSA, SLedgerSA, SProceduresSA, SSnapshotSA, STemplateSA, STurnUsesSA, SUsesSA, SWithoutSA

SAssertionsSA · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SAdmissionChecksSA, SAvailabilityChecksSA, SConditionalBindingChecksSA, SHistoryChecksSA, SInvalidCatalogChecksSA, SLedgerBindingChecksSA, SMalformedChecksSA, SPaidBindingChecksSA, SProjectionChecksSA, SProvenanceChecksSA, SQueryChecksSA, registryCaseSA

SAvailabilityChecksSA · operator

reference-profile · input revision 2 · CC0 1.0

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]]))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalActive96, PaidEligibility95, BasisValidSA, RegistryValidSA, PJoin, SBasisSA, SCatalogSA, SConditionalSA, SContextSA, SPaidSA, SSnapshotSA, SWindowSA, SWithoutSA

SBasisSA · operator

reference-profile · input revision 2 · CC0 1.0

SBasisSA == BasisSA(4,SCatalogSA,EmptyT11,{"SharedRegistryControl","Specimen0070RegistryControl"})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: BasisSA, SCatalogSA, EmptyT11

SCasesSA · operator

reference-profile · input revision 2 · CC0 1.0

SCasesSA == 1..11

Exact module download · Source bundle and reproduction instructions

SCatalogSA · operator

reference-profile · input revision 2 · CC0 1.0

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)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SConditionalSA, SMidSA, SPaidSA, SRowSA, SSpecimen0070SA

SConditionalBindingChecksSA · operator

reference-profile · input revision 2 · CC0 1.0

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])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, ConditionalBindingSA, MinimalCaptureSA, SBasisSA, SCatalogSA, SConditionalSA, SLedgerSA, SSnapshotSA, EmptyT11

SConditionalSA · operator

reference-profile · input revision 2 · CC0 1.0

SConditionalSA == [PChildDefinition EXCEPT !.syntax.source=SRuleSA,!.activity.source=SRuleSA]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PChildDefinition, SRuleSA

SContextSA · operator

reference-profile · input revision 2 · CC0 1.0

SContextSA(basis) == PaidContextFromRegistrySA(SCatalogSA,basis,SLedgerSA,EmptyT11,EmptyT11,STemplateSA,3)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PaidContextFromRegistrySA, SCatalogSA, SLedgerSA, STemplateSA, EmptyT11

SFlaggedConditionalSA · operator

reference-profile · input revision 2 · CC0 1.0

SFlaggedConditionalSA == [SConditionalSA.syntax EXCEPT !.units= <<TextUnit93(99,"AbilityFlag","OncePerTurn",FALSE,0)>> \o @]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: TextUnit93, SConditionalSA

SHistoryChecksSA · operator

reference-profile · input revision 2 · CC0 1.0

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))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalActive96, ConditionalBindingSA, MinimalCaptureSA, SBasisSA, SCatalogSA, SConditionalSA, SLedgerSA, SSnapshotSA

SIndexSA · operator

reference-profile · input revision 2 · CC0 1.0

SIndexSA == [id \in 1..4 |-> CASE id=1 -> 1 [] id=2 -> 2 [] id=3 -> 4 [] OTHER -> 3]

Exact module download · Source bundle and reproduction instructions

SInitSA · operator

reference-profile · input revision 2 · CC0 1.0

SInitSA == registryCaseSA \in SCasesSA /\ guideCaseT11=0 /\ qT11=EmptyT11

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SCasesSA, registryCaseSA, EmptyT11, guideCaseT11, qT11

SInvalidCatalogChecksSA · operator

reference-profile · input revision 2 · CC0 1.0

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]]))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RuleAbilitySource9, CatalogValidSA, RegistryValidSA, PJoin, SCatalogSA, SWithoutSA

SLedgerBindingChecksSA · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalKey96, ConditionalBindingSA, MinimalCaptureSA, SBasisSA, SCatalogSA, SConditionalSA, SLedgerSA, SSnapshotSA

SLedgerSA · operator

reference-profile · input revision 2 · CC0 1.0

SLedgerSA == NewConditionalLedger96([PInitialSnapshot EXCEPT !.definitions=ConditionalDefinitionsSA(SCatalogSA),
 !.present=ConditionalPresentSA(SCatalogSA),!.objects=EmptyT11,
 !.activationEpoch=[key \in DOMAIN ConditionalDefinitionsSA(SCatalogSA) |-> 0]])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewConditionalLedger96, ConditionalDefinitionsSA, ConditionalPresentSA, PInitialSnapshot, SCatalogSA, EmptyT11

SMalformedChecksSA · operator

reference-profile · input revision 2 · CC0 1.0

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"]])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalHeaderSA, RowHeaderSA, RowValidSA, RuleSourceValidSA, SCatalogSA, SConditionalSA

SMidSA · operator

reference-profile · input revision 2 · CC0 1.0

SMidSA == [ItemInspectionPaidDefinitionT11([NeutralValue00013 |-> "FacilityObserve0"]) EXCEPT !.syntax.source=SRuleSA,!.activity.source=SRuleSA]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ItemInspectionPaidDefinitionT11, SRuleSA

SNextSA · operator

reference-profile · input revision 2 · CC0 1.0

SNextSA == UNCHANGED <<registryCaseSA,guideCaseT11,qT11>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: registryCaseSA, guideCaseT11, qT11

SPaidBindingChecksSA · operator

reference-profile · input revision 2 · CC0 1.0

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])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MinimalCaptureSA, PaidBindingSA, PObjects, SBasisSA, SCatalogSA, SContextSA, SLedgerSA, STemplateSA, EmptyT11

SPaidSA · operator

reference-profile · input revision 2 · CC0 1.0

SPaidSA == [ProtocolP!RootDefinition9p EXCEPT !.syntax.id="RepeatableControl",!.syntax.source=SRuleSA,
 !.activity.id="RepeatableControl",!.activity.source=SRuleSA,!.activity.provider="Rule"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ProtocolP!RootDefinition9p, SRuleSA

SProcedureSA · operator

reference-profile · input revision 2 · CC0 1.0

SProcedureSA(key,id) == [id |-> id,definition |-> SCatalogSA[key].definition,
 ability |-> [source |-> SCatalogSA[key].source],turnId |-> 1]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SCatalogSA

SProceduresSA · operator

reference-profile · input revision 2 · CC0 1.0

SProceduresSA == [id \in 11..14 |-> SProcedureSA(CASE id=11 -> 1 [] id=12 -> 2 [] id=13 -> 4 [] OTHER -> 3,id)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SProcedureSA

SProjectionChecksSA · operator

reference-profile · input revision 2 · CC0 1.0

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))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalActive96, ConditionalDefinitionValid96, ConditionalKey96, PaidEligibility95, ConditionalDefinitionsSA, ConditionalPresentSA, PaidPresentSA, RegistryValidSA, MidOption7, MidOptionsValid7, SBasisSA, SCatalogSA, SConditionalSA, SContextSA, SMidSA, SPaidSA, SSnapshotSA, SWindowSA

SProvenanceChecksSA · operator

reference-profile · input revision 2 · CC0 1.0

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])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RuleAbilitySource9, UseProvenanceValidSA, SCatalogSA, SIndexSA, SProceduresSA, STurnUsesSA, SUsesSA, SWithoutSA

SQueryChecksSA · operator

reference-profile · input revision 2 · CC0 1.0

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))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OncePerTurnAllowed93, FamilyTurnUsesSA, RegistryValidSA, UseProvenanceValidSA, SCatalogSA, SFlaggedConditionalSA, SIndexSA, SMidSA, SProceduresSA, SRuleSA, STurnUsesSA, SUsesSA, SWithoutSA

SRowSA · operator

reference-profile · input revision 2 · CC0 1.0

SRowSA(kind,d) == [kind |-> kind,nativeId |-> d.syntax.id,source |-> d.syntax.source,definition |-> d]

Exact module download · Source bundle and reproduction instructions

SRuleSA · operator

reference-profile · input revision 2 · CC0 1.0

SRuleSA == RuleAbilitySource9("SharedRegistryControl")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RuleAbilitySource9

SSnapshotSA · operator

reference-profile · input revision 2 · CC0 1.0

SSnapshotSA(basis) == ConditionalSnapshotFromRegistrySA(SCatalogSA,basis,SLedgerSA,SLedgerSA.lastSnapshot)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ConditionalSnapshotFromRegistrySA, SCatalogSA, SLedgerSA

SSpecSA · operator

reference-profile · input revision 2 · CC0 1.0

SSpecSA == SInitSA /\ [][SNextSA]_<<registryCaseSA,guideCaseT11,qT11>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SInitSA, SNextSA, registryCaseSA, guideCaseT11, qT11

SSpecimen0070SA · operator

reference-profile · input revision 2 · CC0 1.0

SSpecimen0070SA == [SPaidSA EXCEPT !.syntax.id="Specimen0070Control",!.activity.id="Specimen0070Control",
 !.syntax.source=RuleAbilitySource9("Specimen0070RegistryControl"),!.activity.source=RuleAbilitySource9("Specimen0070RegistryControl")]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RuleAbilitySource9, SPaidSA

STemplateSA · operator

reference-profile · input revision 2 · CC0 1.0

STemplateSA == [ProtocolP!RootContext9p EXCEPT !.ownRestrictions.ability=SPaidSA.syntax.id,!.ownRestrictions.source=SRuleSA,
 !.otherRestrictions.ability=SPaidSA.syntax.id,!.otherRestrictions.source=SRuleSA]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ProtocolP!RootContext9p, SPaidSA, SRuleSA

STurnUsesSA · operator

reference-profile · input revision 2 · CC0 1.0

STurnUsesSA == [id \in 1..4 |-> [turnId |-> 1,ability |-> SCatalogSA[SIndexSA[id]].nativeId,
 source |-> SCatalogSA[SIndexSA[id]].source,useId |-> id]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SCatalogSA, SIndexSA

SUsesSA · operator

reference-profile · input revision 2 · CC0 1.0

SUsesSA == [id \in 1..4 |-> [tag |-> "AbilityUsed",useId |-> id,abilityInstance |-> 10+id,
 source |-> SCatalogSA[SIndexSA[id]].source,player |-> "SideB"]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SCatalogSA, SIndexSA

SWindowSA · operator

reference-profile · input revision 2 · CC0 1.0

SWindowSA == [ProtocolP!Window9p(30,"Paid",EmptyT11,0) EXCEPT !.stage="Ready",!.checkpoint=1]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ProtocolP!Window9p, EmptyT11

SWithoutSA · operator

reference-profile · input revision 2 · CC0 1.0

SWithoutSA(registry,key) == [id \in DOMAIN registry \ {key} |-> registry[id]]

Exact module download · Source bundle and reproduction instructions

registryCaseSA · variable

reference-profile · input revision 2 · CC0 1.0

registryCaseSA

Exact module download · Source bundle and reproduction instructions