---- MODULE MC ----
EXTENDS ICenSeq1, TLC

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

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

\* CONSTRAINT definition @modelParameterContraint:0
constr_17292544981153000 ==
Len(aw) < 4
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_17292544981154000 ==
IC2!ICenSeq2
----
=============================================================================
\* Modification History
\* Created Fri Oct 18 14:28:18 CEST 2024 by lamport
