CompletionOrderChecksMC

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.

CheckpointAssertions · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointAssertions ==
    /\ (pc = 0 => (ENABLED Next) = (caseNo \in InitiallyEnabled))
    /\ (caseNo \notin InitiallyEnabled => s = CheckpointStart(caseNo))
    /\ (caseNo = 1 /\ pc = 1 =>
         s.event = "CardOverride" /\ s.checkpointDue /\ ResourceUnits(s, "SideB") = 0)
    /\ (caseNo = 1 /\ pc = 2 => s.event = "Checkpoint" /\ ~s.checkpointDue)
    /\ (caseNo = 1 /\ pc = 3 => s.event = "GainResourceUnits" /\ ResourceUnits(s, "SideB") = 1)
    /\ (caseNo = 4 /\ pc = 1 => s.event = "Checkpoint" /\ ~s.checkpointDue)
    /\ (caseNo = 5 /\ pc = 1 => s.event = "PayResourceUnits" /\ s.checkpointDue)
    /\ (caseNo = 5 /\ pc = 2 => s.event = "Checkpoint" /\ ~s.checkpointDue)
    /\ (caseNo = 5 /\ pc = 3 => s.event = "GainResourceUnits" /\ ResourceUnits(s, "SideB") = 1)
    /\ (caseNo = 6 /\ pc = 1 => s.event = "CardOverride" /\ ~s.checkpointDue)
    /\ (caseNo = 12 /\ pc = 1 => s.event = "GainResourceUnits" /\ ResourceUnits(s, "SideB") = 1)
    /\ (caseNo = 15 /\ pc = 1 => s.event = "CardOverride" /\ ~s.checkpointDue)
    /\ (caseNo = 15 /\ pc = 2 => s.event = "GainResourceUnits" /\ ResourceUnits(s, "SideB") = 1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointStart, InitiallyEnabled, Next, ResourceUnits, s, caseNo, pc

CheckpointCompleted · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointCompleted == <>(pc = CheckpointLimit(caseNo))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointLimit, caseNo, pc

CheckpointInit · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointInit == /\ caseNo \in 1..16 /\ pc = 0 /\ s = CheckpointStart(caseNo)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointStart, s, caseNo, pc

CheckpointLimit · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointLimit(n) == IF n \in {1,5} THEN 3 ELSE IF n = 15 THEN 2 ELSE 1

Exact module download · Source bundle and reproduction instructions

CheckpointNext · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointNext ==
    CheckpointProgress \/
    (pc = CheckpointLimit(caseNo) /\ UNCHANGED mcvars)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointLimit, CheckpointProgress, mcvars, caseNo, pc

CheckpointProgress · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointProgress ==
    /\ pc < CheckpointLimit(caseNo)
    /\ IF caseNo \in InitiallyEnabled
       THEN /\ Next /\ pc' = pc + 1 /\ UNCHANGED caseNo
       ELSE /\ pc = 0 /\ ~ENABLED Next
            /\ pc' = 1 /\ UNCHANGED <<s, caseNo>>

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointLimit, InitiallyEnabled, Next, s, caseNo, pc

CheckpointSpec · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointSpec ==
    CheckpointInit /\ [][CheckpointNext]_mcvars /\ WF_mcvars(CheckpointProgress)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: CheckpointInit, CheckpointNext, CheckpointProgress, mcvars

CheckpointStart · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointStart(n) ==
    Put([Empty EXCEPT !.checkpointDue = n \notin {5,6,12,16},
                     !.outcome = IF n = 11 THEN "SideA" ELSE "Playing",
                     !.turn = IF n = 13 THEN "SideA" ELSE "SideB"],
        "testCase", n)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Put, Empty

CheckpointTestCommands · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointTestCommands(t) ==
    CASE t.event = "Initial" -> {InitialCheckpointCommand(t.testCase)}
      [] t.testCase = 1 /\ t.event = "CardOverride" -> {Check}
      [] t.testCase = 1 /\ t.event = "Checkpoint" -> {GainCommand}
      [] t.testCase = 5 /\ t.event = "PayResourceUnits" ->
           {GainCommand, OrdinaryOverride, Check}
      [] t.testCase = 5 /\ t.event = "Checkpoint" -> {GainCommand}
      [] t.testCase = 15 /\ t.event = "CardOverride" -> {GainCommand}
      [] OTHER -> {}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: GainCommand, InitialCheckpointCommand, OrdinaryOverride, Check

CheckpointTestOverride · operator

reference-profile · input revision 2 · CC0 1.0

CheckpointTestOverride(before, c, after) ==
    /\ c.body
    /\ after = [before EXCEPT !.event = "CardOverride",
                  !.checkpointDue = IF c.discharge THEN FALSE ELSE @]

Exact module download · Source bundle and reproduction instructions

GainCommand · operator

reference-profile · input revision 2 · CC0 1.0

GainCommand == [op |-> "GainResourceUnits", amount |-> 1, player |-> "SideB"]

Exact module download · Source bundle and reproduction instructions

InitialCheckpointCommand · operator

reference-profile · input revision 2 · CC0 1.0

InitialCheckpointCommand(n) ==
    CASE n = 1 -> ScopedOverride
      [] n = 2 -> OrdinaryOverride
      [] n = 3 -> GainCommand
      [] n = 4 -> Check
      [] n = 5 -> ZeroPayment
      [] n = 6 -> OrdinaryOverride
      [] n = 7 -> [ScopedOverride EXCEPT !.prohibited = TRUE]
      [] n = 8 -> [ScopedOverride EXCEPT !.authorized = FALSE]
      [] n = 9 -> [ScopedOverride EXCEPT !.directContradiction = FALSE]
      [] n = 10 ->
           [op |-> "GainResourceUnits", amount |-> 1, player |-> "SideB",
            rule |-> "CheckpointOrder", authorized |-> TRUE,
            directContradiction |-> TRUE, prohibited |-> FALSE]
      [] n = 11 -> ScopedOverride
      [] n = 12 -> GainCommand
      [] n = 13 -> ScopedOverride
      [] n = 14 -> [ScopedOverride EXCEPT !.body = FALSE]
      [] n = 15 -> [ScopedOverride EXCEPT !.discharge = TRUE]
      [] n = 16 -> [OrdinaryOverride EXCEPT !.prohibited = TRUE]
      [] OTHER -> OrdinaryOverride

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: GainCommand, OrdinaryOverride, ScopedOverride, ZeroPayment, Check

InitiallyEnabled · operator

reference-profile · input revision 2 · CC0 1.0

InitiallyEnabled == {1,4,5,6,12,15}

Exact module download · Source bundle and reproduction instructions

OrdinaryOverride · operator

reference-profile · input revision 2 · CC0 1.0

OrdinaryOverride ==
    OverrideCommand("OtherRule", TRUE, TRUE, FALSE, TRUE, FALSE)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OverrideCommand

OverrideCommand · operator

reference-profile · input revision 2 · CC0 1.0

OverrideCommand(rule, authorized, contradiction, prohibited, body, discharge) ==
    [op |-> "CardOverride", rule |-> rule, authorized |-> authorized,
     directContradiction |-> contradiction, prohibited |-> prohibited,
     body |-> body, discharge |-> discharge]

Exact module download · Source bundle and reproduction instructions

ScopedOverride · operator

reference-profile · input revision 2 · CC0 1.0

ScopedOverride ==
    OverrideCommand("CheckpointOrder", TRUE, TRUE, FALSE, TRUE, FALSE)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: OverrideCommand

SpecificCheckpointPermission · operator

reference-profile · input revision 2 · CC0 1.0

SpecificCheckpointPermission(t, c) ==
    t.checkpointDue /\ t.turn = "SideB" /\ c.rule = "CheckpointOrder"

Exact module download · Source bundle and reproduction instructions

ZeroPayment · operator

reference-profile · input revision 2 · CC0 1.0

ZeroPayment ==
    [op |-> "SpendResourceUnits", player |-> "SideB", selected |-> {}, amount |-> 0,
     permittedHosted |-> {}, permissionSources |-> [i \in {} |-> i],
     announced |-> TRUE, restrictionsHold |-> TRUE, mandatoryPrevents |-> FALSE]

Exact module download · Source bundle and reproduction instructions