[tlaplus] Specifying MessagePassing [Call for Feedback]

Hi folks, first time poster here looking for feedback on a spec :)

I'm new to TLA+, having read some material (SpecSys by Lamport, Practical TLA+ by Wayne, some of Ron Pressler's essays),

I've decided to start working on specifying something. Since in my spare time I've been toying with the idea of an actor-model

abstract machine in the spirit of Erlang's BEAM, I figured this would be a good project to get some specs down before

doing the implementation.

So I set to specify the delivery and ordering guarantees of message passing across processes within the same Node. I *think*

this spec means what I wanted it to mean, but even if it does it has helped me understand the problem space a lot better, and

it has forced me to research a lot more about how message passing is implemented elsewhere, and what sort of guarantees

other platforms have. For that I am already thankful.

Anyway, I'm writing y'all to get some feedback on the spec (in particular the PlusCal and the temporal formulas) since access

to other TLA+ spec'ers is a little lacking for me at the moment. I'm interested in feedback on:

style,
performance,
maybe alternative ways of writing this that'd make it a little clearer,
anything that I could've missed as a beginner

Here's the spec: https://gist.github.com/ostera/56e78205f5a73cef86a4b6d15be2fed3

Thanks a lot for your time!

PS: I'm inlining it as well just in case github is down.

------------------------ MODULE MessagePassing ------------------------

EXTENDS TLC, Naturals, Sequences, Prelude
CONSTANTS MaxProc, MaxDeliveries
ASSUME MaxProc >= 1
ASSUME MaxDeliveries >= 1

\* BEGIN PRELUDE: relevant Prelude module defs are inlined here for convenience

SetAny(S) == CHOOSE x \in S: TRUE

SeqIsOrdered(S) ==
    IF S = <<>> THEN TRUE
    ELSE IF Len(S) = 1 THEN TRUE
    ELSE LET
        a == Head(S)
        b == Head(Tail(S))
        r == Tail(Tail(S))
    IN a <= b /\ SeqIsOrdered(r)

\* END PRELUDE

Processes == { <<"Process", i>>: i \in 1..MaxProc }
Queues == { <<"Queue", i>>: i \in 1..1 }

(*--algorithm process_lifecycle
variables
      mailboxes = [ p \in Processes |-> <<>> ]
    , queues = [ q \in Queues |-> <<>> ]
    , deliveries = 0 \* Number of messages delivered
    , sends = 0      \* Number of messages sent
    , ghost_halt = FALSE \* used to halt the system after MaxDeliveries
    ;
    
define    
    TypeInvariant == /\ deliveries \in Nat
                     /\ sends \in Nat
                     
    NoMessageWasDeliveredThatWasNotSent == deliveries <= sends
    
    RespectModelLimits == sends <= MaxDeliveries
    
    AllMessagesAreSent == sends = MaxDeliveries
    
    AllMessagesAreDelivered == deliveries = MaxDeliveries
    
end define;

fair+ process g \in { <<"ghost_halt_process", 0>> }
begin MaybeHalt:
    if AllMessagesAreDelivered then
       ghost_halt := TRUE;
       goto Done;
    else goto MaybeHalt;
    end if;
end process;

fair process s \in Processes
variables
    process_receiver = SetAny(Processes)
  , process_queue = SetAny(Queues)
  ;
begin SenderWork:
    if ghost_halt \/ AllMessagesAreSent then goto Done;
    else
        \* pick a random process (even myself!)
        process_receiver := SetAny(Processes);
        \* add to my delivery queue that message
        queues[process_queue] := Append(queues[process_queue], <<process_receiver, sends>>);
        \* increment the send counter by 1
        sends := sends + 1;
        goto SenderWork;
    end if;
end process;

fair process q \in Queues
variables
      message_queue = <<>>
    , msg_desc = << <<"Process", 0>>, 0 >>
    , msg_body = 0
    , msg_receiver = <<"Process", 0>>
    ;
begin QueueWork:
    if ghost_halt then goto Done;
    else
        message_queue := queues[self];
        if Len(message_queue) > 0 then
            \* extract first message from queue
            msg_desc := Head(message_queue);
            
            \* add it to the end of the current receiver's mailbox
            msg_receiver := msg_desc[1];
            msg_body     := msg_desc[2];
            mailboxes[msg_receiver] := Append(mailboxes[msg_receiver], msg_body);
            
            \* discard first message after processing it
            queues[self] := Tail(message_queue);
            
            \* increment deliveries count
            deliveries := deliveries + 1;
        end if;
        goto QueueWork;
    end if;
end process;

end algorithm; *)

\* generated code omitted

AllMessagesAreEventuallyDelivered ==
    <>[] AllMessagesAreDelivered
    
AllQueuesAreEventuallyEmpty ==
    \A q0 \in Queues:
        <>[]( queues[q0] = << >> )
        
AllMessagesArriveInOrder ==
    \A p \in Processes:
        <>[]( SeqIsOrdered(mailboxes[p]) )