CONSTANTS
  Users = {u1, u2}
  Roles = {"admin", "member", "readonly"}
  Tokens = {t1, t2}
  Invites = {i1}
  NoUser = NoUser
  NoRole = NoRole
  NoUse = NoUse

SPECIFICATION Spec
INVARIANT TypeOK
INVARIANT RemovedMemberNeverServes
INVARIANT RoleAtDecisionTime
INVARIANT SingleUseInvite
INVARIANT TokensNameMembers
CHECK_DEADLOCK FALSE