\* 3 crew nodes, a 2-hop relay budget, 2 beacons each.  Small enough to
\* enumerate, large enough for a twice-relayed copy of beacon 1 to land at a
\* node that already accepted beacon 2 -- the reordering the guard exists for.
CONSTANTS
  Nodes = {n1, n2, n3}
  Senders = {n1, n2, n3}
  MaxHops = 2
  MaxBeacons = 2

INIT Init
NEXT Next

INVARIANTS
  TypeOK
  Sound
  Freshest
  BoundedRelay

PROPERTIES
  Monotonic

CHECK_DEADLOCK FALSE