PriorityProtocol

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.

finished · operator

priority · input revision 1 · CC0 1.0

finished ==
        [before EXCEPT !.busyActor = "None", !.call = 0, !.transaction = 0,
         !.child = 0, !.childComplete = FALSE,
         !.previousPass = IF keepPreviousPass THEN @ ELSE FALSE,
         !.consecutivePasses = 0, !.usedReceipts = @ \cup {receipt.id},
         !.nextReceipt = @ + 1, !.lastReturn = receipt,
         !.returnAudit =
           [expectedWindow |-> 1, actualWindow |-> receipt.window,
            expectedCall |-> before.call, actualCall |-> receipt.call,
            expectedChild |-> before.child, actualChild |-> receipt.child,
            expectedTransaction |-> before.transaction, actualTransaction |-> receipt.transaction,
            expectedReception |-> before.reception, actualReception |-> receipt.reception],
         !.lastEvent = "Return", !.lastActor = before.busyActor]

Exact module download · Source bundle and reproduction instructions

passed · operator

priority · input revision 1 · CC0 1.0

passed == [before EXCEPT !.consecutivePasses = @ + 1, !.lastEvent = "Pass"]

Exact module download · Source bundle and reproduction instructions

BeginOption · operator

priority · input revision 1 · CC0 1.0

BeginOption(before) ==
    [before EXCEPT !.phase = "Resolving", !.holder = "None", !.busyActor = before.holder,
                   !.call = before.nextCall, !.transaction = before.nextCall,
                   !.usedCalls = @ \cup {before.nextCall}, !.nextCall = @ + 1,
                   !.lastEvent = "Begin"]

Exact module download · Source bundle and reproduction instructions

CompleteChild · operator

priority · input revision 1 · CC0 1.0

CompleteChild(before) ==
    [before EXCEPT !.childComplete = TRUE, !.lastEvent = "ChildComplete"]

Exact module download · Source bundle and reproduction instructions

CompleteOption · operator

priority · input revision 1 · CC0 1.0

CompleteOption(before, receipt, returnedHolder, keepPreviousPass) ==
    LET finished ==
        [before EXCEPT !.busyActor = "None", !.call = 0, !.transaction = 0,
         !.child = 0, !.childComplete = FALSE,
         !.previousPass = IF keepPreviousPass THEN @ ELSE FALSE,
         !.consecutivePasses = 0, !.usedReceipts = @ \cup {receipt.id},
         !.nextReceipt = @ + 1, !.lastReturn = receipt,
         !.returnAudit =
           [expectedWindow |-> 1, actualWindow |-> receipt.window,
            expectedCall |-> before.call, actualCall |-> receipt.call,
            expectedChild |-> before.child, actualChild |-> receipt.child,
            expectedTransaction |-> before.transaction, actualTransaction |-> receipt.transaction,
            expectedReception |-> before.reception, actualReception |-> receipt.reception],
         !.lastEvent = "Return", !.lastActor = before.busyActor]
    IN ReceivePriority(finished, returnedHolder)

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: finished, ReceivePriority

ExpectedReturn · operator

priority · input revision 1 · CC0 1.0

ExpectedReturn(before) ==
    [id |-> before.nextReceipt, window |-> 1, call |-> before.call,
     child |-> before.child, transaction |-> before.transaction,
     reception |-> before.reception, actor |-> before.busyActor,
     complete |-> TRUE, childrenReturned |-> before.childComplete, drained |-> TRUE]

Exact module download · Source bundle and reproduction instructions

InitialWindow · operator

priority · input revision 1 · CC0 1.0

InitialWindow ==
    [phase |-> "NeedCheckpoint", holder |-> "A", reception |-> 1, checkpoint |-> 0,
     previousPass |-> FALSE, consecutivePasses |-> 0, busyActor |-> "None",
     call |-> 0, transaction |-> 0, child |-> 0, childComplete |-> FALSE,
     nextCall |-> 1, usedCalls |-> {}, nextReceipt |-> 1, usedReceipts |-> {},
     lastReturn |-> NoReceipt, returnAudit |-> NoAudit,
     lastEvent |-> "Open", lastActor |-> "None"]

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: NoAudit, NoReceipt

NoAudit · operator

priority · input revision 1 · CC0 1.0

NoAudit ==
    [expectedWindow |-> 0, actualWindow |-> 0, expectedCall |-> 0, actualCall |-> 0,
     expectedChild |-> 0, actualChild |-> 0, expectedTransaction |-> 0, actualTransaction |-> 0,
     expectedReception |-> 0, actualReception |-> 0]

Exact module download · Source bundle and reproduction instructions

NoReceipt · operator

priority · input revision 1 · CC0 1.0

NoReceipt ==
    [id |-> 0, window |-> 0, call |-> 0, child |-> 0, transaction |-> 0,
     reception |-> 0, actor |-> "None", complete |-> FALSE,
     childrenReturned |-> FALSE, drained |-> FALSE]

Exact module download · Source bundle and reproduction instructions

Other · operator

priority · input revision 1 · CC0 1.0

Other(seat) == IF seat = "A" THEN "B" ELSE "A"

Exact module download · Source bundle and reproduction instructions

PassWindow · operator

priority · input revision 1 · CC0 1.0

PassWindow(before) ==
    LET passed == [before EXCEPT !.consecutivePasses = @ + 1, !.lastEvent = "Pass"]
    IN IF before.previousPass
       THEN [passed EXCEPT !.phase = "Closed", !.holder = "None", !.checkpoint = 0]
       ELSE ReceivePriority([passed EXCEPT !.previousPass = TRUE], Other(before.holder))

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: passed, Other, ReceivePriority

ReceiveCheckpoint · operator

priority · input revision 1 · CC0 1.0

ReceiveCheckpoint(before) ==
    [before EXCEPT !.phase = "Ready", !.checkpoint = before.nextReceipt,
                   !.usedReceipts = @ \cup {before.nextReceipt},
                   !.nextReceipt = @ + 1, !.lastEvent = "Checkpoint"]

Exact module download · Source bundle and reproduction instructions

ReceivePriority · operator

priority · input revision 1 · CC0 1.0

ReceivePriority(before, seat) ==
    [before EXCEPT !.holder = seat, !.reception = @ + 1,
                   !.checkpoint = 0, !.phase = "NeedCheckpoint"]

Exact module download · Source bundle and reproduction instructions

ReturnCandidates · operator

priority · input revision 1 · CC0 1.0

ReturnCandidates(before) ==
    {ExpectedReturn(before), [ExpectedReturn(before) EXCEPT !.call = 0],
     [ExpectedReturn(before) EXCEPT !.window = 2], before.lastReturn}

Exact module download · Source bundle and reproduction instructions

Resolved project definitions: ExpectedReturn

ReturnMatches · operator

priority · input revision 1 · CC0 1.0

ReturnMatches(before, receipt) ==
    /\ before.phase = "Paused" /\ before.childComplete
    /\ receipt.id = before.nextReceipt /\ receipt.id \notin before.usedReceipts
    /\ receipt.window = 1 /\ receipt.call = before.call /\ receipt.child = before.child
    /\ receipt.transaction = before.transaction /\ receipt.reception = before.reception
    /\ receipt.actor = before.busyActor
    /\ receipt.complete /\ receipt.childrenReturned /\ receipt.drained

Exact module download · Source bundle and reproduction instructions

Seats · operator

priority · input revision 1 · CC0 1.0

Seats == {"A", "B"}

Exact module download · Source bundle and reproduction instructions

SuspendForChild · operator

priority · input revision 1 · CC0 1.0

SuspendForChild(before) ==
    [before EXCEPT !.phase = "Paused", !.child = before.call,
                   !.childComplete = FALSE, !.lastEvent = "ChildSuspend"]

Exact module download · Source bundle and reproduction instructions