----------------------- MODULE VisibilityChecksMC -----------------------
EXTENDS RuntimeChecksMC

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"]]
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]
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)])
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"]
ExposureCommands(t) == {ExposureCommand(caseNo,pc)}
ExposureEnabled == {1,2,3,4,11}
ExposureLimit(n) == IF n = 1 THEN 2 ELSE 1
ExposureInit == /\ caseNo \in 1..13 /\ pc = 0 /\ s = ExposureStart(caseNo)
ExposureProgress ==
    /\ pc < ExposureLimit(caseNo)
    /\ IF caseNo \in ExposureEnabled THEN /\ Next /\ pc' = pc + 1 /\ UNCHANGED caseNo
       ELSE /\ ~ENABLED Next /\ pc' = 1 /\ UNCHANGED <<s,caseNo>>
ExposureNext == ExposureProgress \/ (pc = ExposureLimit(caseNo) /\ UNCHANGED mcvars)
ExposureSpec == ExposureInit /\ [][ExposureNext]_mcvars /\
                WF_pc(pc < ExposureLimit(caseNo) /\ pc' = pc + 1)
ExposureCompleted == <>(pc = ExposureLimit(caseNo))
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")
=============================================================================