------------------------ MODULE ControlChecksMC ------------------------
EXTENDS RuntimeChecksMC

CostObjects == [i \in 1..7 |->
    CASE i = 1 -> Card("barrierCard","Play",TRUE,"Up",0)
      [] i = 2 -> Token("LiabilityMarker","Play",1,"SideA",FALSE)
      [] i = 3 -> Token("LiabilityMarker","SideALiabilityMarker",0,"SideA",FALSE)
      [] i = 4 -> Token("ExposureMarker","Play",1,"SideA",FALSE)
      [] i = 5 -> Token("ExposureMarker","SideBExposureMarkers",0,"SideB",FALSE)
      [] i = 6 -> Token("LiabilityMarker","Play",1,"SideA",TRUE)
      [] OTHER -> Token("ResourceUnit","Play",1,"SideA",FALSE)]
ControlStart(n) ==
    IF n = 7 THEN WithObjects(CostObjects)
    ELSE WithObjects([i \in {1,2} |->
      IF i = 1 THEN Card(IF n \in {2,3} THEN "barrierCard" ELSE "host","Play",TRUE,"Up",0)
      ELSE IF n = 3 THEN Card("technique","SideBHand",FALSE,"NA",0)
      ELSE IF n = 5 THEN Card("objective","Play",TRUE,"Down",0)
      ELSE IF n = 6 THEN Token("Power","Outside",0,"SideA",FALSE)
      ELSE Card("objective","SideAHand",FALSE,"NA",0)])
ControlCommand(n) ==
    IF n = 4 THEN
      [op |-> "Move",object |-> 2,zone |-> "Play",loc |-> "placed",
       hidden |-> FALSE,actor |-> "SideB"]
    ELSE [op |-> "Host",object |-> 2,host |-> 1,permission |-> TRUE,
          capacityOK |-> TRUE,requiredDestinationOK |-> TRUE,
          explicitRehost |-> TRUE,face |-> "Default",
          actor |-> IF n = 3 THEN "SideA" ELSE "SideB"]
ControlCommands(t) == IF caseNo = 7 THEN {} ELSE {ControlCommand(caseNo)}
ControlInit == /\ caseNo \in 1..7 /\ pc = 0 /\ s = ControlStart(caseNo)
ControlProgress ==
    /\ pc = 0
    /\ IF caseNo # 7 THEN /\ Next /\ pc' = 1 /\ UNCHANGED caseNo
       ELSE /\ ~ENABLED Next /\ pc' = 1 /\ UNCHANGED <<s,caseNo>>
ControlNext == ControlProgress \/ (pc = 1 /\ UNCHANGED mcvars)
                                                                        
                                                                           
                                                                              
ControlSpec == ControlInit /\ [][ControlNext]_mcvars /\ WF_pc(pc = 0 /\ pc' = 1)
ControlCompleted == <>(pc = 1)
PlacerAssertions ==
    /\ (pc = 0 => (ENABLED Next) = (caseNo # 7))
    /\ (caseNo \in {1,2,4} /\ pc = 1 =>
          Controller(s,3) = "SideB" /\ Owner(s,3) = "SideA" /\
          s.obj[3].placedBy = "SideB")
    /\ (caseNo = 3 /\ pc = 1 =>
          Controller(s,3) = "SideA" /\ Owner(s,3) = "SideB" /\
          s.obj[3].placedBy = "SideA")
    /\ (caseNo = 5 /\ pc = 1 =>
          Controller(s,2) = "SideA" /\ s.obj[2].placedBy = "SideA" /\ Owner(s,2) = "SideA")
    /\ (caseNo = 6 /\ pc = 1 =>
          Owner(s,3) = NoPlayer /\ Controller(s,3) = "SideB")
CostControlAssertions ==
    caseNo = 7 =>
      /\ ~CanPayWith(s,"SideB",2,FALSE)
      /\ ~CanPayWith(s,"SideB",4,FALSE)
      /\ ~CanPayWith(s,"SideB",7,FALSE)
      /\ ~SetupMayUseForCost("SideB",s.obj[2],"SideA",FALSE)
      /\ ~SetupMayUseForCost("SideB",s.obj[4],"SideA",FALSE)
      /\ ~SetupMayUseForCost("SideB",s.obj[7],"SideA",FALSE)
      /\ CanPayWith(s,"SideA",2,FALSE) /\ CanPayWith(s,"SideA",4,FALSE)
      /\ CanPayWith(s,"SideB",3,FALSE) /\ CanPayWith(s,"SideA",5,FALSE)
      /\ SetupMayUseForCost("SideB",s.obj[3],"SideA",FALSE)
      /\ SetupMayUseForCost("SideA",s.obj[5],"SideB",FALSE)
      /\ CanPayWith(s,"SideB",2,TRUE) /\ CanPayWith(s,"SideB",4,TRUE)
      /\ SetupMayUseForCost("SideB",s.obj[2],"SideA",TRUE)
      /\ ~CanPayWith(s,"SideA",6,FALSE) /\ ~CanPayWith(s,"SideB",6,TRUE)
      /\ PlayerCounters(s,"SideA","LiabilityMarker") = 1
      /\ PlayerCounters(s,"SideB","ExposureMarker") = 1
ControlAssertions == PlacerAssertions /\ CostControlAssertions
=============================================================================