HostingChecksMC

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 1 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.

HostingAssertions · operator

reference-profile · input revision 2 · CC0 1.0

HostingAssertions ==
    /\ (pc = 0 => (ENABLED Next) = (caseNo # 7))
    /\ (caseNo = 7 => s = HostingStart(caseNo))
    /\ (pc = 1 /\ caseNo # 7 =>
         LET id == IF caseNo = 5 THEN 3 ELSE 2 IN
         /\ s.obj[id].host = 1 /\ s.obj[id].zone = "Play"
         /\ s.obj[id].face = IF caseNo = 3 THEN "Down" ELSE "Up"
         /\ s.obj[id].deployed = (caseNo \in {1,3,4,8})
         /\ IF caseNo = 5 THEN ~Live(s,2) /\ Live(s,3) ELSE Live(s,2))
    /\ (caseNo = 1 /\ pc = 1 => Active(s,2))
    /\ (caseNo = 3 /\ pc = 1 => ~Active(s,2))

Exact module download · Source bundle and reproduction instructions

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

HostingCommand · operator

reference-profile · input revision 2 · CC0 1.0

HostingCommand(n) ==
    [op |-> "Host",object |-> 2,host |-> 1,permission |-> TRUE,
     capacityOK |-> TRUE,requiredDestinationOK |-> TRUE,
     explicitRehost |-> n # 7,
     face |-> CASE n = 3 -> "Down" [] n = 4 -> "Up" [] OTHER -> "Default",
     actor |-> IF n = 8 THEN "SideA" ELSE "SideB"]

Exact module download · Source bundle and reproduction instructions

HostingCommands · operator

reference-profile · input revision 2 · CC0 1.0

HostingCommands(t) == {HostingCommand(caseNo)}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HostingCommand, caseNo

HostingCompleted · operator

reference-profile · input revision 2 · CC0 1.0

HostingCompleted == <>(pc = 1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: pc

HostingInit · operator

reference-profile · input revision 2 · CC0 1.0

HostingInit == /\ caseNo \in 1..8 /\ pc = 0 /\ s = HostingStart(caseNo)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HostingStart, s, caseNo, pc

HostingNext · operator

reference-profile · input revision 2 · CC0 1.0

HostingNext == HostingProgress \/ (pc = 1 /\ UNCHANGED mcvars)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HostingProgress, mcvars, pc

HostingProgress · operator

reference-profile · input revision 2 · CC0 1.0

HostingProgress ==
    /\ 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

HostingSpec · operator

reference-profile · input revision 2 · CC0 1.0

HostingSpec == HostingInit /\ [][HostingNext]_mcvars /\ WF_mcvars(HostingProgress)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: HostingInit, HostingNext, HostingProgress, mcvars

HostingStart · operator

reference-profile · input revision 2 · CC0 1.0

HostingStart(n) == WithObjects([i \in {1,2} |->
    IF i = 1 THEN Card(IF n = 8 THEN "barrierCard" ELSE "host","Play",TRUE,"Up",0)
    ELSE IF n = 6 THEN Token("Power","Play",0,"SideB",FALSE)
    ELSE IF n = 5 THEN Card("technique","SideBHand",FALSE,"NA",0)
    ELSE Card(IF n \in {2,8} THEN "objective" ELSE "technique",
              "Play",TRUE,"Down",0)])

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Token, Card, WithObjects