\* CONSTANT declarations
CONSTANT defaultInitValue = defaultInitValue
\* CONSTANT definitions
CONSTANT
N <- const_155500668328598000
\* SPECIFICATION definition
SPECIFICATION
spec_155500668328599000
\* Generated on Thu Apr 11 14:18:03 EDT 2019