\* CONSTANT declarations
CONSTANT defaultInitValue = defaultInitValue
\* CONSTANT definitions
CONSTANT
MAX_STACK_SIZE <- const_1555007603462135000
\* CONSTANT definitions
CONSTANT
MAX_ITER_THR_A <- const_1555007603462136000
\* CONSTANT definitions
CONSTANT
MAX_ITER_THR_B <- const_1555007603462137000
\* CONSTANT definition
CONSTANT
NULL = NULL
\* SPECIFICATION definition
SPECIFICATION
spec_1555007603462139000
\* Generated on Thu Apr 11 14:33:23 EDT 2019