A FIFO queue per machine, or per pair of machines?

[dotnwat]

The documentation states that there is a FIFO queue per machine into which messages are deposited, but I'm curious if there is actually a queue per pair of machines, and if the difference affects the way in which models are written.

For example, if we assume that there is a single FIFO queue inbox per machine, then if some machine A sends a set of messages to a machine B in one-shot (i.e. no scheduling points), then those messages would be contiguous within the FIFO queue, and any schedule would not interleave dequeues of those messages with out messages sent to machine B.

On the other hand, it would seem that if there is a FIFO queue per pair of machines, then machine A could still send a bunch of messages in one shot to machine B, but a schedule would then have the freedom to pop off multiple queues resulting in a wider variety of schedules that are accessible.