------------------------ MODULE RuntimeChecksMC ------------------------ EXTENDS ObjectRuntime VARIABLE caseNo, pc mcvars == <> Data == [c \in {"host", "technique", "objective", "objective2", "barrierCard"} |-> [owner |-> IF c \in {"host", "technique"} THEN "SideB" ELSE "SideA", side |-> IF c \in {"host", "technique"} THEN "SideB" ELSE "SideA", kind |-> CASE c = "host" -> "Support" [] c = "technique" -> "Technique" [] c = "barrierCard" -> "Barrier" [] OTHER -> "Objective", name |-> c, recurring |-> IF c = "host" THEN 2 ELSE 0]] NoCommands(state) == {} NoOverride(before, command, after) == FALSE NoCheckpointOverride(state, command) == FALSE Card(c, zone, deployed, face, host) == [card |-> c, form |-> "Card", kind |-> Data[c].kind, zone |-> zone, loc |-> IF host = 0 THEN "original" ELSE host, deployed |-> deployed, face |-> face, front |-> TRUE, activated |-> FALSE, host |-> host, placedBy |-> Data[c].owner, virtual |-> FALSE, objectivePoints |-> IF c \in {"objective", "objective2"} THEN 7 ELSE 0, marks |-> {"used"}] Empty == [obj |-> [i \in {} |-> i], past |-> [i \in {} |-> i], next |-> 1, pendingRetire |-> {}, reveals |-> {}, started |-> TRUE, turn |-> "SideB", actionPoints |-> [p \in Players |-> 4], spent |-> [p \in Players |-> 0], handLimit |-> [p \in Players |-> 5], checkpointDue |-> FALSE, outcome |-> "Playing", event |-> "Initial", used |-> {}, lastObjective |-> [mode |-> "none", before |-> 0, after |-> 0, progress |-> 0], instruction |-> [phase |-> "Choosing", announcements |-> <<>>, ability |-> "a", ifAble |-> FALSE]] DummyInitial == Empty WithObjects(objects) == [Empty EXCEPT !.obj = objects, !.next = IF DOMAIN objects = {} THEN 1 ELSE 1 + CHOOSE n \in DOMAIN objects : \A j \in DOMAIN objects : j <= n] HostObjects == [i \in 1..4 |-> IF i = 1 THEN Card("host", "Play", TRUE, "Up", 0) ELSE Token("ResourceUnit", "Play", 1, "SideB", FALSE)] HostStart == WithObjects(HostObjects) TreeStart == WithObjects([i \in 1..3 |-> CASE i = 1 -> Card("host", "Play", TRUE, "Up", 0) [] i = 2 -> Card("technique", "Play", TRUE, "Up", 1) [] OTHER -> Token("Power", "Play", 2, "SideB", FALSE)]) ObjectiveAreaTree == WithObjects([i \in 1..3 |-> CASE i = 1 -> Card("objective", "SideAObjectiveCompletion", FALSE, "Up", 0) [] i = 2 -> Token("SchemaAtom043", "SideAObjectiveCompletion", 1, "SideA", FALSE) [] OTHER -> Token("Power", "SideAObjectiveCompletion", 2, "SideA", FALSE)]) Start(n) == CASE n \in {1, 2, 3, 4, 5, 6, 8, 17, 18} -> HostStart [] n = 7 -> WithObjects([i \in {1} |-> Card("barrierCard", "SideADeck", FALSE, "NA", 0)]) [] n = 9 -> TreeStart [] n = 10 -> ObjectiveAreaTree [] n \in {11, 19} -> [WithObjects([i \in {1} |-> Card("objective", "Play", TRUE, "Down", 0)]) EXCEPT !.turn = "SideA"] [] n = 12 -> WithObjects([i \in {1,2} |-> IF i = 1 THEN Card("objective", "SideAObjectiveCompletion", FALSE, "Up", 0) ELSE Card("objective2", "SideBObjectiveCompletion", FALSE, "Up", 0)]) [] n \in {13, 14} -> WithObjects([i \in {1} |-> Card("technique", "SideBHand", FALSE, "NA", 0)]) [] n = 16 -> [Empty EXCEPT !.handLimit["SideB"] = -1] [] n = 20 -> [WithObjects([i \in {1} |-> Card("objective", "Play", TRUE, "Down", 0)]) EXCEPT !.turn = "SideA"] [] n = 21 -> WithObjects([i \in {1,2} |-> IF i = 1 THEN Card("host", "Play", TRUE, "Up", 0) ELSE Card("technique", "SideBHand", FALSE, "NA", 0)]) [] n = 22 -> WithObjects([i \in {1} |-> Token("ResourceUnit", "SideBResourceUnits", 0, "SideB", TRUE)]) [] n = 23 -> WithObjects([i \in {1,2} |-> IF i = 1 THEN Token("SchemaAtom043", "Play", 0, "SideB", FALSE) ELSE Token("Power", "Play", 1, "SideB", FALSE)]) [] n = 24 -> HostStart [] n = 25 -> WithObjects([i \in {1,2} |-> IF i = 1 THEN Card("host", "Play", TRUE, "Up", 0) ELSE Card("barrierCard", "Play", TRUE, "Up", 0)]) [] n = 26 -> WithObjects([i \in {1} |-> Card("host", "Play", TRUE, "Down", 0)]) [] OTHER -> Empty Limit(n) == CASE n \in {3, 4, 8, 9, 11, 15, 16, 17, 19, 20, 23, 24} -> 2 [] n = 5 -> 3 [] OTHER -> 1 Check == [op |-> "Checkpoint", readyForSection1Checks |-> TRUE, simultaneous |-> {}] MoveCmd(id, zone, loc, hidden) == [op |-> "Move", object |-> id, zone |-> zone, loc |-> loc, hidden |-> hidden, actor |-> "SideB"] FlipCmd(face) == [op |-> "Flip", object |-> 1, face |-> face] Fatal(reason, amount, required) == [op |-> "Fatal", reason |-> reason, amount |-> amount, required |-> required, simultaneous |-> {}, validProcedure |-> TRUE] ObjectiveCmd(mode) == [op |-> "Objective", object |-> 1, player |-> "SideA", mode |-> mode, objectivePlacementWindow |-> TRUE, progressRequirement |-> 0, accessing |-> FALSE, costsComplete |-> TRUE, allowed |-> TRUE] Cmd(n, step) == CASE n = 1 -> [op |-> "LoseResourceUnits", player |-> "SideB", amount |-> 2, selected |-> {}] [] n = 2 -> [op |-> "Refill", object |-> 1] [] n = 3 -> FlipCmd(IF step = 0 THEN "Down" ELSE "Up") [] n = 4 -> IF step = 0 THEN [op |-> "SpendResourceUnits", player |-> "SideB", selected |-> {}, amount |-> 0, permittedHosted |-> {}, announced |-> TRUE, permissionSources |-> [i \in {} |-> i], restrictionsHold |-> TRUE, mandatoryPrevents |-> FALSE] ELSE Check [] n = 5 -> IF step < 2 THEN [op |-> "ActionPoints", player |-> "SideB", amount |-> 1, mode |-> IF step = 0 THEN "Lose" ELSE "Spend", announced |-> TRUE] ELSE Check [] n = 6 -> MoveCmd(1, "Play", "new-known-position", FALSE) [] n = 7 -> MoveCmd(1, "SideADeck", "original", TRUE) [] n = 8 -> IF step = 0 THEN [op |-> "Reveal", object |-> 1, mode |-> "Reveal", viewers |-> Players, ability |-> "a"] ELSE MoveCmd(1, "Play", "new-known-position", FALSE) [] n = 9 -> IF step = 0 THEN MoveCmd(1, "SideBHand", "hand", FALSE) ELSE Check [] n = 10 -> MoveCmd(1, "SideBObjectiveCompletion", "score", FALSE) [] n = 11 -> IF step = 0 THEN ObjectiveCmd("ObjectiveCompletion") ELSE Check [] n = 12 -> Check [] n = 13 -> Fatal("Damage", 1, FALSE) [] n = 14 -> Fatal("Damage", 2, FALSE) [] n = 15 -> Fatal("RequiredDraw", 0, step = 1) [] n = 16 -> IF step = 0 THEN Fatal("Damage", 0, FALSE) ELSE Fatal("DiscardStep", 0, FALSE) [] n = 17 -> IF step = 0 THEN [op |-> "Announce", announcements |-> <<{ObjectTarget(1)}>>, available |-> <<{ObjectTarget(1)}>>, wanted |-> <<2>>, ability |-> "a", ifAble |-> FALSE] ELSE [op |-> "Reveal", object |-> 1, mode |-> "Look", viewers |-> {"SideB"}, ability |-> "interrupt"] [] n = 18 -> [op |-> "SpendResourceUnits", player |-> "SideB", selected |-> {2,3}, amount |-> 2, permittedHosted |-> {1}, announced |-> TRUE, permissionSources |-> [i \in {1} |-> i], restrictionsHold |-> TRUE, mandatoryPrevents |-> FALSE] [] n = 19 -> IF step = 0 THEN ObjectiveCmd("Add") ELSE Check [] n = 20 -> IF step = 0 THEN [op |-> "Mint", kind |-> "Progress", amount |-> 1, zone |-> "Play", host |-> 1, actor |-> "SideA", virtual |-> FALSE] ELSE [op |-> "AddProgress", object |-> 1, actor |-> "SideA", canAddProgress |-> TRUE] [] n = 21 -> [op |-> "Host", object |-> 2, host |-> 1, permission |-> TRUE, capacityOK |-> TRUE, requiredDestinationOK |-> TRUE, explicitRehost |-> FALSE, face |-> "Default", actor |-> "SideB"] [] n = 23 -> IF step = 0 THEN [op |-> "Retire", object |-> 1, allowed |-> TRUE] ELSE Check [] n = 24 -> IF step = 0 THEN [op |-> "Pay", player |-> "SideB", bundle |-> {}, candidate |-> s, evidence |-> [announced |-> TRUE, full |-> TRUE, restrictionBefore |-> TRUE, restrictionAfter |-> TRUE, mandatoryPrevents |-> FALSE, staticPrevents |-> FALSE, additionalAccepted |-> TRUE, controlExceptions |-> {}, procedureValid |-> TRUE]] ELSE Check [] n = 25 -> [op |-> "Host", object |-> 2, host |-> 1, permission |-> TRUE, capacityOK |-> TRUE, requiredDestinationOK |-> TRUE, explicitRehost |-> TRUE, face |-> "Default", actor |-> "SideB"] [] n = 26 -> [op |-> "Reveal", object |-> 1, mode |-> "Reveal", viewers |-> Players, ability |-> "a"] [] OTHER -> [op |-> "LoseResourceUnits", player |-> "SideB", amount |-> 1, selected |-> {}] InitMC == /\ caseNo \in 1..26 /\ pc = 0 /\ s = Start(caseNo) AdvanceMC == /\ pc < Limit(caseNo) /\ s.outcome = "Playing" /\ LET c == Cmd(caseNo, pc) IN /\ CheckpointOrderAllows(s, c) /\ Dispatch(c) /\ pc' = pc + 1 /\ UNCHANGED caseNo NextMC == AdvanceMC \/ (pc = Limit(caseNo) /\ UNCHANGED mcvars) SpecMC == InitMC /\ [][NextMC]_mcvars /\ WF_mcvars(AdvanceMC) Completed == <>(pc = Limit(caseNo)) RuntimeAssertions == /\ (caseNo = 1 /\ pc = 1 => ResourceUnits(s, "SideB") = 0 /\ HostedCount(s, 1, "ResourceUnit") = 3) /\ (caseNo = 2 /\ pc = 1 => HostedCount(s, 1, "ResourceUnit") = 3) /\ (caseNo = 3 /\ pc = 2 => HostedCount(s, 1, "ResourceUnit") = 5 /\ Live(s, 1) /\ DOMAIN s.past = {}) /\ (caseNo = 4 /\ pc = 1 => s.checkpointDue /\ s.event = "PayResourceUnits") /\ (caseNo = 4 /\ pc = 2 => ~s.checkpointDue /\ s.event = "Checkpoint") /\ (caseNo = 5 /\ pc = 1 => PriorityAllowed(s, "SideB", TRUE)) /\ (caseNo = 5 /\ pc >= 2 => ~PriorityAllowed(s, "SideB", TRUE)) /\ (caseNo = 5 /\ pc = 2 => s.checkpointDue) /\ (caseNo = 6 /\ pc = 1 => Live(s, 1) /\ s.obj[1].marks = {"used"}) /\ (caseNo = 7 /\ pc = 1 => ~Live(s, 1) /\ Live(s, 2) /\ s.obj[2].marks = {} /\ 1 \in DOMAIN s.past) /\ (caseNo = 8 /\ pc = 1 => s.obj[1].face = "Up" /\ s.reveals # {}) /\ (caseNo = 8 /\ pc = 2 => Live(s, 1) /\ s.reveals = {}) /\ (caseNo = 9 /\ pc = 1 => s.pendingRetire = {2,3} /\ Live(s, 2) /\ Live(s, 3)) /\ (caseNo = 9 /\ pc = 2 => s.pendingRetire = {} /\ ~Live(s, 2) /\ ~Live(s, 3) /\ Cardinality(CardsIn(s, "SideBDiscard")) = 1) /\ (caseNo = 10 /\ pc = 1 => DOMAIN s.obj = {4,5,6} /\ DOMAIN s.past = {1,2,3} /\ s.pendingRetire = {} /\ s.obj[5].host = 4 /\ s.obj[6].host = 5 /\ \A i \in DOMAIN s.obj : s.obj[i].zone = "SideBObjectiveCompletion" /\ s.obj[i].marks = {}) /\ (caseNo \in {11,19} /\ pc = 1 => Points(s, "SideA") = 7 /\ s.outcome = "Playing") /\ (caseNo = 11 /\ pc = 2 => s.outcome = "SideA" /\ s.lastObjective.mode = "ObjectiveCompletion") /\ (caseNo = 12 /\ pc = 1 => s.outcome = "Draw") /\ (caseNo = 13 /\ pc = 1 => s.outcome = "Playing") /\ (caseNo = 14 /\ pc = 1 => s.outcome = "SideA") /\ (caseNo = 15 /\ pc = 1 => s.outcome = "Playing") /\ (caseNo = 15 /\ pc = 2 => s.outcome = "SideB") /\ (caseNo = 16 /\ pc = 1 => s.outcome = "Playing") /\ (caseNo = 16 /\ pc = 2 => s.outcome = "SideA") /\ (caseNo = 17 /\ pc >= 1 => s.instruction.phase = "Imminent" /\ s.instruction.announcements = <<{ObjectTarget(1)}>>) /\ (caseNo = 18 /\ pc = 1 => s.used = {1} /\ s.checkpointDue /\ HostedCount(s, 1, "ResourceUnit") = 1) /\ (caseNo = 19 /\ pc = 2 => s.outcome = "SideA" /\ s.lastObjective.mode = "Add") /\ (caseNo = 20 /\ pc = 1 => s.event = "PlaceCounters" /\ ProgressAdded(s, 1)) /\ (caseNo = 20 /\ pc = 2 => s.event = "AddProgress" /\ HostedCount(s, 1, "Progress") = 2) /\ (caseNo = 21 /\ pc = 1 => ~Live(s, 2) /\ s.obj[3].host = 1 /\ ~s.obj[3].deployed /\ s.obj[3].face = "Up") /\ (caseNo = 22 /\ pc = 1 => ResourceUnits(s, "SideB") = 1 /\ ~SpendResourceUnitsOK(s, "SideB", {1}, 1, {})) /\ (caseNo = 23 /\ pc = 1 => ~Live(s, 1) /\ Live(s, 2) /\ s.pendingRetire = {2}) /\ (caseNo = 23 /\ pc = 2 => DOMAIN s.obj = {} /\ s.pendingRetire = {}) /\ (caseNo = 24 /\ pc = 1 => s.checkpointDue /\ s.event = "Pay") /\ (caseNo = 24 /\ pc = 2 => ~s.checkpointDue) /\ (caseNo = 25 /\ pc = 1 => s.obj[2].host = 1 /\ ~s.obj[2].deployed) /\ (caseNo = 26 /\ pc = 1 => s.obj[1].face = "Down" /\ Live(s, 1) /\ MayLook(s, "SideA", 1)) /\ LET evidence == [announced |-> TRUE, full |-> TRUE, restrictionBefore |-> TRUE, restrictionAfter |-> TRUE, mandatoryPrevents |-> FALSE, staticPrevents |-> FALSE, additionalAccepted |-> TRUE, controlExceptions |-> {}, procedureValid |-> TRUE] IN /\ PaymentValid(s, "SideB", {}, s, evidence) /\ ~PaymentValid(s, "SideB", {}, s, [evidence EXCEPT !.restrictionAfter = FALSE]) /\ ~PaymentValid(s, "SideB", {}, s, [evidence EXCEPT !.additionalAccepted = FALSE]) /\ ~PaymentValid(s, "SideB", {}, s, [evidence EXCEPT !.mandatoryPrevents = TRUE]) /\ ~PaymentValid(s, "SideB", {}, s, [evidence EXCEPT !.announced = FALSE]) PureRuntimeContracts == /\ ~RuleAllowed(TRUE, TRUE, TRUE, TRUE) /\ RuleAllowed(FALSE, TRUE, TRUE, FALSE) /\ InstructionParts(TRUE, {1,2}, {1}) = {} /\ InstructionParts(FALSE, {1,2}, {1}) = {1} /\ AnnouncementValid({ObjectTarget(1)}, {ObjectTarget(1)}, 2) /\ UsedRetireAbility(<<[kind |-> "RetireSelf"]>>) /\ ~UsedRetireAbility(<<[kind |-> "ResourceUnit"]>>) =============================================================================