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

CONSTANT
    Procs <- const_1729435057526151000
\* INIT definition
INIT
Init
\* NEXT definition
NEXT
Next
\* INVARIANT definition
INVARIANT
Inv
\* Generated on Sun Oct 20 16:37:37 CEST 2024