---- MODULE MC ----
EXTENDS IPOFifo_pqs, TLC

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

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

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

\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
id1, id2
----

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

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

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

\* MV CONSTANT definitions Ids
const_1729346640002139000 == 
{id1, id2}
----

\* SYMMETRY definition
symm_1729346640002140000 == 
Permutations(const_1729346640002136000) \union Permutations(const_1729346640002137000) \union Permutations(const_1729346640002139000)
----

\* CONSTANT definition @modelParameterDefinitions:0
def_ov_1729346640002141000 ==
pgE
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_1729346640002142000 ==
F!IFifo
----
=============================================================================
\* Modification History
\* Created Sat Oct 19 16:04:00 CEST 2024 by lamport
