CONSTANTS
  RegisterVal = {v1, v2, v3, v4}

SPECIFICATION OCSSpec
INVARIANTS MCOCSTypeInvariant 
PROPERTY MCLiveness