TargetChecksMC

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.

AnnounceCommand · operator

reference-profile · input revision 2 · CC0 1.0

AnnounceCommand(first) ==
    [op |-> "Announce",announcements |-> <<{ObjectTarget(1)}>>,
     available |-> <<{ObjectTarget(1)}>>,wanted |-> <<1>>,ability |-> "a",ifAble |-> first]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectTarget

BeginCommand · operator

reference-profile · input revision 2 · CC0 1.0

BeginCommand == [op |-> "BeginInstruction",ability |-> "a"]

Exact module download · Source bundle and reproduction instructions

InstructionBase · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Card, WithObjects

ResolveCommand · operator

reference-profile · input revision 2 · CC0 1.0

ResolveCommand(t) ==
    [op |-> "Resolve",requested |-> {"place"},feasible |-> {"place"},applied |-> {"place"},
     revalidated |-> TRUE,effectContract |-> TRUE,
     candidate |-> Mint(t,"ResourceUnit",1,"Play",1,"SideB",FALSE)]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Mint

TargetAssertions · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Next, s, caseNo, pc, InstructionBase, TargetCycleAssertions, TargetStart, TargetZoneAssertions

TargetCommands · operator

reference-profile · input revision 2 · CC0 1.0

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}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Check, caseNo, pc, AnnounceCommand, BeginCommand, ResolveCommand

TargetCompleted · operator

reference-profile · input revision 2 · CC0 1.0

TargetCompleted == <>(pc = TargetLimit(caseNo))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: caseNo, pc, TargetLimit

TargetCycleAssertions · operator

reference-profile · input revision 2 · CC0 1.0

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)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HostedCount, Next, ObjectTarget, s, caseNo, pc

TargetInit · operator

reference-profile · input revision 2 · CC0 1.0

TargetInit == /\ caseNo \in 1..6 /\ pc = 0 /\ s = TargetStart(caseNo)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: s, caseNo, pc, TargetStart

TargetLimit · operator

reference-profile · input revision 2 · CC0 1.0

TargetLimit(n) == IF n = 2 THEN 7 ELSE 1

Exact module download · Source bundle and reproduction instructions

TargetNext · operator

reference-profile · input revision 2 · CC0 1.0

TargetNext == TargetProgress \/ (pc = TargetLimit(caseNo) /\ UNCHANGED mcvars)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: mcvars, caseNo, pc, TargetLimit, TargetProgress

TargetObjects · operator

reference-profile · input revision 2 · CC0 1.0

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Token, Card

TargetProgress · operator

reference-profile · input revision 2 · CC0 1.0

TargetProgress ==
    /\ pc < TargetLimit(caseNo)
    /\ IF caseNo \in {2,6} 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, TargetLimit

TargetSpec · operator

reference-profile · input revision 2 · CC0 1.0

TargetSpec == TargetInit /\ [][TargetNext]_mcvars /\
              WF_pc(pc < TargetLimit(caseNo) /\ pc' = pc + 1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: mcvars, caseNo, pc, TargetInit, TargetLimit, TargetNext

TargetStart · operator

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

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ObjectTarget, WithObjects, InstructionBase, TargetObjects

TargetZoneAssertions · operator

reference-profile · input revision 2 · CC0 1.0

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",{})

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: DefaultTarget, ObjectTarget, s, caseNo