CONSTANT
  null = 0
  N = 3
  T = {1,2}
  Ref = {1,2,3}
  empty = 0
  undef = <<3,3>> 

SPECIFICATION
  Spec

INVARIANTS
  ABS 
  INV 
  STATUS