RuntimeChecksMC¶
Complete selected asymmetric reference profile. Definitions and supplied fixtures are distinct from the three teaching specializations; review and qualification are stated in the bound evidence and release.
Package reference-profile, input revision 2. Exact prepared source; CC0 1.0.
This is a definition inventory. Start with the learning chapters for the contract and its assumptions.
This model/fact module also contains 2 local fixture helpers outside the selected contract inventory. Their complete executable text remains in the exact module download and owning definition bodies. Listed dependencies include paths through those helpers. All selected contracts and frozen nested helpers retain their own entries.
AdvanceMC · operator
reference-profile · input revision 2 · CC0 1.0
AdvanceMC ==
/\ pc < Limit(caseNo) /\ s.outcome = "Playing"
/\ LET c == Cmd(caseNo, pc)
IN /\ CheckpointOrderAllows(s, c)
/\ Dispatch(c)
/\ pc' = pc + 1 /\ UNCHANGED caseNoExact module download · Source bundle and reproduction instructions
Resolved project definitions: CheckpointOrderAllows, Dispatch, s, Cmd, Limit, caseNo, pc
Card · operator
reference-profile · input revision 2 · CC0 1.0
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"}]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: Data
Check · operator
reference-profile · input revision 2 · CC0 1.0
Check == [op |-> "Checkpoint", readyForSection1Checks |-> TRUE,
simultaneous |-> {}]Exact module download · Source bundle and reproduction instructions
Cmd · operator
reference-profile · input revision 2 · CC0 1.0
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 |-> {}]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: ObjectTarget, Players, s, Check, Fatal, FlipCmd, MoveCmd, ObjectiveCmd
Completed · operator
reference-profile · input revision 2 · CC0 1.0
Completed == <>(pc = Limit(caseNo))Exact module download · Source bundle and reproduction instructions
Data · operator
reference-profile · input revision 2 · CC0 1.0
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]]Exact module download · Source bundle and reproduction instructions
DummyInitial · operator
reference-profile · input revision 2 · CC0 1.0
DummyInitial == EmptyExact module download · Source bundle and reproduction instructions
Resolved project definitions: Empty
Empty · operator
reference-profile · input revision 2 · CC0 1.0
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]]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: Players
Fatal · operator
reference-profile · input revision 2 · CC0 1.0
Fatal(reason, amount, required) ==
[op |-> "Fatal", reason |-> reason, amount |-> amount, required |-> required,
simultaneous |-> {}, validProcedure |-> TRUE]Exact module download · Source bundle and reproduction instructions
FlipCmd · operator
reference-profile · input revision 2 · CC0 1.0
FlipCmd(face) == [op |-> "Flip", object |-> 1, face |-> face]Exact module download · Source bundle and reproduction instructions
HostObjects · operator
reference-profile · input revision 2 · CC0 1.0
HostObjects ==
[i \in 1..4 |->
IF i = 1 THEN Card("host", "Play", TRUE, "Up", 0)
ELSE Token("ResourceUnit", "Play", 1, "SideB", FALSE)]Exact module download · Source bundle and reproduction instructions
HostStart · operator
reference-profile · input revision 2 · CC0 1.0
HostStart == WithObjects(HostObjects)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: HostObjects, WithObjects
InitMC · operator
reference-profile · input revision 2 · CC0 1.0
InitMC == /\ caseNo \in 1..26 /\ pc = 0 /\ s = Start(caseNo)Exact module download · Source bundle and reproduction instructions
Limit · operator
reference-profile · input revision 2 · CC0 1.0
Limit(n) ==
CASE n \in {3, 4, 8, 9, 11, 15, 16, 17, 19, 20, 23, 24} -> 2
[] n = 5 -> 3
[] OTHER -> 1Exact module download · Source bundle and reproduction instructions
MoveCmd · operator
reference-profile · input revision 2 · CC0 1.0
MoveCmd(id, zone, loc, hidden) ==
[op |-> "Move", object |-> id, zone |-> zone, loc |-> loc, hidden |-> hidden,
actor |-> "SideB"]Exact module download · Source bundle and reproduction instructions
NextMC · operator
reference-profile · input revision 2 · CC0 1.0
NextMC == AdvanceMC \/ (pc = Limit(caseNo) /\ UNCHANGED mcvars)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: AdvanceMC, Limit, mcvars, caseNo, pc
NoCheckpointOverride · operator
reference-profile · input revision 2 · CC0 1.0
NoCheckpointOverride(state, command) == FALSEExact module download · Source bundle and reproduction instructions
NoCommands · operator
reference-profile · input revision 2 · CC0 1.0
NoCommands(state) == {}Exact module download · Source bundle and reproduction instructions
NoOverride · operator
reference-profile · input revision 2 · CC0 1.0
NoOverride(before, command, after) == FALSEExact module download · Source bundle and reproduction instructions
ObjectiveAreaTree · operator
reference-profile · input revision 2 · CC0 1.0
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)])Exact module download · Source bundle and reproduction instructions
Resolved project definitions: Token, Card, WithObjects
ObjectiveCmd · operator
reference-profile · input revision 2 · CC0 1.0
ObjectiveCmd(mode) ==
[op |-> "Objective", object |-> 1,
player |-> "SideA", mode |-> mode, objectivePlacementWindow |-> TRUE,
progressRequirement |-> 0, accessing |-> FALSE,
costsComplete |-> TRUE, allowed |-> TRUE]Exact module download · Source bundle and reproduction instructions
PureRuntimeContracts · operator
reference-profile · input revision 2 · CC0 1.0
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"]>>)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: AnnouncementValid, InstructionParts, ObjectTarget, RuleAllowed, UsedRetireAbility
RuntimeAssertions · operator
reference-profile · input revision 2 · CC0 1.0
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])Exact module download · Source bundle and reproduction instructions
Resolved project definitions: CardsIn, HostedCount, Live, MayLook, ObjectTarget, PaymentValid, Points, PriorityAllowed, ProgressAdded, ResourceUnits, SpendResourceUnitsOK, s, caseNo, pc
SpecMC · operator
reference-profile · input revision 2 · CC0 1.0
SpecMC == InitMC /\ [][NextMC]_mcvars /\ WF_mcvars(AdvanceMC)Exact module download · Source bundle and reproduction instructions
Resolved project definitions: AdvanceMC, InitMC, NextMC, mcvars
Start · operator
reference-profile · input revision 2 · CC0 1.0
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 -> EmptyExact module download · Source bundle and reproduction instructions
Resolved project definitions: Token, Card, Empty, HostStart, ObjectiveAreaTree, TreeStart, WithObjects
TreeStart · operator
reference-profile · input revision 2 · CC0 1.0
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)])Exact module download · Source bundle and reproduction instructions
Resolved project definitions: Token, Card, WithObjects
WithObjects · operator
reference-profile · input revision 2 · CC0 1.0
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]Exact module download · Source bundle and reproduction instructions
Resolved project definitions: Empty
mcvars · operator
reference-profile · input revision 2 · CC0 1.0
mcvars == <<s, caseNo, pc>>Exact module download · Source bundle and reproduction instructions
caseNo · variable
reference-profile · input revision 2 · CC0 1.0
caseNoExact module download · Source bundle and reproduction instructions
pc · variable
reference-profile · input revision 2 · CC0 1.0
pcExact module download · Source bundle and reproduction instructions