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

OperationProceduresMC¶

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

ActualPaymentT8 · operator

reference-profile · input revision 2 · CC0 1.0

ActualPaymentT8 ==
 [id |-> 10,procedureId |-> 1,object |-> 2,allPaid |-> TRUE,
  basePart |-> PlayInherentPart8(q8.objects[2],IF q8.plan.x THEN 2 ELSE 0),
  playCostIgnored |-> q8.plan.ignored,paidSomething |-> ~q8.plan.ignored,checkpointRequired |-> ~q8.plan.ignored]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: PlayInherentPart8, q8

CardT8 · operator

reference-profile · input revision 2 · CC0 1.0

CardT8(side,cost,x) ==
 [card |-> "SchemaAtom149",form |-> "Card",side |-> side,kind |-> IF side="SideA" THEN "Plan" ELSE "Action",
  zone |-> side \o "Hand",loc |-> side \o "Hand",area |-> "NoValue",targetSite |-> "NoValue",targetSiteKind |-> "NoValue",
  position |-> "NoValue",host |-> 0,deployed |-> FALSE,face |-> "Down",activated |-> FALSE,
  marks |-> {"old"},subtypes |-> {},playCost |-> cost,playX |-> x]

Exact module download · Source bundle and reproduction instructions

DoneT8 · operator

reference-profile · input revision 2 · CC0 1.0

DoneT8 == q8.f.returned

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q8

DrainPlayCostT8 · operator

reference-profile · input revision 2 · CC0 1.0

DrainPlayCostT8 ==
 /\ q8.scheduler = "CostCheckpoint"
 /\ LET after == [q8.f EXCEPT !.stage = "ProcedureCodecbf6b11f0ae0"]
    IN /\ DrainPlayCostBarrier8(q8.f,after,10,IF q8.plan.ignored THEN 0 ELSE 11,TRUE)
       /\ q8' = [q8 EXCEPT !.f = after,!.scheduler = "Work",!.costDrained = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DrainPlayCostBarrier8, q8

DrainPlayEndT8 · operator

reference-profile · input revision 2 · CC0 1.0

DrainPlayEndT8 ==
 /\ q8.scheduler = "EndCheckpoint" /\ (q8.nestedPending => q8.nestedRemoved)
 /\ q8' = [q8 EXCEPT !.endDrained = TRUE,!.scheduler = "Return"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q8

DrainPlayedT8 · operator

reference-profile · input revision 2 · CC0 1.0

DrainPlayedT8 ==
 /\ q8.scheduler = "PlayedCheckpoint"
 /\ LET after == [q8.f EXCEPT !.stage = "ProcedureCode3d7f756d78f7"]
    IN /\ OpenPlayAbilities8(q8.f,after,12,TRUE)
       /\ q8' = [q8 EXCEPT !.f = after,!.scheduler = "Work",!.playedDrained = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenPlayAbilities8, q8

DrainSourceEndT8 · operator

reference-profile · input revision 2 · CC0 1.0

DrainSourceEndT8 ==
 /\ q8.scheduler = "SourceEndTriggers" /\ q8.childReturned
 /\ q8' = [q8 EXCEPT !.ownEndTriggers = TRUE,!.scheduler = "Work"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q8

EmptyT8 · operator

reference-profile · input revision 2 · CC0 1.0

EmptyT8 == [i \in {} |-> i]

Exact module download · Source bundle and reproduction instructions

EventuallyReturns8 · operator

reference-profile · input revision 2 · CC0 1.0

EventuallyReturns8 == <>DoneT8

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DoneT8

HostT8 · operator

reference-profile · input revision 2 · CC0 1.0

HostT8(side) ==
 [CardT8(side,0,FALSE) EXCEPT !.card = "Host",!.kind = IF side="SideA" THEN "Facility" ELSE "Equipment",
    !.zone = "Play",!.loc = "HostLocation",!.area = "Host",!.deployed = TRUE,!.face = "Up",
    !.activated = side="SideA",!.marks = {}]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardT8

IndependentEffectT8 · operator

reference-profile · input revision 2 · CC0 1.0

IndependentEffectT8 == [id |-> 50,source |-> 2,kind |-> "IndependentDelayed"]

Exact module download · Source bundle and reproduction instructions

InitProcedures8 · operator

reference-profile · input revision 2 · CC0 1.0

InitProcedures8 ==
 \E side \in SetupPlayers,cost \in {0,3},ignored \in BOOLEAN,x \in BOOLEAN,timing \in BOOLEAN:
 \E cleanup \in {"Retire","LeftPlay","Converted","Hosted","Retention","Nested"}:
  q8 = [plan |-> [side |-> side,cost |-> cost,ignored |-> ignored,x |-> x,timing |-> timing,cleanup |-> cleanup],
     f |-> OpenPlay8(1,1,side,"Parent"),objects |-> [id \in {1,9} |-> IF id=1 THEN CardT8(side,cost,x) ELSE HostT8(side)],
     effects |-> EmptyT8,scheduler |-> "Work",paid |-> FALSE,costDrained |-> FALSE,playedDrained |-> FALSE,
     childReturned |-> ~timing,ownEndTriggers |-> ~timing,endDrained |-> FALSE,
     played |-> 0,resolved |-> 0,cleanupDone |-> FALSE,trash |-> 0,nestedPending |-> FALSE,nestedRemoved |-> FALSE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenPlay8, CardT8, EmptyT8, HostT8, q8, SetupPlayers

NestedRemovalT8 · operator

reference-profile · input revision 2 · CC0 1.0

NestedRemovalT8 ==
 /\ q8.scheduler = "EndCheckpoint" /\ q8.nestedPending /\ ~q8.nestedRemoved
 /\ LET objects == RelocatedSourceT8(q8.objects,"Removed")
    IN /\ CardBatchTransfer8(q8.objects,objects,{2},[id \in {2} |-> 3],{1,2,9},"Removed","Up",[id \in {2} |-> "Removed"])
       /\ q8' = [q8 EXCEPT !.objects = objects,!.nestedRemoved = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CardBatchTransfer8, RelocatedSourceT8, q8

NextProcedures8 · operator

reference-profile · input revision 2 · CC0 1.0

NextProcedures8 ==
 WorkPlayT8 \/ DrainPlayCostT8 \/ DrainPlayedT8 \/ ReturnChildT8 \/ DrainSourceEndT8 \/
 NestedRemovalT8 \/ DrainPlayEndT8 \/ ReturnPlayT8 \/ (DoneT8 /\ UNCHANGED q8)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DoneT8, DrainPlayCostT8, DrainPlayEndT8, DrainPlayedT8, DrainSourceEndT8, NestedRemovalT8, ReturnChildT8, ReturnPlayT8, WorkPlayT8, q8

ProceduresInvariant8 · operator

reference-profile · input revision 2 · CC0 1.0

ProceduresInvariant8 ==
 /\ DOMAIN q8.objects \subseteq {1,2,3,9}
 /\ Cardinality({id \in DOMAIN q8.objects : q8.objects[id].card="SchemaAtom149"}) = 1
 /\ \A id \in DOMAIN q8.objects : ActivationCacheValid8(q8.objects[id])
 /\ q8.f.activationReached => q8.costDrained /\ q8.paid
 /\ q8.played = IF q8.f.stage \in {"ProcedureCodebddd9a1a600b","ProcedureCode3d7f756d78f7","ProcedureCodee977e478b45b","ProcedureCodec610fc738935","ProcedureCode03de9212dc90","Complete"} THEN 1 ELSE 0
 /\ q8.f.stage \in {"ProcedureCodee977e478b45b","ProcedureCodec610fc738935","ProcedureCode03de9212dc90","Complete"} => q8.playedDrained /\ q8.childReturned /\ q8.ownEndTriggers
 /\ q8.paid => q8.f.x = [exists |-> q8.plan.x,amount |-> IF q8.plan.x THEN 2 ELSE 0]
 /\ (2 \in DOMAIN q8.objects /\ ~q8.f.activationReached) => ~PlayEffectiveCardActivity8(q8.f,2,q8.objects[2],TRUE)
 /\ q8.cleanupDone => 50 \in DOMAIN q8.effects /\ q8.effects[50] = IndependentEffectT8
 /\ q8.trash = IF q8.cleanupDone /\ q8.plan.cleanup="Retire" THEN 1 ELSE 0
 /\ q8.f.complete => q8.cleanupDone /\ q8.resolved = 1
 /\ q8.nestedRemoved => q8.nestedPending /\ q8.resolved = 1 /\ q8.f.complete
 /\ q8.f.returned => q8.endDrained /\ q8.played = 1 /\ q8.resolved = 1
 /\ IF q8.f.returned THEN
       CASE q8.plan.cleanup="Retire" -> 3 \in DOMAIN q8.objects /\ q8.objects[3].zone=q8.plan.side \o "Discard"
         [] q8.plan.cleanup="LeftPlay" \/ q8.plan.cleanup="Nested" -> 3 \in DOMAIN q8.objects /\ q8.objects[3].zone="Removed"
         [] q8.plan.cleanup="Converted" -> q8.objects[2].form="Counter" /\ q8.objects[2].host=9
         [] q8.plan.cleanup="Hosted" -> q8.objects[2].host=9 /\ ~q8.objects[2].deployed
         [] OTHER -> 51 \in DOMAIN q8.effects /\ q8.objects[2].zone="Play"
    ELSE TRUE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActivationCacheValid8, PlayEffectiveCardActivity8, IndependentEffectT8, q8

PutEffectT8 · operator

reference-profile · input revision 2 · CC0 1.0

PutEffectT8(effects,receipt) ==
 [id \in DOMAIN effects \cup {receipt.id} |-> IF id=receipt.id THEN receipt ELSE effects[id]]

Exact module download · Source bundle and reproduction instructions

RelocatedSourceT8 · operator

reference-profile · input revision 2 · CC0 1.0

RelocatedSourceT8(objects,zone) ==
 [id \in {3,9} |-> IF id=3 THEN
    [WithCardLocation8(objects[2],[NoDeployDestination8 EXCEPT !.zone = zone,!.loc = zone,!.area = "NoValue"]) EXCEPT
       !.deployed = FALSE,!.face = "Up",!.activated = FALSE,!.marks = {}]
    ELSE objects[id]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NoDeployDestination8, WithCardLocation8

RetentionT8 · operator

reference-profile · input revision 2 · CC0 1.0

RetentionT8 == [id |-> 51,playId |-> 1,source |-> 2,created |-> TRUE,expiryEffect |-> "NextTurn"]

Exact module download · Source bundle and reproduction instructions

ReturnChildT8 · operator

reference-profile · input revision 2 · CC0 1.0

ReturnChildT8 ==
 /\ q8.scheduler = "ChildReturn"
 /\ q8' = [q8 EXCEPT !.childReturned = TRUE,!.scheduler = "SourceEndTriggers"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q8

ReturnPlayT8 · operator

reference-profile · input revision 2 · CC0 1.0

ReturnPlayT8 ==
 /\ q8.scheduler = "Return" /\ q8.endDrained
 /\ ReturnPlayToCaller8(q8.f,[q8.f EXCEPT !.returned = TRUE],TRUE,"Parent")
 /\ q8' = [q8 EXCEPT !.f.returned = TRUE,!.scheduler = "Done"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ReturnPlayToCaller8, q8

SpecProcedures8 · operator

reference-profile · input revision 2 · CC0 1.0

SpecProcedures8 == InitProcedures8 /\ [][NextProcedures8]_q8 /\ WF_q8(NextProcedures8)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InitProcedures8, NextProcedures8, q8

WorkPlayT8 · operator

reference-profile · input revision 2 · CC0 1.0

WorkPlayT8 ==
 /\ q8.scheduler = "Work"
 /\ LET f == q8.f
    IN CASE f.stage = "ProcedureCodebfd1895de2c0" ->
        LET objects == [id \in {2,9} |-> IF id=2 THEN PlayedPlacementRow8(q8.objects[1],TRUE) ELSE q8.objects[id]]
            after == [f EXCEPT !.object = 2,!.stage = "ProcedureCode0f076861472c",!.kind = q8.objects[1].kind,!.subtypes = {}]
        IN /\ BeginPlay8(f,after,q8.objects,objects,2,{1,9},TRUE)
           /\ q8' = [q8 EXCEPT !.f = after,!.objects = objects]
      [] f.stage = "ProcedureCode0f076861472c" ->
        LET after == [f EXCEPT !.stage = "CostBarrier",!.transaction = 10,!.checkpointRequired = ~q8.plan.ignored,
              !.x = [exists |-> q8.plan.x,amount |-> IF q8.plan.x THEN 2 ELSE 0]]
        IN /\ PayPlayStep8(f,after,q8.objects,ActualPaymentT8,q8.plan.ignored,IF q8.plan.x THEN 2 ELSE 0,TRUE)
           /\ q8' = [q8 EXCEPT !.f = after,!.paid = TRUE,!.scheduler = "CostCheckpoint"]
      [] f.stage = "ProcedureCodecbf6b11f0ae0" ->
        LET after == [f EXCEPT !.stage = "ProcedureCode7647b901fcb1",!.activationReached = TRUE]
        IN /\ ActivatePlayedCard8(f,after)
           /\ q8' = [q8 EXCEPT !.f = after]
      [] f.stage = "ProcedureCode7647b901fcb1" ->
        LET after == [f EXCEPT !.stage = "ProcedureCodebddd9a1a600b"]
        IN /\ MeetPlayedConditions8(f,after,{PlayedCondition8(f)})
           /\ q8' = [q8 EXCEPT !.f = after,!.played = @+1,!.scheduler = "PlayedCheckpoint"]
      [] f.stage = "ProcedureCode3d7f756d78f7" ->
        IF ~q8.childReturned THEN q8' = [q8 EXCEPT !.scheduler = "ChildReturn"]
        ELSE LET receipt == [playId |-> 1,object |-> 2,allPlayAbilitiesResolved |-> TRUE,
                     ownedTimingIds |-> IF q8.plan.timing THEN {77} ELSE {},
                     returnedTimingIds |-> IF q8.childReturned /\ q8.plan.timing THEN {77} ELSE {},
                     ownEndTriggersResolved |-> q8.ownEndTriggers]
                 after == [f EXCEPT !.stage = "ProcedureCodee977e478b45b"]
                 objects == CASE q8.plan.cleanup = "LeftPlay" -> RelocatedSourceT8(q8.objects,"Removed")
                   [] q8.plan.cleanup = "Converted" ->
                       [q8.objects EXCEPT ![2].form = "Counter",![2].kind = "SchemaAtom043",![2].host = 9,
                            ![2].loc = <<"Host",9>>,![2].area = "Hosted",![2].deployed = TRUE]
                   [] q8.plan.cleanup = "Hosted" ->
                       [q8.objects EXCEPT ![2].host = 9,![2].loc = <<"Host",9>>,![2].area = "Hosted"]
                   [] OTHER -> q8.objects
             IN /\ FinishPlayAbilities8(f,after,receipt)
                /\ IF q8.plan.cleanup = "LeftPlay" THEN
                     CardBatchTransfer8(q8.objects,objects,{2},[id \in {2} |-> 3],{1,2,9},"Removed","Up",[id \in {2} |-> "Removed"])
                   ELSE TRUE
                /\ q8' = [q8 EXCEPT !.f = after,!.objects = objects,!.effects = PutEffectT8(@,IndependentEffectT8)]
      [] f.stage = "ProcedureCodee977e478b45b" ->
        LET disposition == PlayCleanupDisposition8(f,q8.objects,q8.plan.cleanup="Retention",q8.plan.cleanup="Nested")
            cleanupReceipt == [playId |-> 1,object |-> 2,disposition |-> disposition,trashInstructionComplete |-> TRUE]
            effects == IF disposition="RetainSelf" THEN PutEffectT8(q8.effects,RetentionT8) ELSE q8.effects
            objects == IF disposition="Retire" THEN RelocatedSourceT8(q8.objects,q8.plan.side \o "Discard") ELSE q8.objects
            after == [f EXCEPT !.stage = "ProcedureCodec610fc738935"]
        IN /\ FinishPlayCleanup8(f,after,q8.objects,q8.plan.cleanup="Retention",q8.plan.cleanup="Nested",
                    cleanupReceipt,q8.effects,effects,RetentionT8)
           /\ IF disposition="Retire" THEN CardBatchTransfer8(q8.objects,objects,{2},[id \in {2} |-> 3],
                  {1,2,9},q8.plan.side \o "Discard","Up",[id \in {2} |-> q8.plan.side \o "Discard"]) ELSE TRUE
           /\ q8' = [q8 EXCEPT !.f = after,!.objects = objects,!.effects = effects,!.cleanupDone = TRUE,
                          !.trash = IF disposition="Retire" THEN 1 ELSE 0]
      [] f.stage = "ProcedureCodec610fc738935" ->
        LET after == [f EXCEPT !.stage = "ProcedureCode03de9212dc90"]
        IN /\ MeetPlayResolvedConditions8(f,after,{[tag |-> "PlayResolved",object |-> 2,kind |-> f.kind,actor |-> f.actor,playId |-> 1]})
           /\ q8' = [q8 EXCEPT !.f = after,!.resolved = @+1,!.nestedPending = q8.plan.cleanup="Nested"]
      [] f.stage = "ProcedureCode03de9212dc90" ->
        LET after == [f EXCEPT !.stage = "Complete",!.complete = TRUE]
        IN /\ CompletePlay8(f,after)
           /\ q8' = [q8 EXCEPT !.f = after,!.scheduler = "EndCheckpoint"]
      [] OTHER -> FALSE

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActivatePlayedCard8, BeginPlay8, CardBatchTransfer8, CompletePlay8, FinishPlayAbilities8, FinishPlayCleanup8, MeetPlayResolvedConditions8, MeetPlayedConditions8, PayPlayStep8, PlayCleanupDisposition8, PlayedCondition8, PlayedPlacementRow8, ActualPaymentT8, IndependentEffectT8, PutEffectT8, RelocatedSourceT8, RetentionT8, q8

q8 · variable

reference-profile · input revision 2 · CC0 1.0

q8

Exact module download · Source bundle and reproduction instructions