---- MODULE MC ----
EXTENDS ICenSet1, TLC

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

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

\* PROPERTY definition @modelCorrectnessProperties:0
prop_172925564943517000 ==
IC2!ICenSet2
----
=============================================================================
\* Modification History
\* Created Fri Oct 18 14:47:29 CEST 2024 by lamport
