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

CONSTANT
    Procs <- const_1728919255409260000
\* CONSTANT definitions

CONSTANT
    epsilon <- const_1728919255409261000
\* CONSTANT definitions

CONSTANT
    Times <- const_1728919255409262000
\* CONSTANT definitions

CONSTANT
    delta <- const_1728919255409263000
\* CONSTANT definition
CONSTANT
none = none
\* INIT definition
INIT
LInv
\* NEXT definition
NEXT
Next
\* INVARIANT definition
INVARIANT
LInv
\* Generated on Mon Oct 14 17:20:55 CEST 2024