RetirementChecksMC

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

RetireAssertions · operator

reference-profile · input revision 2 · CC0 1.0

RetireAssertions ==
    /\ (pc = 0 => (ENABLED Next) = (caseNo # 8))
    /\ (caseNo = 8 => s = RetireStart(8))
    /\ (pc >= 1 /\ caseNo \in {1,2,5,6,7,9} =>
          LET id == IF caseNo = 1 THEN 3 ELSE 2 IN
          /\ s.obj[id].zone = "SideBDiscard" /\ s.obj[id].face = "Up"
          /\ ~s.obj[id].deployed /\ ~s.obj[id].activated /\ Owner(s,id) = "SideB")
    /\ (pc = 1 /\ caseNo \in {3,4} => s.obj[2].zone = "SideADiscard" /\
          s.obj[2].face = IF caseNo = 3 THEN "Down" ELSE "Up")
    /\ (pc = 1 /\ caseNo \in {1,2,3,4,6} => s.event = "Retire")
    /\ (pc = 1 /\ caseNo = 5 => s.event = "Discard")
    /\ (pc = 1 /\ caseNo \in {7,9,10} => s.event = "Move")
    /\ (caseNo = 1 /\ pc = 1 => Live(s,2) /\ ~Active(s,2) /\ s.pendingRetire = {2})
    /\ (caseNo = 1 /\ pc = 2 => ~Live(s,2) /\ s.pendingRetire = {})
    /\ (caseNo = 10 /\ pc = 1 => s.obj[2].zone = "SideBHand" /\ s.obj[2].face = "NA")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Active, Live, Next, Owner, s, RetireStart, caseNo, pc

RetireCommand · operator

reference-profile · input revision 2 · CC0 1.0

RetireCommand(n, step) ==
    IF n = 1 /\ step = 1 THEN Check
    ELSE IF n = 5 THEN [op |-> "Discard",object |-> 1,allowed |-> FALSE]
    ELSE IF n \in {7,9} THEN MoveCmd(1,"SideBDiscard","discard",FALSE)
    ELSE IF n = 10 THEN MoveCmd(1,"SideBHand","hand",FALSE)
    ELSE [op |-> "Retire",object |-> 1,allowed |-> n # 8]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Check, MoveCmd

RetireCommands · operator

reference-profile · input revision 2 · CC0 1.0

RetireCommands(t) == {RetireCommand(caseNo,pc)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RetireCommand, caseNo, pc

RetireCompleted · operator

reference-profile · input revision 2 · CC0 1.0

RetireCompleted == <>(pc = RetireLimit(caseNo))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RetireLimit, caseNo, pc

RetireInit · operator

reference-profile · input revision 2 · CC0 1.0

RetireInit == /\ caseNo \in 1..10 /\ pc = 0 /\ s = RetireStart(caseNo)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: s, RetireStart, caseNo, pc

RetireLimit · operator

reference-profile · input revision 2 · CC0 1.0

RetireLimit(n) == IF n = 1 THEN 2 ELSE 1

Exact module download · Source bundle and reproduction instructions

RetireNext · operator

reference-profile · input revision 2 · CC0 1.0

RetireNext == RetireProgress \/ (pc = RetireLimit(caseNo) /\ UNCHANGED mcvars)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RetireLimit, RetireProgress, mcvars, caseNo, pc

RetireProgress · operator

reference-profile · input revision 2 · CC0 1.0

RetireProgress ==
    /\ pc < RetireLimit(caseNo)
    /\ IF caseNo # 8 THEN /\ Next /\ pc' = pc + 1 /\ UNCHANGED caseNo
       ELSE /\ ~ENABLED Next /\ pc' = 1 /\ UNCHANGED <<s,caseNo>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Next, s, RetireLimit, caseNo, pc

RetireSpec · operator

reference-profile · input revision 2 · CC0 1.0

RetireSpec == RetireInit /\ [][RetireNext]_mcvars /\
             WF_pc(pc < RetireLimit(caseNo) /\ pc' = pc + 1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: RetireInit, RetireLimit, RetireNext, mcvars, caseNo, pc

RetireStart · operator

reference-profile · input revision 2 · CC0 1.0

RetireStart(n) ==
    IF n = 1 THEN WithObjects([i \in {1,2} |->
         IF i = 1 THEN Card("technique","Play",TRUE,"Down",0)
         ELSE Token("SchemaAtom043","Play",1,"SideB",FALSE)])
    ELSE WithObjects([i \in {1} |->
         IF n = 6 THEN Card("technique","SideBHand",FALSE,"NA",0)
         ELSE IF n = 9 THEN Card("technique","SetAside",FALSE,"Down",0)
         ELSE [Card(IF n \in {3,4} THEN "barrierCard" ELSE IF n = 2 THEN "host" ELSE "technique",
                    "Play",TRUE,IF n = 4 THEN "Up" ELSE "Down",0)
               EXCEPT !.activated = n = 4]])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Token, Card, WithObjects