---- MODULE MC ----
EXTENDS IFifo, TLC

\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
e1, e2
----

\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
d1, d2
----

\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
D1, D2
----

\* MV CONSTANT definitions EnQers
const_172933066381572000 == 
{e1, e2}
----

\* MV CONSTANT definitions DeQers
const_172933066381573000 == 
{d1, d2}
----

\* MV CONSTANT definitions Data
const_172933066381574000 == 
{D1, D2}
----

\* CONSTRAINT definition @modelParameterContraint:0
constr_172933066381575000 ==
Len(queue) < 4
----
=============================================================================
\* Modification History
\* Created Sat Oct 19 11:37:43 CEST 2024 by lamport
