-- (C) Copyright International Business Machines Corporation 23 January 
-- 1990.  All Rights Reserved. 
--  
-- See the file USERAGREEMENT distributed with this software for full 
-- terms and conditions of use. 
-- File: tsapre.d
-- Author: Rob Strom
-- SCCS Info: @(#)tsapre.d	1.2 3/13/90

tsapre: USING()
  DEFINITIONS
-- association between a formal TS and the actual object it is resolve against  
LabelledFormalTypestates : TABLE OF LabelledFormalTypestate {full} keys(*);

LabelledFormalTypestate: RECORD(
  Label: Integer, -- n such that formal typestate is to be compared against components >= n of object being checked
  Minimum: Formal_Typestate -- formal typestate of that CM
  );
  END DEFINITIONS
