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

TurnProceduresMC¶

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

ActionWorkT5 · operator

reference-profile · input revision 2 · CC0 1.0

ActionWorkT5 ==
 /\ ~DoneT5 /\ ~q5.ready /\ InfoT5(q5.flow).kind = "NeutralValue00001" /\ q5.flow.decision = "NeutralValue00001"
 /\ LET a == q5.action
    IN \/ /\ a.status = "CostReactions"
          /\ ActionEffectsBegin5(a,[a EXCEPT !.status = "Effects"],TRUE)
          /\ q5' = [q5 EXCEPT !.action.status = "Effects"]
       \/ /\ a.status = "Effects" /\ ~q5.nestedUsed /\ ~q5.tailDone
          /\ ActionNestedBegin5(a,[a EXCEPT !.status = "Nested",!.nested = "sampleNested"],"sampleNested")
          /\ q5' = [q5 EXCEPT !.action.status = "Nested",!.action.nested = "sampleNested",!.nestedUsed = TRUE]
       \/ /\ a.status = "Nested"
          /\ ActionNestedReturn5(a,[a EXCEPT !.status = "Effects",!.nested = "NoValue"],"sampleNested",TRUE)
          /\ q5' = [q5 EXCEPT !.action.status = "Effects",!.action.nested = "NoValue"]
       \/ /\ a.status = "Effects" /\ ~q5.tailDone
          /\ q5' = [q5 EXCEPT !.tailDone = TRUE]
       \/ /\ a.status = "Effects" /\ q5.tailDone
          /\ ActionComplete5(a,[a EXCEPT !.status = "Complete"],TRUE)
          /\ q5' = [q5 EXCEPT !.action.status = "Complete",!.ready = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActionComplete5, ActionEffectsBegin5, ActionNestedBegin5, ActionNestedReturn5, DoneT5, InfoT5, q5

AdvanceT5 · operator

reference-profile · input revision 2 · CC0 1.0

AdvanceT5 ==
 /\ ~DoneT5 /\ q5.ready
 /\ LET g == NextFrameT5(q5.flow)
    IN /\ IF q5.flow.turn.owner = "SideA" THEN SideAStepAdvance5(q5.flow,g,TRUE)
          ELSE SideBStepAdvance5(q5.flow,g,TRUE)
       /\ q5' = [q5 EXCEPT !.flow = g,!.ready = FALSE,
                   !.action = IF g.turn.id # q5.flow.turn.id THEN IdleActionT5 ELSE @]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAStepAdvance5, SideBStepAdvance5, DoneT5, IdleActionT5, NextFrameT5, q5

DoneT5 · operator

reference-profile · input revision 2 · CC0 1.0

DoneT5 == q5.flow.turn.id = 3

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: q5

EventuallyHandoff5 · operator

reference-profile · input revision 2 · CC0 1.0

EventuallyHandoff5 == <>DoneT5

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DoneT5

IdleActionT5 · operator

reference-profile · input revision 2 · CC0 1.0

IdleActionT5 == [NewAction5(0,"SideA",<<"Sample">>) EXCEPT !.status = "Idle"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NewAction5

InfoT5 · operator

reference-profile · input revision 2 · CC0 1.0

InfoT5(f) == IF f.turn.owner = "SideA" THEN SideAStepInfo5(f.step) ELSE SideBStepInfo5(f.step)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideAStepInfo5, SideBStepInfo5

InitTurns5 · operator

reference-profile · input revision 2 · CC0 1.0

InitTurns5 ==
 \E c \in {0,1,3}, r \in {0,1,4}:
  q5 = [flow |-> OpenSideAProcedure5(OpenTurn5("SideA",1,[p \in SetupPlayers |-> 0])),
         plan |-> [SideA |-> c,SideB |-> r],actionPoints |-> [p \in SetupPlayers |-> 0],
         recurring |-> [p \in SetupPlayers |-> 0],ready |-> FALSE,windowToken |-> FALSE,
         action |-> IdleActionT5,tailDone |-> FALSE,nestedUsed |-> FALSE,actionCount |-> 0,
         allotted |-> {},refilled |-> {},begun |-> {},ended |-> {},phaseEnded |-> {},draws |-> 0,
         windows |-> [p \in SetupPlayers |-> 0]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers, OpenSideAProcedure5, OpenTurn5, IdleActionT5, q5

LatchT5 · operator

reference-profile · input revision 2 · CC0 1.0

LatchT5 ==
 /\ ~DoneT5 /\ ~q5.ready /\ InfoT5(q5.flow).kind = "NeutralValue00001"
 /\ q5.flow.decision = "NoValue" /\ q5.windowToken
 /\ LET p == q5.flow.turn.owner
        g == [q5.flow EXCEPT !.decision = IF q5.actionPoints[p] > 0 THEN "NeutralValue00001" ELSE "End"]
    IN /\ IF p = "SideA" THEN SideALatchDecision5(q5.flow,g,q5.actionPoints[p],TRUE)
          ELSE SideBLatchDecision5(q5.flow,g,q5.actionPoints[p],TRUE)
       /\ q5' = [q5 EXCEPT !.flow = g,!.windowToken = FALSE,!.ready = q5.actionPoints[p] <= 0]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SideALatchDecision5, SideBLatchDecision5, DoneT5, InfoT5, q5

NextFrameT5 · operator

reference-profile · input revision 2 · CC0 1.0

NextFrameT5(f) ==
 IF f.step \in {"ProcedureCode72a65676fb11","ProcedureCode49c3ccade13b"} THEN
    IF f.turn.owner = "SideA" THEN OpenSideBProcedure5(OpenTurn5("SideB",f.turn.id+1,f.turn.begunCounts))
    ELSE OpenSideAProcedure5(OpenTurn5("SideA",f.turn.id+1,f.turn.begunCounts))
 ELSE LET next == IF f.turn.owner = "SideA" THEN SideANextStep5(f.step,f.decision)
                  ELSE SideBNextStep5(f.step,f.decision)
          phase == IF f.turn.owner = "SideA" THEN SideAStepInfo5(next).phase ELSE SideBStepInfo5(next).phase
      IN [f EXCEPT !.step = next,!.turn.phase = phase,!.decision = "NoValue"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OpenSideAProcedure5, OpenSideBProcedure5, OpenTurn5, SideANextStep5, SideAStepInfo5, SideBNextStep5, SideBStepInfo5

NextTurns5 · operator

reference-profile · input revision 2 · CC0 1.0

NextTurns5 == WorkStepT5 \/ LatchT5 \/ StartActionT5 \/ ActionWorkT5 \/ AdvanceT5 \/ (DoneT5 /\ UNCHANGED q5)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActionWorkT5, AdvanceT5, DoneT5, LatchT5, StartActionT5, WorkStepT5, q5

SpecTurns5 · operator

reference-profile · input revision 2 · CC0 1.0

SpecTurns5 == InitTurns5 /\ [][NextTurns5]_q5 /\ WF_q5(NextTurns5)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: InitTurns5, NextTurns5, q5

StartActionT5 · operator

reference-profile · input revision 2 · CC0 1.0

StartActionT5 ==
 /\ ~DoneT5 /\ ~q5.ready /\ InfoT5(q5.flow).kind = "NeutralValue00001"
 /\ q5.flow.decision = "NeutralValue00001" /\ q5.action.status \in {"Idle","Complete"}
 /\ LET p == q5.flow.turn.owner
        a == NewAction5(q5.actionCount+1,p,BasicActionKey5(p,"GainResourceUnit"))
    IN /\ q5.actionPoints[p] > 0
       /\ ActionStart5(q5.flow.turn,p,TRUE,<<[kind |-> "SpendActionPoints",amount |-> 1]>>,
                        TRUE,TRUE,TRUE,q5.actionCount+1,a.key,a)
       /\ q5' = [q5 EXCEPT !.actionPoints[p] = @-1,!.action = a,!.actionCount = @+1,
                           !.tailDone = FALSE,!.nestedUsed = FALSE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActionStart5, BasicActionKey5, NewAction5, DoneT5, InfoT5, q5

TurnsInvariant5 · operator

reference-profile · input revision 2 · CC0 1.0

TurnsInvariant5 ==
 /\ IF q5.flow.turn.owner = "SideA" THEN SideAProcedureValid5(q5.flow) ELSE SideBProcedureValid5(q5.flow)
 /\ q5.flow.turn.id \in 1..3 /\ NoBetweenTurns5(TRUE,q5.flow.turn)
 /\ q5.actionPoints \in [SetupPlayers -> 0..4] /\ q5.recurring \in [SetupPlayers -> {0,2}]
 /\ q5.refilled \subseteq q5.allotted /\ q5.begun \subseteq q5.refilled
 /\ q5.draws \in 0..1 /\ (q5.draws = 1 => "SideA" \in q5.begun)
 /\ (q5.flow.turn.formalBegun => q5.flow.turn.owner \in q5.begun)
 /\ (q5.flow.turn.formalEnded => q5.flow.turn.owner \in q5.ended /\ q5.flow.turn.phase = "Discard")
 /\ (q5.flow.turn.id >= 2 => "SideA" \in q5.ended /\ q5.draws = 1)
 /\ (q5.action.status \in {"CostReactions","Effects","Nested"} =>
       InfoT5(q5.flow).kind = "NeutralValue00001" /\ ~q5.ready /\ q5.flow.decision = "NeutralValue00001")
 /\ (InfoT5(q5.flow).kind = "NeutralValue00001" /\ q5.flow.decision = "NeutralValue00001" /\ q5.ready =>
       q5.action.status = "Complete")
 /\ (q5.flow.decision # "NoValue" => ~q5.windowToken)
 /\ (q5.action.status = "Complete" => q5.tailDone)
 /\ (DoneT5 => q5.ended = SetupPlayers /\ q5.begun = SetupPlayers /\
       q5.flow.turn.begunCounts = [p \in SetupPlayers |-> 1] /\ ~q5.flow.turn.formalBegun /\
       q5.actionCount = q5.plan["SideA"]+q5.plan["SideB"] /\
       q5.actionPoints = [p \in SetupPlayers |-> 0] /\
       q5.windows = [p \in SetupPlayers |-> q5.plan[p]+3])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: SetupPlayers, NoBetweenTurns5, SideAProcedureValid5, SideBProcedureValid5, DoneT5, InfoT5, q5

WorkStepT5 · operator

reference-profile · input revision 2 · CC0 1.0

WorkStepT5 ==
 /\ ~DoneT5 /\ ~q5.ready /\ InfoT5(q5.flow).kind # "NeutralValue00001"
 /\ LET f == q5.flow
        p == f.turn.owner
        kind == InfoT5(f).kind
    IN CASE kind = "AllotActionPoints" ->
         /\ GainAllottedActionPoints5(q5.actionPoints,[q5.actionPoints EXCEPT ![p] = @+q5.plan[p]],p,q5.plan[p])
         /\ q5' = [q5 EXCEPT !.actionPoints[p] = @+q5.plan[p],!.allotted = @ \cup {p},!.ready = TRUE]
       [] kind = "Refill" ->
         /\ IF p = "SideA" THEN SideARefillAtStep5(f,q5.recurring[p],2,2,TRUE)
            ELSE SideBRefillAtStep5(f,q5.recurring[p],2,2,TRUE)
         /\ q5' = [q5 EXCEPT !.recurring[p] = 2,!.refilled = @ \cup {p},!.ready = TRUE]
       [] kind = "TurnBegins" ->
         LET g == [f EXCEPT !.turn.formalBegun = TRUE,!.turn.begunCounts[p] = @+1]
         IN /\ IF p = "SideA" THEN SideAFormalBeginAtStep5(f,g,{TurnBeginEvent5(f.turn)})
               ELSE SideBFormalBeginAtStep5(f,g,{TurnBeginEvent5(f.turn)})
            /\ q5' = [q5 EXCEPT !.flow = g,!.begun = @ \cup {p},!.ready = TRUE]
       [] kind = "MandatoryDraw" ->
         /\ SideAMandatoryDrawAtStep5(f,[deck |-> <<"top","next">>,hand |-> {},actionPoints |-> q5.actionPoints[p]],
               [deck |-> <<"next">>,hand |-> {"top"},actionPoints |-> q5.actionPoints[p]],TRUE,"NoValue",{MandatoryDrawEvent5})
         /\ q5' = [q5 EXCEPT !.draws = @+1,!.ready = TRUE]
       [] kind = "ActionPhaseEnds" ->
         LET g == [f EXCEPT !.phaseEndMet = TRUE]
         IN /\ IF p = "SideA" THEN SideAActionPhaseEndAtStep5(f,g,{ActionPhaseEndEvent5(f.turn)})
               ELSE SideBActionPhaseEndAtStep5(f,g,{ActionPhaseEndEvent5(f.turn)})
            /\ q5' = [q5 EXCEPT !.flow = g,!.phaseEnded = @ \cup {p},!.ready = TRUE]
       [] kind = "TurnEnds" ->
         LET g == [f EXCEPT !.turn.formalEnded = TRUE]
         IN /\ IF p = "SideA" THEN SideAFormalEndAtStep5(f,g,TurnEndEvents5(f.turn))
               ELSE SideBFormalEndAtStep5(f,g,TurnEndEvents5(f.turn))
            /\ q5' = [q5 EXCEPT !.flow = g,!.ended = @ \cup {p},!.ready = TRUE]
       [] kind = "LoseUnspentActionPoints" ->
         /\ LoseUnspentActionPoints5(q5.actionPoints,[q5.actionPoints EXCEPT ![p] = 0],p)
         /\ q5' = [q5 EXCEPT !.actionPoints[p] = 0,!.ready = TRUE]
       [] kind = "PaidWindow" ->
         q5' = [q5 EXCEPT !.ready = TRUE,!.windows[p] = @+1,
                 !.windowToken = f.step \in {"ProcedureCoded6fbcb09dd4f","ProcedureCode484be3e50aa9"}]
       [] OTHER -> q5' = [q5 EXCEPT !.ready = TRUE]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ActionPhaseEndEvent5, GainAllottedActionPoints5, LoseUnspentActionPoints5, MandatoryDrawEvent5, SideAActionPhaseEndAtStep5, SideAFormalBeginAtStep5, SideAFormalEndAtStep5, SideAMandatoryDrawAtStep5, SideARefillAtStep5, SideBActionPhaseEndAtStep5, SideBFormalBeginAtStep5, SideBFormalEndAtStep5, SideBRefillAtStep5, TurnBeginEvent5, TurnEndEvents5, DoneT5, InfoT5, q5

q5 · variable

reference-profile · input revision 2 · CC0 1.0

q5

Exact module download · Source bundle and reproduction instructions