\* MV CONSTANT declarations
CONSTANTS
p1 = p1
p2 = p2
p3 = p3
\* MV CONSTANT definitions

CONSTANT
    Procs <- const_1728918948504241000
\* CONSTANT definitions

CONSTANT
    epsilon <- const_1728918948504242000
\* CONSTANT definitions

CONSTANT
    Times <- const_1728918948504243000
\* CONSTANT definitions

CONSTANT
    delta <- const_1728918948504244000
\* CONSTANT definition
CONSTANT
none = none
\* INIT definition
INIT
Inv
\* NEXT definition
NEXT
Next
\* INVARIANT definition
INVARIANT
Inv
\* Generated on Mon Oct 14 17:15:48 CEST 2024