----------------------------- MODULE PriorityMC -----------------------------
EXTENDS PriorityProtocol
CONSTANTS MaxCalls, MaxReceipts, Defect
ASSUME /\ MaxCalls \in 1..2 /\ MaxReceipts \in 8..10
       /\ Defect \in {"None", "AlternateHolder", "KeepPass", "WrongCaller"}
VARIABLE state
Init == state = InitialWindow
Checkpoint ==
    /\ state.phase = "NeedCheckpoint" /\ state.nextReceipt <= MaxReceipts
    /\ state' = ReceiveCheckpoint(state)
Pass == /\ state.phase = "Ready" /\ state' = PassWindow(state)
Act ==
    /\ state.phase = "Ready" /\ state.nextCall <= MaxCalls
    /\ state' = BeginOption(state)
Suspend == /\ state.phase = "Resolving" /\ state' = SuspendForChild(state)
ChildComplete ==
    /\ state.phase = "Paused" /\ ~state.childComplete
    /\ state' = CompleteChild(state)
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")
Next == Checkpoint \/ Pass \/ Act \/ Suspend \/ ChildComplete \/ Return
Spec == Init /\ [][Next]_state

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
FreshCalls == state.usedCalls = 1..(state.nextCall - 1)
FreshReceipts == state.usedReceipts = 1..(state.nextReceipt - 1)
SuspendedCallerCannotAct ==
    state.phase \in {"Resolving", "Paused"} =>
        state.holder = "None" /\ state.busyActor \in Seats /\ state.call \in state.usedCalls
ReturnStaysWithActor == state.lastEvent = "Return" => state.holder = state.lastActor
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
TwoConsecutivePasses == state.phase = "Closed" => state.consecutivePasses = 2
ReadyPassMarker ==
    state.phase \in {"NeedCheckpoint", "Ready"} =>
        state.previousPass = (state.consecutivePasses = 1)
StaleReturnRejected ==
    state.lastReturn.id # 0 /\ state.phase = "Paused" /\ state.childComplete =>
        ~ReturnMatches(state, state.lastReturn)

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