\* Three friends, messages live two ticks, at most two held on the device
\* (three fits the design but not the checker's budget once dancing is in).
CONSTANTS
  Peers = {a, b, c}
  TTL = 2
  MaxMsgs = 2
  None = None

INIT Init
NEXT Next

INVARIANTS
  TypeOK
  FocusNotInSight
  SomeoneToWalkToward
  Ephemeral
  TapOnlyForAPerson
  NoTapWhileDancing
  OwedOnlyWhileDancing

CHECK_DEADLOCK FALSE