------------------------ MODULE HostingChecksMC ------------------------
EXTENDS RuntimeChecksMC

                                                                          
                                                                         
HostingStart(n) == WithObjects([i \in {1,2} |->
    IF i = 1 THEN Card(IF n = 8 THEN "barrierCard" ELSE "host","Play",TRUE,"Up",0)
    ELSE IF n = 6 THEN Token("Power","Play",0,"SideB",FALSE)
    ELSE IF n = 5 THEN Card("technique","SideBHand",FALSE,"NA",0)
    ELSE Card(IF n \in {2,8} THEN "objective" ELSE "technique",
              "Play",TRUE,"Down",0)])
HostingCommand(n) ==
    [op |-> "Host",object |-> 2,host |-> 1,permission |-> TRUE,
     capacityOK |-> TRUE,requiredDestinationOK |-> TRUE,
     explicitRehost |-> n # 7,
     face |-> CASE n = 3 -> "Down" [] n = 4 -> "Up" [] OTHER -> "Default",
     actor |-> IF n = 8 THEN "SideA" ELSE "SideB"]
HostingCommands(t) == {HostingCommand(caseNo)}
HostingInit == /\ caseNo \in 1..8 /\ pc = 0 /\ s = HostingStart(caseNo)
HostingProgress ==
    /\ pc = 0
    /\ IF caseNo # 7 THEN /\ Next /\ pc' = 1 /\ UNCHANGED caseNo
       ELSE /\ ~ENABLED Next /\ pc' = 1 /\ UNCHANGED <<s,caseNo>>
HostingNext == HostingProgress \/ (pc = 1 /\ UNCHANGED mcvars)
HostingSpec == HostingInit /\ [][HostingNext]_mcvars /\ WF_mcvars(HostingProgress)
HostingCompleted == <>(pc = 1)
HostingAssertions ==
    /\ (pc = 0 => (ENABLED Next) = (caseNo # 7))
    /\ (caseNo = 7 => s = HostingStart(caseNo))
    /\ (pc = 1 /\ caseNo # 7 =>
         LET id == IF caseNo = 5 THEN 3 ELSE 2 IN
         /\ s.obj[id].host = 1 /\ s.obj[id].zone = "Play"
         /\ s.obj[id].face = IF caseNo = 3 THEN "Down" ELSE "Up"
         /\ s.obj[id].deployed = (caseNo \in {1,3,4,8})
         /\ IF caseNo = 5 THEN ~Live(s,2) /\ Live(s,3) ELSE Live(s,2))
    /\ (caseNo = 1 /\ pc = 1 => Active(s,2))
    /\ (caseNo = 3 /\ pc = 1 => ~Active(s,2))
=============================================================================