---- MODULE MC ----
EXTENDS Fischer, TLC

\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
p1, p2, p3, p4
----

\* MV CONSTANT definitions Procs
const_1728919141029247000 == 
{p1, p2, p3, p4}
----

\* SYMMETRY definition
symm_1728919141036248000 == 
Permutations(const_1728919141029247000)
----

\* CONSTANT definitions @modelParameterConstants:1epsilon
const_1728919141036249000 == 
3
----

\* CONSTANT definitions @modelParameterConstants:2Times
const_1728919141036250000 == 
0..15
----

\* CONSTANT definitions @modelParameterConstants:3delta
const_1728919141036251000 == 
2
----

=============================================================================
\* Modification History
\* Created Mon Oct 14 17:19:01 CEST 2024 by lamport
