------------------------ MODULE UnitChecksMC ------------------------
EXTENDS RuntimeChecksMC

                                                                        
                                                                          
                                                                            
CounterHost == WithObjects([i \in {1} |-> Card("technique","Play",TRUE,"Up",0)])
ConditionHost == WithObjects([i \in 1..3 |->
    CASE i = 1 -> Card("technique","Play",TRUE,"Up",0)
      [] i = 2 -> Token("SchemaAtom043","Play",1,"SideB",FALSE)
      [] OTHER -> Token("SchemaAtom043","Play",2,"SideB",FALSE)])
CounterStart(n) ==
    CASE n \in {1,2} -> CounterHost
      [] n = 3 -> WithObjects([i \in 1..3 |->
          IF i = 3 THEN Token("Power","Play",1,"SideB",FALSE)
          ELSE Card(IF i = 1 THEN "technique" ELSE "host","Play",TRUE,"Up",0)])
      [] n \in {4,9,10,11} -> WithObjects([i \in {1,2} |->
          IF i = 1 THEN Card("technique","Play",TRUE,"Up",0)
          ELSE Token("SchemaAtom180","Play",1,"SideB",TRUE)])
      [] n \in {5,6,12} -> ConditionHost
      [] n = 7 -> WithObjects([i \in {1} |-> Token("SchemaAtom043","Play",0,"SideB",FALSE)])
      [] OTHER -> WithObjects([i \in {1,2} |->
          IF i = 1 THEN Card("technique","Play",TRUE,"Up",0)
          ELSE Token("Power","Play",1,"SideB",FALSE)])
CounterCommand(n, step) ==
    CASE n \in {1,2} ->
          [op |-> "Mint",kind |-> "SchemaAtom180",amount |-> 1,zone |-> "Play",
           host |-> 1,actor |-> "SideB",virtual |-> n = 1]
      [] n \in {3,4} ->
          [op |-> "Host",object |-> IF n = 3 THEN 3 ELSE 2,
           host |-> IF n = 3 THEN 2 ELSE 1,permission |-> TRUE,
           capacityOK |-> TRUE,requiredDestinationOK |-> TRUE,
           explicitRehost |-> TRUE,face |-> "Default",actor |-> "SideB"]
      [] n \in {5,6} -> IF step = 0 THEN
          [op |-> "Retire",object |-> IF n = 5 THEN 1 ELSE 2,allowed |-> TRUE]
          ELSE Check
      [] n = 9 -> MoveCmd(2,"Play","elsewhere",FALSE)
      [] n = 10 -> [op |-> "Retire",object |-> 2,allowed |-> TRUE]
      [] n = 12 -> FlipCmd("Down")
      [] OTHER -> Check
CounterCommands(t) ==
    IF caseNo \in {7,8,11} THEN {} ELSE {CounterCommand(caseNo,pc)}
CounterEnabled == {1,2,3,5,6,12}
CounterLimit(n) == IF n \in {5,6} THEN 2 ELSE 1
CounterInit == /\ caseNo \in 1..12 /\ pc = 0 /\ s = CounterStart(caseNo)
CounterProgress ==
    /\ pc < CounterLimit(caseNo)
    /\ IF caseNo \in CounterEnabled
       THEN /\ Next /\ pc' = pc + 1 /\ UNCHANGED caseNo
       ELSE /\ ~ENABLED Next /\ pc' = 1 /\ UNCHANGED <<s,caseNo>>
CounterNext == CounterProgress \/ (pc = CounterLimit(caseNo) /\ UNCHANGED mcvars)
CounterSpec == CounterInit /\ [][CounterNext]_mcvars /\ WF_mcvars(CounterProgress)
CounterCompleted == <>(pc = CounterLimit(caseNo))
CounterPlacementAssertions ==
    /\ (caseNo = 1 /\ pc = 1 => HostedCount(s,1,"SchemaAtom180") = 1 /\
          ~CountsAsCounterPlacement(CounterHost,s,2,1) /\
          s.event = "ConsiderCounters")
    /\ (caseNo = 2 /\ pc = 1 => HostedCount(s,1,"SchemaAtom180") = 1 /\
          CountsAsCounterPlacement(CounterHost,s,2,1) /\ s.event = "PlaceCounters")
    /\ (caseNo = 3 /\ pc = 1 => s.obj[3].host = 2 /\
          CountsAsCounterPlacement(CounterStart(3),s,3,2))
    /\ (caseNo \in {4,9,10,11} => ~CanPayWith(s,"SideB",2,TRUE))
CounterActivityAssertions ==
    /\ (caseNo \in {5,6,12} /\ pc = 0 => Active(s,2) /\ Active(s,3))
    /\ (caseNo = 5 /\ pc = 1 => ~Live(s,1) /\ ~Active(s,2) /\
          s.pendingRetire = {2,3})
    /\ (caseNo = 6 /\ pc = 1 => ~Live(s,2) /\ ~Active(s,3) /\
          s.pendingRetire = {3})
    /\ (caseNo = 5 /\ pc = 2 => ~Live(s,2) /\ ~Live(s,3))
    /\ (caseNo = 6 /\ pc = 2 => ~Live(s,3))
    /\ (caseNo = 7 => ~Active(s,1))
    /\ (caseNo = 8 => ~Active(s,2))
    /\ (caseNo = 12 /\ pc = 1 => ~Active(s,1) /\ Active(s,2) /\ Active(s,3))
CounterAssertions ==
    /\ (pc = 0 => (ENABLED Next) = (caseNo \in CounterEnabled))
    /\ (caseNo \notin CounterEnabled => s = CounterStart(caseNo))
    /\ CounterPlacementAssertions /\ CounterActivityAssertions
=============================================================================