VisibilityChecksMC

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.

ExposureAssertions · operator

reference-profile · input revision 2 · CC0 1.0

ExposureAssertions ==
    /\ (pc = 0 => (ENABLED Next) = (caseNo \in ExposureEnabled))
    /\ (caseNo \notin ExposureEnabled => s = ExposureStart(caseNo))
    /\ (pc >= 1 /\ caseNo \in ExposureEnabled =>
          s.obj = ExposureStart(caseNo).obj /\ s.obj[1].face = "Down")
    /\ (pc = 1 /\ caseNo \in ExposureEnabled =>
          MayLook(s,"SideA",1) /\ MayLook(s,"SideB",1) /\
          s.event = IF caseNo = 11 THEN "Reveal" ELSE "Expose")
    /\ (caseNo = 1 /\ pc = 2 => ~MayLook(s,"SideB",1) /\
          MayLook(s,"SideA",1) /\ s.reveals = {} /\ s.event = "AbilityEnd")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MayLook, Next, s, caseNo, pc, ExposureEnabled, ExposureStart

ExposureCard · operator

reference-profile · input revision 2 · CC0 1.0

ExposureCard(c, zone, deployed, face, activated) ==
    [Card(IF c \in DOMAIN Data THEN c ELSE "barrierCard",zone,deployed,face,0)
     EXCEPT !.card = c, !.kind = ExposureData[c].kind, !.activated = activated]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Card, Data, ExposureData

ExposureCommand · operator

reference-profile · input revision 2 · CC0 1.0

ExposureCommand(n, step) ==
    IF step = 1 THEN [op |-> "AbilityEnd",ability |-> "expose"]
    ELSE [op |-> "Reveal",object |-> 1,mode |-> IF n = 11 THEN "Reveal" ELSE "Expose",
          viewers |-> IF n = 12 THEN {"SideB"} ELSE Players,ability |-> "expose"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Players

ExposureCommands · operator

reference-profile · input revision 2 · CC0 1.0

ExposureCommands(t) == {ExposureCommand(caseNo,pc)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: caseNo, pc, ExposureCommand

ExposureCompleted · operator

reference-profile · input revision 2 · CC0 1.0

ExposureCompleted == <>(pc = ExposureLimit(caseNo))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: caseNo, pc, ExposureLimit

ExposureData · operator

reference-profile · input revision 2 · CC0 1.0

ExposureData == [c \in DOMAIN Data \cup {"facility","upgrade","operation"} |->
    IF c \in DOMAIN Data THEN Data[c]
    ELSE [owner |-> "SideA",side |-> "SideA",name |-> c,recurring |-> 0,
          kind |-> CASE c = "facility" -> "Facility" [] c = "upgrade" -> "Attachment"
                     [] OTHER -> "Plan"]]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Data

ExposureEnabled · operator

reference-profile · input revision 2 · CC0 1.0

ExposureEnabled == {1,2,3,4,11}

Exact module download · Source bundle and reproduction instructions

ExposureInit · operator

reference-profile · input revision 2 · CC0 1.0

ExposureInit == /\ caseNo \in 1..13 /\ pc = 0 /\ s = ExposureStart(caseNo)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: s, caseNo, pc, ExposureStart

ExposureLimit · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

ExposureNext · operator

reference-profile · input revision 2 · CC0 1.0

ExposureNext == ExposureProgress \/ (pc = ExposureLimit(caseNo) /\ UNCHANGED mcvars)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: mcvars, caseNo, pc, ExposureLimit, ExposureProgress

ExposureProgress · operator

reference-profile · input revision 2 · CC0 1.0

ExposureProgress ==
    /\ pc < ExposureLimit(caseNo)
    /\ IF caseNo \in ExposureEnabled 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, caseNo, pc, ExposureEnabled, ExposureLimit

ExposureSpec · operator

reference-profile · input revision 2 · CC0 1.0

ExposureSpec == ExposureInit /\ [][ExposureNext]_mcvars /\
                WF_pc(pc < ExposureLimit(caseNo) /\ pc' = pc + 1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: mcvars, caseNo, pc, ExposureInit, ExposureLimit, ExposureNext

ExposureStart · operator

reference-profile · input revision 2 · CC0 1.0

ExposureStart(n) == WithObjects([i \in {1} |->
    CASE n = 10 -> Token("Power","Play",0,"SideA",FALSE)
      [] n = 9 -> ExposureCard("barrierCard","SetAside",FALSE,"Down",FALSE)
      [] n = 13 -> ExposureCard("operation","Play",FALSE,"Up",FALSE)
      [] OTHER -> ExposureCard(
          CASE n \in {2,6} -> "objective" [] n = 3 -> "facility" [] n = 4 -> "upgrade"
            [] n \in {7,11} -> "technique" [] n = 8 -> "host" [] OTHER -> "barrierCard",
          "Play",TRUE,IF n \in {5,6,8} THEN "Up" ELSE "Down",n = 5)])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Token, WithObjects, ExposureCard