\* MV CONSTANT declarations
CONSTANTS
e1 = e1
e2 = e2
\* MV CONSTANT declarations
CONSTANTS
d1 = d1
d2 = d2
\* MV CONSTANT declarations
CONSTANTS
D1 = D1
D2 = D2
\* MV CONSTANT definitions

CONSTANT
    EnQers <- const_172933066381572000
\* CONSTANT declarations
CONSTANT Done = Done
\* CONSTANT declarations
CONSTANT Busy = Busy
\* CONSTANT declarations
CONSTANT NoData = NoData
\* MV CONSTANT definitions

CONSTANT
    DeQers <- const_172933066381573000
\* MV CONSTANT definitions

CONSTANT
    Data <- const_172933066381574000
\* CONSTRAINT definition
CONSTRAINT
constr_172933066381575000
\* SPECIFICATION definition
SPECIFICATION
IFifo
\* INVARIANT definition
INVARIANT
TypeOK
\* Generated on Sat Oct 19 11:37:43 CEST 2024