PriorityMC

Original finite optional-use priority window with explicit child suspension and supplied receipt provider; not a full scheduler.

Package priority, input revision 1. Exact prepared source; CC0 1.0.

This is a definition inventory. Start with the learning chapters for the contract and its assumptions.

Defect · constant

priority · input revision 1 · CC0 1.0

Defect

Exact module download · Source bundle and reproduction instructions

MaxCalls · constant

priority · input revision 1 · CC0 1.0

MaxCalls

Exact module download · Source bundle and reproduction instructions

MaxReceipts · constant

priority · input revision 1 · CC0 1.0

MaxReceipts

Exact module download · Source bundle and reproduction instructions

Act · operator

priority · input revision 1 · CC0 1.0

Act ==
    /\ state.phase = "Ready" /\ state.nextCall <= MaxCalls
    /\ state' = BeginOption(state)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MaxCalls, state, BeginOption

Checkpoint · operator

priority · input revision 1 · CC0 1.0

Checkpoint ==
    /\ state.phase = "NeedCheckpoint" /\ state.nextReceipt <= MaxReceipts
    /\ state' = ReceiveCheckpoint(state)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MaxReceipts, state, ReceiveCheckpoint

ChildComplete · operator

priority · input revision 1 · CC0 1.0

ChildComplete ==
    /\ state.phase = "Paused" /\ ~state.childComplete
    /\ state' = CompleteChild(state)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state, CompleteChild

ExactCallerReceipt · operator

priority · input revision 1 · CC0 1.0

ExactCallerReceipt ==
    /\ state.returnAudit.expectedWindow = state.returnAudit.actualWindow
    /\ state.returnAudit.expectedCall = state.returnAudit.actualCall
    /\ state.returnAudit.expectedChild = state.returnAudit.actualChild
    /\ state.returnAudit.expectedTransaction = state.returnAudit.actualTransaction
    /\ state.returnAudit.expectedReception = state.returnAudit.actualReception

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state

FreshCalls · operator

priority · input revision 1 · CC0 1.0

FreshCalls == state.usedCalls = 1..(state.nextCall - 1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state

FreshReceipts · operator

priority · input revision 1 · CC0 1.0

FreshReceipts == state.usedReceipts = 1..(state.nextReceipt - 1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state

Init · operator

priority · input revision 1 · CC0 1.0

Init == state = InitialWindow

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state, InitialWindow

Next · operator

priority · input revision 1 · CC0 1.0

Next == Checkpoint \/ Pass \/ Act \/ Suspend \/ ChildComplete \/ Return

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Act, Checkpoint, ChildComplete, Pass, Return, Suspend

Pass · operator

priority · input revision 1 · CC0 1.0

Pass == /\ state.phase = "Ready" /\ state' = PassWindow(state)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state, PassWindow

ReadyPassMarker · operator

priority · input revision 1 · CC0 1.0

ReadyPassMarker ==
    state.phase \in {"NeedCheckpoint", "Ready"} =>
        state.previousPass = (state.consecutivePasses = 1)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state

Return · operator

priority · input revision 1 · CC0 1.0

Return ==
    /\ state.phase = "Paused" /\ state.childComplete /\ state.nextReceipt <= MaxReceipts
    /\ \E receipt \in ReturnCandidates(state) :
        /\ ReturnMatches(state, receipt) \/
             (Defect = "WrongCaller" /\ ReturnMatches(state, [receipt EXCEPT !.call = state.call]))
        /\ state' = CompleteOption(state, receipt,
               IF Defect = "AlternateHolder" THEN Other(state.busyActor) ELSE state.busyActor,
               Defect = "KeepPass")

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Defect, MaxReceipts, state, CompleteOption, Other, ReturnCandidates, ReturnMatches

ReturnStaysWithActor · operator

priority · input revision 1 · CC0 1.0

ReturnStaysWithActor == state.lastEvent = "Return" => state.holder = state.lastActor

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state

Spec · operator

priority · input revision 1 · CC0 1.0

Spec == Init /\ [][Next]_state

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: Init, Next, state

StaleReturnRejected · operator

priority · input revision 1 · CC0 1.0

StaleReturnRejected ==
    state.lastReturn.id # 0 /\ state.phase = "Paused" /\ state.childComplete =>
        ~ReturnMatches(state, state.lastReturn)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state, ReturnMatches

Suspend · operator

priority · input revision 1 · CC0 1.0

Suspend == /\ state.phase = "Resolving" /\ state' = SuspendForChild(state)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state, SuspendForChild

SuspendedCallerCannotAct · operator

priority · input revision 1 · CC0 1.0

SuspendedCallerCannotAct ==
    state.phase \in {"Resolving", "Paused"} =>
        state.holder = "None" /\ state.busyActor \in Seats /\ state.call \in state.usedCalls

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state, Seats

TwoConsecutivePasses · operator

priority · input revision 1 · CC0 1.0

TwoConsecutivePasses == state.phase = "Closed" => state.consecutivePasses = 2

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: state

TypeOK · operator

priority · input revision 1 · CC0 1.0

TypeOK ==
    /\ state.phase \in {"NeedCheckpoint", "Ready", "Resolving", "Paused", "Closed"}
    /\ state.holder \in Seats \cup {"None"} /\ state.busyActor \in Seats \cup {"None"}
    /\ state.previousPass \in BOOLEAN /\ state.childComplete \in BOOLEAN
    /\ state.reception \in 1..7 /\ state.consecutivePasses \in 0..2
    /\ state.nextCall \in 1..(MaxCalls + 1) /\ state.usedCalls \subseteq 1..MaxCalls
    /\ state.nextReceipt \in 1..(MaxReceipts + 1)
    /\ state.usedReceipts \subseteq 1..MaxReceipts

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: MaxCalls, MaxReceipts, state, Seats

state · variable

priority · input revision 1 · CC0 1.0

state

Exact module download · Source bundle and reproduction instructions