---- MODULE MC ----
EXTENDS ICen2, TLC

\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
a1, a2, a3, a4, a5
----

\* MV CONSTANT definitions Art
const_172908733197347000 == 
{a1, a2, a3, a4, a5}
----

\* PROPERTY definition @modelCorrectnessProperties:0
prop_172908733197348000 ==
I!ICen1
----
=============================================================================
\* Modification History
\* Created Wed Oct 16 16:02:11 CEST 2024 by lamport
