------------------------- MODULE ObjectiveChecksMC -------------------------
EXTENDS RuntimeChecksMC

ObjectiveStart(n) ==
    IF n = 7 THEN [ObjectiveAreaTree EXCEPT !.obj[1].objectivePoints = 2]
    ELSE IF n \in {8,9} THEN WithObjects([i \in {1} |-> Card("barrierCard","Play",TRUE,"Down",0)])
    ELSE IF n = 10 THEN WithObjects([i \in {1} |-> Card("objective","SideADeck",FALSE,"NA",0)])
    ELSE [WithObjects([i \in {1,2} |->
           IF i = 1 THEN [Card("objective","Play",TRUE,"Down",0) EXCEPT !.objectivePoints = 2]
           ELSE Token("Progress","Play",1,"SideA",FALSE)]) EXCEPT !.turn = "SideA"]
ObjectiveCommand(n) ==
    CASE n \in {1,2} -> MoveCmd(1,IF n = 1 THEN "SideBObjectiveCompletion" ELSE "SideAObjectiveCompletion","score",FALSE)
      [] n \in {3,4,5,6} ->
          [op |-> "Objective",object |-> 1,player |-> IF n \in {3,6} THEN "SideB" ELSE "SideA",
           mode |-> CASE n = 5 -> "ObjectiveCompletion" [] n = 6 -> "ClaimObjective" [] OTHER -> "Add",
           objectivePlacementWindow |-> TRUE,progressRequirement |-> 1,accessing |-> TRUE,
           costsComplete |-> TRUE,allowed |-> TRUE]
      [] n = 7 -> MoveCmd(1,"SideBObjectiveCompletion","score",FALSE)
      [] n = 8 -> MoveCmd(1,"Play","elsewhere",FALSE)
      [] n = 9 -> MoveCmd(1,"SideADiscard","discard",FALSE)
      [] OTHER -> MoveCmd(1,"SideBObjectiveCompletion","score",FALSE)
ObjectiveCommands(t) == {ObjectiveCommand(caseNo)}
ObjectiveInit == /\ caseNo \in 1..10 /\ pc = 0 /\ s = ObjectiveStart(caseNo)
ObjectiveProgress == /\ pc = 0 /\ Next /\ pc' = 1 /\ UNCHANGED caseNo
ObjectiveNext == ObjectiveProgress \/ (pc = 1 /\ UNCHANGED mcvars)
ObjectiveSpec == ObjectiveInit /\ [][ObjectiveNext]_mcvars /\ WF_pc(pc = 0 /\ pc' = 1)
ObjectiveCompleted == <>(pc = 1)
ObjectiveAssertions ==
    /\ (pc = 0 => ENABLED Next)
    /\ (pc = 1 /\ caseNo \in {1,2,3,4,5,6,7,10} =>
         LET id == IF caseNo = 7 THEN 4 ELSE IF caseNo = 10 THEN 2 ELSE 3 IN
         /\ s.obj[id].face = "Up" /\ ~s.obj[id].deployed
         /\ Owner(s,id) = "SideA"
         /\ Controller(s,id) = IF caseNo \in {2,4,5} THEN "SideA" ELSE "SideB")
    /\ (pc = 1 /\ caseNo \in {1,2,3,4} => Live(s,2) /\ s.pendingRetire = {2})
    /\ (pc = 1 /\ caseNo \in {5,6} => ~Live(s,2) /\
          s.lastObjective.progress = 1 /\ s.event = IF caseNo = 5 THEN "ObjectiveCompletion" ELSE "ClaimObjective")
    /\ (pc = 1 /\ caseNo \in {3,4} => s.event = "Add")
    /\ (pc = 1 /\ caseNo \in {1,2,7,8,9,10} => s.event = "Move")
    /\ (pc = 1 /\ caseNo = 7 => s.obj[5].host = 4 /\ s.obj[6].host = 5 /\
          s.obj[5].kind = "SchemaAtom043" /\ s.obj[6].kind = "Power" /\ s.pendingRetire = {})
    /\ (pc = 1 /\ caseNo = 8 => Live(s,1) /\ s.obj[1].face = "Down" /\ s.obj[1].deployed)
    /\ (pc = 1 /\ caseNo = 9 => s.obj[2].zone = "SideADiscard" /\
          s.obj[2].face = "Down" /\ ~s.obj[2].deployed)
=============================================================================