---- MODULE MC ----
EXTENDS ICen1, TLC

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

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

\* CONSTRAINT definition @modelParameterContraint:0
constr_172908461028131000 ==
Len(aw)<4
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_172908461028133000 ==
I!ICen2
----
=============================================================================
\* Modification History
\* Created Wed Oct 16 15:16:50 CEST 2024 by lamport
