ControlChecksMC

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.

ControlAssertions · operator

reference-profile · input revision 2 · CC0 1.0

ControlAssertions == PlacerAssertions /\ CostControlAssertions

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CostControlAssertions, PlacerAssertions

ControlCommand · operator

reference-profile · input revision 2 · CC0 1.0

ControlCommand(n) ==
    IF n = 4 THEN
      [op |-> "Move",object |-> 2,zone |-> "Play",loc |-> "placed",
       hidden |-> FALSE,actor |-> "SideB"]
    ELSE [op |-> "Host",object |-> 2,host |-> 1,permission |-> TRUE,
          capacityOK |-> TRUE,requiredDestinationOK |-> TRUE,
          explicitRehost |-> TRUE,face |-> "Default",
          actor |-> IF n = 3 THEN "SideA" ELSE "SideB"]

Exact module download · Source bundle and reproduction instructions

ControlCommands · operator

reference-profile · input revision 2 · CC0 1.0

ControlCommands(t) == IF caseNo = 7 THEN {} ELSE {ControlCommand(caseNo)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ControlCommand, caseNo

ControlCompleted · operator

reference-profile · input revision 2 · CC0 1.0

ControlCompleted == <>(pc = 1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: pc

ControlInit · operator

reference-profile · input revision 2 · CC0 1.0

ControlInit == /\ caseNo \in 1..7 /\ pc = 0 /\ s = ControlStart(caseNo)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ControlStart, s, caseNo, pc

ControlNext · operator

reference-profile · input revision 2 · CC0 1.0

ControlNext == ControlProgress \/ (pc = 1 /\ UNCHANGED mcvars)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ControlProgress, mcvars, pc

ControlProgress · operator

reference-profile · input revision 2 · CC0 1.0

ControlProgress ==
    /\ pc = 0
    /\ IF caseNo # 7 THEN /\ Next /\ pc' = 1 /\ UNCHANGED caseNo
       ELSE /\ ~ENABLED Next /\ pc' = 1 /\ UNCHANGED <<s,caseNo>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Next, s, caseNo, pc

ControlSpec · operator

reference-profile · input revision 2 · CC0 1.0

ControlSpec == ControlInit /\ [][ControlNext]_mcvars /\ WF_pc(pc = 0 /\ pc' = 1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ControlInit, ControlNext, mcvars, pc

ControlStart · operator

reference-profile · input revision 2 · CC0 1.0

ControlStart(n) ==
    IF n = 7 THEN WithObjects(CostObjects)
    ELSE WithObjects([i \in {1,2} |->
      IF i = 1 THEN Card(IF n \in {2,3} THEN "barrierCard" ELSE "host","Play",TRUE,"Up",0)
      ELSE IF n = 3 THEN Card("technique","SideBHand",FALSE,"NA",0)
      ELSE IF n = 5 THEN Card("objective","Play",TRUE,"Down",0)
      ELSE IF n = 6 THEN Token("Power","Outside",0,"SideA",FALSE)
      ELSE Card("objective","SideAHand",FALSE,"NA",0)])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CostObjects, Token, Card, WithObjects

CostControlAssertions · operator

reference-profile · input revision 2 · CC0 1.0

CostControlAssertions ==
    caseNo = 7 =>
      /\ ~CanPayWith(s,"SideB",2,FALSE)
      /\ ~CanPayWith(s,"SideB",4,FALSE)
      /\ ~CanPayWith(s,"SideB",7,FALSE)
      /\ ~SetupMayUseForCost("SideB",s.obj[2],"SideA",FALSE)
      /\ ~SetupMayUseForCost("SideB",s.obj[4],"SideA",FALSE)
      /\ ~SetupMayUseForCost("SideB",s.obj[7],"SideA",FALSE)
      /\ CanPayWith(s,"SideA",2,FALSE) /\ CanPayWith(s,"SideA",4,FALSE)
      /\ CanPayWith(s,"SideB",3,FALSE) /\ CanPayWith(s,"SideA",5,FALSE)
      /\ SetupMayUseForCost("SideB",s.obj[3],"SideA",FALSE)
      /\ SetupMayUseForCost("SideA",s.obj[5],"SideB",FALSE)
      /\ CanPayWith(s,"SideB",2,TRUE) /\ CanPayWith(s,"SideB",4,TRUE)
      /\ SetupMayUseForCost("SideB",s.obj[2],"SideA",TRUE)
      /\ ~CanPayWith(s,"SideA",6,FALSE) /\ ~CanPayWith(s,"SideB",6,TRUE)
      /\ PlayerCounters(s,"SideA","LiabilityMarker") = 1
      /\ PlayerCounters(s,"SideB","ExposureMarker") = 1

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CanPayWith, PlayerCounters, s, caseNo, SetupMayUseForCost

CostObjects · operator

reference-profile · input revision 2 · CC0 1.0

CostObjects == [i \in 1..7 |->
    CASE i = 1 -> Card("barrierCard","Play",TRUE,"Up",0)
      [] i = 2 -> Token("LiabilityMarker","Play",1,"SideA",FALSE)
      [] i = 3 -> Token("LiabilityMarker","SideALiabilityMarker",0,"SideA",FALSE)
      [] i = 4 -> Token("ExposureMarker","Play",1,"SideA",FALSE)
      [] i = 5 -> Token("ExposureMarker","SideBExposureMarkers",0,"SideB",FALSE)
      [] i = 6 -> Token("LiabilityMarker","Play",1,"SideA",TRUE)
      [] OTHER -> Token("ResourceUnit","Play",1,"SideA",FALSE)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Token, Card

PlacerAssertions · operator

reference-profile · input revision 2 · CC0 1.0

PlacerAssertions ==
    /\ (pc = 0 => (ENABLED Next) = (caseNo # 7))
    /\ (caseNo \in {1,2,4} /\ pc = 1 =>
          Controller(s,3) = "SideB" /\ Owner(s,3) = "SideA" /\
          s.obj[3].placedBy = "SideB")
    /\ (caseNo = 3 /\ pc = 1 =>
          Controller(s,3) = "SideA" /\ Owner(s,3) = "SideB" /\
          s.obj[3].placedBy = "SideA")
    /\ (caseNo = 5 /\ pc = 1 =>
          Controller(s,2) = "SideA" /\ s.obj[2].placedBy = "SideA" /\ Owner(s,2) = "SideA")
    /\ (caseNo = 6 /\ pc = 1 =>
          Owner(s,3) = NoPlayer /\ Controller(s,3) = "SideB")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Controller, Next, NoPlayer, Owner, s, caseNo, pc