ObjectiveChecksMC

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.

ObjectiveAssertions · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Controller, Live, Next, Owner, s, caseNo, pc

ObjectiveCommand · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MoveCmd

ObjectiveCommands · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveCommands(t) == {ObjectiveCommand(caseNo)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectiveCommand, caseNo

ObjectiveCompleted · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveCompleted == <>(pc = 1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: pc

ObjectiveInit · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveInit == /\ caseNo \in 1..10 /\ pc = 0 /\ s = ObjectiveStart(caseNo)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: s, ObjectiveStart, caseNo, pc

ObjectiveNext · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveNext == ObjectiveProgress \/ (pc = 1 /\ UNCHANGED mcvars)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectiveProgress, mcvars, pc

ObjectiveProgress · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveProgress == /\ pc = 0 /\ Next /\ pc' = 1 /\ UNCHANGED caseNo

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Next, caseNo, pc

ObjectiveSpec · operator

reference-profile · input revision 2 · CC0 1.0

ObjectiveSpec == ObjectiveInit /\ [][ObjectiveNext]_mcvars /\ WF_pc(pc = 0 /\ pc' = 1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectiveInit, ObjectiveNext, mcvars, pc

ObjectiveStart · operator

reference-profile · input revision 2 · CC0 1.0

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"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Token, Card, ObjectiveAreaTree, WithObjects