SPECIFICATION Spec
CONSTANTS
  r1 = r1
  c1 = c1
  u1 = u1
  l1 = l1
  Star = Star
  NoRecord = NoRecord
  NoRead = NoRead
  NoList = NoList
INVARIANTS
  TypeOK
  DecisionFromCurrentState
  ListIsCheck
  RevokedLinkNeverServes
  NoOrphanTuples
  VisitorOnlyThroughStar