-------------------------- MODULE PriorityProtocol --------------------------
EXTENDS Naturals, FiniteSets, Sequences

(* One ordinary optional-use window. Completing an option returns priority to
   that option's actor. Supplied checkpoints and child completion are explicit
   assumptions; this model does not execute a checkpoint or effect interpreter. *)
Seats == {"A", "B"}
Other(seat) == IF seat = "A" THEN "B" ELSE "A"
NoReceipt ==
    [id |-> 0, window |-> 0, call |-> 0, child |-> 0, transaction |-> 0,
     reception |-> 0, actor |-> "None", complete |-> FALSE,
     childrenReturned |-> FALSE, drained |-> FALSE]
NoAudit ==
    [expectedWindow |-> 0, actualWindow |-> 0, expectedCall |-> 0, actualCall |-> 0,
     expectedChild |-> 0, actualChild |-> 0, expectedTransaction |-> 0, actualTransaction |-> 0,
     expectedReception |-> 0, actualReception |-> 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"]

ReceivePriority(before, seat) ==
    [before EXCEPT !.holder = seat, !.reception = @ + 1,
                   !.checkpoint = 0, !.phase = "NeedCheckpoint"]
ReceiveCheckpoint(before) ==
    [before EXCEPT !.phase = "Ready", !.checkpoint = before.nextReceipt,
                   !.usedReceipts = @ \cup {before.nextReceipt},
                   !.nextReceipt = @ + 1, !.lastEvent = "Checkpoint"]
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))
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"]
SuspendForChild(before) ==
    [before EXCEPT !.phase = "Paused", !.child = before.call,
                   !.childComplete = FALSE, !.lastEvent = "ChildSuspend"]
CompleteChild(before) ==
    [before EXCEPT !.childComplete = TRUE, !.lastEvent = "ChildComplete"]
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]
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
ReturnCandidates(before) ==
    {ExpectedReturn(before), [ExpectedReturn(before) EXCEPT !.call = 0],
     [ExpectedReturn(before) EXCEPT !.window = 2], before.lastReturn}
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)

=============================================================================