\* CONSTANT declarations
CONSTANT defaultInitValue = defaultInitValue
\* CONSTANT definitions
CONSTANT
MAX_STACK_SIZE <- const_1555008106484175000
\* CONSTANT definitions
CONSTANT
MAX_ITER_THR_A <- const_1555008106484176000
\* CONSTANT definitions
CONSTANT
MAX_ITER_THR_B <- const_1555008106484177000
\* CONSTANT definition
CONSTANT
NULL = NULL
\* SPECIFICATION definition
SPECIFICATION
spec_1555008106484179000
\* Generated on Thu Apr 11 14:41:46 EDT 2019