------------------------ MODULE RetirementChecksMC ------------------------
EXTENDS RuntimeChecksMC

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]])
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]
RetireCommands(t) == {RetireCommand(caseNo,pc)}
RetireLimit(n) == IF n = 1 THEN 2 ELSE 1
RetireInit == /\ caseNo \in 1..10 /\ pc = 0 /\ s = RetireStart(caseNo)
RetireProgress ==
    /\ pc < RetireLimit(caseNo)
    /\ IF caseNo # 8 THEN /\ Next /\ pc' = pc + 1 /\ UNCHANGED caseNo
       ELSE /\ ~ENABLED Next /\ pc' = 1 /\ UNCHANGED <<s,caseNo>>
RetireNext == RetireProgress \/ (pc = RetireLimit(caseNo) /\ UNCHANGED mcvars)
RetireSpec == RetireInit /\ [][RetireNext]_mcvars /\
             WF_pc(pc < RetireLimit(caseNo) /\ pc' = pc + 1)
RetireCompleted == <>(pc = RetireLimit(caseNo))
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")
=============================================================================