SPECIFICATION Spec

CONSTANTS
  Users = {u1, u2}
  Ids = {a, b}
  Refs = {1, 2, 3}
  MaxPerKind = 2
  NoRef = NoRef

INVARIANTS
  TypeOK
  NoDuplicateCreate
  RefIffComplete
  UniqueRefs
  OneRefPerTransition

PROPERTIES
  TerminalStatesFrozen
  OwnerOnly

CHECK_DEADLOCK FALSE