\* The fixed design: the '+' advert carries the window's session, the invite
\* echoes it, the tag checks it.  Two honest crews and one attacker in range,
\* two presses (so a stale invite from window 1 can meet window 2).
CONSTANTS
  Inviters = {C1, C2, CA}
  Attackers = {CA}
  NoCrew = NoCrew
  MaxPresses = 2
  CheckSession = TRUE

INIT Init
NEXT Next

INVARIANTS
  TypeOK
  WindowMeansNoCrew
  NoUninvitedJoin
  OneJoinPerWindow
  HonestUnlessAttacked
  NoStaleJoin

PROPERTIES
  WindowGate

CHECK_DEADLOCK FALSE