UnitChecksMC

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.

ConditionHost · operator

reference-profile · input revision 2 · CC0 1.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)])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Token, Card, WithObjects

CounterActivityAssertions · operator

reference-profile · input revision 2 · CC0 1.0

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))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Active, Live, s, caseNo, pc

CounterAssertions · operator

reference-profile · input revision 2 · CC0 1.0

CounterAssertions ==
    /\ (pc = 0 => (ENABLED Next) = (caseNo \in CounterEnabled))
    /\ (caseNo \notin CounterEnabled => s = CounterStart(caseNo))
    /\ CounterPlacementAssertions /\ CounterActivityAssertions

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Next, s, caseNo, pc, CounterActivityAssertions, CounterEnabled, CounterPlacementAssertions, CounterStart

CounterCommand · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Check, FlipCmd, MoveCmd

CounterCommands · operator

reference-profile · input revision 2 · CC0 1.0

CounterCommands(t) ==
    IF caseNo \in {7,8,11} THEN {} ELSE {CounterCommand(caseNo,pc)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: caseNo, pc, CounterCommand

CounterCompleted · operator

reference-profile · input revision 2 · CC0 1.0

CounterCompleted == <>(pc = CounterLimit(caseNo))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: caseNo, pc, CounterLimit

CounterEnabled · operator

reference-profile · input revision 2 · CC0 1.0

CounterEnabled == {1,2,3,5,6,12}

Exact module download · Source bundle and reproduction instructions

CounterHost · operator

reference-profile · input revision 2 · CC0 1.0

CounterHost == WithObjects([i \in {1} |-> Card("technique","Play",TRUE,"Up",0)])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Card, WithObjects

CounterInit · operator

reference-profile · input revision 2 · CC0 1.0

CounterInit == /\ caseNo \in 1..12 /\ pc = 0 /\ s = CounterStart(caseNo)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: s, caseNo, pc, CounterStart

CounterLimit · operator

reference-profile · input revision 2 · CC0 1.0

CounterLimit(n) == IF n \in {5,6} THEN 2 ELSE 1

Exact module download · Source bundle and reproduction instructions

CounterNext · operator

reference-profile · input revision 2 · CC0 1.0

CounterNext == CounterProgress \/ (pc = CounterLimit(caseNo) /\ UNCHANGED mcvars)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: mcvars, caseNo, pc, CounterLimit, CounterProgress

CounterPlacementAssertions · operator

reference-profile · input revision 2 · CC0 1.0

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))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CanPayWith, CountsAsCounterPlacement, HostedCount, s, caseNo, pc, CounterHost, CounterStart

CounterProgress · operator

reference-profile · input revision 2 · CC0 1.0

CounterProgress ==
    /\ pc < CounterLimit(caseNo)
    /\ IF caseNo \in CounterEnabled
       THEN /\ Next /\ pc' = 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, CounterEnabled, CounterLimit

CounterSpec · operator

reference-profile · input revision 2 · CC0 1.0

CounterSpec == CounterInit /\ [][CounterNext]_mcvars /\ WF_mcvars(CounterProgress)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: mcvars, CounterInit, CounterNext, CounterProgress

CounterStart · operator

reference-profile · input revision 2 · CC0 1.0

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)])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Token, Card, WithObjects, ConditionHost, CounterHost