------------------------ MODULE TargetChecksMC ------------------------
EXTENDS RuntimeChecksMC

TargetObjects == [i \in 1..12 |->
    CASE i = 1 -> Token("ResourceUnit","SideBResourceUnits",0,"SideB",FALSE)
      [] i = 2 -> Token("ExposureMarker","SideBExposureMarkers",0,"SideB",FALSE)
      [] i = 3 -> Token("LiabilityMarker","SideALiabilityMarker",0,"SideA",FALSE)
      [] i = 4 -> Token("PersistentCapacityLoss","SideBPersistentCapacityLoss",0,"SideB",FALSE)
      [] i = 5 -> Token("Power","Play",8,"SideB",FALSE)
      [] i = 6 -> Token("Power","SideAObjectiveCompletion",9,"SideA",FALSE)
      [] i = 7 -> Token("ResourceUnit","Outside",0,"SideB",FALSE)
      [] i = 8 -> Card("technique","Play",TRUE,"Up",0)
      [] i = 9 -> [Card("objective","SideAObjectiveCompletion",FALSE,"Up",0) EXCEPT !.objectivePoints = 0]
      [] i = 10 -> Card("host","Play",FALSE,"Up",0)
      [] i = 11 -> Token("Power","Play",0,"SideB",FALSE)
      [] OTHER -> Token("ResourceUnit","SideAResourceUnits",0,"SideA",FALSE)]
InstructionBase == WithObjects([i \in {1} |-> Card("technique","Play",TRUE,"Up",0)])
TargetStart(n) ==
    IF n = 1 THEN WithObjects(TargetObjects)
    ELSE IF n = 2 THEN InstructionBase
    ELSE [InstructionBase EXCEPT
            !.instruction = [phase |-> CASE n = 3 -> "Choosing"
                                      [] n = 4 -> "Imminent" [] OTHER -> "Finished",
                announcements |-> <<{ObjectTarget(1)}>>,ability |-> "old",ifAble |-> TRUE],
            !.checkpointDue = n = 5,
            !.reveals = {[object |-> 1,loc |-> "original",viewers |-> {"SideB"},ability |-> "old"]}]
BeginCommand == [op |-> "BeginInstruction",ability |-> "a"]
AnnounceCommand(first) ==
    [op |-> "Announce",announcements |-> <<{ObjectTarget(1)}>>,
     available |-> <<{ObjectTarget(1)}>>,wanted |-> <<1>>,ability |-> "a",ifAble |-> first]
ResolveCommand(t) ==
    [op |-> "Resolve",requested |-> {"place"},feasible |-> {"place"},applied |-> {"place"},
     revalidated |-> TRUE,effectContract |-> TRUE,
     candidate |-> Mint(t,"ResourceUnit",1,"Play",1,"SideB",FALSE)]
TargetCommands(t) ==
    IF caseNo = 1 THEN {}
    ELSE IF caseNo # 2 THEN {BeginCommand}
    ELSE CASE pc = 0 -> {AnnounceCommand(TRUE)}
           [] pc \in {1,5} -> {ResolveCommand(t)}
           [] pc = 2 -> {BeginCommand,Check}
           [] pc = 3 -> {BeginCommand}
           [] pc = 4 -> {AnnounceCommand(FALSE)}
           [] OTHER -> {Check}
TargetLimit(n) == IF n = 2 THEN 7 ELSE 1
TargetInit == /\ caseNo \in 1..6 /\ pc = 0 /\ s = TargetStart(caseNo)
TargetProgress ==
    /\ pc < TargetLimit(caseNo)
    /\ IF caseNo \in {2,6} THEN /\ Next /\ pc' = pc + 1 /\ UNCHANGED caseNo
       ELSE /\ ~ENABLED Next /\ pc' = 1 /\ UNCHANGED <<s,caseNo>>
TargetNext == TargetProgress \/ (pc = TargetLimit(caseNo) /\ UNCHANGED mcvars)
TargetSpec == TargetInit /\ [][TargetNext]_mcvars /\
              WF_pc(pc < TargetLimit(caseNo) /\ pc' = pc + 1)
TargetCompleted == <>(pc = TargetLimit(caseNo))
TargetZoneAssertions ==
    caseNo = 1 =>
      /\ \A id \in {1,2,3,4,5,8,11,12} :
          DefaultTarget(s,ObjectTarget(id),"none",{ObjectTarget(id)})
      /\ \A id \in {6,7,9,10} :
          ~DefaultTarget(s,ObjectTarget(id),"none",{ObjectTarget(id)})
      /\ DefaultTarget(s,ObjectTarget(1),"SideBResourceUnits",{ObjectTarget(1)})
      /\ ~DefaultTarget(s,ObjectTarget(1),"SideAResourceUnits",{ObjectTarget(1)})
      /\ ~DefaultTarget(s,ObjectTarget(1),"none",{})
TargetCycleAssertions ==
    /\ (caseNo = 2 /\ pc = 2 => s.instruction.phase = "Finished" /\ s.checkpointDue)
    /\ (caseNo = 2 /\ pc = 3 => s.event = "Checkpoint" /\
          ~s.checkpointDue /\ ENABLED Next)
    /\ (caseNo = 2 /\ pc = 4 => s.instruction.phase = "Choosing" /\
          s.instruction.announcements = <<>> /\ ~s.instruction.ifAble /\
          s.instruction.ability = "a")
    /\ (caseNo = 2 /\ pc = 5 => s.instruction.phase = "Imminent" /\
          s.instruction.announcements = <<{ObjectTarget(1)}>>)
    /\ (caseNo = 2 /\ pc = 7 => HostedCount(s,1,"ResourceUnit") = 2 /\
          s.instruction.phase = "Finished" /\ ~s.checkpointDue)
TargetAssertions ==
    /\ TargetZoneAssertions /\ TargetCycleAssertions
    /\ (pc = 0 => (ENABLED Next) = (caseNo \in {2,6}))
    /\ (caseNo \in {1,3,4,5} => s = TargetStart(caseNo))
    /\ (caseNo = 6 /\ pc = 1 => s.instruction.phase = "Choosing" /\
          s.instruction.announcements = <<>> /\ s.instruction.ability = "a" /\
          ~s.instruction.ifAble /\ s.reveals = TargetStart(6).reveals /\
          s.obj = InstructionBase.obj)
=============================================================================