\* CONSTANT declarations
CONSTANT defaultInitValue = defaultInitValue
\* CONSTANT definitions
CONSTANT
MAX_STACK_SIZE <- const_1555008081149165000
\* CONSTANT definitions
CONSTANT
MAX_ITER_THR_A <- const_1555008081149166000
\* CONSTANT definitions
CONSTANT
MAX_ITER_THR_B <- const_1555008081149167000
\* CONSTANT definition
CONSTANT
NULL = NULL
\* SPECIFICATION definition
SPECIFICATION
spec_1555008081149169000
\* Generated on Thu Apr 11 14:41:21 EDT 2019